The Boolean Differential Calculus (BDC) significantly extends the Boolean
Algebra because not only Boolean values 0 and 1, but also changes of Boolean
values or Boolean functions can be described. A Boolean Differential Equation
(BDe) is a Boolean equation that includes derivative operations of the
Boolean Differential Calculus. This paper aims at the classification of BDEs,
the characterization of the respective solutions, algorithms to calculate the
solution of a BDe, and selected applications. We will show that not only
classes and arbitrary sets of Boolean functions but also lattices of Boolean
functions can be expressed by Boolean Differential equations. In order to
reach this aim, we give a short introduction into the BDC, emphasize the
general difference between the solutions of a Boolean equation and a BDE,
explain the core algorithms to solve a BDe that is restricted to all
vectorial derivatives of f (x) and optionally contains Boolean variables. We
explain formulas for transforming other derivative operations to vectorial
derivatives in order to solve more general BDEs. New fields of applications
for BDEs are simple and generalized lattices of Boolean functions. We
describe the construction, simplification and solution. The basic operations
of XBOOLE are sufficient to solve BDEs. We demonstrate how a XBooLe-problem
program (PRP) of the freely available XBooLe-Monitor quickly solves some
BDes.
Verification of reactive systems via instantiation of Parameterised Boolean Equation Systems