This tool is aimed at generating the reachable part of the bisimulation quotient of systems with an infinite state space. Classical state-space enumeration, such as implemented in lps2lts, relies on enumeration and stores each state explicitly. To avoid this, lpssymbolicbisim applies symbolic techniques to represent infinite sets.

To run this tool, the Z3 SMT-solver should be installed and its bin-directory has to be added to the PATH variable.


The tool can only deal with specifications of limited complexity. Furthermore, there are several other restrictions:

  • The tool cannot deal very well with actions that have data parameters. Actions with Boolean parameters will not lead to a large slowdown, but for larger domains, scalability will be an issue.

In any case, pbessymbolicbisim is probably more powerful, since its abstractions can also rely on the information of the property being checked and it does not have to deal with actions and their parameters.



lpssymbolicbisim   [OPTION]... [INFILE [OUTFILE]]


Performs partition refinement on INFILE and outputs the resulting LTS. This tool is highly experimental.

Command line options

-QNUM , --qlimit=NUM

limit enumeration of universal and existential quantifiers in data expressions to NUM iterations (default NUM=10, NUM=0 for unlimited).

-rNAME , --rewriter=NAME

use rewrite strategy NAME:


jitty rewriting


compiled jitty rewriting


jitty rewriting with prover

-sMODE , --simplifier=MODE

set the simplifying strategy for expressions


Use functions from the mCRL2 data library to eliminate redundant inequalities


Only simplify expressions over finite discrete data


Do not simplify expressions


Automatically select the best simplifier


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


display log messages up to and including level; either warn, verbose, debug or trace

-h , --help

display help information


display version information


display help information, including hidden and experimental options


Thomas Neele