Parameterised Boolean Equation Systems (Extended Abstract)

Systems (extended abstract) Simona Orzan and Tim A.C. Willemse Department of Mathematics and Computer Science, Eindhoven University of Technology P.O. Box 513, 5600 MB Eindhoven, The Netherlands Abstract. The concept of invariance for Parameterised Boolean Equation Systems (PBESs) is studied in greater detail. We identify a weakness 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. automa...

• Type: Conference
• Year: 2004
• Where: CONCUR
• Authors: Jan Friso Groote, Tim A. C. Willemse
• Keywords: CONCUR 2004, Global Invariance, Global Invariants, Parameterised Boolean Equation