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.

Manual page for ltspbisim

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 , --equivalenceNAME

generate an equivalent LTS, preserving equivalence NAME:

none

identity equivalence

pbisim

probabilistic bisimulation equivalence using the O(m(log n)) algorithm by Groote, Rivera-Verduzco and de Vink, 2017

pbisim-bem

probabilistic 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 intermediate messages

-d , --debug

display detailed intermediate messages

--log-levelLEVEL

display intermediate messages up to and including level

-h , --help

display help information

--version

display version information

Author

Hector Joao Rivera Verduzco