Convert Boolean equation systems (BESs) from and to different formats. Optionally, a minimisation method can be selected that is applied on the input.

The reductions that can be done are either strong bisimulation reduction or stuttering bisimulation reduction.

Strong bisimulation reduction of BESs is described in [KW11]. Correctness of stuttering equivalence for BESs follows from the corresponding results on parity games in [CKW11]



besconvert   [OPTION]... [INFILE [OUTFILE]]


reduce the (P)BES in INFILE modulo write the result to OUTFILE (as PBES).If INFILE is not present, stdin is used. If OUTFILE is not present, stdout is used.

Command line options

-eNAME , --equivalence=NAME

generate an equivalent BES, preserving equivalence NAME:’none’ for no reduction (default),’bisim’ for strong bisimulation,’stuttering’ for stuttering equivalence


use input format FORMAT:


PBES in internal format


BES in PGSolver format


PBES in textual (mCRL2) format

-lFILE , --intermediate=FILE

save the intermediate LTS to FILE

-n , --noreduction

do not perform the reduction, only store the intermediate LTS


use output format FORMAT:


BES in internal format


PBES in internal format


BES in PGSolver format


PBES in textual (mCRL2) format


append timing measurements to FILE. Measurements are written to standard error if no FILE is provided


translate to intermediate LTS using TRANSLATION:’deadlock’ for an additional deadlock state recording labels, ‘selfloop’ for a self-loop recording the information in each state, ‘successor’ for an edge with the label of the current state to each successor state (may only be used with –equivalence=bisim)

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


Jeroen Keiren