ltspbisim
The tool ltspbisim reduces a transition system modulo strong probabilistic bisimulation.
The supported formats are either .aut, .lts and .fsm.
There are implemented algorithms. A fast algorithm by Groote, Rivera-Verduzco and de Vink and a classical and much slower algorithm by Baier, Engelen and Majster-Cederbaum. The last algorithms is primarily available for comparison purposes.
It is expected that in the future more probabilistic equivalences will be supported.
- orphan:
Usage
ltspbisim [OPTION]... [INFILE [OUTFILE]]
Description
Convert the labelled transition system (LTS) from INFILE to OUTFILE in the requested format after applying the selected minimisation method (default is none). If OUTFILE is not supplied, stdout is used. If INFILE is not supplied, stdin is used.
The output format is determined by the extension of OUTFILE, whereas the input format is determined by the content of INFILE. Options –in and –out can be used to force the input and output formats. The supported formats are:
‘aut’ for the Aldebaran format (CADP), ‘dot’ for the GraphViz format (no longer supported as input format), ‘fsm’ for the Finite State Machine format, or ‘lts’ for the mCRL2 LTS format (default)
Command line options
-eNAME , --equivalence=NAME
generate an equivalent LTS, preserving equivalence NAME:
noneidentity equivalence
pbisimprobabilistic bisimulation equivalence using the O(m(log n)) algorithm by Groote, Rivera-Verduzco and de Vink, 2017
pbisim-bemprobabilistic bisimulation equivalence using the O(mn (log n + log m)) algorithm by Baier, Engelen and Majster-Cederbaum, 2000
--timings[=FILE]
append timing measurements to FILE. Measurements are written to standard error if no FILE is provided
Standard options
-q , --quiet
do not display warning messages
-v , --verbose
display short log messages
-d , --debug
display detailed log messages
--log-level=LEVEL
display log messages up to and including level; either warn, verbose, debug or trace
-h , --help
display help information
--version
display version information
--help-all
display help information, including hidden and experimental options