Parameterised Boolean Equation Systems

Parameterised Boolean equation systems (PBESs) can be used to encode model checking problems (such as verifying first-order modal $\mu$ -calculus formulae on LPSs, implemented in the tool lps2pbes; the translation of the first-order modal $\mu$ -calculus model checking problem on LPSs is documented in the PBES library manual. Furthermore, PBESs can be used to code equivalence and preorder relations on processes with data, see [CPPW07a].

PBES expression

The right hand sides of equations in a PBES are predicate formulae, adhering to the following syntax.

PropVarInst PbesExpr

PropVarInst ::=  Id ('(' DataExprList ')')?
PbesExpr    ::=  DataValExpr |
                 '(' PbesExpr ')' |
                 'true' |
                 'false' |
                 Id ('(' DataExprList ')')? |
                 'forall' VarsDeclList '.' PbesExpr |
                 'exists' VarsDeclList '.' PbesExpr |
                 PbesExpr '=>' PbesExpr |
                 PbesExpr '||' PbesExpr |
                 PbesExpr '&&' PbesExpr |
                 '!' PbesExpr

The val operator stands for the value of a boolean data expression, true and false are the booleans true and false, ! is negation, && stands for and, || for or and => for implication. The rules starting with forall and exists stand for univeral and existential quantification.

The following restrictions apply to propositional variables:

monotonicity: every occurrence of a propositional variable should be in a scope such that the number of ! operators plus the number of left hand sides of => is even.
no overloading: it is not allowed to declare two propositional variables with the same name but with a different type.

In mathematical notation, a predicate formula is defined as

$\varphi ::= b \mid X(e) \mid \varphi \land \varphi \mid \varphi \lor \varphi \mid \forall d \colon D . \varphi \mid \exists d \colon D . \varphi$

where $b$ is a Boolean expression, $d$ is a sorted data variable and $e$ is a data expression of the sort of variable $X$ .

PBES equation

Parameterised Boolean equations are fixed point equations with a propositional variable declaration as left hand side and a predicate formula as right hand side. A propositional variable declaration is a sorted predicate variable, with a finite number of sorted data variables.

PropVarDecl PbesEqnDecl PbesEqnSpec

PropVarDecl ::=  Id ('(' VarsDeclList ')')?
PbesEqnDecl ::=  FixedPointOperator PropVarDecl '=' PbesExpr ';'
PbesEqnSpec ::=  'pbes' PbesEqnDecl+

In mathematical notation, we write $(\mu X(d:D) = \varphi)$ or $(\nu X(d:D) = \varphi)$ for least and greatest fixpoint equations, where $\varphi$ is a predicate formula.

PBES specification

A PBES specification contains a sequence of parameterised Boolean equations, preceded by the pbes keyword. Furthermore, an initial propositional variable instantiation must be specified after the init keyword.

PbesInit PbesSpec

PbesInit ::=  'init' PropVarInst ';'
PbesSpec ::=  DataSpec? GlobVarSpec? PbesEqnSpec PbesInit

Files containing a PBES specification can be parsed using txt2pbes.

Transforming PBESs

Several operations on PBESs can be done without these operations influencing the solution to the equation system. Such operations include “migration”, “substitution”, which form the basis for the so-called Gauß elimination strategy for solving PBESs. Let $\mathcal{E}$ , $\mathcal{F}$ and $\mathcal{G}$ denote arbitrary PBESs. Substitution, for instance is based on the following transformation:

$\mathcal{E} (\sigma X(d:D) = \varphi) \mathcal{F} (\sigma' Y(e: E) = \psi) \mathcal{G}$

to

$\mathcal{E} (\sigma X(d:D) = \varphi[Y := \lambda e: E . \psi]) \mathcal{F} (\sigma' Y(e: E) = \psi) \mathcal{G}$

A note of warning: substitution in the other direction (i.e. substituting $\varphi$ for $X$ in the equation for $Y$ ) is not allowed as it affects the solution to the PBES. The PBES library provides the basic facilities for performing a substitution such as $\varphi[Y := \lambda e:E. \psi]$ , in which every occurrence of $Y$ in $\varphi$ is replaced by the predicate $\psi$ .

Migration, which is a transformation defined by the following correspondence:

$\mathcal{E} (\sigma X(d \colon D) = \varphi) \mathcal{F} \mathcal{G}$

to

$\mathcal{E} \mathcal{F} (\sigma X(d \colon D) = \varphi) \mathcal{G}$

is only allowed when $\varphi$ contains no predicate variables. Such a predicate formula is called simple, and an equation for which its right-hand side expression is a simple predicate formula is called solved. The PBES library offers methods to check whether an equation is solved and whether a predicate formula is simple.

Solving PBESs

The PBES library provides the means to construct PBESs and modify these. As may be clear, one is most-often interested in the solution of a PBES, as it provides the answer to some verification task. There are two main approaces to solving PBESs:

Symbolic approximation, combined with Gauß elimination
Enumerative

Currently, the following strategies have been implemented for solving PBESs:

Enumerative, by translation to BES, implemented in pbessolve.
Enumerative, by translation to parity games, implemented in pbespgsolve.
Symbolic approximation, implemented in pbesfixpointsolve.

Symbolic approximation + Gauß elimination

As a running example, consider the following PBES:

$\mu X(b \colon Bool) & = b \lor X(\neg b) \lor Y(b)\\ \nu Y(b \colon Bool) & = X(b) \land Y(b)$

Gauß Elimination basically employs the migration and substitution transformations to solve the global PBES, whereas symbolic approximation tries to solve a single equation by means of an approximation procedure, in which the approximants are represented by predicate formulae. For instance, the following sequence of approximations is needed for computing the solution to $Y$ :

$Y_0 & = true \\ Y_1 & = (X(b) \land Y(b))[Y := \lambda b \colon Bool. true] \\ & = X(b) \\ Y_2 & = (X(b) \land Y(b))[Y := \lambda b \colon Bool. X(b)] \\ & = X(b) \land X(b) \\ & = X(b)$

Since the approximation process stabilises at the second approximant, the solution to $Y$ is the predicate formula $X(b)$ . A solution that is found by means of approximation can be plugged into the original PBES without changing the solution to the PBES; in this case, this results in the following PBES:

$\mu X(b \colon Bool) & = b \lor X(\neg b) \lor Y(b) \\ \nu Y(b \colon Bool) & = X(b)$

Substitution then gives the following equivalent PBES:

mu X(b colon Bool) & = b lor X(neg b) lor X(b) \ nu Y(b colon Bool) & = X(b)

Observe that the equation for $X$ is closed, meaning that it does not refer to predicate variables, other than $X$ . Solving the equation for $X$ using symbolic approximation, we get:

$X_0 & = false \\ X_1 & = (b \lor X(\neg b) \lor X(b))[ X := \lambda b \colon Bool . false]\\ & = b\\ X_2 & = (b \lor X(\neg b) \lor X(b))[ X := \lambda b \colon Bool . b]\\ & = b \lor \neg b \lor b\\ & = true$

Since there is no predicate formula weaker than $true$ , the solution to $X$ is also $true$ . Replacing the solution $true$ for the predicate formula in the equation for $X$ results in the following equivalent equation system:

$\mu X(b \colon Bool) & = true \\ \nu Y(b \colon Bool) & = X(b)$

Using migration, and, subsequently a substitution, the following solved PBES is obtained:

$\nu Y(b \colon Bool) & = true \\ \mu X(b \colon Bool) & = true$

Suppose we would be interested in knowning whether $X(false)$ would be $true$ or $false$ then requires looking at the solved PBES and results in the answer $true$ for $X(false)$ .

Enumerative

Again, as a running example, consider the following PBES:

$\mu X(b \colon Bool) & = b \lor X(\neg b) \lor Y(b)\\ \nu Y(b \colon Bool) & = X(b) \land Y(b)$

The enumerative approach explores the equations of a PBES on demand. Suppose we are interested in knowning whether $X(false)$ would be $true$ or $false$ . This question can be answered by looking at the equations that are needed for $X(false)$ . This can be found out by the following procedure:

replace the data variable $b$ with $false$ in the predicate formula for $X$
simplify the resulting expression,
introduce an equation for $X_{false}$ , encoding $X(false)$ , which has the resulting expression as its right-hand side,
recursively compute all equations for the predicate variables instances that occur in the resulting expression.
as a final step: order every equation according to the ordering of the original PBES.

For the example, this yields the following strategy:

$& (b \lor X(\neg b) \lor Y(b) )[b := false]\\ = & X(true) \lor Y(false)$

Introduce an equation $(\mu X_{false} = X_{true} \lor Y_{false} )$ and continue with the computation for the equations for $X(true)$ and $Y(false)$ . This yields two more equations: $(\mu X_{true} = true )$ and $(\nu Y_{false} = X_{false} \land Y_{false})$ . The resulting equations are ordered with respect to the ordering of the original PBES, leading to the following PBES:

$\mu X_{false} & = X_{true} \lor Y_{false} \\ \mu X_{true} & = true \\ \nu Y_{false} & = X_{false} \land Y_{false}$

The resulting PBES is a BES, for which several well-documented algorithms exist for computing the solution. The solution to $X(false)$ is effectively encoded by the variable $X_{false}$ .

References

[CPPW07a]

T. Chen, B. Ploeger, J. van de Pol and T.A.C. Willemse. Equivalence Checking for Infinite Systems using Parameterized Boolean Equation Systems. In L. Caires, V.T. Vasconcelos (eds.), Concurrency Theory, 18th International Conference, CONCUR 2007, Lisbon, Portugal, Lecture Notes in Computer Science 4703, Springer-Verlag, pp. 120–135, 2007. (DOI)