Liveness analysis for parameterised Boolean equation systems

DOI10.1007/978-3-319-11936-6_16zbMATH Open1448.68302arXiv1304.6482OpenAlexW2165846252MaRDI QIDQ3457791FDOQ3457791

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)

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.

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

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

Mathematics Subject Classification ID

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

Cited In (8)

• Partial-order reduction for parity games with an application on parameterised Boolean equation systems
• Title not available (Why is that?)
• Simplifying process parameters by unfolding algebraic data types
• Exponential automatic amortized resource analysis
• 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)