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 ::=IdBesExpr ::=BesVar| 'true' | 'false' |BesExpr'=>'BesExpr|BesExpr'||'BesExpr|BesExpr'&&'BesExpr| '!'BesExpr| '('BesExpr')'
Mathematically, we also write the following.
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 ::=BesEqnSpecBesInit
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].