# Boolean Equation Systems

Boolean equation systems (BESs) are a subset of PBESs in which the left hand side does not bind data variables, and the predicate formulae that are allowed on the right hand sides of the equations do not contain data variables, have no quantifiers, and only refer to predicate variables without arguments.

## BES expression

Expressions in a BES can take the following form.

BesVar BesExpr

BesVar  ::=  Id
BesExpr ::=  BesVar |
'true' |
'false' |
BesExpr '=>' BesExpr |
BesExpr '||' BesExpr |
BesExpr '&&' BesExpr |
'!' BesExpr |
'(' BesExpr ')'


Mathematically, we also write the following.

$f ::= true \mid false \mid X \mid f \land f \mid f \lor f$

## BES equation

Boolean equations are defined according to the following syntax.

FixedPointOperator BesEqnDecl BesEqnSpec

FixedPointOperator ::=  'mu' |
'nu'
BesEqnDecl         ::=  FixedPointOperator BesVar '=' BesExpr ';'
BesEqnSpec         ::=  'bes' BesEqnDecl+


Mathematically, we also write $$(\mu X = f)$$ or $$(\nu X = f)$$

## BES specification

A Boolean equation system is a sequence of Boolean equations,

BesInit BesSpec

BesInit ::=  'init' BesVar ';'
BesSpec ::=  BesEqnSpec BesInit


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 [DPW08], 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 [Mad97].