Invariants for parameterised Boolean equation systems

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

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

5 Citaten (Scopus)


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.
Originele taal-2Engels
TitelCONCUR 2008 - Concurrency Theory (19th International Conference, Toronto, Canada, August 19-22, 2008, Proceedings)
RedacteurenF. Breugel, van, M. Chechik
Plaats van productieBerlin
ISBN van geprinte versie978-3-540-85360-2
StatusGepubliceerd - 2008

Publicatie series

NaamLecture Notes in Computer Science
ISSN van geprinte versie0302-9743


Duik in de onderzoeksthema's van 'Invariants for parameterised Boolean equation systems'. Samen vormen ze een unieke vingerafdruk.

Citeer dit