Invariants for parameterised Boolean equation systems

S.M. Orzan, T.A.C. Willemse

Research output: Chapter in Book/Report/Conference proceedingConference contributionAcademicpeer-review

5 Citations (Scopus)

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. automatically discovered) process invariants to PBESs. Several examples are provided that illustrate the advantages of using global invariants in various verification problems.
Original languageEnglish
Title of host publicationCONCUR 2008 - Concurrency Theory (19th International Conference, Toronto, Canada, August 19-22, 2008, Proceedings)
EditorsF. Breugel, van, M. Chechik
Place of PublicationBerlin
PublisherSpringer
Pages187-202
ISBN (Print)978-3-540-85360-2
DOIs
Publication statusPublished - 2008

Publication series

NameLecture Notes in Computer Science
Volume5201
ISSN (Print)0302-9743

Fingerprint Dive into the research topics of 'Invariants for parameterised Boolean equation systems'. Together they form a unique fingerprint.

Cite this