Instantiation for parameterised Boolean equation systems

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

Onderzoeksoutput: Hoofdstuk in Boek/Rapport/CongresprocedureConferentiebijdrageAcademicpeer review

9 Citaten (Scopus)
2 Downloads (Pure)


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.
Originele taal-2Engels
TitelTheoretical Aspects of Computing - ICTAC 2008 (5th International Colloquium, Istanbul, Turkey, September 1-3, 2008, Proceedings)
RedacteurenJ.S. Fitzgerald, A.E. Haxthausen, H. Yenigun
Plaats van productieBerlin
ISBN van geprinte versie978-3-540-85761-7
StatusGepubliceerd - 2008

Publicatie series

NaamLecture Notes in Computer Science
ISSN van geprinte versie0302-9743

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

Citeer dit