BCG_MIN manual page

Table of Contents## Name

bcg_min - minimization or reduction of normal, probabilistic, or
stochastic labeled transitions systems (LTS) encoded in the BCG format
## Synopsis

**bcg_min** [*bcg_options*] [**-strong** | **-branching** | **-divbranching** | **-observational**
| **-sharp** [**-total** | **-partial** | **-gate**] *sharp_filename*] | **-divsharp** [**-total** | **-partial**
| **-gate**] *sharp_filename*] [**-normal** | **-prob** | **-rate** [**-self**]] [**-epsilon** *eps*] [**-format**
*format_string*] [**-class** *class_file*] *input***.bcg** [*output***.bcg**] ## Description

**bcg_min**
implements various algorithms to perform reduction of graphs encoded in
the BCG format according to strong bisimulation, branching bisimulation,
divbranching bisimulation, observational equivalence, sharp bisimulation,
or divsharp bisimulation. A graph input or output by **bcg_min** can be:
## General Options

The
following *bcg_options* are currently supported: **-version**, **-create**, **-update**,
**-remove**, **-cc**, **-tmp**, **-uncompress**, **-compress**, **-register**, **-short**, **-medium**, and **-size**.
See the **bcg**
manual page for a description of these options.
## Particular
Options

The following options are also supported:
## Unreachable
States and Transitions

## Format for Sharp Label Partitioning

Sharp
and divsharp bisimulations assume a partitioning of labels between so-called
strong and weak actions [LMM20]. This partitioning is made through a file,
which must respect the following grammar: ## Environment Variables

See the **bcg**
manual page for a description
of the environment variables used by all the BCG application tools.
## Exit
Status

Exit status is 0 if everything is alright, 1 otherwise.
## Authors

Version
1.* of **bcg_min** was developed by Damien Bergamini (INRIA/VASY), Moez Cherif
(INRIA/VASY), Hubert Garavel (INRIA/VASY) and Holger Hermanns (University
of Twente). Pepijn Crouzen added -self sub-option. Version 1.* of **bcg_min** used
the following algorithms:
## Operands

## Files

## See Also

**bcg**
, **sprintf**(3C)
## Bugs

Please report bugs to Hubert.Garavel@inria.fr.
## Annex
1 - Probabilistic Models

The probabilistic LTS model used in **bcg_min** is general
enough to support the following models, which can be considered as special
cases of probabilistic LTS:
## Annex 2 - Stochastic Models

The stochastic LTS model used in
**bcg_min** is general enough to support the following models, which can be
considered as special cases of stochastic LTS:
## Bibliography

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**.

- either
a "normal" LTS, whose transitions are either labelled with "normal" labels
or with the "internal" label (usually noted "tau" in the scientific literature
and displayed as the character string "
`i`

" by the various BCG tools), - or
a "probabilistic LTS": these are LTS with "normal" labelled transitions,
as well as "special" transitions, whose labels are either of the form
"
`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), - or a "stochastic LTS":
these are LTS with "normal" labelled transitions, as well as "special"
transitions, whose labels are either of the form "
`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).

**-strong**- Perform LTS minimization according to strong bisimulation [Par81]. On (Discrete or Continuous Time) Markov Chains and on Markov Reward Models, this reduction agrees with lumpability of [KS76,KSK76,Buc94,Hil94] (see ANNEX 1, ANNEX 2, and BIBLIOGRAPHY below). Default option.
**-branching**- Perform LTS minimization according to branching bisimulation [GW96]. It is worth noticing that the notion of branching bisimulation is rather meaningless for probabilistic systems. Not a default option.
**-divbranching**- Perform LTS minimization according to divbranching (shorthand for divergence-preserving branching) bisimulation [GW96]. Divbranching bisimulation differs from branching bisimulation only in the way cycles of internal transitions (also called divergences) are treated. It is known that all states traversed by a cycle of internal transitions belong to the same branching equivalence class. While divergences are eliminated in the LTS obtained by reduction modulo ordinary branching bisimulation, a self-looping internal transition is kept in each such equivalence class in the LTS obtained by divbranching bisimulation. Unlike branching bisimulation, divbranching bisimulation preserves inevitability properties. Like branching bisimulation, it is worth noticing that the notion of divbranching bisimulation is rather meaningless for probabilistic systems. Not a default option.
**-observational**- Perform LTS minimization according to
observational equivalence [Mil89]. It is worth noticing that observational
equivalence is computationally more expensive than branching bisimulation,
so that reduction may fail even for graphs containing only few thousands
of states. To reduce the risk of failure, in a first step the input graph
is automatically minimized according to branching bisimulation. This is
sound because branching bisimulation is a graph relation stronger than
observational equivalence. However, this optimisation is not applied if
the
**-class**option is set, so that**bcg_min**can print the equivalence classes relatively to the states of the input graph, instead of the states of the branching minimal intermediate graph produced in the first step. This option cannot be combined with neither**-prob**nor**-rate**options. Not a default option. **-sharp [ -total|-partial|-gate ]***sharp_filename*- Perform LTS minimization according
to sharp bisimulation (the variant of the bisimulation defined in [LMM20]
that does not preserve the divergences present in
*input***.bcg**), using the rules defined in*sharp_filename*to partition labels between strong and weak actions. See Section FORMAT FOR SHARP LABEL PARTITIONING below for details on the syntax of*sharp_filename*. The**-total**,**-partial**, and**-gate**options specify the "total matching", "partial matching", and "gate matching" semantics, respectively.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. **-divsharp [ -total|-partial|-gate ]***sharp_filename*- Perform LTS minimization according to divsharp bisimulation
(the variant of the bisimulation defined in [LMM20] that preserves the
divergences present in
*input***.bcg**). See**-sharp**option above for the partitioning of labels between strong and weak actions. This option cannot be combined with neither**-prob**nor**-rate**options. Not a default option. **-normal**- Consider
*input***.bcg**as a normal LTS. With this option, labels of the form "`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**- Consider
*input***.bcg**as a probabilistic LTS. With this option, each label of the form "`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 [ -self ]**- Consider
*input***.bcg**as a stochastic LTS. With this option, each label of the form "`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.

If**-self**sub-option is given, all self loops (i.e., transitions that remain within the same equivalence class) having labels of the form "`rate %f`

" are removed. This implements the weak Markovian equivalences described in [Bra02] and [BHKW05]. Not a default sub-option. **-epsilon***eps*- Set the precision
of floating-point comparisons to
*eps*, where*eps*is a real value. When*eps*is out of [0..1[,**bcg_min**reports an error. Default value for*eps*is 1E-6. **-format***format_string*- Use
*format_string*to control the format of the floating-point numbers contained in transition labels (these numbers correspond to the occurrences of`%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). **-class***class_file*- If
*class_file*is the character '-', then display the equivalence classes on the standard output. Otherwise, display the equivalence classes in a file named*class_file*. Not a default option.

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''.

- It used the algorithm of [KS90] to compute strong bisimulation on a normal LTS.
- It used the algorithm of [HS99] to compute strong bisimulation on probabilistic and stochastic LTS.
- It used the algorithm
of [GV90] to compute branching bisimulation on a normal LTS. The implementation
in
**bcg_min**was derived from a Pascal program written by Jan Friso Groote (CWI). - It used a variant of the algorithm of [HS99] to compute branching bisimulation on a stochastic (resp. probabilistic) LTS: the branching bisimulation condition was applied only to the "normal" fragment of the transition relation, while the stochastic (resp. probabilistic) fragments were mimimized with respect to strong bisimulation.

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.

*input***.bcg**- BCG graph (input)
*output***.bcg**- BCG graph (output)
*input***@1.o**- dynamic library (input or output)

**$CADP/bin.`arch`/bcg_min**- ``
**bcg_min**'' binary program

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**.

**Discrete Time Markov Chains**[Nor97]- The graph
contains transitions of the form "
`prob %p`

" only. **Discrete Time Markov Reward Models**[How71]- The graph contains transitions of the form "
`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`

". **Alternating Probabilistic LTS**[Han91]- The graph
contains transitions of the form "
`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. **Discrete Time Markov Decision Processes**[Put94]- The
graph contains transitions of the form "
`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]. **Generative Probabilistic LTS**[GSS95]- The graph contains transitions of the
type "
*label*`; prob %p`

" only, and for each state the sum of "`%p`

" values leaving a state is equal to (or smaller than) 1. **Reactive Probabilistic LTS**[GSS95]- The graph contains transitions of the type "
*label*`; 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. **Stratified Probabilistic LTS**[GSS95]- The graph
contains transitions of the form "
`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.

**Continuous Time Markov Chains**[Nor97]- The graph contains transitions of the form "
`rate %f`

" only. **Continuous Time Markov Reward Models**[How71]- The graph contains transitions
of the form "
`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`

". **Continuous Time Markov Decision Processes**[Put94]- The graph contains transitions of the form "
`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]. **Interactive Markov Chains**[Her98]- The graph
contains transitions of the form "
`rate %f`

", as well as normal transitions. **Timed Processes for Performance (TIPP) Models**[HHM98]- The graph contains
transitions of the form "
*label*`; rate %f`

", as well as normal transitions. **Performance Evaluation Process Algebra (PEPA) Models**[Hil94]- The graph contains
transitions of the form "
*label*`; 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`

". **Extended Markovian Process Algebra (EMPA) Models**[BG98]- The graph contains transitions of the form
"
*label*`; 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.