ltscompare
The tool ltscompare compares two transition systems that both must have
either the extension .aut, .lts or .fsm. The transition systems should not
be probabilistic.
The transition systems can either be compared using an equivalence relation
(option --equivalence) or a preorder (option --preorder). The list of
available equivalences is provided below.
There are two useful options. One allows to generate counter examples (option
--counter-example). The counter example consist of a Hennessy-Milner formula
which is true in the first input LTS and false in the second. Counter-examples
are implemented and tested for the bisim, branching-bisim and trace
equivalence options.
The second useful option is to hide some actions while doing the comparisons
(option --tau= followed by a comma separated list of actions). Counter examples
will only be distinguishing for the input transition systems with the hiding operation
applied.
Usage
ltscompare [OPTION]... [INFILE1] INFILE2
Description
Determine whether or not the labelled transition systems (LTSs) in INFILE1 and INFILE2 are related by some equivalence or preorder. If INFILE1 is not supplied, stdin is used. If INFILE1 and/or INFILE2 is ‘-’, stdin is used. Reading two LTSs via stdin is only supported for the ‘aut’ format, these LTSs must be separated by an EOT character (x04).
- The input formats are determined by the contents of INFILE1 and INFILE2. Options –in1 and –in2 can be used to force the input format of INFILE1 and INFILE2, respectively. 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
Command line options
-c , --counter-example
generate counter example if the input lts’s are not equivalent
--counter-example-file=NAME
the file to which the counterexample should be written
-eNAME) , --equivalence=NAME)
use equivalence NAME (not allowed in combination with -p/–preorder, use –help-all for all possible arguments):
noneidentity equivalence
bisimdefault strong bisimilarity (using the O(m log n) algorithm [Groote/Jansen 2025])
bisim-gvstrong bisimilarity using the O(mn) algorithm [Groote/Vaandrager 1990]
bisim-gjkwstrong bisimilarity using the O(m log m) algorithm [Groote/Jansen/Keiren/Wijs 2017]
bisim-jgkwstrong bisimilarity using the O(m log n) algorithm [Jansen/Groote/Keiren/Wijs 2019]
bisim-gjstrong bisimilarity using an O(m log n) algorithm [Groote/Jansen 2025]
bisim-gj-lazy-BLCstrong bisimilarity using an O(m log n) algorithm [Groote/Jansen 2025] with lazy BLC set construction (experimental)
branching-bisimdefault branching bisimilarity (using the O(m log n) algorithm [Groote/Jansen 2025])
branching-bisim-gvbranching bisimilarity using the O(mn) algorithm [Groote/Vaandrager 1990]
branching-bisim-gjkwbranching bisimilarity using the O(m log m) algorithm [Groote/Jansen/Keiren/Wijs 2017]
branching-bisim-jgkwbranching bisimilarity using the O(m log n) algorithm [Jansen/Groote/Keiren/Wijs 2019]
branching-bisim-gjbranching bisimilarity using an O(m log n) algorithm [Groote/Jansen 2025]
branching-bisim-gj-lazy-BLCbranching bisimilarity using an O(m log n) algorithm [Groote/Jansen 2025] with lazy BLC set construction (experimental)
dpbranching-bisimdefault divergence-preserving branching bisimilarity (using the O(m log n) algorithm [Groote/Jansen 2025])
dpbranching-bisim-gvdivergence-preserving branching bisimilarity using the O(mn) algorithm [Groote/Vaandrager 1990]
dpbranching-bisim-gjkwdivergence-preserving branching bisimilarity using the O(m log m) algorithm [Groote/Jansen/Keiren/Wijs 2017]
dpbranching-bisim-jgkwdivergence-preserving branching bisimilarity using the O(m log n) algorithm [Jansen/Groote/Keiren/Wijs 2019]
dpbranching-bisim-gjdivergence-preserving branching bisimilarity using an O(m log n) algorithm [Groote/Jansen 2025]
dpbranching-bisim-gj-lazy-BLCdivergence-preserving branching bisimilarity using an O(m log n) algorithm [Groote/Jansen 2025] with lazy BLC sets (experimental)
weak-bisimweak bisimilarity
dpweak-bisimdivergence-preserving weak bisimilarity
simstrong simulation equivalence
ready-simstrong ready simulation equivalence
tracestrong trace equivalence
weak-traceweak trace equivalence
coupled-simcoupled simulation equivalence
-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):
unknowndefault void preorder
simstrong simulation preorder
ready-simstrong ready simulation preorder
tracestrong trace preorder
weak-traceweak trace preorder
trace-actrace preorder based on an anti chain algorithm
weak-trace-acweak trace preorder based on an anti chain algorithm
failuresfailures refinement
weak-failuresweak failures refinement
failures-divergencefailures divergence refinement (automatically weak)
impossible-futuresimpossible futures
-sNAME , --strategy=NAME
explore the state space using strategy NAME (only for antichain based algorithms; includes all failures refinements) :
b,breadthbreadth-first search
d,depthdepth-first search
--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
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