{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T21:15:07Z","timestamp":1760044507978,"version":"3.40.3"},"publisher-location":"Cham","reference-count":38,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031664373"},{"type":"electronic","value":"9783031664380"}],"license":[{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2024,1,1]],"date-time":"2024-01-01T00:00:00Z","timestamp":1704067200000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"}],"content-domain":{"domain":["link.springer.com"],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2024]]},"DOI":"10.1007\/978-3-031-66438-0_1","type":"book-chapter","created":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:03:08Z","timestamp":1721890988000},"page":"1-22","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":1,"title":["Coalgebraic CTL: Fixpoint Characterization and\u00a0Polynomial-Time Model Checking"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0009-0005-5392-2054","authenticated-orcid":false,"given":"Ryota","family":"Kojima","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3165-5678","authenticated-orcid":false,"given":"Corina","family":"C\u00eerstea","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0454-6900","authenticated-orcid":false,"given":"Koko","family":"Muroya","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-8300-4650","authenticated-orcid":false,"given":"Ichiro","family":"Hasuo","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2024,7,26]]},"reference":[{"key":"1_CR1","volume-title":"Principles of Model Checking","author":"C Baier","year":"2008","unstructured":"Baier, C., Katoen, J.: Principles of Model Checking. MIT Press, Cambridge (2008)"},{"doi-asserted-by":"publisher","unstructured":"Bhat, G., Cleaveland, R.: Efficient model checking via the equational $$\\rm \\mu $$-calculus. In: Proceedings, 11th Annual IEEE Symposium on Logic in Computer Science, New Brunswick, New Jersey, USA, 27\u201330 July 1996, pp. 304\u2013312. IEEE Computer Society (1996). https:\/\/doi.org\/10.1109\/LICS.1996.561358","key":"1_CR2","DOI":"10.1109\/LICS.1996.561358"},{"doi-asserted-by":"publisher","unstructured":"Br\u00e1zdil, T., Forejt, V., Kret\u00ednsk\u00fd, J., Kucera, A.: The satisfiability problem for probabilistic CTL. In: Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24\u201327 June 2008, Pittsburgh, PA, USA, pp. 391\u2013402. IEEE Computer Society (2008). https:\/\/doi.org\/10.1109\/LICS.2008.21","key":"1_CR3","DOI":"10.1109\/LICS.2008.21"},{"issue":"4","key":"1_CR4","doi-asserted-by":"publisher","first-page":"371","DOI":"10.1145\/990010.990011","volume":"12","author":"M Chechik","year":"2003","unstructured":"Chechik, M., Devereux, B., Easterbrook, S.M., Gurfinkel, A.: Multi-valued symbolic model-checking. ACM Trans. Softw. Eng. Methodol. 12(4), 371\u2013408 (2003). https:\/\/doi.org\/10.1145\/990010.990011","journal-title":"ACM Trans. Softw. Eng. Methodol."},{"issue":"38","key":"1_CR5","doi-asserted-by":"publisher","first-page":"5025","DOI":"10.1016\/j.tcs.2011.04.025","volume":"412","author":"C C\u00eerstea","year":"2011","unstructured":"C\u00eerstea, C.: Maximal traces and path-based coalgebraic temporal logics. Theor. Comput. Sci. 412(38), 5025\u20135042 (2011). https:\/\/doi.org\/10.1016\/j.tcs.2011.04.025","journal-title":"Theor. Comput. Sci."},{"doi-asserted-by":"crossref","unstructured":"Cirstea, C.: Linear-time logics \u2013 a coalgebraic perspective (2023)","key":"1_CR6","DOI":"10.46298\/lmcs-20(2:13)2024"},{"key":"1_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"179","DOI":"10.1007\/978-3-642-04027-6_15","volume-title":"Computer Science Logic","author":"C C\u00eerstea","year":"2009","unstructured":"C\u00eerstea, C., Kupke, C., Pattinson, D.: EXPTIME tableaux for the coalgebraic $${\\mu }$$-calculus. In: Gr\u00e4del, E., Kahle, R. (eds.) CSL 2009. LNCS, vol. 5771, pp. 179\u2013193. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-04027-6_15"},{"unstructured":"Clarke, E.M., Grumberg, O., Kroening, D., Peled, D.A., Veith, H.: Model Checking, 2nd edn. MIT Press, Cambridge (2018). https:\/\/mitpress.mit.edu\/books\/model-checking-second-edition","key":"1_CR8"},{"issue":"1","key":"1_CR9","doi-asserted-by":"publisher","first-page":"43","DOI":"10.2140\/pjm.1979.82.43","volume":"82","author":"P Cousot","year":"1979","unstructured":"Cousot, P., Cousot, R.: Constructive versions of Tarski\u2019s fixed point theorems. Pac. J. Math. 82(1), 43\u201357 (1979)","journal-title":"Pac. J. Math."},{"issue":"1","key":"1_CR10","doi-asserted-by":"publisher","first-page":"77","DOI":"10.1016\/0304-3975(94)90269-0","volume":"126","author":"M Dam","year":"1994","unstructured":"Dam, M.: CTL* and ECTL* as fragments of the modal mu-calculus. Theor. Comput. Sci. 126(1), 77\u201396 (1994). https:\/\/doi.org\/10.1016\/0304-3975(94)90269-0","journal-title":"Theor. Comput. Sci."},{"key":"1_CR11","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4612-0877-8","volume-title":"Measure Theory","author":"JL Doob","year":"1994","unstructured":"Doob, J.L.: Measure Theory. Springer, New York (1994). https:\/\/doi.org\/10.1007\/978-1-4612-0877-8"},{"issue":"3","key":"1_CR12","doi-asserted-by":"publisher","first-page":"241","DOI":"10.1016\/0167-6423(83)90017-5","volume":"2","author":"EA Emerson","year":"1982","unstructured":"Emerson, E.A., Clarke, E.M.: Using branching time temporal logic to synthesize synchronization skeletons. Sci. Comput. Program. 2(3), 241\u2013266 (1982). https:\/\/doi.org\/10.1016\/0167-6423(83)90017-5","journal-title":"Sci. Comput. Program."},{"issue":"1","key":"1_CR13","doi-asserted-by":"publisher","first-page":"1","DOI":"10.1016\/0022-0000(85)90001-7","volume":"30","author":"EA Emerson","year":"1985","unstructured":"Emerson, E.A., Halpern, J.Y.: Decision procedures and expressiveness in the temporal logic of branching time. J. Comput. Syst. Sci. 30(1), 1\u201324 (1985). https:\/\/doi.org\/10.1016\/0022-0000(85)90001-7","journal-title":"J. Comput. Syst. Sci."},{"issue":"1","key":"1_CR14","doi-asserted-by":"publisher","first-page":"151","DOI":"10.1145\/4904.4999","volume":"33","author":"EA Emerson","year":"1986","unstructured":"Emerson, E.A., Halpern, J.Y.: \u201csometimes\u2019\u2019 and \u201cnot never\u2019\u2019 revisited: on branching versus linear time temporal logic. J. ACM 33(1), 151\u2013178 (1986). https:\/\/doi.org\/10.1145\/4904.4999","journal-title":"J. ACM"},{"key":"1_CR15","series-title":"Lecture Notes in Mathematics","doi-asserted-by":"publisher","first-page":"68","DOI":"10.1007\/BFb0092872","volume-title":"Categorical Aspects of Topology and Analysis","author":"M Giry","year":"1982","unstructured":"Giry, M.: A categorical approach to probability theory. In: Banaschewski, B. (ed.) Categorical Aspects of Topology and Analysis. LNM, vol. 915, pp. 68\u201385. Springer, Heidelberg (1982). https:\/\/doi.org\/10.1007\/BFb0092872"},{"doi-asserted-by":"publisher","unstructured":"Hansen, H.H., Kupke, C.: A coalgebraic perspective on monotone modal logic. In: Ad\u00e1mek, J., Milius, S. (eds.) Proceedings of the Workshop on Coalgebraic Methods in Computer Science, CMCS 2004, Barcelona, Spain, 27\u201329 March 2004. Electronic Notes in Theoretical Computer Science, vol.\u00a0106, pp. 121\u2013143. Elsevier (2004). https:\/\/doi.org\/10.1016\/j.entcs.2004.02.028","key":"1_CR16","DOI":"10.1016\/j.entcs.2004.02.028"},{"unstructured":"Hansen, H.H., Kupke, C., Marti, J., Venema, Y.: Parity games and automata for game logic (extended version). CoRR abs\/1709.00777 (2017). http:\/\/arxiv.org\/abs\/1709.00777","key":"1_CR17"},{"issue":"5","key":"1_CR18","doi-asserted-by":"publisher","first-page":"512","DOI":"10.1007\/BF01211866","volume":"6","author":"H Hansson","year":"1994","unstructured":"Hansson, H., Jonsson, B.: A logic for reasoning about time and reliability. Formal Aspects Comput. 6(5), 512\u2013535 (1994). https:\/\/doi.org\/10.1007\/BF01211866","journal-title":"Formal Aspects Comput."},{"doi-asserted-by":"publisher","unstructured":"Hasuo, I., Shimizu, S., C\u00eerstea, C.: Lattice-theoretic progress measures and coalgebraic model checking. In: Bod\u00edk, R., Majumdar, R. (eds.) Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, 20\u201322 January 2016, pp. 718\u2013732. ACM (2016). https:\/\/doi.org\/10.1145\/2837614.2837673","key":"1_CR19","DOI":"10.1145\/2837614.2837673"},{"doi-asserted-by":"publisher","unstructured":"Hausmann, D., Schr\u00f6der, L.: Game-based local model checking for the coalgebraic mu-calculus. In: Fokkink, W.J., van Glabbeek, R. (eds.) 30th International Conference on Concurrency Theory, CONCUR 2019, 27\u201330 August 2019, Amsterdam, the Netherlands. LIPIcs, vol.\u00a0140, pp. 35:1\u201335:16. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2019.35","key":"1_CR20","DOI":"10.4230\/LIPIcs.CONCUR.2019.35"},{"issue":"1","key":"1_CR21","doi-asserted-by":"publisher","first-page":"73","DOI":"10.1016\/0168-0072(94)90020-5","volume":"69","author":"B Jacobs","year":"1994","unstructured":"Jacobs, B.: Semantics of weakening and contraction. Ann. Pure Appl. Log. 69(1), 73\u2013106 (1994). https:\/\/doi.org\/10.1016\/0168-0072(94)90020-5","journal-title":"Ann. Pure Appl. Log."},{"doi-asserted-by":"publisher","unstructured":"Jacobs, B.: Trace semantics for coalgebras. In: Ad\u00e1mek, J., Milius, S. (eds.) Proceedings of the Workshop on Coalgebraic Methods in Computer Science, CMCS 2004, Barcelona, Spain, 27\u201329 March 2004. Electronic Notes in Theoretical Computer Science, vol.\u00a0106, pp. 167\u2013184. Elsevier (2004). https:\/\/doi.org\/10.1016\/j.entcs.2004.02.031","key":"1_CR22","DOI":"10.1016\/j.entcs.2004.02.031"},{"key":"1_CR23","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"53","DOI":"10.1007\/978-3-319-40370-0_5","volume-title":"Coalgebraic Methods in Computer Science","author":"B Jacobs","year":"2016","unstructured":"Jacobs, B.: Affine monads and side-effect-freeness. In: Hasuo, I. (ed.) CMCS 2016. LNCS, vol. 9608, pp. 53\u201372. Springer, Cham (2016). https:\/\/doi.org\/10.1007\/978-3-319-40370-0_5"},{"doi-asserted-by":"publisher","unstructured":"Jacobs, B.: Introduction to Coalgebra: Towards Mathematics of States and Observation. Cambridge Tracts in Theoretical Computer Science. Cambridge University Press, Cambridge (2016). https:\/\/doi.org\/10.1017\/CBO9781316823187","key":"1_CR24","DOI":"10.1017\/CBO9781316823187"},{"key":"1_CR25","doi-asserted-by":"publisher","first-page":"161","DOI":"10.7146\/math.scand.a-11042","volume":"29","author":"A Kock","year":"1971","unstructured":"Kock, A.: Bilinearity and cartesian closed monads. Math. Scand. 29, 161\u2013174 (1971)","journal-title":"Math. Scand."},{"key":"1_CR26","doi-asserted-by":"publisher","first-page":"333","DOI":"10.1016\/0304-3975(82)90125-6","volume":"27","author":"D Kozen","year":"1983","unstructured":"Kozen, D.: Results on the propositional mu-calculus. Theor. Comput. Sci. 27, 333\u2013354 (1983). https:\/\/doi.org\/10.1016\/0304-3975(82)90125-6","journal-title":"Theor. Comput. Sci."},{"doi-asserted-by":"crossref","unstructured":"MacLane, S.: Categories for the Working Mathematician. Graduate Texts in Mathematics, vol. 5. Springer, New York (1971)","key":"1_CR27","DOI":"10.1007\/978-1-4612-9839-7"},{"unstructured":"Milner, R.: Communication and Concurrency. PHI Series in Computer Science. Prentice Hall, Hoboken (1989)","key":"1_CR28"},{"issue":"1\u20133","key":"1_CR29","doi-asserted-by":"publisher","first-page":"277","DOI":"10.1016\/S0168-0072(98)00042-6","volume":"96","author":"LS Moss","year":"1999","unstructured":"Moss, L.S.: Coalgebraic logic. Ann. Pure Appl. Log. 96(1\u20133), 277\u2013317 (1999). https:\/\/doi.org\/10.1016\/S0168-0072(98)00042-6","journal-title":"Ann. Pure Appl. Log."},{"key":"1_CR30","doi-asserted-by":"publisher","first-page":"45","DOI":"10.1016\/J.TCS.2015.10.014","volume":"612","author":"H Pan","year":"2016","unstructured":"Pan, H., Li, Y., Cao, Y., Ma, Z.: Model checking computation tree logic over finite lattices. Theor. Comput. Sci. 612, 45\u201362 (2016). https:\/\/doi.org\/10.1016\/J.TCS.2015.10.014","journal-title":"Theor. Comput. Sci."},{"doi-asserted-by":"crossref","unstructured":"Parikh, R.: The logic of games and its applications. In: Selected Papers of the International Conference on \u201cFoundations of Computation Theory\u201d on Topics in the Theory of Computation, pp. 111\u2013139. Elsevier North-Holland, Inc., USA (1985)","key":"1_CR31","DOI":"10.1016\/S0304-0208(08)73078-0"},{"issue":"1\u20133","key":"1_CR32","doi-asserted-by":"publisher","first-page":"177","DOI":"10.1016\/S0304-3975(03)00201-9","volume":"309","author":"D Pattinson","year":"2003","unstructured":"Pattinson, D.: Coalgebraic modal logic: soundness, completeness and decidability of local consequence. Theor. Comput. Sci. 309(1\u20133), 177\u2013193 (2003). https:\/\/doi.org\/10.1016\/S0304-3975(03)00201-9","journal-title":"Theor. Comput. Sci."},{"doi-asserted-by":"publisher","unstructured":"Schr\u00f6der, L., Pattinson, D.: PSPACE bounds for rank-1 modal logics. ACM Trans. Comput. Log. 10(2), 13:1\u201313:33 (2009). https:\/\/doi.org\/10.1145\/1462179.1462185","key":"1_CR33","DOI":"10.1145\/1462179.1462185"},{"key":"1_CR34","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"325","DOI":"10.1007\/978-3-642-02017-9_35","volume-title":"Theory and Applications of Models of Computation","author":"C Schubert","year":"2009","unstructured":"Schubert, C.: Terminal coalgebras for measure-polynomial functors. In: Chen, J., Cooper, S.B. (eds.) TAMC 2009. LNCS, vol. 5532, pp. 325\u2013334. Springer, Heidelberg (2009). https:\/\/doi.org\/10.1007\/978-3-642-02017-9_35"},{"doi-asserted-by":"crossref","unstructured":"Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pac. J. Math. 5, 285\u2013309 (1955). https:\/\/api.semanticscholar.org\/CorpusID:13651629","key":"1_CR35","DOI":"10.2140\/pjm.1955.5.285"},{"key":"1_CR36","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"214","DOI":"10.1007\/978-3-030-00389-0_12","volume-title":"Coalgebraic Methods in Computer Science","author":"N Urabe","year":"2018","unstructured":"Urabe, N., Hasuo, I.: Categorical B\u00fcchi and parity conditions via alternating fixed points of functors. In: C\u00eerstea, C. (ed.) CMCS 2018. LNCS, vol. 11202, pp. 214\u2013234. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-030-00389-0_12"},{"doi-asserted-by":"publisher","unstructured":"Urabe, N., Hasuo, I.: Coalgebraic infinite traces and kleisli simulations. Log. Methods Comput. Sci. 14(3) (2018). https:\/\/doi.org\/10.23638\/LMCS-14(3:15)2018","key":"1_CR37","DOI":"10.23638\/LMCS-14(3:15)2018"},{"issue":"4","key":"1_CR38","doi-asserted-by":"publisher","first-page":"637","DOI":"10.1016\/J.IC.2005.06.003","volume":"204","author":"Y Venema","year":"2006","unstructured":"Venema, Y.: Automata and fixed point logic: a coalgebraic perspective. Inf. Comput. 204(4), 637\u2013678 (2006). https:\/\/doi.org\/10.1016\/J.IC.2005.06.003","journal-title":"Inf. Comput."}],"container-title":["Lecture Notes in Computer Science","Coalgebraic Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-66438-0_1","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,7,25]],"date-time":"2024-07-25T07:08:49Z","timestamp":1721891329000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-66438-0_1"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2024]]},"ISBN":["9783031664373","9783031664380"],"references-count":38,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-66438-0_1","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2024]]},"assertion":[{"value":"26 July 2024","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"CMCS","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Workshop on Coalgebraic Methods in Computer Science","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg City","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Luxembourg","order":4,"name":"conference_country","label":"Conference Country","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"2024","order":5,"name":"conference_year","label":"Conference Year","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"6 April 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"7 April 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"17","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"cmcs2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/www.coalg.org\/cmcs24\/","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}}]}}