Liveness analysis for parameterised Boolean equation systems

DOI10.1007/978-3-319-11936-6_16MaRDI QIDQ3457791zbMATH OpenOpenAlexFDO

Authors Jeroen J. A. Keiren, Wieger Wesselink, T. A. C. Willemse

Publication date 17 December 2015

Published in Automated Technology for Verification and Analysis (Search for Journal in Brave)

Full work available at URL https://arxiv.org/abs/1304.6482

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Logic in computer science (03B70) Abstract data types; algebraic specification (68Q65)

Abstract: 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.

Recommendations

• Static Analysis Techniques for Parameterised Boolean Equation Systems
• Proof graphs for parameterised Boolean equation systems
• Parameterised Boolean equation systems
• CONCUR 2004 - Concurrency Theory
• Instantiation for Parameterised Boolean Equation Systems

Cited in

(8)

• Partial-order reduction for parity games with an application on parameterised Boolean equation systems
• scientific article; zbMATH DE number 7269247 (Why is no real title available?)
• Exponential automatic amortized resource analysis
• Simplifying process parameters by unfolding algebraic data types
• Parity game reductions
• Liveness characterization for GFC systems. II
• A formalisation of consistent consequence for Boolean equation systems
• Static Analysis Techniques for Parameterised Boolean Equation Systems

This page was built for publication: Liveness analysis for parameterised Boolean equation systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3457791)