|
| What is CADP? |
|---|
|
Home Page
Tools Overview Current Status Recent Changes |
| Installation |
|
How to obtain CADP?
Usage Statistics |
| Documentation |
|
FAQ
Tutorials Publications Manual Pages Demo Examples Wikipedia |
| CADP Community |
|
Newsletters
Education & Training Case Studies Research Tools |
| CADP Resources |
|
VLSAT Benchmarks
VLTS Benchmarks Other Resources |
| About CADP |
| Contributors |
where bcg_options is defined below (see GENERAL OPTIONS).
bcg_min takes as input the BCG graph input.bcg, minimizes this graph according to some bisimulation relation, and writes the resulting reduced graph to output.bcg, replacing input.bcg if output.bcg is omitted. Minimization means that distinct states of output.bcg are always non-bisimilar; As a consequence, output.bcg is the smallest graph (in number of states and transitions) bisimilar to input.bcg.
i" by the various BCG tools), prob %p" or "label; prob %p", where %p denotes a floating-point number in
the range ]0..1] and label denotes a character string that does not contain
the ";" character. For each state, the sum of "%p" values on special transitions
leaving the state must be less or equal than 1 (see ANNEX 1 below for a
discussion on how the probabilistic LTS model of bcg_min generalizes other
theoretical models published in the literature), rate %f" or "label; rate %f",
where %f denotes a strictly positive floating-point number and label denotes
a character string that does not contain the ";" character (see ANNEX 2
below for a discussion on how the stochastic LTS model of bcg_min generalizes
other theoretical models published in the literature).
In "total matching" semantics, the regular expressions contained in sharp_filename denote full labels (i.e., gates possibly followed by experiment offers). A label matches if it matches some rule in sharp_filename entirely.
In "partial matching" semantics, the regular expressions contained in sharp_filename denote substrings of labels. A label matches if it contains a substring that matches some rule in sharp_filename.
At last, in "gate matching" semantics, the regular expressions contained in sharp_filename denote gates. A label matches if its first word (called gate) matches some rule in sharp_filename. In this case, regular expressions in sharp_filename should not contain characters forbidden in gate identifiers (e.g., " ", "(", or "!").
Option -total is the default.
This option cannot be combined with neither -prob nor -rate options. Not a default option.
rate %f"
or "label; rate %f" or "prob %p" or "label; prob %p" are processed as ordinary
labels, without special meaning attached. Default option.
prob %p"
or "label; prob %p" is recognized as denoting a probabilistic transition
with probability %p. bcg_min will stop with an error message if, for some
probabilistic transition, %p is out of ]0..1], or if the probabilistic transitions
going out of the same state have a cumulated sum strictly greater than
1. With this option, labels of the form "rate %f" or "label; rate %f" are
processed as ordinary labels. Not a default option.
rate %f"
or "label; rate %f" is recognized as denoting a stochastic transition with
rate %f. bcg_min will stop with an error message if, for some stochastic
transition, %f is less or equal to 0. If the -branching or the -divbranching
option is selected, and some state has both an outgoing stochastic transition
and an outgoing internal (i.e., "tau") transition, bcg_min will print a
warning and remove the stochastic transition in order to preserve the
notion of maximal progress. With this option, labels of the form "prob %p"
or "label; prob %p" are processed as ordinary labels. Not a default option.
rate %f"
are removed. This implements the weak Markovian equivalences described in
[Bra02] and [BHKW05]. Not a default sub-option.
%f
and %p mentioned in section DESCRIPTION above). The value of format_string
should obey the same conventions as the format parameter of function sprintf(3C)
for values of type double. Default value for format_string is "%g", meaning
that floating-point numbers are printed with at most six digits after the
"." (i.e., the radix character). Other values can be used, for instance "%.9g"
to obtain nine digits instead of six, or by replacing the "%g" flag with
other flags, namely "%e", "%E", "%f", "%G", possibly combined with additional
flags (e.g., to specify precision).
Note: In bcg_min versions up to 2.1, option -class was not followed by a class_file argument and equivalence classes were always displayed on the standard output. The class_file argument was introduced in bcg_min version 2.2. Because such evolution breaks backward compatibility, bcg_min issues an error message and stops if the argument following option -class is either an option (i.e., starts with a hyphen) or a file name with extension .bcg, which prevents overwriting an existing BCG file.
Note: Options -strong, -branching, -divbranching, -sharp, -divsharp, and -observational are mutually exclusive. If they occur simultaneously on the command line, the option occurring last is selected.
Note: Options -normal, -prob, and -rate (with or without -self sub-option) are mutually exclusive. If they occur simultaneously on the command line, the option occurring last is selected.
By principle and for efficiency reasons, bcg_min does not check whether states and transitions are reachable, neither in input.bcg nor in output.bcg.
As a consequence, output.bcg may contain unreachable states and transitions, meaning that input.bcg itself contained unreachable states and transitions. The converse is not true. In particular, if every state unreachable in input.bcg is equivalent to one that is reachable, then all states and transitions of output.bcg are reachable.
There is a single exception to this principle. Indeed, bcg_min may itself remove stochastic or probabilistic transitions, either due to maximal progress (when bcg_min is called with the -rate option) or because the value of a stochastic or probabilistic transition is less or equal to the precision of floating-point comparisons (when bcg_min is called with either -prob or -rate option, see the -epsilon option). In this case, bcg_min performs reachability analysis to eliminate those states and transitions made unreachable by such transition removal. If input.bcg contained states and transitions that were already unreachable before transition removal, then those states and transitions are also removed by the reachability analysis.
Note however that reachability analysis is not performed when bcg_min is called with the -class option, so that the unreachable states are listed explicitly in the class file. In that case, output.bcg may have more states and transitions than without the -class option, the additional states and transitions being unreachable.
If needed, unreachable states and transitions can be removed from input.bcg or from output.bcg by using the tools bcg_open and generator. See the bcg_open and generator manual pages.
<sharp-set> ::= <positive-header> '\n' <label-list>
| <negative-header> '\n' <label-list>
<label-list> ::= <label>
| <label> '\n' <label-list>
<label> ::= <regexp-denoting-a-label>
<positive-header> ::= 'hold'
<negative-header> ::= 'hold all but'
If the header is the positive header (hold), then any label matching a regular expression of the file will be considered to be a strong action. On the contrary, if the header is the negative header (hold all but), then any label matching a regular expression of the file will be considered to be a weak action. See the regexp manual page for details about regular expressions.
There is no mandatory suffix (i.e., file extension) for
this file: any file name can be used; however, it is recommended to use
the suffix ``.hold''.
Version 2.* of bcg_min was developed by Frederic Lang (INRIA/VASY). It uses (sequential) variants of the signature-based algorithm of [BO03] to compute strong, branching, and divbranching bisimulation on normal, probabilistic and stochastic LTS.
See the bcg manual page for a description of the other files.
Additional information is available from the CADP Web page located at http://cadp.inria.fr
Directives for installation are given in files $CADP/INSTALLATION_*.
Recent changes and improvements to this software are reported and commented in file $CADP/HISTORY.
prob %p" only.
prob %p" to represent
transitions not obtaining an impulse reward. State rewards are associated
to states by "normal" transitions with source and target states being
identical. The label indicates the state reward such as "reward 5". Impulse
rewards are associated to probabilistic transitions by prefixing the "prob %p"
label with a label indicating the reward obtained by taking this transition,
as in "impulse 4; prob %p".
prob %p", as well as normal transitions
in such a way that there is no state possessing both normal as well as
"prob %p" transitions.
prob %p", as well as normal transitions
in such a way that there is no state possessing both normal as well as
"prob %p" transitions. Normal and probabilistic transitions strictly alternate,
i.e. normal (resp. "prob %p") transitions are not directly followed by normal
(resp. "prob %p") transitions. Uses an encoding of Discrete Time Markov Decision
Processes into strictly Alternating Probabilistic LTS proposed in [Arg00].
; prob %p" only, and for each state the sum of "%p" values leaving
a state is equal to (or smaller than) 1.
; prob %p" only, and for
each state and each "label" the sum of "%p" values leaving a state is
equal to (or smaller than) 1.
prob %p", as well as normal transitions
in such a way that there is no state possessing both normal as well as
"prob %p" transitions. Normal transitions are not directly followed by normal
transitions.
rate %f" only.
rate %f" to represent transitions not obtaining an impulse
reward. State rewards are assigned to states by "normal" transitions with
source and target states being identical. The label indicates the state
reward such as "reward 5". Impulse rewards are assigned to probabilistic
transitions by prefixing the "rate %f" label with a label indicating the
reward obtained, as in "impulse 4; rate %f".
rate %f", as
well as normal transitions in such a way that there is no state possessing
both normal as well as "rate %f" transitions. Normal and stochastic transitions
strictly alternate, meaning that normal (resp. "rate %f") transitions are
not directly followed by normal (resp. "rate %f") transitions. Inspired by
an encoding proposed in [Arg00].
rate %f", as well as normal transitions.
; rate %f", as well as normal transitions.
; rate %f" only. Passsive transitions are represented
by abuse of the "rate" keyword. The transition label of a passive transition
is augmented by a distinguishing string to indicate that the rate value
has to be interpreted as a weight, such as in "THIS IS A PASSIVE TRANSITION
LABELLED label WITH WEIGHT; rate %f". The actual distinguishing string used
for this purpose is of no importance for bcg_min, but it must not contain
";" and must not start with the keyword "rate".
; rate %f" only. Passive and immediate transitions are represented by
abuse of the "rate" keyword. The transition label of a passive transition
is augmented by a distinguishing string to indicate that the rate value
has to be interpreted as a weight, such as in "THIS IS A PASSIVE TRANSITION
LABELLED label WITH PRIORITY p AND WEIGHT; rate %f". The transition label
of an immediate transition is augmented in a similar way, as in "THIS IS
AN IMMEDIATE TRANSITION LABELLED label WITH PRIORITY p AND WEIGHT; rate %f".
The actual distinguishing strings used for these purposes are of no importance
for bcg_min, but they must not contain ";" and must not start with the
keyword "rate".
[Arg00] P. R. D'Argenio. On the relation among different probabilistic transition systems and probabilistic bisimulations. CTIT Tech Report, to appear 2000.
[BG98] M. Bernardo and R. Gorrieri. A Tutorial on EMPA: A Theory of Concurrent Processes with Nondeterminism, Priorities, Probabilities and Time. Theoretical Computer Science 202, pp. 1-54, 1998.
[BHKW05] C. Baier, H. Hermanns, J.P. Katoen, V. Wolf. Comparative branching-time semantics for Markov chains. Information and Computation, vol. 200(2), pp. 149-214, 2005.
[BO03] S. Blom, S. Orzan. Distributed State Space Minimization. Electronic Notes in Theoretical Computer Science, vol. 80, 2003.
[Bra02] M. Bravetti. Revisiting Interactive Markov Chains. Electronic Notes on Theoretical Computer Science, vol. 68(5), 2002.
[Buc94] P. Buchholz. Exact and ordinary lumpability in finite Markov chains. Journal of Applied Probability 31(1), 59-75 (1994).
[GH02] H. Garavel and H. Hermanns. On Combining Functional Verification and Performance Evaluation using CADP. Proc. 11th Int. Symp. of Formal Methods Europe FME'2002 (Copenhagen, Denmark), LNCS 2391, July 2002. Available from http://cadp.inria.fr/publications/Garavel-Hermanns-02.html
[GSS95] R. J. van Glabbeek, S. A. Smolka, and B. Steffen. Reactive, generative, and stratified models of probabilistic processes. Information and Computation 121, pp. 59-80, 1995.
[GW96] R.J. van Glabbeek and W.P. Weijland. Branching Time and Abstraction in Bisimulation Semantics. Journal of the ACM 43(3):555-600, 1996.
[GV90] J. F. Groote and F. Vaandrager. An efficient algorithm for branching bisimulation and stuttering equivalence. Proceedings of the 17th ICALP (Warwick), LNCS 443, pp. 626-638, 1990.
[Han91] H. A. Hansson. Time and Probability in Formal Design of Distributed Systems. PhD thesis, University of Uppsala, 1991.
[Her98] H. Hermanns. Interactive Markov Chains. Ph.D. Thesis, University of Erlangen-Nuernberg, Germany, 1998.
[HHM98] H. Hermanns, U. Herzog, and V. Mertsiotakis. Stochastic Process Algebras - Between LOTOS and Markov Chains. Computer Networks and ISDN Systems 30, pp. 901-924, 1998.
[Hil94] J. Hillston. A Compositional Approach to Performance Modelling. Cambridge University Press, 1996.
[How71] R. A. Howard. Dynamic Probabilistic Systems, Vol II: Semi-Markov and Decision Processes. Wiley, 1971.
[HS99] H. Hermanns and M. Siegle. Bisimulation algorithms for stochastic process algebras and their BDD-based implementation. Proceedings of the 5th ARTS, LNCS 1601, pp. 244-265, 1999.
[KS76] J. G. Kemeny and J. L. Snell. Finite Markov Chains. Springer, 1976.
[KSK76] J. G. Kemeny, J. L. Snell, and A. Knapp. Denumerable Markov Chains. Springer, 1976.
[KS90] P. C. Kanellakis and S. A. Smolka. CCS expressions, finite state processes, and three problems of equivalence. Information and Computation 86(1), pp. 43-68, May 1990.
[LMM20] F. Lang, R. Mateescu, and F. Mazzanti. Sharp Congruences Adequate with Temporal Logics Combining Weak and Strong Modalities. Proceedings of the 26th TACAS, LNCS 12079, pp. 57-76, 2020.
[Mil89] R. Milner. Communication and Concurrency. Prentice-Hall, 1989.
[Nor97] J. R. Norris. Markov Chains. Cambridge University Press, 1997.
[Par81] D. Park. Concurrency and Automata on Infinite Sequences. In Peter Deussen (Ed.), Theoretical Computer Science, Lecture Notes in Computer Science vol. 104, pp. 167-183. Springer Verlag, March 1981.
[Put94] M. L. Puterman. Markov Decision Processes: Discrete Stochastic Dynamic Programming. Wiley, New York, NY, 1994.