COOL 2 – a generic reasoner for modal fixpoint logics (system description). (English) Zbl 07838490
Pientka, Brigitte (ed.) et al., Automated deduction – CADE 29. 29th international conference on automated deduction, Rome, Italy, July 1–4, 2023. Proceedings. Cham: Springer. Lect. Notes Comput. Sci. 14132, 234-247 (2023).
Summary: There is a wide range of modal logics whose semantics goes beyond relational structures, and instead involves, e.g., probabilities, multi-player games, weights, or neighbourhood structures. Coalgebraic logic serves as a unifying semantic and algorithmic framework for such logics. It provides uniform reasoning algorithms that are easily instantiated to particular, concretely given logics. The COOL 2 reasoner provides an implementation of such generic algorithms for coalgebraic modal fixpoint logics. As concrete instances, we obtain in particular reasoners for the aconjunctive and alternation-free fragments of the graded \(\mu \)-calculus and the alternating-time \(\mu \)-calculus. We evaluate the tool on standard benchmark sets for fixpoint-free graded modal logic and alternating-time temporal logic (ATL), as well as on a dedicated set of benchmarks for the graded \(\mu \)-calculus.
For the entire collection see [Zbl 1535.68012].
For the entire collection see [Zbl 1535.68012].
MSC:
| 03B35 | Mechanization of proofs and logical operations |
| 68V15 | Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) |
References:
| [1] | Alur, R.; Henzinger, T.; Kupferman, O., Alternating-time temporal logic, J. ACM, 49, 672-713 (2002) · Zbl 1326.68181 · doi:10.1145/585265.585270 |
| [2] | Calin, G., Myers, R., Pattinson, D., Schröder, L.: CoLoSS: the coalgebraic logic satisfiability solver. In: Methods for Modalities, M4M-5. ENTCS, vol. 231, pp. 41-54. Elsevier (2009). doi:10.1016/j.entcs.2009.02.028 · Zbl 1347.68300 |
| [3] | Cîrstea, C., Kupke, C., Pattinson, D.: EXPTIME tableaux for the coalgebraic \(\mu \)-calculus. Log. Meth. Comput. Sci. 7 (2011). doi:10.2168/LMCS-7(3:3)2011 · Zbl 1237.03014 |
| [4] | Cîrstea, C.; Kurz, A.; Pattinson, D.; Schröder, L.; Venema, Y., Modal logics are coalgebraic, Comput. J., 54, 31-41 (2011) · doi:10.1093/comjnl/bxp004 |
| [5] | D’Agostino, G.; Visser, A., Finality regained: a coalgebraic study of Scott-sets and multisets, Arch. Math. Logic, 41, 267-298 (2002) · Zbl 1023.03049 · doi:10.1007/s001530100110 |
| [6] | David, A.; Galmiche, D.; Larchey-Wendling, D., TATL: implementation of ATL tableau-based decision procedure, Automated Reasoning with Analytic Tableaux and Related Methods, 97-103 (2013), Heidelberg: Springer, Heidelberg · Zbl 1401.68276 · doi:10.1007/978-3-642-40537-2_10 |
| [7] | David, A.; Felty, AP; Middeldorp, A., Deciding \(\sf ATL^*\) satisfiability by tableaux, Automated Deduction - CADE-25, 214-228 (2015), Cham: Springer, Cham · Zbl 1465.68278 · doi:10.1007/978-3-319-21401-6_14 |
| [8] | Eén, N.; Sörensson, N.; Giunchiglia, E.; Tacchella, A., An extensible SAT-solver, Theory and Applications of Satisfiability Testing, 502-518 (2004), Heidelberg: Springer, Heidelberg · Zbl 1204.68191 · doi:10.1007/978-3-540-24605-3_37 |
| [9] | Esparza, J.; Kretínský, J.; Raskin, J.; Sickert, S., From linear temporal logic and limit-deterministic Büchi automata to deterministic parity automata, Int. J. Softw. Tools Technol. Transf., 24, 4, 635-659 (2022) · Zbl 1452.68105 · doi:10.1007/s10009-022-00663-1 |
| [10] | Friedmann, O., Lange, M.: The PGSolver collection of parity game solvers. Technical report, LMU Munich (2009) |
| [11] | Friedmann, O., Lange, M.: A solver for modal fixpoint logics. In: Methods for Modalities, M4M-6 2009. ENTCS, vol. 262, pp. 99-111 (2010). doi:10.1016/j.entcs.2010.04.008 |
| [12] | Glimm, B.; Horrocks, I.; Motik, B.; Stoilos, G.; Wang, Z., HermiT: an OWL 2 reasoner, J. Autom. Reason., 53, 3, 245-269 (2014) · Zbl 1314.68280 · doi:10.1007/s10817-014-9305-1 |
| [13] | Goré, R.; Kupke, C.; Pattinson, D.; Schröder, L.; Giesl, J.; Hähnle, R., Global caching for coalgebraic description logics, Automated Reasoning, 46-60 (2010), Heidelberg: Springer, Heidelberg · Zbl 1291.03017 · doi:10.1007/978-3-642-14203-1_5 |
| [14] | Goré, R., Thomson, J., Widmann, F.: An experimental comparison of theorem provers for CTL. In: Temporal Representation and Reasoning, TIME 2011, pp. 49-56. IEEE (2011). doi:10.1109/TIME.2011.16 |
| [15] | Gorín, D.; Pattinson, D.; Schröder, L.; Widmann, F.; Wißmann, T.; Demri, S.; Kapur, D.; Weidenbach, C., Cool – a generic reasoner for coalgebraic hybrid logics (system description), Automated Reasoning, 396-402 (2014), Cham: Springer, Cham · doi:10.1007/978-3-319-08587-6_31 |
| [16] | Göttlinger, M., Schröder, L., Pattinson, D.: The alternating-time \(\mu \)-calculus with disjunctive explicit strategies. In: Baier, C., Goubault-Larrecq, J. (eds.) Computer Science Logic, CSL 2021. LIPIcs, vol. 183, pp. 26:1-26:22. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2021). doi:10.4230/LIPIcs.CSL.2021.26 |
| [17] | Görlitz, O., Hausmann, D., Humml, M., Pattinson, D., Prucker, S., Schröder, L.: Cool 2 - a generic reasoner for modal fixpoint logics (2023). https://arxiv.org/abs/2305.11015 |
| [18] | Haarslev, V.; Möller, R.; Goré, R.; Leitsch, A.; Nipkow, T., RACER system description, Automated Reasoning, 701-705 (2001), Heidelberg: Springer, Heidelberg · Zbl 0988.68599 · doi:10.1007/3-540-45744-5_59 |
| [19] | Hansen, HH; Kupke, C.; Marti, J.; Venema, Y.; Madeira, A.; Benevides, M., Parity games and automata for game logic, Dynamic Logic. New Trends and Applications, 115-132 (2018), Cham: Springer, Cham · Zbl 1499.03024 · doi:10.1007/978-3-319-73579-5_8 |
| [20] | Hansson, H.; Jonsson, B., A logic for reasoning about time and reliability, Formal Asp. Comput., 6, 512-535 (1994) · Zbl 0820.68113 · doi:10.1007/BF01211866 |
| [21] | Hausmann, D.; Schröder, L.; Bojańczyk, M.; Simpson, A., Optimal satisfiability checking for arithmetic \(\mu \)-calculi, Foundations of Software Science and Computation Structures, 277-294 (2019), Cham: Springer, Cham · Zbl 1524.68191 · doi:10.1007/978-3-030-17127-8_16 |
| [22] | Hausmann, D.; Schröder, L.; Deifel, H-P; Beyer, D.; Huisman, M., Permutation games for the weakly aconjunctive \(\mu \)-calculus, Tools and Algorithms for the Construction and Analysis of Systems, 361-378 (2018), Cham: Springer, Cham · Zbl 1423.68307 · doi:10.1007/978-3-319-89963-3_21 |
| [23] | Hausmann, D., Schröder, L., Egger, C.: Global caching for the alternation-free coalgebraic \(\mu \)-calculus. In: Concurrency Theory, CONCUR 2016. LIPIcs, vol. 59, pp. 34:1-34:15. Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2016). doi:10.4230/LIPIcs.CONCUR.2016.34 · Zbl 1392.68301 |
| [24] | Kozen, D., Results on the propositional \(\mu \)-calculus, Theor. Comput. Sci., 27, 333-354 (1983) · Zbl 0553.03007 · doi:10.1016/0304-3975(82)90125-6 |
| [25] | Kupferman, O.; Piterman, N.; Vardi, MY; Dershowitz, N., Fair equivalence relations, Verification: Theory and Practice, 702-732 (2003), Heidelberg: Springer, Heidelberg · Zbl 1274.68194 · doi:10.1007/978-3-540-39910-0_30 |
| [26] | Kupferman, O.; Sattler, U.; Vardi, MY; Voronkov, A., The complexity of the graded \(\mu \)-calculus, Automated Deduction—CADE-18, 423-437 (2002), Heidelberg: Springer, Heidelberg · Zbl 1072.03014 · doi:10.1007/3-540-45620-1_34 |
| [27] | Kupke, C., Marti, J., Venema, Y.: Size measures and alphabetic equivalence in the \(\mu \)-calculus. In: Baier, C., Fisman, D. (eds.) Logic in Computer Science, LICS 2022, pp. 18:1-18:13. ACM (2022). doi:10.1145/3531130.3533339 |
| [28] | Kupke, C., Pattinson, D.: On modal logics of linear inequalities. In: Advances in Modal Logic, AiML 2010, pp. 235-255. College Publications (2010) · Zbl 1254.03036 |
| [29] | Kupke, C., Pattinson, D., Schröder, L.: Coalgebraic reasoning with global assumptions in arithmetic modal logics. ACM Trans. Comput. Log. 23(2), 11:1-11:34 (2022). doi:10.1145/3501300 · Zbl 1502.68285 |
| [30] | Larsen, K.; Skou, A., Bisimulation through probabilistic testing, Inform. Comput., 94, 1-28 (1991) · Zbl 0756.68035 · doi:10.1016/0890-5401(91)90030-6 |
| [31] | Miyano, S.; Hayashi, T., Alternating finite automata on \(\omega \)-words, Theor. Comput. Sci., 32, 321-330 (1984) · Zbl 0544.68042 · doi:10.1016/0304-3975(84)90049-5 |
| [32] | Nalon, C., Zhang, L., Dixon, C., Hustadt, U.: A resolution prover for coalition logic. In: Mogavero, F., Murano, A., Vardi, M.Y. (eds.) Strategic Reasoning, SR 2014. EPTCS, vol. 146, pp. 65-73 (2014). doi:10.4204/EPTCS.146.9 · Zbl 1464.68432 |
| [33] | Niwiński, D.; Kott, L., On fixed-point clones, Automata, Languages and Programming, 464-473 (1986), Heidelberg: Springer, Heidelberg · Zbl 0596.68036 · doi:10.1007/3-540-16761-7_96 |
| [34] | Parikh, R.: Propositional game logic. In: Foundations of Computer Science, FOCS 1983. IEEE Computer Society (1983). doi:10.1109/SFCS.1983.47 · Zbl 0539.68016 |
| [35] | Pattinson, D., Expressive logics for coalgebras via terminal sequence induction, Notre Dame J. Formal Logic, 45, 19-33 (2004) · Zbl 1088.03031 · doi:10.1305/ndjfl/1094155277 |
| [36] | Pauly, M., A modal logic for coalitional power in games, J. Logic Comput., 12, 149-166 (2002) · Zbl 1003.91006 · doi:10.1093/logcom/12.1.149 |
| [37] | Peleg, D., Concurrent dynamic logic, J. ACM, 34, 450-479 (1987) · Zbl 0645.03021 · doi:10.1145/23005.23008 |
| [38] | Rutten, J., Universal coalgebra: a theory of systems, Theor. Comput. Sci., 249, 3-80 (2000) · Zbl 0951.68038 · doi:10.1016/S0304-3975(00)00056-6 |
| [39] | Schewe, S.: Synthesis of distributed systems. Ph.D. thesis, Universität des Saarlands (2008) |
| [40] | Schröder, L., Expressivity of coalgebraic modal logic: the limits and beyond, Theor. Comput. Sci., 390, 2-3, 230-247 (2008) · Zbl 1132.03008 · doi:10.1016/j.tcs.2007.09.023 |
| [41] | Schröder, L., Pattinson, D.: PSPACE bounds for rank-1 modal logics. ACM Trans. Comput. Log. 10(2), 13:1-13:33 (2009). doi:10.1145/1462179.1462185 · Zbl 1351.03015 |
| [42] | Sirin, E.; Parsia, B.; Grau, BC; Kalyanpur, A.; Katz, Y., Pellet: a practical OWL-DL reasoner, J. Web Semant., 5, 2, 51-53 (2007) · doi:10.1016/j.websem.2007.03.004 |
| [43] | Snell, W.; Pattinson, D.; Widmann, F.; Bjørner, N.; Voronkov, A., Solving graded/probabilistic modal logic via linear inequalities (system description), Logic for Programming, Artificial Intelligence, and Reasoning, 383-390 (2012), Heidelberg: Springer, Heidelberg · Zbl 1352.68215 · doi:10.1007/978-3-642-28717-6_30 |
| [44] | Tsarkov, D.; Horrocks, I.; Furbach, U.; Shankar, N., FaCT++ description logic reasoner: system description, Automated Reasoning, 292-297 (2006), Heidelberg: Springer, Heidelberg · doi:10.1007/11814771_26 |
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. In some cases that data have been complemented/enhanced by data from zbMATH Open. This attempts to reflect the references listed in the original paper as accurately as possible without claiming completeness or a perfect matching.
