pbes2bes

Generation of a BES

A BES is generated as follows. First the initial instantiated variable is considered. The instantiated right hand side for this variable is calculated, where all expressions without PBES variables are eliminated. Expressions are reduced to true or false and quantifiers are eliminated by enumerating its elements. As an example consider the PBES (where we use natural numbers as parameters, but these could be different of course).

pbes mu X(n:Nat)=val(n<5)||(forall m:Nat.val(m<=n+1) => X(m));
init X(0);

The initial instantiated variable is X(0). The right hand side belonging to X(0) is

val(0<5)||(forall m:Nat.val(m<=0+1) => X(m))

which using rewriting reduces to:

(forall m:Nat.val(m<=1) => X(m))

The variable m can either be 0 or 1. Using that natural numbers are defined by constructors, a technique called narrowing is used, using which it is calculated that 0 and 1 are the only useful values for m. The expression reduces to:

X(0) && X(1)

So, the first boolean equation that results is

mu X(0)=X(0) && X(1)

The next step is to calculate the equation for X(1).

Strategies

There are different strategies to generate the equations.

0

In strategy 0, all equations are generated in a breadth first search. The equations generated in the order the instantiated variables are encountered.

1

In strategy 1, a small improvement is made. If an equation of the form

nu X(17)=(X(10) && X(18)) || X(19)

is encountered and the right hand side for X(10) is false, then by substituting false for X(10) the equation reduces to

nu X(17)=X(19)

Note

The instantiated variable X(18) disappears. It can be that X(18) does not have to be investigated at all, saving work compared to strategy 0.

2

The idea of substituting true and false and avoiding unnecessary work is taken one step further in strategy 2. Here, whenever a right hand side of an instantiated bes variable is true or false, this value is substituted for the instantiated variable every where. The advantage of strategy 2 is that when the validity of a modal formula can be detected by only investigating parts of the state space, this is detected. The costs of strategy 2 is a higher memory footprint than for strategy 0 and 1. Consider the following partially generated BES from some PBES, which typically is the result of a deadlock check on a transition system with a deadlock.

nu X(0)=X(1) && X(2) && X(3)
nu X(1)=X(4) && X(5)
nu X(2)=X(6)
nu X(3)=false

With strategy 2, the value for X(3)` will be substituted. The result is that ``X(0) becomes false. Furthermore, the instantiated variables X(1) and X(2) cannot be reached and have become superfluous. Using strategy 2, a garbage collection algorithm prevents such variables from being investigated.

3

Strategy 3 is very comparable to strategy 2, except that when a dependency loop of instantiated variables is detected, it attempts to set all the variables in the loop to true in case the fixpoint symbol is a nu, or false if it is a mu. For example

nu X(38)=X(39)
nu X(39)=X(38)

it can set both X(38) and X(39) to true. Moreover, following strategy 2, it can subsequently substitute true for X(38) and X(39) in the generated equations.

Usage

pbes2bes   [OPTION]... [INFILE [OUTFILE]]

Description

Reads the PBES from INFILE and writes an equivalent BES to OUTFILE. If INFILE is not present, stdin is used. If OUTFILE is not present, stdout is used.

Command line options

-eLEVEL , --erase=LEVEL

use remove level LEVEL to remove bes variables

none

never remove a generated bes variable and its equation. This can lead to excessive memory usage.

some

remove generated bes variables that do not occur anymore in the generated BES, except if the right hand side of its equation is true or false. The rhss of removed variables must have to be recalculated, when this bes variable is encountered again.

all

remove the equation for bes variables that do not occur anymore in generated boolean equation system. This is quite memory efficient, but it can be very time consuming as the rhss of removed bes variables may have to be recalculated quite often.

-iFORMAT , --in=FORMAT

use input format FORMAT:

pbes

PBES in internal format

pgsolver

BES in PGSolver format

text

PBES in textual (mCRL2) format

-oFORMAT , --out=FORMAT

use output format FORMAT:

bes

BES in internal format

pbes

PBES in internal format

pgsolver

BES in PGSolver format

text

PBES in textual (mCRL2) format

-QNUM , --qlimit=NUM

limit enumeration of universal and existential quantifiers in data expressions to NUM iterations (default NUM=10, NUM=0 for unlimited).

-rNAME , --rewriter=NAME

use rewrite strategy NAME:

jitty

jitty rewriting

jittyc

compiled jitty rewriting

jittyp

jitty rewriting with prover

-zSEARCH , --search=SEARCH

use search strategy SEARCH:

breadth-first

Compute the right hand side of the boolean variables in a first come first served basis. This is comparable with a breadth-first search. This is good for generating counter examples.

depth-first

Compute the right hand side of a boolean variables where the last generated variable is investigated first. This corresponds to a depth-first search. This can substantially outperform breadth-first search when the validity of a formula is determined at a larger depth.

b

Shorthand for breadth-first.

d

Shorthand for depth-first.

-sSTRAT , --strategy=STRAT

use substitution strategy STRAT:

0

Compute all boolean equations which can be reached from the initial state, without optimization. This is is the most data efficient option per generated equation.

1

Optimize by immediately substituting the right hand sides for already investigated variables that are true or false when generating an expression. This is as memory efficient as 0.

2

In addition to 1, also substitute variables that are true or false into an already generated right hand side. This can mean that certain variables become unreachable (e.g. X0 in X0 and X1, when X1 becomes false, assuming X0 does not occur elsewhere. It will be maintained which variables have become unreachable as these do not have to be investigated. Depending on the PBES, this can reduce the size of the generated BES substantially but requires a larger memory footprint.

3

In addition to 2, investigate for generated variables whether they occur on a loop, such that they can be set to true or false, depending on the fixed point symbol. This can increase the time needed to generate an equation substantially.

--timings[=FILE]

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

-u , --unused_data

do not remove unused parts of the data specification

Standard options

-q , --quiet

do not display warning messages

-v , --verbose

display short log messages

-d , --debug

display detailed log messages

--log-level=LEVEL

display log messages up to and including level; either warn, verbose, debug or trace

-h , --help

display help information

--version

display version information

--help-all

display help information, including hidden and experimental options

Author

Jan Friso Groote