Experiments for the paper "(Re)moving Quantifiers to Simplify Parameterised Boolean Equation Systems"



This archive contains files for experiments with quantifier elimination for parameterised Boolean equation systems, as described in the paper Thomas Neele, (Re)moving Quantifiers to Simplify Parameterised Boolean Equation Systems, in ARQNL 2022, CEUR-WS. Each folder contains an mCRL2 process specification, a modal mu-calculus formula and a bash script run.sh. To run the experiments, an installation of the mCRL2 tool set (version 202206.0 or newer) should be available in the PATH. Source code and binaries are available via https://mcrl2.org or https://github.com/mCRL2org/mCRL2. The run scripts automatically generate a linear process (LPS) and a PBES. The latter is used to compare three approaches: Not applying any constant elimination. Applying the standard constant elimination algorithm from the paper "Static Analysis Techniques for Parameterised Boolean Equation Systems" by Simona Orzan, Wieger Wesselink and Tim A. C. Willemse. Applying the quantifier analysis of the paper mentioned at the top. In case of the motivating example, the resulting PBES for each approach is printed to stdout. For the ABP and cache coherence examples, the size of the underlying BES (called structure graph in the tools) is printed.
Date made available4 Jul 2022
  • (Re)moving Quantifiers to Simplify Parameterised Boolean Equation Systems

    Neele, T., 2022, Proceedings of the 4th International Workshop on Automated Reasoning in Quantified Non-Classical Logics (ARQNL 2022). p. 64-80 17 p. (CEUR Workshop Proceedings; vol. 3326).

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

    Open Access

Cite this