Static analysis techniques for parameterised Boolean equation systems

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

12 Citations (Scopus)
2 Downloads (Pure)

Abstract

Parameterised Boolean Equation Systems (PBESs) can be used to encode and solve various types of model checking and equivalence checking problems. PBESs are typically solved by symbolic approximation or by instantiation to Boolean Equation Systems (BESs). The latter technique suffers from something similar to the state space explosion problem and we propose to tackle it by static analysis techniques, which we tailor for PBESs. We introduce a method to eliminate redundant parameters and a method to detect constant parameters. Both lead to a better performance of the instantiation and they can sometimes even reduce problems that are intractable due to the infinity of the underlying BES to tractable ones. This research has been partially funded by the Netherlands Organisation for Scientific Research (NWO) under FOCUS/BRICKS grant number 642.000.602.
Original languageEnglish
Title of host publicationTools and Algorithms for the Construction and Analysis of Systems (Proceedings 15th International Conference, TACAS 2009, part of ETAPS 2009, York, UK, March 22-29, 2009)
EditorsS. Kowalewski, A. Philippou
Place of PublicationBerlin
PublisherSpringer
Pages230-245
ISBN (Print)978-3-642-00767-5
DOIs
Publication statusPublished - 2009

Publication series

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

Fingerprint

Dive into the research topics of 'Static analysis techniques for parameterised Boolean equation systems'. Together they form a unique fingerprint.

Cite this