Verification of reactive systems via instantiation of parameterised Boolean equation systems

Research output: Contribution to journalArticleAcademicpeer-review

8 Citations (Scopus)

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 then solves the encoded problem. The decidability of solving a PBES depends on the data sorts that occur in the PBES. We describe a pragmatic methodology for solving PBESs, viz, by attempting to instantiate them to the sub-fragment of Boolean Equation Systems (BESs). Unlike solving PBESs, solving BESs is a decidable problem. Based on instantiation, verification using PBESs can effectively be done fully automatically in most practical cases. We demonstrate this by solving several complex verification problems using a prototype implementation of our instantiation technique. In addition, practical issues concerning this implementation are addressed. Furthermore, we illustrate the effectiveness of instantiation as a transformation on PBESs when solving verification problems involving systems of infinite size.
Original languageEnglish
Pages (from-to)637-663
JournalInformation and Computation
Volume209
Issue number4
DOIs
Publication statusPublished - 2011

Fingerprint

Dive into the research topics of 'Verification of reactive systems via instantiation of parameterised Boolean equation systems'. Together they form a unique fingerprint.

Cite this