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.
ltspbisim [OPTION]... [INFILE [OUTFILE]]
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
generate an equivalent LTS, preserving equivalence NAME:
probabilistic bisimulation equivalence using the O(m(log n)) algorithm by Groote, Rivera-Verduzco and de Vink, 2017
probabilistic bisimulation equivalence using the O(mn (log n + log m)) algorithm by Baier, Engelen and Majster-Cederbaum, 2000
append timing measurements to FILE. Measurements are written to standard error if no FILE is provided
do not display warning messages
display short intermediate messages
display detailed intermediate messages
display intermediate messages up to and including level
display help information
display version information
display help information, including hidden and experimental options