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.
Expressions in a BES can take the following form.
Mathematically, we also write the following.
Boolean equations are defined according to the following syntax.
FixedPointOperator BesEqnDecl BesEqnSpec
FixedPointOperator ::= 'mu' | 'nu' BesEqnDecl ::=
BesExpr';' BesEqnSpec ::= 'bes'
Mathematically, we also write \((\mu X = f)\) or \((\nu X = f)\)
A Boolean equation system is a sequence of Boolean equations,
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].
A. van Dam, B. Ploeger and Tim A.C. Willemse. Instantiation for Parameterised Boolean Equation Systems, Eindhoven University of Technology, Department of Computer Science, CSR 08-11, 2008, 24 pp. (PDF)