Permutation Games for the Weakly Aconjunctive mu-Calculus (artifact)

<div>Artifact for the Paper "<i>Permutation Games for the Weakly Aconjunctive mu-Calculus</i>" TACAS 2018</div><div><br></div><div>This artifact is concerned with Section 4 (Implementation and Benchmarking) of the Paper "<i>Permutation Games for the Weakly Aconjunctive mu-Calculus</i>" by Daniel Hausmann, Lutz Schröder and Hans-Peter Deifel. The artifact consists of the binaries of the two satisfiability checkers <b>COOL </b>(Coalgebraic Ontology Logic Reasoner, implementing the algorithm that is introduced in the paper) and <b>MLSolver </b>(<a href="http://files.oliverfriedmann.com/papers/a_solver_for_modal_fixpoint_logics.pdf">Solver for Modal Fixpoint Logics</a>), a binary that generates test-formulas and a script that benchmarks various families of generated formulas with different variants of the two provers.</div><div><br></div><div>This artifact is provided as a single <b>.zip</b> archive. Scripts are provided in bash shell <b>.sh</b> format and .Perl <b>.pl</b> format. Additional copyright, source and licence details are provided in the 'licenses' subdirectory. Binary file types for <b>COOL </b>and <b>MLSolver</b> can be openly used via the script files provided.</div><div><br></div><div>The below comments relate to the related TACAS publication accessible via this data record. The related study presents a method that uses limit-deterministic parity<br>automata to construct satisfiability games for the weakly aconjunctive fragment of the μ-calculus.</div><div><br></div><div>The tested variants of the provers are the ones that occur in Figures 1-4 of the paper:</div><div><br></div><div>"COOL": COOL without on-the-fly solving, using PGSolver with algorithm "stratimprloc2" to solve games; in the script, this variant is called "cool-pgsolver-noprop"</div><div>"COOL on-the-fly": COOL with on-the-fly solving, using our own implementation of the fixpoint iteration algorithm to solve games; in the script, this variant is called "cool"</div><div>"MLSolver": MSolver without -opt litpro and -opt comp, using PGSolver with algorithm "stratimprloc2" to solve games; in the script, this variant is called "mlsolver"</div><div>"MLSolverOpt": MSolver with -opt litpro and -opt comp enabled, using PGSolver with algorithm "stratimprloc2" to solve games; in the script, this variant is called "mlsolver-opt"</div><div><br></div><div>Figure 1 shows the runtimes for the unsatisfiable theta_1-formulas (in the script, this family of formulas is called "enpa_is_enba_neg").</div><div>Figure 2 shows the runtimes for the unsatisfiable theta_2-formulas (in the script, this family of formulas is called "pg_domgame_neg").</div><div><br></div><div>Some observations regarding Figures 1 and 2: From theoretical results, we know that the satisfiability games in COOL are of size O((n^2)!) while the games in MLSolver are of size O(((n^2)!)^2), thus COOL has shorter runtimes. On-the-fly solving does not help for these formulas since no nodes in these games can be decided early; instead, on-the-fly solving requires additional computations and leads to longer runtimes on these formulas. Additionally our implementation of the fixpoint iteration is slower than the optimized PGSolver with algorithm "stratimprloc2", which however cannot be used for on-the-fly solving.</div><div><br></div><div>Figure 3 shows the runtimes for the unsatisfiable early-ac(n,4,2) formulas (in the script, these formulas are called "early_ac").</div><div>Figure 4 shows the runtimes for the unsatisfiable early-ac_gc(n,4,2) formulas (in the script, these formulas are called "early_caching_ac").</div><div><br></div><div>Some observations regarding Figures 3 and 4: The games in COOL are of size O(n^2)!, games in MLSolver are of size O(((n^2)!)^2), thus COOL has shorter runtimes. On-the-fly solving significantly reduces the runtimes for these formulas. Even though our implementation of the fixpoint iteration is unoptimized and slower than PGSolver with algorithm "stratimprloc2", the on-the-fly capabilities allow to reduce the size of the satisfiability games significantly, resulting in shorter runtimes. In Figure 3, the gain from on-the-fly solving outweighs the slower performance of our game solver from n=11 on, in Figure 4 this is the case from n=8 on.</div><div><br></div><div>The artifact also includes a file <b>results.txt</b> that contains our runtimes for all formulas and reasoners that are depicted in Figures 1-4 in the paper. We conducted all experiments on a machine with Intel Core i7 3.60GHz CPU with 64 bit word size and 16GB RAM and used a timeout of 100s for the experiments in Figures 1 and 2 and a timeout of 1000s for the experiments in Figures 3 and 4. </div><div><br></div><div>As mentioned above, the script that is included in this artifact allows the user to replicate all the experiments that are presented in the paper.</div><div><br>