pbesiteration

This tool is aimed at solving parameterised Boolean equation systems with an infinite underlying Boolean equation system using iteration or symbolic approximation [GW05]. In the context of finite data types, it is guaranteed (at least in theory) that we reach a fixpoint for each equation in a finite number of steps. In practice, we can also reach fixpoints in some cases with infinite data types.

Fixpoint checking can be done using the internal EQ-BDD library or SMT library. By default, EQ-BDD are used.

The option -s/--smt runs the tool using the SMT library. It is often much faster, however, it can be used in more limited cases than the EQ-BDD option, due to the fact that the translation to SMT of certain data sorts are hard (if not impossible), e.g. lists or sets. When using the SMT option, the Z3 SMT-solver should be installed and its bin-directory has to be added to the PATH variable.

Iteration

Iteration, or symbolic approximation, is based on fixpoint theory. Let $(\sigma X(d:D) = \varphi_X)$ be an equation where $\sigma \in \{\mu, \nu\}$ .

$\begin{split} X^0(d) &= \begin{cases} \bot & \text{if } \sigma = \mu \\ \top & \text{if } \sigma = \nu \end{cases}\\ X^{n+1}(d) &= \varphi_X[X^n/X](d) \end{split}$

We reach a fixpoint when $\varphi_X[X^{n+1}/X] \equiv \varphi_X[X^n/X]$ , so when substituting again does not semantically change the right-hand side anymore. We are guaranteed to reach a fixpoint if the equation is monotone, i.e. when for all $d$ we have that $X^{n+1}(d) \implies X^{n}(d)$ if $\sigma = \nu$ , and $X^{n}(d) \implies X^{n+1}(d)$ if $\sigma = \mu$ . All PBES generated from mcrl2 specifications are monotone. Due to Knaster-Tarski, we know the fixpoint is not just any fixpoint, but also that it is the least/greatest fixpoint.

Let’s show an example.

$\begin{split} \mathcal{E} = (\nu X(a,b : Nat) = &\ \ \neg (a = 3) \\ &\land (a = 1) \implies X(2, b) \\ & \land (a = 2) \implies X(3, b)) \\ \end{split}$

Iteration goes as follows:

$\begin{split} X^0(a,b) =&\ \top \\ \\ X^1(a,b) = &\ \ \neg (a = 3) \\ &\land (a = 1) \implies X^0(2,b) \\ & \land (a = 2) \implies X^0(3,b) \\ = &\ \ \neg (a = 3) \\ &\land (a = 1) \implies \top \\ & \land (a = 2) \implies \top \\ = &\ \ \neg (a = 3) \\ \\ X^2(a,b) = &\ \ \neg (a = 3) \\ &\land (a = 1) \implies X^1(2,b) \\ & \land (a = 2) \implies X^1(3,b) \\ = &\ \ \neg (a = 3) \\ &\land (a = 1) \implies \neg(2 = 3) \\ & \land (a = 2) \implies \neg(3 = 3) \\ = &\ \ \neg (a = 3) \\ &\land (a = 1) \implies \top \\ & \land (a = 2) \implies \bot \\ = &\ \ \neg (a = 3) \land \neg (a = 2) \\ \\ X^3(a,b) = &\ \ldots = \neg (a = 3) \land \neg (a = 2) \land \neg (a = 1) \\ \\ X^4(a,b) = &\ \ldots = \neg (a = 3) \land \neg (a = 2) \land \neg (a = 1) \end{split}$

Thus $X^3$ is $\nu X$ . The final equation system becomes

$\mathcal{E} \equiv (\nu X(a,b : Nat) = \ \neg (a = 3) \land \neg (a = 2) \land \neg (a = 1))$

One might notice that we can now indeed conclude that parameter $b$ is irrelevant, as it does not occur syntactically in the fixpoint solution.

Alternating equations

If the equation we are currently iterating contains a predicate variable instance (PVI) refering to another equation, we need to translate the PVI to some data expression for the BDD and SMT libraries. We make use of uninterpreted functions (see also [GP00]) to do this. I.e. translating the PVI to a function of type ‘parameters’ to boolean. Two function expression are then equal if all of the parameters match and the function symbol matches.

In practice

Rewrite rules

Due to the nature of EQ-BDD, when your specification contains operators other than equality, it might not terminate. For instance, when trying to verify the mutual exclusion property of Lamport’s bakery protocol, the BDD solver could not reduce BDDs where nodes included the ‘less-than’ operator that were clearly true or false. For instance, $0 = n + 1$ or $n + 1 < n$ for $n \in \mathbb{N}$ . To solve this, the following rewrite rules needed to be added to the mCRL2 specification.:

var n, m : Nat;
eqn (n + m < n) = false;
(n < n + m) = m > 0;
m > 0 -> (0 == n + m) = false;

PBES optimization

At one point, we studied an equation of some PBES of the following form.:

mu X0(b1: Bool) = ... || exists n1: Nat. val(b1 && 0 == n1) && ....

Here, we can apply the one-point rule to rewrite all instances of n1 to 0. Adding pbesrewr -pquantifier-inside and pbesrewr -pquantifier-one-point before solving the PBES resulted in a solving time of 413ms compared to 8m7s without the one-point rule.

Usage

pbesiteration   [OPTION]... [INFILE [OUTFILE]]

Description

Reads a file containing a PBES, and iterates to a solution. If OUTFILE is not present, standard output is used. If INFILE is not present, standard input is used.

Command line options

-g , --check-global-invariant

check in nu-formulae if the core constraint is a global invariant for each equation (slow)

-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

-pNAME , --pbes-rewriter=NAME

use pbes rewrite strategy NAME:

simplify

for simplification

quantifier-all

for eliminating all quantifiers

quantifier-finite

for eliminating finite quantifier variables

quantifier-inside

for pushing quantifiers inside

quantifier-one-point

for one point rule quantifier elimination

pfnf

for rewriting into PFNF normal form

ppg

for rewriting into Parameterised Parity Game form

bqnf-quantifier

for rewriting quantifiers over conjuncts to conjuncts of quantifiers (experimental)

-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

-s , --smt

use SMT-based fixpoint checking instead of EQ-BDD-based checking (limited support)

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

Jore Booy