{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T04:09:19Z","timestamp":1750219759429,"version":"3.41.0"},"reference-count":67,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2023,11,18]],"date-time":"2023-11-18T00:00:00Z","timestamp":1700265600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"US National Science Foundation","doi-asserted-by":"crossref","award":["CNS-1446365"],"award-info":[{"award-number":["CNS-1446365"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/100000006","name":"US Office of Naval Research","doi-asserted-by":"crossref","award":["N00014-17-1-2622"],"award-info":[{"award-number":["N00014-17-1-2622"]}],"id":[{"id":"10.13039\/100000006","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Comput. Logic"],"published-print":{"date-parts":[[2024,1,31]]},"abstract":"<jats:p>This article revisits soundness and completeness of proof systems for proving that sets of states in infinite-state labeled transition systems satisfy formulas in the modal mu-calculus in order to develop proof techniques that permit the seamless inclusion of new features in this logic. Our approach relies on novel results in lattice theory, which give constructive characterizations of both greatest and least fixpoints of monotonic functions over complete lattices. We show how these results may be used to reason about the sound and complete tableau method for this problem due to Bradfield and Stirling. We also show how the flexibility of our lattice-theoretic basis simplifies reasoning about tableau-based proof strategies for alternative classes of systems. In particular, we extend the modal mu-calculus with timed modalities, and prove that the resulting tableau method is sound and complete for timed transition systems.<\/jats:p>","DOI":"10.1145\/3622786","type":"journal-article","created":{"date-parts":[[2023,9,13]],"date-time":"2023-09-13T12:19:09Z","timestamp":1694607549000},"page":"1-60","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Extensible Proof Systems for Infinite-State Systems"],"prefix":"10.1145","volume":"25","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-4952-5380","authenticated-orcid":false,"given":"Rance","family":"Cleaveland","sequence":"first","affiliation":[{"name":"Department of Computer Science, University of Maryland, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-5772-9527","authenticated-orcid":false,"given":"Jeroen J. A.","family":"Keiren","sequence":"additional","affiliation":[{"name":"Department of Mathematics and Computer Science, Eindhoven University of Technology, The Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2023,11,18]]},"reference":[{"key":"e_1_3_3_2_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(02)00334-1"},{"key":"e_1_3_3_3_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0054177"},{"key":"e_1_3_3_4_2","doi-asserted-by":"publisher","DOI":"10.1016\/S1567-8326(02)00022-X"},{"key":"e_1_3_3_5_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2017.8005088"},{"key":"e_1_3_3_6_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)90010-8"},{"key":"e_1_3_3_7_2","doi-asserted-by":"publisher","DOI":"10.7146\/dpb.v22i445.6762"},{"key":"e_1_3_3_8_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-07964-5"},{"key":"e_1_3_3_9_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1995.523273"},{"key":"e_1_3_3_10_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10849-010-9127-4"},{"key":"e_1_3_3_11_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0039055"},{"key":"e_1_3_3_12_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90183-G"},{"key":"e_1_3_3_13_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10575-8_26"},{"key":"e_1_3_3_14_2","volume-title":"Verifying Temporal Properties of Systems with Applications to Petri Nets","author":"Bradfield Julian C.","year":"1991","unstructured":"Julian C. Bradfield. 1991. Verifying Temporal Properties of Systems with Applications to Petri Nets. Ph.D. Dissertation. University of Edinburgh, Edinburgh. Retrieved from http:\/\/hdl.handle.net\/1842\/6565"},{"key":"e_1_3_3_15_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56496-9_25"},{"key":"e_1_3_3_16_2","doi-asserted-by":"publisher","DOI":"10.1093\/jigpal\/jzu030"},{"key":"e_1_3_3_17_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9781139173131"},{"key":"e_1_3_3_18_2","doi-asserted-by":"crossref","DOI":"10.1007\/978-3-319-10575-8","volume-title":"Model Checking (2nd. ed.)","author":"Jr Edmund M. Clarke","year":"2018","unstructured":"Edmund M. Clarke Jr, Orna Grumberg, Daniel Kroening, Doron Peled, and Helmut Veith. 2018. Model Checking (2nd. ed.). The MIT Press, Cambridge, Massachusetts. QA76.76.V47 C553 2018"},{"key":"e_1_3_3_19_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF00264284"},{"key":"e_1_3_3_20_2","doi-asserted-by":"publisher","DOI":"10.1145\/151646.151648"},{"key":"e_1_3_3_21_2","doi-asserted-by":"publisher","DOI":"10.1007\/BF01383878"},{"key":"e_1_3_3_22_2","volume-title":"Implementing Mathematics","author":"Constable Robert L.","year":"1986","unstructured":"Robert L. Constable, Stuart F. Allen, H. M. Bromley, W. Rance Cleaveland, J. F. Cremer, Robert W. Harper, Doug J. Howe, Todd B. Knoblock, Nax P. Mendler, Prakash Panangaden, James T. Sasaki, and Scott F. Smith. 1986. Implementing Mathematics. Prentice-Hall, NJ."},{"key":"e_1_3_3_23_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CSL.2015.78"},{"key":"e_1_3_3_24_2","doi-asserted-by":"publisher","DOI":"10.1109\/SFCS.1991.185392"},{"key":"e_1_3_3_25_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00034-7"},{"key":"e_1_3_3_26_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-10512-3_9"},{"key":"e_1_3_3_27_2","volume-title":"Towards a Unified Theory of Timed Automata","author":"Fontana Peter Christopher","year":"2014","unstructured":"Peter Christopher Fontana. 2014. Towards a Unified Theory of Timed Automata. Ph.D. Dissertation. University of Maryland, College Park. Retrieved from http:\/\/drum.lib.umd.edu\/handle\/1903\/15232"},{"key":"e_1_3_3_28_2","doi-asserted-by":"publisher","DOI":"10.1080\/11663081.2013.861181"},{"key":"e_1_3_3_29_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-36387-4"},{"key":"e_1_3_3_30_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-49253-4_8"},{"key":"e_1_3_3_31_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2005.06.016"},{"key":"e_1_3_3_32_2","volume-title":"Encyclopaedia of Mathematics, Supplement III","author":"Hazewinkel Michiel","year":"2001","unstructured":"Michiel Hazewinkel (Ed.). 2001. Encyclopaedia of Mathematics, Supplement III. Springer. 458 pages."},{"key":"e_1_3_3_33_2","doi-asserted-by":"publisher","DOI":"10.1145\/2455.2460"},{"key":"e_1_3_3_34_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1045"},{"key":"e_1_3_3_35_2","doi-asserted-by":"publisher","DOI":"10.1017\/CBO9780511792588.003"},{"key":"e_1_3_3_36_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2008.02.005"},{"key":"e_1_3_3_37_2","volume-title":"Set Theory","author":"Jech Thomas J.","year":"1978","unstructured":"Thomas J. Jech. 1978. Set Theory. Academic Press, New York."},{"key":"e_1_3_3_38_2","volume-title":"The Axiom of Choice","author":"Jech Thomas J.","year":"2008","unstructured":"Thomas J. Jech. 2008. The Axiom of Choice. Courier Corporation."},{"key":"e_1_3_3_39_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02716-1_17"},{"key":"e_1_3_3_40_2","unstructured":"Jeroen J. A. Keiren and Rance Cleaveland. 2022. Extensible proof systems for infinite-state systems. arXiv:2207.12953. Retrieved from https:\/\/arxiv.org\/abs\/2207.12953"},{"key":"e_1_3_3_41_2","volume-title":"Tableaux and Witnesses for the Mu\u2013 Calculus","author":"Kick Alexander","year":"1995","unstructured":"Alexander Kick. 1995. Tableaux and Witnesses for the Mu\u2013 Calculus. Technical Report. Fakult\u00e4t f\u00fcr Informatik, Universit\u00e4t Karlsruhe, Karlsruhe."},{"key":"e_1_3_3_42_2","volume-title":"Progress Measures and Finite Arguments for Infinite Computations","author":"Klarlund Nils","year":"1990","unstructured":"Nils Klarlund. 1990. Progress Measures and Finite Arguments for Infinite Computations. Ph.D. Dissertation. Cornell University. Retrieved from https:\/\/hdl.handle.net\/1813\/6993"},{"key":"e_1_3_3_43_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-55511-0_25"},{"key":"e_1_3_3_44_2","doi-asserted-by":"publisher","DOI":"10.1145\/135419.135462"},{"key":"e_1_3_3_45_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(82)90125-6"},{"key":"e_1_3_3_46_2","volume-title":"Set Theory: An Introduction to Independence Proofs","author":"Kunen Kenneth","year":"1980","unstructured":"Kenneth Kunen. 1980. Set Theory: An Introduction to Independence Proofs. Elsevier Science, Amsterdam, Lausanne, New York. Retrieved from http:\/\/opac.inria.fr\/record=b1117475"},{"key":"e_1_3_3_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60246-1_158"},{"key":"e_1_3_3_48_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0026106"},{"key":"e_1_3_3_49_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60249-6_41"},{"key":"e_1_3_3_50_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-56496-9_26"},{"key":"e_1_3_3_51_2","volume-title":"Verification of Modal Properties Using Boolean Equation Systems","author":"Mader Angelika H.","year":"1997","unstructured":"Angelika H. Mader. 1997. Verification of Modal Properties Using Boolean Equation Systems. Ph.D. Dissertation. Technische Universit\u00e4t M\u00fcnchen, M\u00fcnchen."},{"key":"e_1_3_3_52_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-86059-2_22"},{"key":"e_1_3_3_53_2","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-6423(02)00094-1"},{"key":"e_1_3_3_54_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58179-0_67"},{"key":"e_1_3_3_55_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-60045-0_52"},{"key":"e_1_3_3_56_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-1-4757-3550-5"},{"key":"e_1_3_3_57_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.129.2"},{"key":"e_1_3_3_58_2","doi-asserted-by":"publisher","DOI":"10.29007\/lwqm"},{"key":"e_1_3_3_59_2","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90110-4"},{"key":"e_1_3_3_60_2","doi-asserted-by":"publisher","DOI":"10.1016\/0890-5401(89)90031-X"},{"key":"e_1_3_3_61_2","doi-asserted-by":"publisher","DOI":"10.1007\/s11225-008-9133-6"},{"key":"e_1_3_3_62_2","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45657-0_37"},{"key":"e_1_3_3_63_2","doi-asserted-by":"publisher","DOI":"10.2140\/pjm.1955.5.285"},{"key":"e_1_3_3_64_2","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.1993.287593"},{"key":"e_1_3_3_65_2","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1999.2836"},{"key":"e_1_3_3_66_2","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0035797"},{"key":"e_1_3_3_67_2","doi-asserted-by":"publisher","DOI":"10.1007\/11562436_8"},{"key":"e_1_3_3_68_2","doi-asserted-by":"publisher","DOI":"10.1109\/RTSS.2005.22"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622786","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3622786","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3622786","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T16:37:04Z","timestamp":1750178224000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3622786"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2023,11,18]]},"references-count":67,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2024,1,31]]}},"alternative-id":["10.1145\/3622786"],"URL":"https:\/\/doi.org\/10.1145\/3622786","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"type":"print","value":"1529-3785"},{"type":"electronic","value":"1557-945X"}],"subject":[],"published":{"date-parts":[[2023,11,18]]},"assertion":[{"value":"2022-09-20","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-08-11","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2023-11-18","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}