Improved static analysis of parameterised Boolean equation systems using control flow reconstruction

Research output: Book/ReportReportAcademic

34 Downloads (Pure)

Abstract

We present a method for fighting the state space explosion of parameterised Boolean equation systems (PBESs); these essentially are systems of mutually recursive Boolean fixed point equations, parameterised with data. PBESs can encode equivalence checking problems and model checking problems for symbolic, process algebraic specifications. Our method essentially consists of three phases: (1) the control flow in the PBES is reconstructed, detecting control flow parameters that were encoded in the description of the process, as well as control flow parameters that were introduced during the construction of the PBES; (2) we use a data flow analysis based on the control flow in the PBES to detect irrelevant data parameters and (3) we reset those data parameters of the equations in the PBES that were found to be irrelevant. Our reduction preserves the solution to the PBES, and never increases the size of the underlying Boolean equation system. The reduction is evaluated using a number of case studies.
Original languageEnglish
Publishers.n.
Number of pages27
Publication statusPublished - 2013

Publication series

NamearXiv.org
Volume1304.6482 [cs.LO]

Fingerprint Dive into the research topics of 'Improved static analysis of parameterised Boolean equation systems using control flow reconstruction'. Together they form a unique fingerprint.

  • Cite this