×

Coalgebraic satisfiability checking for arithmetic \(\mu\)-calculi. (English) Zbl 07906371

Summary: The coalgebraic \(\mu\)-calculus provides a generic semantic framework for fixpoint logics over systems whose branching type goes beyond the standard relational setup, e.g. probabilistic, weighted, or game-based. Previous work on the coalgebraic \(\mu\)-calculus includes an exponential-time upper bound on satisfiability checking, which however relies on the availability of tableau rules for the next-step modalities that are sufficiently well-behaved in a formally defined sense; in particular, rule matches need to be representable by polynomial-sized codes, and the sequent duals of the rules need to absorb cut. While such rule sets have been identified for some important cases, they are not known to exist in all cases of interest, in particular ones involving either integer weights as in the graded \(\mu\)-calculus, or real-valued weights in combination with non-linear arithmetic. In the present work, we prove the same upper complexity bound under more general assumptions, specifically regarding the complexity of the (much simpler) satisfiability problem for the underlying one-step logic, roughly described as the nesting-free next-step fragment of the logic. The bound is realized by a generic global caching algorithm that supports on-the-fly satisfiability checking. Notably, our approach directly accommodates unguarded formulae, and thus avoids use of the guardedness transformation. Example applications include new exponential-time upper bounds for satisfiability checking in an an extension of the graded \(\mu\)-calculus with polynomial inequalities (including positive Presburger arithmetic), as well as an extension of the (two-valued) probabilistic \(\mu\)-calculus with polynomial inequalities.

MSC:

03B70 Logic in computer science
68-XX Computer science

References:

[1] 9:18 D. Hausmann and L. Schröder Vol. 20:3
[2] 9:24 D. Hausmann and L. Schröder Vol. 20:3
[3] 9:30 D. Hausmann and L. Schröder Vol. 20:3
[4] 9:32 D. Hausmann and L. Schröder Vol. 20:3
[5] ψ n = ⊥: By the invariant and the definition of pre-tableaux, this case does not occur.
[6] ψ n = ϕ 1 ∧ ϕ 2 : Then (q n , ψ n ) belongs to ∀, who moves to (q n+1 , ψ n+1 ) where q n+1 = q n and ψ n+1 ∈ {ϕ 1 , ϕ 2 }. The invariant is preserved by taking u n+1 = δ ′ (u i , τ ).
[7] 9:36 D. Hausmann and L. Schröder Vol. 20:3
[8] Rajeev Alur, Thomas Henzinger, and Orna Kupferman. Alternating-time temporal logic. J. ACM, 49:672-713, 2002. doi:10.1145/585265.585270. · Zbl 1326.68181 · doi:10.1145/585265.585270
[9] Jiří Adámek, Horst Herrlich, and George Strecker. Abstract and concrete categories. Wiley, 1990. Also: Reprints in Theory and Applications of Categories 17 (2006), 1-507. URL: http: //www.tac.mta.ca/tac/reprints/articles/17/tr17.pdf. · Zbl 1113.18001
[10] Peter Aczel and Nax Paul Mendler. A final coalgebra theorem. In David H. Pitt, David E. Rydeheard, Peter Dybjer, Andrew M. Pitts, and Axel Poigné, editors, Category Theory and Computer Science, CTCS 1989, volume 389 of LNCS, pages 357-365. Springer, 1989. doi: 10.1007/BFB0018361. · Zbl 1496.03206 · doi:10.1007/BFB0018361
[11] Patrick Blackburn, Maarten de Rijke, and Yde Venema. Modal Logic, volume 53 of Cam-bridge Tracts in Theoretical Computer Science. Cambridge University Press, 2001. doi: 10.1017/CBO9781107050884. · Zbl 0988.03006 · doi:10.1017/CBO9781107050884
[12] Florian Bruse, Oliver Friedmann, and Martin Lange. On guarded transformation in the modal µ-calculus. Log. J. IGPL, 23(2):194-216, 2015. doi:10.1093/jigpal/jzu030. · Zbl 1405.03048 · doi:10.1093/jigpal/jzu030
[13] Paolo Baldan, Barbara König, Christina Mika-Michalski, and Tommaso Padoan. Fixpoint games on continuous lattices. Proc. ACM Program. Lang., 3(POPL):26:1-26:29, 2019. doi: 10.1145/3290339. · doi:10.1145/3290339
[14] Julian C. Bradfield and Colin Stirling. Modal mu-calculi. In Patrick Blackburn, J. F. A. K. van Benthem, and Frank Wolter, editors, Handbook of Modal Logic, volume 3 of Studies in logic and practical reasoning, pages 721-756. North-Holland, 2007. doi:10.1016/S1570-2464(07)80015-2. · Zbl 1114.03001 · doi:10.1016/S1570-2464(07)80015-2
[15] Falk Bartels, Ana Sokolova, and Erik P. de Vink. A hierarchy of probabilistic system types. Theor. Comput. Sci., 327(1-2):3-22, 2004. doi:10.1016/J.TCS.2004.07.019. · Zbl 1071.68071 · doi:10.1016/J.TCS.2004.07.019
[16] Julian Bradfield and Igor Walukiewicz. The mu-calculus and model checking. In Edmund Clarke, Thomas Henzinger, Helmut Veith, and Roderick Bloem, editors, Handbook of Model Checking, pages 871-919. Springer, 2018. doi:10.1007/978-3-319-10575-8. · doi:10.1007/978-3-319-10575-8
[17] John F. Canny. Some algebraic and geometric computations in PSPACE. In Janos Simon, editor, Symposium on Theory of Computing, STOC 1988, pages 460-467. ACM, 1988. doi: 10.1145/62212.62257. · doi:10.1145/62212.62257
[18] Patrick Cousot and Radhia Cousot. Constructive versions of Tarski’s fixed point theorems. Pacific J. Math., 81(1):43-57, 1979. doi:10.2140/pjm.1979.82.43. · Zbl 0413.06004 · doi:10.2140/pjm.1979.82.43
[19] Rance Cleaveland, S. Purushothaman Iyer, and Murali Narasimha. Probabilistic temporal logics via the modal mu-calculus. Theor. Comput. Sci., 342(2-3):316-350, 2005. doi:10.1016/J.TCS. 2005.03.048. · Zbl 1077.68058 · doi:10.1016/J.TCS.2005.03.048
[20] Souymodip Chakraborty and Joost-Pieter Katoen. On the satisfiability of some simple probabilis-tic logics. In Martin Grohe, Eric Koskinen, and Natarajan Shankar, editors, Logic in Computer Science, LICS 2016, pages 56-65. ACM, 2016. doi:10.1145/2933575.2934526. · Zbl 1394.68169 · doi:10.1145/2933575.2934526
[21] Corina Cîrstea, Clemens Kupke, and Dirk Pattinson. EXPTIME tableaux for the coalgebraic µ-calculus. Log. Meth. Comput. Sci., 7, 2011. doi:10.2168/LMCS-7(3:3)2011. · Zbl 1237.03014 · doi:10.2168/LMCS-7(3:3)2011
[22] CKP + 11b] Corina Cîrstea, Alexander Kurz, Dirk Pattinson, Lutz Schröder, and Yde Venema. Modal logics are coalgebraic. Comput. J., 54(1):31-41, 2011. doi:10.1093/COMJNL/BXP004. · doi:10.1093/COMJNL/BXP004
[23] Sjoerd Cranen, Jeroen J. A. Keiren, and Tim A. C. Willemse. Parity game reductions. Acta Informatica, 55(5):401-444, 2018. doi:10.1007/s00236-017-0301-x. · Zbl 1398.68337 · doi:10.1007/s00236-017-0301-x
[24] Anuj Dawar and Erich Grädel. The descriptive complexity of parity games. In Michael Kaminski and Simone Martini, editors, Computer Science Logic, CSL 2008, volume 5213 of LNCS, pages 354-368. Springer, 2008. doi:10.1007/978-3-540-87531-4. · doi:10.1007/978-3-540-87531-4
[25] Stéphane Demri and Denis Lugiez. Presburger modal logic is PSPACE-complete. In Ulrich Furbach and Natarajan Shankar, editors, Automated Reasoning, IJCAR 2006, volume 4130 of LNCS, pages 541-556. Springer, 2006. doi:10.1007/11814771. · doi:10.1007/11814771
[26] Giovanna D’Agostino and Albert Visser. Finality regained: A coalgebraic study of Scott-sets and multisets. Arch. Math. Log., 41(3):267-298, 2002. doi:10.1007/S001530100110. · Zbl 1023.03049 · doi:10.1007/S001530100110
[27] E.A. Emerson and C.S. Jutla. Tree automata, mu-calculus and determinacy. In [1991] Proceedings 32nd Annual Symposium of Foundations of Computer Science, pages 368-377, 1991. doi:10. 1109/SFCS.1991.185392. · doi:10.1109/SFCS.1991.185392
[28] E. Allen Emerson and Charanjit S. Jutla. The complexity of tree automata and logics of programs. SIAM J. Comput., 29(1):132-158, 1999. doi:10.1137/S0097539793304741. · Zbl 0937.68074 · doi:10.1137/S0097539793304741
[29] Javier Esparza, Jan Kretínský, Jean-François Raskin, and Salomon Sickert. From LTL and limit-deterministic Büchi automata to deterministic parity automata. In Axel Legay and Tiziana Margaria, editors, Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2017, volume 10205 of LNCS, pages 426-442. Springer, 2017. doi:10.1007/978-3-662-54577-5. · doi:10.1007/978-3-662-54577-5
[30] Friedrich Eisenbrand and Gennady Shmonin. Carathéodory bounds for integer cones. Oper. Res. Lett., 34(5):564-568, 2006. doi:10.1016/J.ORL.2005.09.008. · Zbl 1152.90662 · doi:10.1016/J.ORL.2005.09.008
[31] Sebastian Enqvist, Fatemeh Seifan, and Yde Venema. An expressive theorem for coalgebraic modal mu-calculi. Log. Methods Comput. Sci., 13(2), 2017. doi:10.23638/LMCS-13(2: 14)2017. · Zbl 1448.03013 · doi:10.23638/LMCS-13(2:14)2017
[32] Sebastian Enqvist, Fatemeh Seifan, and Yde Venema. Completeness for µ-calculi: A coalgebraic approach. Ann. Pure Appl. Log., 170(5):578-641, 2019. doi:10.1016/j.apal.2018.12.004. · Zbl 1443.03012 · doi:10.1016/j.apal.2018.12.004
[33] Ronald Fagin, Joseph Y. Halpern, and Nimrod Megiddo. A logic for reasoning about probabilities. Inf. Comput., 87(1/2):78-128, 1990. doi:10.1016/0890-5401(90)90060-U. · Zbl 0811.03014 · doi:10.1016/0890-5401(90)90060-U
[34] Oliver Friedmann and Martin Lange. Deciding the unguarded modal µ-calculus. J. Appl. Non-Classical Log., 23:353-371, 2013. doi:10.1080/11663081.2013.861181. · Zbl 1398.03092 · doi:10.1080/11663081.2013.861181
[35] Oliver Friedmann, Markus Latte, and Martin Lange. Satisfiability games for branching-time logics. Log. Methods Comput. Sci., 9, 2013. doi:10.2168/LMCS-9(4:5)2013. · Zbl 1312.03023 · doi:10.2168/LMCS-9(4:5)2013
[36] Gaëlle Fontaine, Raul Andres Leal, and Yde Venema. Automata for coalgebras: An approach using predicate liftings. In Samson Abramsky, Cyril Gavoille, Claude Kirchner, Friedhelm Meyer auf der Heide, and Paul Spirakis, editors, Automata, Languages and Programming, ICALP 2010, volume 6199 of LNCS, pages 381-392. Springer, 2010. doi:10.1007/978-3-642-14162-1. · doi:10.1007/978-3-642-14162-1
[37] GHH + 23] Oliver Görlitz, Daniel Hausmann, Merlin Humml, Dirk Pattinson, Simon Prucker, and Lutz Schröder. COOL 2 -A generic reasoner for modal fixpoint logics (system description). In Brigitte Pientka and Cesare Tinelli, editors, Automated Deduction, CADE 2023, volume 14132 of LNAI, pages 1-14. Springer, 2023. Extended version available as arXiv eprint 2305.11015. doi:10.1007/978-3-031-38499-8_14. · Zbl 07838490 · doi:10.1007/978-3-031-38499-8_14
[38] Víctor Gutiérrez-Basulto, Jean Christoph Jung, Carsten Lutz, and Lutz Schröder. Probabilistic description logics for subjective uncertainty. J. Artif. Intell. Res., 58:1-66, 2017. doi:10.1613/ jair.5222. · Zbl 1401.68305 · doi:10.1613/jair.5222
[39] Rajeev Goré and Linh Anh Nguyen. Exptime tableaux for ALC using sound global caching. J. Autom. Reason., 50(4):355-381, 2013. doi:10.1007/S10817-011-9243-0. · Zbl 1361.68188 · doi:10.1007/S10817-011-9243-0
[40] Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors. Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 of LNCS. Springer, 2002. doi:10.1007/ 3-540-36387-4. · Zbl 1011.00037 · doi:10.1007/3-540-36387-4
[41] Rajeev Goré and Florian Widmann. Sound global state caching for ALC with inverse roles. In Martin Giese and Arild Waaler, editors, Automated Reasoning with Analytic Tableaux and Related Methods, TABLEAUX 2009, volume 5607 of LNCS, pages 205-219. Springer, 2009. doi:10.1007/978-3-642-02716-1_16. · Zbl 1260.68372 · doi:10.1007/978-3-642-02716-1_16
[42] Michael Huth and Marta Kwiatkowska. Quantitative analysis and model checking. In Logic in Computer Science, LICS 1997, pages 111-122. IEEE, 1997. doi:10.1109/LICS.1997.614940. · doi:10.1109/LICS.1997.614940
[43] Thomas A. Henzinger and Nir Piterman. Solving games without determinization. In Zoltán Ésik, editor, Computer Science Logic, CSL 2006, volume 4207 of LNCS, pages 395-410. Springer, 2006. doi:10.1007/11874683_26. · Zbl 1225.68118 · doi:10.1007/11874683_26
[44] Daniel Hausmann and Lutz Schröder. Global caching for the flat coalgebraic µ-calculus. In Fabio Grandi, Martin Lange, and Alessio Lomuscio, editors, Temporal Representation and Reasoning, TIME 2015, pages 121-143. IEEE, 2015. doi:10.1109/TIME.2015.15. · doi:10.1109/TIME.2015.15
[45] Daniel Hausmann and Lutz Schröder. Optimal satisfiability checking for arithmetic µ-calculi. In Mikolaj Bojanczyk and Alex Simpson, editors, Foundations of Software Science and Computation Structures, FOSSACS 2019, volume 11425 of LNCS, pages 277-294. Springer, 2019. doi:10. 1007/978-3-030-17127-8_16. · Zbl 1524.68191 · doi:10.1007/978-3-030-17127-8_16
[46] Daniel Hausmann and Lutz Schröder. Quasipolynomial computation of nested fixpoints. In Jan Friso Groote and Kim Guldstrand Larsen, editors, Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2021, volume 12651 of LNCS, pages 38-56. Springer, 2021. doi:10.1007/978-3-030-72016-2_3. · Zbl 1467.68085 · doi:10.1007/978-3-030-72016-2_3
[47] 9:48 D. Hausmann and L. Schröder Vol. 20:3
[48] Daniel Hausmann, Lutz Schröder, and Hans-Peter Deifel. Permutation games for the weakly aconjunctive µ-calculus. In Dirk Beyer and Marieke Huisman, editors, Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2018, volume 10806 of LNCS, pages 361-378. · Zbl 1423.68307
[49] Springer, 2018. doi:10.1007/978-3-319-89963-3_21. · Zbl 1423.68307 · doi:10.1007/978-3-319-89963-3_21
[50] Daniel Hausmann, Lutz Schröder, and Christoph Egger. Global caching for the alternation-free coalgebraic µ-calculus. In Josée Desharnais and Radha Jagadeesan, editors, Concurrency Theory, CONCUR 2016, volume 59 of LIPIcs, pages 34:1-34:15. Schloss Dagstuhl -Leibniz-Zentrum für Informatik, 2016. doi:10.4230/LIPICS.CONCUR.2016.34. · doi:10.4230/LIPICS.CONCUR.2016.34
[51] Valerie King, Orna Kupferman, and Moshe Vardi. On the complexity of parity word automata. In Furio Honsell and Marino Miculan, editors, Foundations of Software Science and Computation Structures, FOSSACS 2001, volume 2030 of LNCS, pages 276-286. Springer, 2001. doi:10.1007/ 3-540-45315-6_18. · Zbl 0978.68077 · doi:10.1007/3-540-45315-6_18
[52] Clemens Kupke, Johannes Marti, and Yde Venema. Size matters in the modal µ-calculus. CoRR, abs/2010.14430, 2020. URL: https://arxiv.org/abs/2010.14430, arXiv:2010.14430.
[53] Clemens Kupke, Johannes Marti, and Yde Venema. Succinct graph representations of µ-calculus formulas. In Florin Manea and Alex Simpson, editors, Computer Science Logic, CSL 2022, volume 216 of LIPIcs, pages 29:1-29:18. Schloss Dagstuhl -Leibniz-Zentrum für Informatik, 2022. doi:10.4230/LIPIcs.CSL.2022.29. · Zbl 07830385 · doi:10.4230/LIPIcs.CSL.2022.29
[54] Dexter Kozen. Results on the propositional µ-calculus. Theor. Comput. Sci., 27:333-354, 1983. doi:10.1016/0304-3975(82)90125-6. · Zbl 0553.03007 · doi:10.1016/0304-3975(82)90125-6
[55] Clemens Kupke and Dirk Pattinson. On modal logics of linear inequalities. In Lev Beklem-ishev, Valentin Goranko, and Valentin Shehtman, editors, Advances in Modal Logic, AiML 2010, pages 235-255. College Publications, 2010. URL: http://www.aiml.net/volumes/volume8/ Kupke-Pattinson.pdf. · Zbl 1254.03036
[56] Clemens Kupke, Dirk Pattinson, and Lutz Schröder. Reasoning with global assumptions in arithmetic modal logics. In Adrian Kosowski and Igor Walukiewicz, editors, Fundamentals of Computation Theory, FCT 2015, volume 9210 of LNCS, pages 367-380. Springer, 2015. doi:10.1007/978-3-319-22177-9. · doi:10.1007/978-3-319-22177-9
[57] Clemens Kupke, Dirk Pattinson, and Lutz Schröder. Coalgebraic reasoning with global as-sumptions in arithmetic modal logics. ACM Trans. Comput. Log., 23(2):11:1-11:34, 2022. doi:10.1145/3501300. · Zbl 1502.68285 · doi:10.1145/3501300
[58] Orna Kupferman, Ulrike Sattler, and Moshe Vardi. The complexity of the graded µ-calculus. In Andrei Voronkov, editor, Automated Deduction, CADE 02, volume 2392 of LNCS, pages 423-437. · Zbl 1072.03014
[59] Springer, 2002. doi:10.1007/3-540-45620-1_34. · doi:10.1007/3-540-45620-1_34
[60] R. Laver. Well-quasi-orders and sets of finite sequences. Math. Proc. Cambridge Philos. Soc., 79:1-10, 1976. doi:10.1017/S030500410005204X. · Zbl 0405.06001 · doi:10.1017/S030500410005204X
[61] LBC + 94] David E. Long, Anca Browne, Edmund M. Clarke, Somesh Jha, and Wilfredo R. Marrero. An improved algorithm for the evaluation of fixpoint expressions. In Computer Aided Verification, CAV 1994, volume 818 of LNCS, pages 338-350. Springer, 1994. doi:10.1007/3-540-58179-0_66. · doi:10.1007/3-540-58179-0_66
[62] Wanwei Liu, Lei Song, Ji Wang, and Lijun Zhang. A simple probabilistic extension of modal mu-calculus. In Qiang Yang and Michael Wooldridge, editors, International Joint Conference on Artificial Intelligence, IJCAI 2015, pages 882-888. AAAI Press, 2015. URL: http://ijcai.org/ proceedings/2015.
[63] Donald A. Martin. Borel determinacy. Annals of Mathematics, 102(2):363-371, 1975. doi: 10.2307/1971035. · Zbl 0336.02049 · doi:10.2307/1971035
[64] Satoru Miyano and Takeshi Hayashi. Alternating finite automata on ω-words. Theor. Comput. Sci., 32:321-330, 1984. doi:10.1016/0304-3975(84)90049-5. · Zbl 0544.68042 · doi:10.1016/0304-3975(84)90049-5
[65] Matteo Mio. Probabilistic modal µ-calculus with independent product. In Martin Hofmann, editor, Foundations of Software Science and Computational Structures, FOSSACS 2011, volume 6604 of LNCS, pages 290-304. Springer, 2011. doi:10.1007/978-3-642-19805-2. · doi:10.1007/978-3-642-19805-2
[66] Annabelle McIver and Carroll Morgan. Results on the quantitative µ-calculus qmµ. ACM Trans. Comput. Log., 8, 2007. doi:10.1145/1182613.1182616. · Zbl 1367.68199 · doi:10.1145/1182613.1182616
[67] Lawrence Moss. Coalgebraic logic. Ann. Pure Appl. Log., 96(1-3):277-317, 1999. doi:10.1016/ S0168-0072(98)00042-6. · Zbl 0969.03026 · doi:10.1016/S0168-0072(98)00042-6
[68] Vol. 20:3 COALGEBRAIC SATISFIABILITY CHECKING FOR ARITHMETIC µ-CALCULI 9:49
[69] Robert Myers, Dirk Pattinson, and Lutz Schröder. Coalgebraic hybrid logic. In Luca de Alfaro, editor, Foundations of Software Science and Computational Structures, FOSSACS 2009, volume 5504 of LNCS, pages 137-151. Springer, 2009. doi:10.1007/978-3-642-00596-1. · doi:10.1007/978-3-642-00596-1
[70] Johannes Marti and Yde Venema. Lax extensions of coalgebra functors and their logic. J. Comput. Syst. Sci., 81(5):880-900, 2015. doi:10.1016/j.jcss.2014.12.006. · Zbl 1328.03061 · doi:10.1016/j.jcss.2014.12.006
[71] Damian Niwinski and Igor Walukiewicz. Games for the µ-calculus. Theor. Comput. Sci., 163:99-116, 1996. doi:10.1016/0304-3975(95)00136-0. · Zbl 0872.03017 · doi:10.1016/0304-3975(95)00136-0
[72] Rohit Parikh. Propositional game logic. In Foundations of Computer Science, FOCS 1983. IEEE Computer Society, 1983. doi:10.1109/SFCS.1983.47. · doi:10.1109/SFCS.1983.47
[73] Rohit Parikh. The logic of games and its applications. Ann. Discrete Math., 24:111-140, 1985. doi:10.1016/S0304-0208(08)73078-0. · Zbl 0552.90110 · doi:10.1016/S0304-0208(08)73078-0
[74] Dirk Pattinson. Coalgebraic modal logic: Soundness, completeness and decidability of local consequence. Theor. Comput. Sci., 309:177-193, 2003. doi:10.1016/S0304-3975(03)00201-9. · Zbl 1052.03009 · doi:10.1016/S0304-3975(03)00201-9
[75] Dirk Pattinson. Expressive logics for coalgebras via terminal sequence induction. Notre Dame J. Formal Logic, 45:19-33, 2004. doi:10.1305/NDJFL/1094155277. · Zbl 1088.03031 · doi:10.1305/NDJFL/1094155277
[76] Marc Pauly. Logic for social software. PhD thesis, University of Amsterdam, 2001. URL: https: //eprints.illc.uva.nl/id/eprint/2029/.
[77] Nir Piterman. From nondeterministic Büchi and Streett automata to deterministic parity automata. Log. Meth. Comput. Sci., 3, 2007. doi:10.2168/LMCS-3(3:5)2007. · Zbl 1125.68067 · doi:10.2168/LMCS-3(3:5)2007
[78] Marc Pauly and Rohit Parikh. Game logic -an overview. Stud. Log., 75(2):165-182, 2003. doi:10.1023/A:1027354826364. · Zbl 1040.03013 · doi:10.1023/A:1027354826364
[79] Dirk Pattinson and Lutz Schröder. Cut elimination in coalgebraic logics. Inf. Comput., 208(12):1447-1468, 2010. doi:10.1016/j.ic.2009.11.008. · Zbl 1255.03052 · doi:10.1016/j.ic.2009.11.008
[80] Jan Rutten and Erik de Vink. Bisimulation for probabilistic transition systems: a coalgebraic approach. Theor. Comput. Sci., 221:271-293, 1999. doi:10.1016/S0304-3975(99)00035-3. · Zbl 0930.68092 · doi:10.1016/S0304-3975(99)00035-3
[81] Jan Rutten. Universal coalgebra: A theory of systems. Theor. Comput. Sci., 249:3-80, 2000. doi:10.1016/S0304-3975(00)00056-6. · Zbl 0951.68038 · doi:10.1016/S0304-3975(00)00056-6
[82] Shmuel Safra. On the complexity of omega-automata. In Foundations of Computer Science, FOCS 1988, pages 319-327. IEEE Computer Society, 1988. doi:10.1109/SFCS.1988.21948. · doi:10.1109/SFCS.1988.21948
[83] Alexander Schrijver. Theory of linear and integer programming. Wiley Interscience, 1986. · Zbl 0665.90063
[84] Lutz Schröder. A finite model construction for coalgebraic modal logic. J. Log. Algebr. Prog., 73:97-110, 2007. doi:10.1016/J.JLAP.2006.11.004. · Zbl 1127.03014 · doi:10.1016/J.JLAP.2006.11.004
[85] Lutz Schröder. Expressivity of coalgebraic modal logic: The limits and beyond. Theor. Comput. Sci., 390(2-3):230-247, 2008. doi:10.1016/j.tcs.2007.09.023. · Zbl 1132.03008 · doi:10.1016/j.tcs.2007.09.023
[86] Robert S. Streett and E. Allen Emerson. An automata theoretic decision procedure for the propositional mu-calculus. Inf. Comput., 81(3):249-264, 1989. · Zbl 0671.03023
[87] Helmut Seidl. Fast and Simple Nested Fixpoints. Inf. Process. Lett., 59:303-308, 1996. doi: 10.1016/0020-0190(96)00130-5. · Zbl 0900.68458 · doi:10.1016/0020-0190(96)00130-5
[88] Lutz Schröder and Dirk Pattinson. Shallow models for non-iterative modal logics. In Andreas Dengel, Karsten Berns, Thomas Breuel, Frank Bomarius, and Thomas Roth-Berghofer, editors, Advances in Artificial Intelligence, KI 2008, volume 5243 of LNCS, pages 324-331. Springer, 2008. doi:10.1007/978-3-540-85845-4. · Zbl 1147.68305 · doi:10.1007/978-3-540-85845-4
[89] Lutz Schröder and Dirk Pattinson. 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 · doi:10.1145/1462179.1462185
[90] Lutz Schröder and Dirk Pattinson. Rank-1 modal logics are coalgebraic. J. Log. Comput., 20:1113-1147, 2010. doi:10.1093/logcom/exn096. · Zbl 1266.03032 · doi:10.1093/logcom/exn096
[91] Lutz Schröder and Dirk Pattinson. Modular algorithms for heterogeneous modal logics via multi-sorted coalgebra. Math. Struct. Comput. Sci., 21:235-266, 2011. doi:10.1017/ S0960129510000563. · Zbl 1260.03061 · doi:10.1017/S0960129510000563
[92] Sven Schewe and Thomas Varghese. Determinising parity automata. In Erzsébet Csuhaj-Varjú, Martin Dietzfelbinger, and Zoltán Ésik, editors, Mathematical Foundations of Com-puter Science, MFCS 2014, volume 8634 of LNCS, pages 486-498. Springer, 2014. doi: 10.1007/978-3-662-44522-8. · doi:10.1007/978-3-662-44522-8
[93] Lutz Schröder and Yde Venema. Completeness of flat coalgebraic fixpoint logics. ACM Trans. Comput. Log., 19(1):4:1-4:34, 2018. doi:10.1145/3157055. · Zbl 1407.03049 · doi:10.1145/3157055
[94] 9:50 D. Hausmann and L. Schröder Vol. 20:3 · Zbl 07906371
[95] M.Y. Vardi. On the complexity of epistemic reasoning. In [1989] Proceedings. Fourth Annual Symposium on Logic in Computer Science, pages 243-252, 1989. doi:10.1109/LICS.1989.39179. · Zbl 0717.03006 · doi:10.1109/LICS.1989.39179
[96] Yde Venema. Automata and fixed point logics for coalgebras. In Jirí Adámek and Stefan Milius, editors, Coalgebraic Methods in Computer Science, CMCS 2004, volume 106 of ENTCS, pages 355-375. Elsevier, 2004. doi:10.1016/j.entcs.2004.02.038. · Zbl 1271.68155 · doi:10.1016/j.entcs.2004.02.038
[97] Yde Venema. Automata and fixed point logic: A coalgebraic perspective. Inf. Comput., 204(4):637-678, 2006. doi:10.1016/j.ic.2005.06.003. · Zbl 1110.68066 · doi:10.1016/j.ic.2005.06.003
[98] Thomas Wilke. Alternating tree automata, parity games, and modal µ-calculus. Bull. Belg. Math. Soc., 8(2):359-391, 2001. doi:10.36045/bbms/1102714178. This work is licensed under the Creative Commons Attribution License. To view a copy of this license, visit https://creativecommons.org/licenses/by/4.0/ or send a letter to Creative Commons, 171 Second St, Suite 300, San Francisco, CA 94105, USA, or Eisenacher Strasse 2, 10777 Berlin, Germany · doi:10.36045/bbms/1102714178
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.