pbessymbolicbisim

This tool is aimed at solving parameterised Boolean equation systems with an infinite underlying Boolean equation system. Most other tools, such as pbessolve and pbesinst, rely on enumeration of the data domain to generate the corresponding BES. To avoid this, pbessymbolicbisim applies symbolic techniques to represent infinite sets.

For intermediate simplification of the symbolic representation, the tool relies on one of several simplifying strategies, which can be selected with the option -s/--simplifier. The fm simplifier is based on the Fourier-Motzkin algorithm and only works on linear inequalities.

To track the progress of the tool, one can use the option --log-level=status. The option --fine-initial causes the algorithm to start off with a finer partition. In general, this will lead to a longer runtimes. However, in certain cases, it drastically speeds up the algorithm.

The option --no-early-termination/-t in some cases also speeds up the algorithm. When this option is supplied, no early termination checks are done at the start of every iteration. This can lead to a speed up of at most a factor two. However, the resulting proof graph may be much larger, negating the speed-up.

If the tool spends a lot of time on parity game generation, it might help to set the option --refine-steps/-n to 2 or 3. It saves some overhead by generating a parity game less often, but it may easily lead to a larger proof graph.

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

Manual page for pbessymbolicbisim

Usage

pbessymbolicbisim   [OPTION]... [INFILE]

Description

Computes the solution to the given PBES using symbolic bismulation techniques. Mostly useful for PBESs of low complexity with an infinite underlying BES. This tool is experimental.

Command line options

--fine-initial

use a fine initial partition, such that each block contains only one PBES variable

-t , --no-early-termination

do not use knowledge of simulation relations to perform early termination detection. Using this option might lead to a larger proof graph, although the runtime might become lower since the overhead of early termination checking is avoided.

-QNUM , --qlimitNUM

limit enumeration of quantifiers to NUM variables. (Default NUM=1000, NUM=0 for unlimited).

-nNUM , --refine-stepsNUM

perform the given number of refinement steps between each search for a proof graph

-rNAME , --rewriterNAME

use rewrite strategy NAME:

jitty

jitty rewriting

jittyc

compiled jitty rewriting

jittyp

jitty rewriting with prover

-sMODE , --simplifierMODE

set the simplifying strategy for expressions

fm

Use functions from the mCRL2 data library to eliminate redundant inequalities

finite

Only simplify expressions over finite discrete data

identity

Do not simplify expressions

auto

Automatically select the best simplifier

--timings[FILE]

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

--log-levelLEVEL

display intermediate messages up to and including level

-h , --help

display help information

--version

display version information

Author

Thomas Neele