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

Artifact for the Paper "<i>Permutation Games for the Weakly Aconjunctive mu-Calculus</i>" TACAS 2018<br>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>(Solver for Modal Fixpoint Logics), a binary that generates test-formulas and a script that benchmarks various families of generated formulas with different variants of the two provers.<br>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.<br>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.<br>The tested variants of the provers are the ones that occur in Figures 1-4 of the paper:<br>"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""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""MLSolver": MSolver without -opt litpro and -opt comp, using PGSolver with algorithm "stratimprloc2" to solve games; in the script, this variant is called "mlsolver""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"<br>Figure 1 shows the runtimes for the unsatisfiable theta_1-formulas (in the script, this family of formulas is called "enpa_is_enba_neg").Figure 2 shows the runtimes for the unsatisfiable theta_2-formulas (in the script, this family of formulas is called "pg_domgame_neg").<br>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.<br>Figure 3 shows the runtimes for the unsatisfiable early-ac(n,4,2) formulas (in the script, these formulas are called "early_ac").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").<br>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.<br>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. <br>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.<br>

本工件对应2018年TACAS会议收录的论文《Permutation Games for the Weakly Aconjunctive μ-Calculus》（弱合取μ演算）。本工件聚焦该论文的第4节（实现与基准测试），论文作者为Daniel Hausmann、Lutz Schröder与Hans-Peter Deifel。

本工件包含两款可满足性检查器的二进制文件：**COOL**（Coalgebraic Ontology Logic Reasoner，余代数本体逻辑推理器，实现了论文中提出的算法）与**MLSolver**（模态不动点逻辑求解器），一个用于生成测试公式的二进制程序，以及一个用于使用两种推理器的不同变体对各类生成公式族进行基准测试的脚本。

本工件以单个**.zip**压缩包形式提供。脚本包含Bash Shell格式（**.sh**）与Perl格式（**.pl**）的版本。额外的版权、源代码与许可细节详见子目录“licenses”。**COOL**与**MLSolver**的二进制文件可通过提供的脚本文件自由使用。

以下说明与本数据集记录关联的TACAS会议出版物相关。该相关研究提出了一种方法，使用极限确定性奇偶自动机为μ演算（mu-Calculus）的弱合取片段构建可满足性博弈。

本次测试的推理器变体与论文图1至图4中所呈现的版本完全一致：
1. "COOL"：未启用实时求解（on-the-fly solving）的COOL，使用PGSolver的"stratimprloc2"算法求解博弈；在配套脚本中，该变体被命名为"cool-pgsolver-noprop"
2. "COOL on-the-fly"：启用实时求解的COOL，使用我们自研的不动点迭代算法求解博弈；在配套脚本中，该变体被命名为"cool"
3. "MLSolver"：未启用`-opt litpro`与`-opt comp`选项的MLSolver，使用PGSolver的"stratimprloc2"算法求解博弈；在配套脚本中，该变体被命名为"mlsolver"
4. "MLSolverOpt"：启用`-opt litpro`与`-opt comp`选项的MLSolver，使用PGSolver的"stratimprloc2"算法求解博弈；在配套脚本中，该变体被命名为"mlsolver-opt"

图1展示了不可满足的theta_1公式的运行时（该公式族在脚本中名为"enpa_is_enba_neg"）。图2展示了不可满足的theta_2公式的运行时（该公式族在脚本中名为"pg_domgame_neg"）。

关于图1与图2的几点观测：根据理论结果，COOL中的可满足性博弈规模为O((n²)!)，而MLSolver中的博弈规模为O(((n²)!)²)，因此COOL的运行时长更短。对于这类公式，实时求解并无增益，因为博弈中不存在可提前判定的节点；反而实时求解会增加额外计算量，导致这类公式的运行时长更长。此外，我们自研的不动点迭代实现的性能低于优化后的采用"stratimprloc2"算法的PGSolver，但该优化求解器无法用于实时求解场景。

图3展示了不可满足的early-ac(n,4,2)公式的运行时（该类公式在脚本中名为"early_ac"）。图4展示了不可满足的early-ac_gc(n,4,2)公式的运行时（该类公式在脚本中名为"early_caching_ac"）。

关于图3与图4的几点观测：COOL中的博弈规模为O((n²)!)，MLSolver中的博弈规模为O(((n²)!)²)，因此COOL的运行时长更短。实时求解可显著降低这类公式的运行时长。尽管我们自研的不动点迭代实现未经过优化，性能低于采用"stratimprloc2"算法的PGSolver，但实时求解能力可大幅缩减可满足性博弈的规模，最终带来更短的运行时长。在图3中，从n=11开始，实时求解带来的增益超过了自研博弈求解器的性能劣势；在图4中，该临界点为n=8。

本工件还包含一个**results.txt**文件，其中收录了论文图1至图4中所有公式与推理器对应的运行时数据。所有实验均在搭载Intel Core i7 3.60GHz CPU、64位字长与16GB RAM的机器上完成，图1与图2的实验设置了100秒的超时限制，图3与图4的实验超时限制为1000秒。

如前所述，本工件包含的脚本允许用户复现论文中展示的所有实验。