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.

Manual page for bessolve


bessolve   [OPTION]... [INFILE]


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

Command line options


use input format FORMAT:


BES in internal format


PBES in internal format


BES in PGSolver format


PBES in textual (mCRL2) format

-j , --print-justification

print justification for solution. Works only with the local fixpoint strategy.


solve the BES using the specified STRATEGY:


Small progress measures


Gauss elimination (inefficient; plain implementation)


Local fixpoints (advanced form of Gauss elimination, especially effective without alternating fixed points)


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


Jeroen Keiren