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.

```
pbessymbolicbisim [OPTION]... [INFILE]
```

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.

`--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

`-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

Thomas Neele