{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:34:49Z","timestamp":1750221289538,"version":"3.41.0"},"reference-count":54,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2018,1,6]],"date-time":"2018-01-06T00:00:00Z","timestamp":1515196800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2018,1,31]]},"abstract":"<jats:p>\n            Modal fixpoint logics traditionally play a central role in computer science, in particular in artificial intelligence and concurrency. The \u03bc-calculus and its relatives are among the most expressive logics of this type. However, popular fixpoint logics tend to trade expressivity for simplicity and readability and in fact often live within the single variable fragment of the \u03bc-calculus. The family of such\n            <jats:italic>flat<\/jats:italic>\n            fixpoint logics includes, e.g., Linear Temporal Logic (LTL), Computation Tree Logic (CTL), and the logic of common knowledge. Extending this notion to the generic semantic framework of\n            <jats:italic>coalgebraic logic<\/jats:italic>\n            enables covering a wide range of logics beyond the standard \u03bc-calculus including, e.g., flat fragments of the graded \u03bc-calculus and the alternating-time \u03bc-calculus (such as alternating-time temporal logic), as well as probabilistic and monotone fixpoint logics. We give a generic proof of completeness of the Kozen-Park axiomatization for such flat coalgebraic fixpoint logics.\n          <\/jats:p>","DOI":"10.1145\/3157055","type":"journal-article","created":{"date-parts":[[2018,1,8]],"date-time":"2018-01-08T13:27:20Z","timestamp":1515418040000},"page":"1-34","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Completeness of Flat Coalgebraic Fixpoint Logics"],"prefix":"10.1145","volume":"19","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3146-5906","authenticated-orcid":false,"given":"Lutz","family":"Schr\u00f6der","sequence":"first","affiliation":[{"name":"Friedrich-Alexander-Universit\u00e4t Erlangen-N\u00fcrnberg, Germany"}]},{"given":"Yde","family":"Venema","sequence":"additional","affiliation":[{"name":"ILLC, Universiteit van Amsterdam, GE Amsterdam, The Netherlands"}]}],"member":"320","published-online":{"date-parts":[[2018,1,6]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/585265.585270"},{"key":"e_1_2_1_2_1","unstructured":"Franz Baader Diego Calvanese Deborah McGuinness Daniele Nardi and Peter Patel-Schneider (Eds.). 2003. The Description Logic Handbook. Cambridge University Press.  Franz Baader Diego Calvanese Deborah McGuinness Daniele Nardi and Peter Patel-Schneider (Eds.). 2003. The Description Logic Handbook. Cambridge University Press."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781107050884"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511621192"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.2168\/LMCS-7(3:3)2011"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2007.06.002"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1007\/s001530100110"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90269-0"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00374047"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1016\/B978-0-444-88074-1.50021-4"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1016\/0167-6423(83)90017-5"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1016\/0022-0000(85)90001-7"},{"key":"e_1_2_1_13_1","volume-title":"Logic in Computer Science","volume":"86","author":"Allen Emerson E.","year":"1986","unstructured":"E. Allen Emerson and Chin-Laung Lei . 1986 . Efficient model checking in fragments of the propositional mu-calculus . In Logic in Computer Science , Vol. 86 . IEEE, 267--278. E. Allen Emerson and Chin-Laung Lei. 1986. Efficient model checking in fragments of the propositional mu-calculus. In Logic in Computer Science, Vol. 86. IEEE, 267--278."},{"key":"e_1_2_1_14_1","volume-title":"Jean-Marc Talbot and Laurent Regnier (Eds.)","volume":"62","author":"Enqvist Sebastian","year":"2016","unstructured":"Sebastian Enqvist , Fatemeh Seifan , and Yde Venema . 2016 . Completeness for coalgebraic fixpoint logic. In Computer Science Logic , Jean-Marc Talbot and Laurent Regnier (Eds.) , Vol. 62 . Schloss Dagstuhl -- Leibniz-Zentrum f\u00fcr Informatik, 7:1--7:19. Sebastian Enqvist, Fatemeh Seifan, and Yde Venema. 2016. Completeness for coalgebraic fixpoint logic. In Computer Science Logic, Jean-Marc Talbot and Laurent Regnier (Eds.), Vol. 62. Schloss Dagstuhl -- Leibniz-Zentrum f\u00fcr Informatik, 7:1--7:19."},{"key":"e_1_2_1_15_1","unstructured":"Sebastian Enqvist Fatemeh Seifan and Yde Venema. 2017. Completeness for &mu;-calculi: a coalgebraic approach (unpublished).  Sebastian Enqvist Fatemeh Seifan and Yde Venema. 2017. Completeness for &mu;-calculi: a coalgebraic approach (unpublished)."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/174652.174658"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1093890715"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/B978-1-4832-1452-8.50115-9"},{"key":"e_1_2_1_19_1","volume-title":"Proceedings of the Conference on Principles of Programming Languages (POPL\u201980)","author":"Gabbay Dov","year":"1980","unstructured":"Dov Gabbay , Amir Pnueli , Saharon Shelah , and Jonathan Stavi . 1980 . On the temporal basis of fairness . In Proceedings of the Conference on Principles of Programming Languages (POPL\u201980) , Paul Abrahams, Richard Lipton, and Stephen Bourne (Eds.). ACM Press, 163--173. Dov Gabbay, Amir Pnueli, Saharon Shelah, and Jonathan Stavi. 1980. On the temporal basis of fairness. In Proceedings of the Conference on Principles of Programming Languages (POPL\u201980), Paul Abrahams, Richard Lipton, and Stephen Bourne (Eds.). ACM Press, 163--173."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.07.043"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1109\/TIME.2015.15"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.1006\/game.1999.0788"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1997.614940"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(81)90019-0"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45620-1_34"},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the Conference on Advances in Modal Logic (AiML\u201910)","author":"Kupke Clemens","year":"2010","unstructured":"Clemens Kupke and Dirk Pattinson . 2010 . On modal logics of linear inequalities . In Proceedings of the Conference on Advances in Modal Logic (AiML\u201910) , Lev Beklemishev, Valentin Goranko, and Valentin Shehtman (Eds.). College Publications, 235--255. Clemens Kupke and Dirk Pattinson. 2010. On modal logics of linear inequalities. In Proceedings of the Conference on Advances in Modal Logic (AiML\u201910), Lev Beklemishev, Valentin Goranko, and Valentin Shehtman (Eds.). College Publications, 235--255."},{"key":"e_1_2_1_28_1","volume-title":"Proceedings of the Foundations of Software Technology and Theoretical Computer Science (FSTTCS\u201916)","volume":"65","author":"Larsen Kim","year":"2016","unstructured":"Kim Larsen , Radu Mardare , and Bingtian Xue . 2016 . Probabilistic -calculus: Decidability and complete axiomatization . In Proceedings of the Foundations of Software Technology and Theoretical Computer Science (FSTTCS\u201916) , Akash Lal, S. Akshay, Saket Saurabh, and Sandeep Sen (Eds.) , Vol. 65 . Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 25:1--25:18. Kim Larsen, Radu Mardare, and Bingtian Xue. 2016. Probabilistic -calculus: Decidability and complete axiomatization. In Proceedings of the Foundations of Software Technology and Theoretical Computer Science (FSTTCS\u201916), Akash Lal, S. Akshay, Saket Saurabh, and Sandeep Sen (Eds.), Vol. 65. Schloss Dagstuhl--Leibniz-Zentrum fuer Informatik, 25:1--25:18."},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(91)90030-6"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1017\/S030500410005204X"},{"key":"e_1_2_1_31_1","volume-title":"Convention, A Philosophical Study","author":"Lewis David","year":"1969","unstructured":"David Lewis . 1969 . Convention, A Philosophical Study . Harvard University Press. David Lewis. 1969. Convention, A Philosophical Study. Harvard University Press."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/8.1.55"},{"key":"e_1_2_1_33_1","volume-title":"Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI\u201915)","author":"Liu Wanwei","year":"2015","unstructured":"Wanwei Liu , Lei Song , Ji Wang , and Lijun Zhang . 2015 . A simple probabilistic extension of modal mu-calculus . In Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI\u201915) , Qiang Yang and Michael Wooldridge (Eds.). AAAI Press, 882--888. Wanwei Liu, Lei Song, Ji Wang, and Lijun Zhang. 2015. A simple probabilistic extension of modal mu-calculus. In Proceedings of the International Joint Conference on Artificial Intelligence (IJCAI\u201915), Qiang Yang and Michael Wooldridge (Eds.). AAAI Press, 882--888."},{"key":"e_1_2_1_34_1","volume-title":"Formal Methods Pacific","author":"Morgan Carroll","year":"1997","unstructured":"Carroll Morgan and Annabelle McIver . 1997. A probabilistic temporal calculus based on expectations . In Formal Methods Pacific 1997 . Springer , 4--22. Carroll Morgan and Annabelle McIver. 1997. A probabilistic temporal calculus based on expectations. In Formal Methods Pacific 1997. Springer, 4--22."},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00596-1_11"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1276920.1276924"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-0208(08)73078-0"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(03)00201-9"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1305\/ndjfl\/1094155277"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-78499-9_6"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2009.11.008"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1093\/logcom\/12.1.149"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/23005.23008"},{"key":"e_1_2_1_44_1","volume-title":"Proceedings of the Foundations of Computer Science (FOCS\u201976)","author":"Pratt Vaughan","year":"1976","unstructured":"Vaughan Pratt . 1976 . Semantical considerations on floyd-hoare logic . In Proceedings of the Foundations of Computer Science (FOCS\u201976) . IEEE, 109--121. Vaughan Pratt. 1976. Semantical considerations on floyd-hoare logic. In Proceedings of the Foundations of Computer Science (FOCS\u201976). IEEE, 109--121."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2007.11.001"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.apal.2010.07.003"},{"key":"e_1_2_1_47_1","first-page":"1","article-title":"A finite model construction for coalgebraic modal logic","volume":"73","author":"Schr\u00f6der Lutz","year":"2007","unstructured":"Lutz Schr\u00f6der . 2007 . A finite model construction for coalgebraic modal logic . J. Log. Algebr. Prog. 73 , 1 -- 2 (2007), 97--110. Lutz Schr\u00f6der. 2007. A finite model construction for coalgebraic modal logic. J. Log. Algebr. Prog. 73, 1--2 (2007), 97--110.","journal-title":"J. Log. Algebr. Prog."},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1145\/1462179.1462185"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129510000563"},{"key":"e_1_2_1_50_1","volume-title":"Proceedings of the European Conference on Artificial Intelligence (ECAI\u201910)","volume":"215","author":"Schr\u00f6der Lutz","year":"2010","unstructured":"Lutz Schr\u00f6der , Dirk Pattinson , and Daniel Hausmann . 2010 . Optimal tableaux for conditional logics with cautious monotonicity . In Proceedings of the European Conference on Artificial Intelligence (ECAI\u201910) , Helder Coelho, Rudi Studer, and Michael Wooldridge (Eds.) , Vol. 215 . IOS Press, 707--712. Lutz Schr\u00f6der, Dirk Pattinson, and Daniel Hausmann. 2010. Optimal tableaux for conditional logics with cautious monotonicity. In Proceedings of the European Conference on Artificial Intelligence (ECAI\u201910), Helder Coelho, Rudi Studer, and Michael Wooldridge (Eds.), Vol. 215. IOS Press, 707--712."},{"key":"e_1_2_1_51_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_36"},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.4064\/-9-1-31-46"},{"key":"e_1_2_1_53_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2836"},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(83)80051-5"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3157055","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3157055","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:11:29Z","timestamp":1750212689000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3157055"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,1,6]]},"references-count":54,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2018,1,31]]}},"alternative-id":["10.1145\/3157055"],"URL":"https:\/\/doi.org\/10.1145\/3157055","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2018,1,6]]},"assertion":[{"value":"2016-06-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2017-10-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-01-06","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}