{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,11,1]],"date-time":"2025-11-01T02:51:10Z","timestamp":1761965470222,"version":"3.40.3"},"publisher-location":"Cham","reference-count":39,"publisher":"Springer Nature Switzerland","isbn-type":[{"type":"print","value":"9783031505232"},{"type":"electronic","value":"9783031505249"}],"license":[{"start":{"date-parts":[[2023,12,30]],"date-time":"2023-12-30T00:00:00Z","timestamp":1703894400000},"content-version":"tdm","delay-in-days":0,"URL":"https:\/\/www.springernature.com\/gp\/researchers\/text-and-data-mining"},{"start":{"date-parts":[[2023,12,30]],"date-time":"2023-12-30T00:00:00Z","timestamp":1703894400000},"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-50524-9_8","type":"book-chapter","created":{"date-parts":[[2023,12,29]],"date-time":"2023-12-29T15:02:28Z","timestamp":1703862148000},"page":"171-185","update-policy":"https:\/\/doi.org\/10.1007\/springer_crossmark_policy","source":"Crossref","is-referenced-by-count":3,"title":["Generic Model Checking for\u00a0Modal Fixpoint Logics in\u00a0COOL-MC"],"prefix":"10.1007","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-0935-8602","authenticated-orcid":false,"given":"Daniel","family":"Hausmann","sequence":"first","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-2251-8519","authenticated-orcid":false,"given":"Merlin","family":"Humml","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0009-0000-2317-5565","authenticated-orcid":false,"given":"Simon","family":"Prucker","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3146-5906","authenticated-orcid":false,"given":"Lutz","family":"Schr\u00f6der","sequence":"additional","affiliation":[]},{"given":"Aaron","family":"Strahlberger","sequence":"additional","affiliation":[]}],"member":"297","published-online":{"date-parts":[[2023,12,30]]},"reference":[{"key":"8_CR1","doi-asserted-by":"publisher","unstructured":"Alur, R., et al.: JMOCHA: a model checking tool that exploits design structure. In: International Conference on Software Engineering, ICSE 2001, pp. 835\u2013836. IEEE Computer Society (2001). https:\/\/doi.org\/10.1109\/ICSE.2001.919196","DOI":"10.1109\/ICSE.2001.919196"},{"key":"8_CR2","doi-asserted-by":"publisher","first-page":"672","DOI":"10.1145\/585265.585270","volume":"49","author":"R Alur","year":"2002","unstructured":"Alur, R., Henzinger, T.A., Kupferman, O.: Alternating-time temporal logic. J. ACM 49, 672\u2013713 (2002). https:\/\/doi.org\/10.1145\/585265.585270","journal-title":"J. ACM"},{"key":"8_CR3","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-23008-0","author":"M Atif","year":"2023","unstructured":"Atif, M., Groote, J.F.: Understanding behaviour of distributed systems using mCRL2. Springer (2023). https:\/\/doi.org\/10.1007\/978-3-031-23008-0","journal-title":"Springer"},{"key":"8_CR4","doi-asserted-by":"publisher","unstructured":"Chakraborty, S., Katoen, J.: On the satisfiability of some simple probabilistic logics. In: Logic in Computer Science, LICS 2016, pp. 56\u201365. ACM (2016). https:\/\/doi.org\/10.1145\/2933575.2934526","DOI":"10.1145\/2933575.2934526"},{"key":"8_CR5","doi-asserted-by":"publisher","unstructured":"C\u00eerstea, C., Kupke, C., Pattinson, D.: EXPTIME tableaux for the coalgebraic mu-calculus. Log. Methods Comput. Sci. 7(3) (2011). https:\/\/doi.org\/10.2168\/LMCS-7(3:3)2011","DOI":"10.2168\/LMCS-7(3:3)2011"},{"key":"8_CR6","doi-asserted-by":"publisher","first-page":"267","DOI":"10.1007\/S001530100110","volume":"41","author":"G D\u2019Agostino","year":"2002","unstructured":"D\u2019Agostino, G., Visser, A.: Finality regained: a coalgebraic study of Scott-sets and multisets. Arch. Math. Logic 41, 267\u2013298 (2002). https:\/\/doi.org\/10.1007\/S001530100110","journal-title":"Arch. Math. Logic"},{"key":"8_CR7","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"291","DOI":"10.1007\/978-3-319-89960-2_16","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"T Dijk","year":"2018","unstructured":"Dijk, T.: Oink: an implementation and evaluation of modern parity game solvers. In: Beyer, D., Huisman, M. (eds.) TACAS 2018. LNCS, vol. 10805, pp. 291\u2013308. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-89960-2_16"},{"key":"8_CR8","doi-asserted-by":"publisher","unstructured":"Enqvist, S., Hansen, H.H., Kupke, C., Marti, J., Venema, Y.: Completeness for game logic. In: Logic in Computer Science, LICS 2019, pp. 1\u201313. IEEE (2019). https:\/\/doi.org\/10.1109\/LICS.2019.8785676","DOI":"10.1109\/LICS.2019.8785676"},{"key":"8_CR9","unstructured":"fauprojects: COOL - The Coalgebraic Ontology Logic Reasoner (git repository). https:\/\/git8.cs.fau.de\/software\/cool\/-\/tree\/VMCAI-2024"},{"key":"8_CR10","doi-asserted-by":"publisher","unstructured":"Ferrante, A., Murano, A., Parente, M.: Enriched $${\\mu }$$-calculi module checking. Log. Methods Comput. Sci. 4(3) (2008). https:\/\/doi.org\/10.2168\/LMCS-4(3:1)2008","DOI":"10.2168\/LMCS-4(3:1)2008"},{"key":"8_CR11","unstructured":"Friedmann, O., Lange, M.: The PGSolver collection of parity game solvers. Technical report, University of Munich (2009)"},{"key":"8_CR12","doi-asserted-by":"publisher","unstructured":"Friedmann, O., Lange, M.: Local strategy improvement for parity game solving. In: Proceedings First Symposium on Games, Automata, Logic, and Formal Verification, GANDALF 2010. EPTCS, vol. 25, pp. 118\u2013131 (2010). https:\/\/doi.org\/10.4204\/EPTCS.25.13","DOI":"10.4204\/EPTCS.25.13"},{"key":"8_CR13","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"396","DOI":"10.1007\/978-3-319-08587-6_31","volume-title":"Automated Reasoning","author":"D Gor\u00edn","year":"2014","unstructured":"Gor\u00edn, D., Pattinson, D., Schr\u00f6der, L., Widmann, F., Wi\u00dfmann, T.: Cool \u2013 a generic reasoner for coalgebraic hybrid logics (system description). In: Demri, S., Kapur, D., Weidenbach, C. (eds.) IJCAR 2014. LNCS (LNAI), vol. 8562, pp. 396\u2013402. Springer, Cham (2014). https:\/\/doi.org\/10.1007\/978-3-319-08587-6_31"},{"key":"8_CR14","series-title":"LNCS","doi-asserted-by":"publisher","first-page":"234","DOI":"10.1007\/978-3-031-38499-8_14","volume-title":"Automated Deduction, CADE 2023","author":"O G\u00f6rlitz","year":"2023","unstructured":"G\u00f6rlitz, O., Hausmann, D., Humml, M., Pattinson, D., Prucker, S., Schr\u00f6der, L.: COOL 2 - a generic reasoner for modal fixpoint logics (system description). In: Pientka, B., Tinelli, C. (eds.) CADE 2023. LNCS, vol. 14132, pp. 234\u2013247. Springer, Cham (2023). https:\/\/doi.org\/10.1007\/978-3-031-38499-8_14"},{"key":"8_CR15","doi-asserted-by":"publisher","unstructured":"Hansen, H.H., Kupke, C.: A coalgebraic perspective on monotone modal logic. In: Coalgebraic Methods in Computer Science, CMCS 2004. ENTCS, vol. 106, pp. 121\u2013143. Elsevier (2004). https:\/\/doi.org\/10.1016\/j.entcs.2004.02.028","DOI":"10.1016\/j.entcs.2004.02.028"},{"key":"8_CR16","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"115","DOI":"10.1007\/978-3-319-73579-5_8","volume-title":"Dynamic Logic. New Trends and Applications","author":"HH Hansen","year":"2018","unstructured":"Hansen, H.H., Kupke, C., Marti, J., Venema, Y.: Parity games and automata for game logic. In: Madeira, A., Benevides, M. (eds.) DALI 2017. LNCS, vol. 10669, pp. 115\u2013132. Springer, Cham (2018). https:\/\/doi.org\/10.1007\/978-3-319-73579-5_8"},{"issue":"5","key":"8_CR17","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."},{"key":"8_CR18","doi-asserted-by":"publisher","unstructured":"Hasuo, I., Shimizu, S., C\u00eerstea, C.: Lattice-theoretic progress measures and coalgebraic model checking. In: Principles of Programming Languages, POPL 2016, pp. 718\u2013732. ACM (2016). https:\/\/doi.org\/10.1145\/2837614.2837673","DOI":"10.1145\/2837614.2837673"},{"key":"8_CR19","doi-asserted-by":"publisher","DOI":"10.5281\/zenodo.8332511","author":"D Hausmann","year":"2023","unstructured":"Hausmann, D., Humml, M., Prucker, S., Schr\u00f6der, L., Strahlberger, A.: Generic model checking for modal fixpoint logics in COOL-MC (artifact). Zenodo (2023). https:\/\/doi.org\/10.5281\/zenodo.8332511","journal-title":"Zenodo"},{"key":"8_CR20","doi-asserted-by":"publisher","unstructured":"Hausmann, D., Humml, M., Prucker, S., Schr\u00f6der, L., Strahlberger, A.: Generic model checking for modal fixpoint logics in COOL-MC (extended version). CoRR abs\/2311.01315 (2023). https:\/\/doi.org\/10.48550\/arXiv.2311.01315","DOI":"10.48550\/arXiv.2311.01315"},{"key":"8_CR21","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"38","DOI":"10.1007\/978-3-030-72016-2_3","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"D Hausmann","year":"2021","unstructured":"Hausmann, D., Schr\u00f6der, L.: Quasipolynomial computation of nested fixpoints. In: TACAS 2021. LNCS, vol. 12651, pp. 38\u201356. Springer, Cham (2021). https:\/\/doi.org\/10.1007\/978-3-030-72016-2_3"},{"key":"8_CR22","doi-asserted-by":"publisher","unstructured":"Hausmann, D., Schr\u00f6der, L.: Coalgebraic satisfiability checking for arithmetic $$\\mu $$-calculi. CoRR abs\/2212.11055 (2022). https:\/\/doi.org\/10.48550\/arXiv.2212.11055","DOI":"10.48550\/arXiv.2212.11055"},{"key":"8_CR23","doi-asserted-by":"publisher","unstructured":"Hausmann, D., Schr\u00f6der, L.: Game-based local model checking for the coalgebraic mu-calculus. In: 30th International Conference on Concurrency Theory, CONCUR 2019. LIPIcs, vol. 140, pp. 35:1\u201335:16. Schloss Dagstuhl - Leibniz-Zentrum f\u00fcr Informatik (2019). https:\/\/doi.org\/10.4230\/LIPIcs.CONCUR.2019.35","DOI":"10.4230\/LIPIcs.CONCUR.2019.35"},{"key":"8_CR24","doi-asserted-by":"publisher","unstructured":"Ka\u0144ski, M., Niewiadomski, A., Kacprzak, M., Penczek, W., Nabia\u0142ek, W.: Unbounded model checking for ATL. Studia Informatica 25(1\u20132) (2021). https:\/\/doi.org\/10.34739\/si.2021.25.01","DOI":"10.34739\/si.2021.25.01"},{"key":"8_CR25","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."},{"key":"8_CR26","series-title":"Lecture Notes in Computer Science (Lecture Notes in Artificial Intelligence)","doi-asserted-by":"publisher","first-page":"423","DOI":"10.1007\/3-540-45620-1_34","volume-title":"Automated Deduction\u2014CADE-18","author":"O Kupferman","year":"2002","unstructured":"Kupferman, O., Sattler, U., Vardi, M.Y.: The complexity of the graded $${\\mu }$$-calculus. In: Voronkov, A. (ed.) CADE 2002. LNCS (LNAI), vol. 2392, pp. 423\u2013437. Springer, Heidelberg (2002). https:\/\/doi.org\/10.1007\/3-540-45620-1_34"},{"key":"8_CR27","doi-asserted-by":"publisher","unstructured":"Kupke, C., Marti, J., Venema, Y.: Size measures and alphabetic equivalence in the $$\\mu $$-calculus. In: Logic in Computer Science, LICS 2022, pp. 18:1\u201318:13. ACM (2022). https:\/\/doi.org\/10.1145\/3531130.3533339","DOI":"10.1145\/3531130.3533339"},{"key":"8_CR28","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"585","DOI":"10.1007\/978-3-642-22110-1_47","volume-title":"Computer Aided Verification","author":"M Kwiatkowska","year":"2011","unstructured":"Kwiatkowska, M., Norman, G., Parker, D.: PRISM 4.0: verification of probabilistic real-time systems. In: Gopalakrishnan, G., Qadeer, S. (eds.) CAV 2011. LNCS, vol. 6806, pp. 585\u2013591. Springer, Heidelberg (2011). https:\/\/doi.org\/10.1007\/978-3-642-22110-1_47"},{"key":"8_CR29","unstructured":"Landsaat, E.: A model checker for game logic via parity games. BSc thesis, University of Groningen (2022). https:\/\/fse.studenttheses.ub.rug.nl\/28126\/"},{"key":"8_CR30","unstructured":"Liu, W., Song, L., Wang, J., Zhang, L.: A simple probabilistic extension of modal mu-calculus. In: International Joint Conference on Artificial Intelligence, IJCAI 2015, pp. 882\u2013888. AAAI Press (2015). http:\/\/ijcai.org\/proceedings\/2015"},{"issue":"1","key":"8_CR31","doi-asserted-by":"publisher","first-page":"9","DOI":"10.1007\/s10009-015-0378-x","volume":"19","author":"A Lomuscio","year":"2017","unstructured":"Lomuscio, A., Qu, H., Raimondi, F.: MCMAS: an open-source model checker for the verification of multi-agent systems. Int. J. Softw. Tools Technol. Transf. 19(1), 9\u201330 (2017). https:\/\/doi.org\/10.1007\/s10009-015-0378-x","journal-title":"Int. J. Softw. Tools Technol. Transf."},{"key":"8_CR32","doi-asserted-by":"publisher","first-page":"111","DOI":"10.1016\/S0304-0208(08)73078-0","volume":"24","author":"R Parikh","year":"1985","unstructured":"Parikh, R.: The logic of games and its applications. Ann. Discr. Math. 24, 111\u2013140 (1985). https:\/\/doi.org\/10.1016\/S0304-0208(08)73078-0","journal-title":"Ann. Discr. Math."},{"issue":"1","key":"8_CR33","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1305\/ndjfl\/1094155277","volume":"45","author":"D Pattinson","year":"2004","unstructured":"Pattinson, D.: Expressive logics for coalgebras via terminal sequence induction. Notre Dame J. Formal Log. 45(1), 19\u201333 (2004). https:\/\/doi.org\/10.1305\/ndjfl\/1094155277","journal-title":"Notre Dame J. Formal Log."},{"key":"8_CR34","unstructured":"Pauly, M.: Logic for Social Software. Ph.D. thesis, Universiteit van Amsterdam (2001)"},{"issue":"1","key":"8_CR35","doi-asserted-by":"publisher","first-page":"3","DOI":"10.1016\/S0304-3975(00)00056-6","volume":"249","author":"JJMM Rutten","year":"2000","unstructured":"Rutten, J.J.M.M.: Universal coalgebra: a theory of systems. Theor. Comput. Sci. 249(1), 3\u201380 (2000). https:\/\/doi.org\/10.1016\/S0304-3975(00)00056-6","journal-title":"Theor. Comput. Sci."},{"issue":"2\u20133","key":"8_CR36","doi-asserted-by":"publisher","first-page":"230","DOI":"10.1016\/j.tcs.2007.09.023","volume":"390","author":"L Schr\u00f6der","year":"2008","unstructured":"Schr\u00f6der, L.: Expressivity of coalgebraic modal logic: the limits and beyond. Theor. Comput. Sci. 390(2\u20133), 230\u2013247 (2008). https:\/\/doi.org\/10.1016\/j.tcs.2007.09.023","journal-title":"Theor. Comput. Sci."},{"key":"8_CR37","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"85","DOI":"10.1007\/BFb0054166","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"P Stevens","year":"1998","unstructured":"Stevens, P., Stirling, C.: Practical model-checking using games. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 85\u2013101. Springer, Heidelberg (1998). https:\/\/doi.org\/10.1007\/BFb0054166"},{"key":"8_CR38","unstructured":"tcsprojects: PGSolver (git repository). https:\/\/github.com\/tcsprojects\/pgsolver"},{"issue":"4","key":"8_CR39","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","Verification, Model Checking, and Abstract Interpretation"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-031-50524-9_8","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,1,3]],"date-time":"2024-01-03T00:11:31Z","timestamp":1704240691000},"score":1,"resource":{"primary":{"URL":"https:\/\/link.springer.com\/10.1007\/978-3-031-50524-9_8"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,12,30]]},"ISBN":["9783031505232","9783031505249"],"references-count":39,"URL":"https:\/\/doi.org\/10.1007\/978-3-031-50524-9_8","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2023,12,30]]},"assertion":[{"value":"30 December 2023","order":1,"name":"first_online","label":"First Online","group":{"name":"ChapterHistory","label":"Chapter History"}},{"value":"VMCAI","order":1,"name":"conference_acronym","label":"Conference Acronym","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"International Conference on Verification, Model Checking, and Abstract Interpretation","order":2,"name":"conference_name","label":"Conference Name","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"London","order":3,"name":"conference_city","label":"Conference City","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"United Kingdom","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":"15 January 2024","order":7,"name":"conference_start_date","label":"Conference Start Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"16 January 2024","order":8,"name":"conference_end_date","label":"Conference End Date","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"25","order":9,"name":"conference_number","label":"Conference Number","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"vmcai2024","order":10,"name":"conference_id","label":"Conference ID","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"https:\/\/popl24.sigplan.org\/home\/VMCAI-2024","order":11,"name":"conference_url","label":"Conference URL","group":{"name":"ConferenceInfo","label":"Conference Information"}},{"value":"Single-blind","order":1,"name":"type","label":"Type","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"EasyChair","order":2,"name":"conference_management_system","label":"Conference Management System","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"74","order":3,"name":"number_of_submissions_sent_for_review","label":"Number of Submissions Sent for Review","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"30","order":4,"name":"number_of_full_papers_accepted","label":"Number of Full Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"0","order":5,"name":"number_of_short_papers_accepted","label":"Number of Short Papers Accepted","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"41% - The value is computed by the equation \"Number of Full Papers Accepted \/ Number of Submissions Sent for Review * 100\" and then rounded to a whole number.","order":6,"name":"acceptance_rate_of_full_papers","label":"Acceptance Rate of Full Papers","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"3","order":7,"name":"average_number_of_reviews_per_paper","label":"Average Number of Reviews per Paper","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"6","order":8,"name":"average_number_of_papers_per_reviewer","label":"Average Number of Papers per Reviewer","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}},{"value":"Yes","order":9,"name":"external_reviewers_involved","label":"External Reviewers Involved","group":{"name":"ConfEventPeerReviewInformation","label":"Peer Review Information (provided by the conference organizers)"}}]}}