The tool ltspcompare
compares two transition systems that both must have
either the extension .aut, .lts or .fsm. The tool is intended to compare
probabilistic transition systems. As it stands there is only one equivalence
implemented, which is strong probabilistic bisimulation for non-deterministic
processes a la Larsen and Skou. There are two implementations, namely the
classical but rather slow algorithm by Baier, Engelen and Majster-Cederbaum, and
the much faster one by Groote, Rivera-Verduzco and de Vink.
The intention is to add more equivalences and preorders when efficient algorithms for them become available.
ltspcompare [OPTION]... [INFILE1] INFILE2
Determine whether the labelled transition systems in INFILE1 and INFILE2 are related by some probabilistic equivalence or preorder. If INFILE1 is not supplied, stdin is used.
-eNAME)
, --equivalence=NAME)
use equivalence NAME (not allowed in combination with -p/–preorder):
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
-iFORMAT
, --in1=FORMAT
use FORMAT as the format for INFILE1 (or stdin)
-jFORMAT
, --in2=FORMAT
use FORMAT as the format for INFILE2
-pNAME
, --preorder=NAME
use preorder NAME (not allowed in combination with -e/–equivalence):
none
identity preorder
--tau=ACTNAMES
consider actions with a name in the comma separated list ACTNAMES to be internal (tau) actions in addition to those defined as such by the input
--timings[=FILE]
append timing measurements to FILE. Measurements are written to standard error if no FILE is provided
-q
, --quiet
do not display warning messages
-v
, --verbose
display short intermediate messages
-d
, --debug
display detailed intermediate messages
--log-level=LEVEL
display intermediate messages up to and including level
-h
, --help
display help information
--version
display version information
--help-all
display help information, including hidden and experimental options
Jan Friso Groote