Parameterised Boolean Equation Systems

From MCRL2

Contents 1 Introduction 2 Concepts 2.1 Parameterised boolean equation systems 2.2 Boolean equation systems 2.3 Operations 2.4 Typical uses 2.5 Solution techniques 2.5.1 Symbolic approximation + Gauß elimination 2.5.2 Enumerative

Introduction

Parameterised Boolean Equation Systems (PBESs) can be used to encode model checking problems (such as verifying first-order modal μ-calculus formulae on LPSs, implemented in the tool lps2pbes; the translation of the first-order modal μ-calculus model checking problem on LPSs is documented in the following note: Implementation notes for the PBES libary ). Furthermore, PBESs can be used to code equivalence and preorder relations on processes with data (see here).

Concepts

Parameterised Boolean Equation Systems (PBESs) are instances of so-called Fixed Point Equation Systems. The latter are ordered sequences of equations of the form

 (μ X = ƒ) or (ν X = ƒ)

where μ is the least fixed point, ν is the greatest fixed point, X is a variable and ƒ is an expression over some complete lattice. The solution to such an equation system is one that:

• makes every equation true,
• respects the fixed point signs μ and ν,
• prioritises left-most equations.

Parameterised boolean equation systems

PBESs are Fixed Point Equation Systems in which the right-hand side expressions are predicate formulae. In addition to sorted predicate variables X, the left-hand side of an equation in a PBES declares a finite number of sorted data variables:

 (μ X(d:D) = φ) or (ν X(d:D) = φ)

The grammar for predicate formulae is the following:

 φ ::= b | X(e) | φ ∧ φ | φ ∨ φ |  ∀ d:D. φ | ∃ d:D. φ   

where b is a Boolean expression, d is a sorted data variable and e is a data expression of the sort of variable X. Negation (¬φ) is supported only for expressions φ that do not contain predicate variables. Implication (φ ⇒ ψ) is supported as a shorthand for ¬ φ ∨ ψ; the constraints imposed by ¬φ apply also to implication.

Boolean equation systems

A special subset of PBESs is the class of Boolean Equation Systems (BESs): the left-hand side of a BES does not bind data variables and the predicate formulae that are allowed on the right-hand side do not contain data variables, has no quantifiers and only predicate variables without arguments. Summarising, BESs are PBESs in which the right-hand side expressions are propositional formulae and equations take on the form:

 (μ X = f) or (ν X = f)

The grammar for propositional formulae is the following:

 f ::= true | false | X | f ∧ f | f ∨ f  

The difference between PBESs and BESs is at the same conceptual level as the difference between LPSs and LTSs: PBESs deal with data as first-class objects whereas BESs do not recognise the concept of data. An on-the-fly translation of PBESs into BESs is described in this paper, which shows an exact correspondence between PBESs and BESs; in a sense, the translation can be considered as an alternative semantics for PBESs containing countable data types. BESs have been used for verifying properties of LTSs and are used extensively in the tool suite CADP. For an excellent and very enlightning study of their use for model checking, see the Ph.D. thesis of Angelika Mader.

Operations

The PBES library provides the basic facilities to construct an empty PBES (i.e. a PBES without equations) and to append a new equation to an existing PBES. Appending an equation to an existing PBES is only possible (and allowed) if the predicate variable that occurs on the left-hand side of the equation does not appear on the left-hand side of any equation in the existing PBES.

Furthermore, the PBES library offers methods to construct predicate formulae, and, if necessary, to transform a given predicate formula to positive normal form.

Typical uses

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 E, F and G denote arbitrary PBESs. Substitution, for instance is based on the following transformation:

 E (σ X(d:D) = φ) F (σ' Y(e:E) = ψ) G

to

 E (σ X(d:D) = φ[Y := λe:E. ψ]) F (σ' Y(e:E) = ψ) G

A note of warning: substitution in the other direction (i.e. substituting φ 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 φ[Y := λe:E. ψ], in which every occurrence of Y in φ is replaced by the predicate ψ.

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

  E (σ X(d:D) = φ) F G

to

  E F (σ X(d:D) = φ) G

is only allowed when φ 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.

Solution techniques

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. Currently, two strategies have been implemented for solving PBESs:

• Symbolic approximation combined with Gauß Elimination, implemented in pbessolve (experimental),
• Enumerative, by translation to BES, implemented in pbes2bool.

Symbolic approximation + Gauß elimination

As a running example, consider the following PBES:

 (μ X(b:Bool) = b ∨ X(¬b) ∨ Y(b) )  (ν Y(b:Bool) = X(b) ∧ 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:

 Y0 = true 
 Y1 = (X(b) ∧ Y(b))[Y := λb:Bool. true]
    =  X(b) 
 Y2 = (X(b) ∧ Y(b))[Y := λb:Bool. X(b)
    =  X(b) ∧ 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:

 (μ X(b:Bool) = b ∨ X(¬b) ∨ Y(b) )  (ν Y(b:Bool) = X(b) )

Substitution then gives the following equivalent PBES:

 (μ X(b:Bool) = b ∨ X(¬b) ∨ X(b) )  (ν Y(b: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:

 X0 =  false 
 X1 = (b ∨ X(¬b) ∨ X(b) )[X := λb:Bool. false]
    =  b 
 X2 = (b ∨ X(¬b) ∨ X(b) )[X := λb:Bool. b]
    =  b ∨ ¬b ∨ 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:

 (μ X(b:Bool) = true )  (ν Y(b:Bool) = X(b) )

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

 (ν Y(b:Bool) = true )  (μ X(b: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:

 (μ X(b:Bool) = b ∨ X(¬b) ∨ Y(b) )  (ν Y(b:Bool) = X(b) ∧ 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 ∨ X(¬b) ∨ Y(b) )[b := false]
 = X(true) ∨ Y(false)

Introduce an equation (μ X_false = X_true ∨ Y_false ) and continue with the computation for the equations for X(true) and Y(false). This yields two more equations: (μ X_true = true ) and (ν Y_false = X_false ∧ Y_false ). The resulting equations are ordered with respect to the ordering of the original PBES, leading to the following PBES:

 (μ Xfalse = Xtrue ∨ Yfalse )  (μ Xtrue = true )   (ν Yfalse = Xfalse ∧ Yfalse )

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.