Invariants for Parameterised Boolean Equation Systems

AbstractThe concept of invariance for Parameterised Boolean Equation Systems (PBESs) is studied in greater detail. We identify an issue with the associated theory and fix this problem by proposing a stronger notion of invariance called global invariance. A precise correspondence is proven between the solution of a PBES and the solution of its invariant-strengthened version; this enables one to exploit global invariants when solving PBESs. Furthermore, we show that global invariants are robust w.r.t. all common PBES transformations and that the existing encodings of verification problems into PBESs preserve the invariants of the processes involved. These traits provide additional support for our notion of global invariants, and, moreover, provide an easy manner for transferring (e.g. automatically discovered) process invariants to PBESs. We provide several examples that illustrate the use of global invariants for a variety of verification problems