The tool bessolve can be used to solve a BES. The solution is printed as true or false on the command line output.

Three different solving algorithms have been implemented:

Gauss elimination

This is a straightforward implementation of the Gauss elimination technique. In general it is very inefficient.

Local fixpoints

This is a more advanced form of Gauss elimination. It is efficient if the BES contains no alternating fixed points. For this algorithm a justification for the solution can be printed.

Small progress measures

This is an implementation of the small progress measures algorithm by Marcin Jurdzinski.

Note that a BES can also be solved by the tool pbessolve. This tool uses Zielonka’s algorithm, which often performs better than the ones implemented in bessolve.



bessolve   [OPTION]... [INFILE]


Solve the BES in INFILE. If INFILE is not present, stdin is used.

Command line options


use input format FORMAT:


PBES in internal format


BES in PGSolver format


PBES in textual (mCRL2) format

-sSTRATEGY , --strategy=STRATEGY

solve the BES using the specified STRATEGY:


Small progress measures


Gauss elimination (inefficient; plain implementation)


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 intermediate messages

-d , --debug

display detailed intermediate messages


display intermediate messages up to and including level

-h , --help

display help information


display version information


display help information, including hidden and experimental options


Jeroen Keiren