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.