ltsmin-compare [OPTIONS] <input 1> <input 2>


-s, --strong

Compare modulo strong bisimulation using the default implementation.

-b, --branching

Compare modulo branching bisimulation using the default implementation.

-l, --lump

Compare modulo CTMC lumping.

-t, --trace

Compare the two LTSs modulo (optionally stuttering) trace equivalence. This happens in multiple steps. First, the LTSs are compared modulo strong bisimulation (or silent step bisimulation if the stutter option is given). If the resulting LTSs are not equal, the LTSs are made deterministic and compared modulo strong bisimulation.


Compare module stuttering during trace equivalence comparison.

LTS I/O Options


Size of a block in bytes. Defaults to 32,768.


Number of blocks in a cluster. Defaults to 32.

General Options


Increase the level of verbosity


Be quiet; do not print anything to the terminal.


Enable debugging output for file.


Print version string of this tool.

-h, --help

Print help text


Print short usage summary.


Enable statistics gathering/printing.


Terminate after the given amount of seconds.


Include file and line number in debug messages.


Include the wall time since program start in all messages.



Successful termination: LTSs are equivalent.


LTSs are not equivalent.


Some error occurred.