Liveness Analysis for Parameterised Boolean Equation Systems

J.J.A. Keiren, J.W. Wesselink, T.A.C. Willemse

Research output: Contribution to JournalArticleAcademicpeer-review


We present a sound static analysis technique for fighting the combinatorial explosion of parameterised Boolean equation systems (PBESs). These essentially are systems of mutually recursive fixed point equations ranging over first-order logic formulae. Our method detects parameters that are not live by analysing a control flow graph of a PBES, and it subsequently eliminates such parameters. We show that a naive approach to constructing a control flow graph, needed for the analysis, may suffer from an exponential blow-up, and we define an approximate analysis that avoids this problem. The effectiveness of our techniques is evaluated using a number of case studies.
Original languageEnglish
Pages (from-to)219-234
JournalLecture Notes in Computer Science
Publication statusPublished - 2014
EventAutomated Technology for Verification and Analysis -
Duration: 1 Jan 20141 Jan 2014

Bibliographical note

Proceedings title: ATVA 2014
Publisher: Springer
ISBN: 978-3-319-11935-9
Editors: F. Cassez, J.-F. Raskin


Dive into the research topics of 'Liveness Analysis for Parameterised Boolean Equation Systems'. Together they form a unique fingerprint.

Cite this