This is a solving tool for parameterised Boolean equation systems (.pbes extension) that is based on a parity game exploration technique that utilises symbolic representations. The symbolic exploration works very similar to the one implemented by lpsreach, where it is described in great detail. The main difference is that the underlying PBES is first transformed into a standard recursive format (SRF), which is in some sense very similar to a linear process.

Next, we describe useful options that are exclusive to pbessolvesymbolic. One option that can be useful to further refine the dependencies of transition groups is –split-conditions, which introduces new transition groups based on the structure of the SRF pbes. Generally, option 1 is safe, but options 2 and 3 can yield an infinite PBES due to the conditions becoming weaker.

Similarly to pbessolve the pbessolvesymbolic tool also contains various partial solving strategies that attempt to optimistically solve the intermediate parity games to present the solution (and terminate) early. These can be enabled with the –solve-strategy option.

Currently, pbessolvesymbolic can not provide counter examples when the property does not hold, and solving PBESs with counter example information is extremely slow.

```
pbessolvesymbolic [OPTION]... [INFILE [OUTFILE]]
```

Solves PBES from INFILE. If INFILE is not present, stdin is used. The PBES is first instantiated into a parity game, which is then solved using Zielonka’s algorithm.

`--cached`

use transition group caching to speed up state space exploration

`--chaining`

reduce the amount of breadth-first iterations by applying the transition groups consecutively

`--groups[=GROUPS]`

‘none’ (default) no summand groups

‘used’ summands with the same variables are joined ‘simple’ summands with the same read/write variables are joined a user defined list of summand groups separated by semicolons, e.g. ‘0; 1 3 4; 2 5’

`--info`

print read/write information of the summands

`--lace-dqsize[=NUM]`

set length of Lace task queue (default 1024*1024*4)

`--lace-stacksize[=NUM]`

set size of program stack in kilobytes (0=default stack size)

`--lace-workers[=NUM]`

set number of Lace workers (threads for parallelization), (0=autodetect, default 1)

`--max-iterations[=NUM]`

limit number of breadth-first iterations to NUM

`-m[NUM]`

, `--memory-limit[=NUM]`

Sylvan memory limit in gigabytes (default 3)

`--print-nodesize`

print the number of LDD nodes in addition to the number of elements represented as ‘elements[nodes]’

`-QNUM`

, `--qlimit=NUM`

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

`--reorder[=ORDER]`

‘none’ (default) no variable reordering

‘random’ variables are put in a random order ‘a user defined permutation e.g. ‘1 3 2 0 4’

`--reset`

set constant values when introducing parameters

`-rNAME`

, `--rewriter=NAME`

use rewrite strategy NAME:

`jitty`

jitty rewriting

`jittyc`

compiled jitty rewriting

`jittyp`

jitty rewriting with prover

`--saturation`

reduce the amount of breadth-first iterations by applying the transition groups until fixed point

`-sNUM`

, `--solve-strategy=NUM`

Use solve strategy NUM. All strategies except 0 periodically apply on-the-fly solving, which may lead to early termination.

`0`

No on-the-fly solving is applied

`1`

Detect solitair winning cycles.

`2`

Detect solitair winning cycles with safe attractors.

`3`

Detect forced winning cycles.

`4`

Detect forced winning cycles with safe attractors.

`5`

Detect fatal attractors.

`6`

Detect fatal attractors with safe attractors.

`7`

Solve subgames using a Zielonka solver.

`-c[NUM]`

, `--split-conditions[=NUM]`

split conditions to obtain possibly smaller transition groups

0 (default) no splitting performed. 1 only split disjunctive conditions. 2 also split conjunctive conditions into multiple equations which often yield more reachable states. 3 alternative split for conjunctive conditions where even more states can become reachable.

`--timings[=FILE]`

append timing measurements to FILE. Measurements are written to standard error if no FILE is provided

`-t`

, `--total`

make the SRF PBES total

`-q`

, `--quiet`

do not display warning messages

`-v`

, `--verbose`

display short intermediate messages

`-d`

, `--debug`

display detailed intermediate messages

`--log-level=LEVEL`

display intermediate messages up to and including level

`-h`

, `--help`

display help information

`--version`

display version information

`--help-all`

display help information, including hidden and experimental options

Wieger Wesselink