Sciweavers

CONCUR
2008
Springer

Invariants for Parameterised Boolean Equation Systems

14 years 2 months ago
Invariants for Parameterised Boolean Equation Systems
The 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 invariantstrengthened 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. Several examples are provided that illustrate the advantages of using global invariants in various verification problems.
Simona Orzan, Tim A. C. Willemse
Added 18 Oct 2010
Updated 18 Oct 2010
Type Conference
Year 2008
Where CONCUR
Authors Simona Orzan, Tim A. C. Willemse
Comments (0)