Instantiation for parameterised Boolean equation systems

A. van Dam, B. Ploeger, T.A.C. Willemse

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

9 Citations (Scopus)
2 Downloads (Pure)

Abstract

Verification problems for finite- and infinite-state processes, like model checking and equivalence checking, can effectively be encoded in Parameterised Boolean Equation Systems (PBESs). Solving the PBES solves the encoded problem. The decidability of solving a PBES depends on the data sorts that occur in the PBES. We describe a manipulation for transforming a given PBES to a simpler PBES that may admit solution methods that are not applicable to the original one. Depending on whether the data sorts occurring in the PBES are finite or countable, the resulting PBES can be a Boolean Equation System (BES) or an Infinite Boolean Equation System (IBES). Computing the solution to a BES is decidable. Computing the global solution to an IBES is still undecidable, but for partial solutions (which suffices for e.g. local model checking), effective tooling is possible. We give examples that illustrate the efficacy of our techniques.
Original languageEnglish
Title of host publicationTheoretical Aspects of Computing - ICTAC 2008 (5th International Colloquium, Istanbul, Turkey, September 1-3, 2008, Proceedings)
EditorsJ.S. Fitzgerald, A.E. Haxthausen, H. Yenigun
Place of PublicationBerlin
PublisherSpringer
Pages440-454
ISBN (Print)978-3-540-85761-7
DOIs
Publication statusPublished - 2008

Publication series

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

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

Cite this