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.

-sSTRATEGY , --strategy=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


display help information, including hidden and experimental options


Jeroen Keiren