{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,11]],"date-time":"2026-01-11T19:38:22Z","timestamp":1768160302839,"version":"3.49.0"},"reference-count":47,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2020,10,26]],"date-time":"2020-10-26T00:00:00Z","timestamp":1603670400000},"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":[[2020,10,31]]},"abstract":"<jats:p>We study the model-checking problem for a logic for true concurrency, whose formulae predicate about events in computations and their causal dependencies. The logic, which represents the logical counterpart of history-preserving bisimilarity, is naturally interpreted over event structures or any formalism that can be given a causal semantics, like Petri nets. It includes least and greatest fixpoint operators and thus it can express properties of infinite computations. Since the event structure associated with a system is typically infinite (even if the system is finite state), already the decidability of model-checking is non-trivial. We first develop a local model-checking technique based on a tableau system, for which, over a class of event structures satisfying a suitable regularity condition, referred to as strong regularity, we prove termination, soundness, and completeness. The tableau system allows for a clean and intuitive proof of decidability, but a direct implementation of the procedure can be extremely inefficient. For easing the development of a more efficient model-checking technique, we move to an automata-theoretic framework. Given a formula and a strongly regular event structure, we show how to construct a parity tree automaton whose language is non-empty if and only if the event structure satisfies the formula. The automaton is usually infinite. We discuss how it can be quotiented to an equivalent finite automaton, where emptiness can be checked effectively. To show the applicability of the approach, we discuss how it instantiates to finite safe Petri nets, providing also a corresponding proof-of-concept model-checking tool.<\/jats:p>","DOI":"10.1145\/3412853","type":"journal-article","created":{"date-parts":[[2020,10,26]],"date-time":"2020-10-26T18:04:21Z","timestamp":1603735461000},"page":"1-49","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":2,"title":["Model Checking a Logic for True Concurrency"],"prefix":"10.1145","volume":"21","author":[{"ORCID":"https:\/\/orcid.org\/0000-0001-9357-5599","authenticated-orcid":false,"given":"Paolo","family":"Baldan","sequence":"first","affiliation":[{"name":"Universit\u00e0 di Padova, Padova, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Tommaso","family":"Padoan","sequence":"additional","affiliation":[{"name":"Universit\u00e0 di Padova, Padova, Italy"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2020,10,26]]},"reference":[{"key":"e_1_2_1_1_1","volume-title":"Proceedings of the CIAA\u201906","volume":"4094","author":"Abdulla P. A."},{"key":"e_1_2_1_2_1","volume-title":"Proceedings of the LICS\u201995","author":"Alur R."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.3233\/FI-2015-1243"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/2629638"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-54458-7_24"},{"key":"e_1_2_1_6_1","volume-title":"Proceedings of the FoSSaCS\u201918","volume":"10803","author":"Baldan P."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01178506"},{"key":"e_1_2_1_9_1","first-page":"102","article-title":"Independence-friendly modal logic and true concurrency","volume":"9","author":"Bradfield J.","year":"2002","journal-title":"Nord. J. Comput."},{"key":"e_1_2_1_10_1","volume-title":"Proceedings of the ICALP\u201917 (LIPIcs","author":"Chalopin J."},{"key":"e_1_2_1_11_1","volume-title":"Handbook of Automated Reasoning","author":"Clarke E. M."},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF00264284"},{"key":"e_1_2_1_13_1","volume-title":"Proceedings of the FST-TCS\u201990 (LNCS","author":"De Nicola R."},{"key":"e_1_2_1_14_1","volume-title":"Proceedings of the REX Workshop (LNCS","volume":"466","author":"Degano P."},{"key":"e_1_2_1_15_1","volume-title":"Proceedings of the Petri Nets\u201915 (LNCS","volume":"48","author":"Dumas M."},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0304-3975(00)00034-7"},{"key":"e_1_2_1_17_1","unstructured":"J. Esparza and K. Heljanko. 2008. Unfoldings\u2014A Partial Order Approach to Model Checking. Springer.  J. Esparza and K. Heljanko. 2008. Unfoldings\u2014A Partial Order Approach to Model Checking. Springer."},{"key":"e_1_2_1_18_1","volume-title":"Proceedings of the CAV\u201906 (LNCS","volume":"328","author":"Farzan A."},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00596-1_5"},{"key":"e_1_2_1_21_1","volume-title":"Proceedings of the CONCUR\u201909 (LNCS","volume":"368","author":"Gutierrez J."},{"key":"e_1_2_1_22_1","volume-title":"Proceedings of the CONCUR\u201996","author":"Janin D."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00132-8"},{"key":"e_1_2_1_24_1","volume-title":"Proceedings of the LICS\u201916","author":"Jeffrey A."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00064-6"},{"key":"e_1_2_1_26_1","volume-title":"Automata, Logics, and Infinite Games: A Guide to Current Research, Erich Gr\u00e4del, Wolfgang Thomas, and Thomas Wilke (Eds.).","author":"Klauck H."},{"key":"e_1_2_1_27_1","volume-title":"Proceedings of the ICALP\u201987","author":"Lodaya K."},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2003.1210077"},{"key":"e_1_2_1_29_1","volume-title":"Proceedings of the STACS\u201997 (LNCS","volume":"425","author":"Montanari U."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-16066-3_15"},{"key":"e_1_2_1_31_1","volume-title":"Proceedings of the FST-TCS\u201989","author":"Mukund M."},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90181-E"},{"key":"e_1_2_1_33_1","first-page":"221","article-title":"Games and logics for a noninterleaving bisimulation","volume":"2","author":"Nielsen M.","year":"1995","journal-title":"Nord. J. Comput."},{"key":"e_1_2_1_34_1","unstructured":"T. Padoan. 2018. True Concurrency Workbench. Retrieved from http:\/\/github.com\/tpadoan\/TCWB.  T. Padoan. 2018. True Concurrency Workbench. Retrieved from http:\/\/github.com\/tpadoan\/TCWB."},{"key":"e_1_2_1_35_1","doi-asserted-by":"crossref","volume-title":"A temporal logic for event structures","author":"Penczek W.","DOI":"10.1007\/978-1-4613-0609-2_23"},{"key":"e_1_2_1_36_1","volume-title":"Time and Logic: A Computational Approach","author":"Penczek W."},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0035386"},{"key":"e_1_2_1_38_1","unstructured":"C. A. Petri. 1962. Kommunikation mit Automaten. Technischen Hoschule Darmstadt.  C. A. Petri. 1962. Kommunikation mit Automaten. Technischen Hoschule Darmstadt."},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129513000510"},{"key":"e_1_2_1_40_1","volume-title":"Proceedings of the POPL\u201916","author":"Pichon-Pharabod J."},{"key":"e_1_2_1_42_1","volume-title":"Higher dimensional modal logic. CoRR abs\/1405.4100","author":"Prisacariu C.","year":"2014"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.3233\/FI-1988-11404"},{"key":"e_1_2_1_44_1","volume-title":"Proceedings of the TACAS\u201998","author":"Stevens P."},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(90)90110-4"},{"key":"e_1_2_1_46_1","volume-title":"Formal and Natural Computing\u2014Essays Dedicated to Grzegorz Rozenberg (on occasion of his 60th birthday) (LNCS","author":"Thiagarajan P. S."},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1007\/s002360000041"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-54233-7_158"},{"key":"e_1_2_1_49_1","volume-title":"Petri Nets: Applications and Relationships to Other Models of Concurrency (LNCS","author":"Winskel G."},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","DOI":"10.1093\/comjnl\/bxp052"}],"container-title":["ACM Transactions on Computational Logic"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3412853","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3412853","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:47:02Z","timestamp":1750193222000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3412853"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,10,26]]},"references-count":47,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2020,10,31]]}},"alternative-id":["10.1145\/3412853"],"URL":"https:\/\/doi.org\/10.1145\/3412853","relation":{},"ISSN":["1529-3785","1557-945X"],"issn-type":[{"value":"1529-3785","type":"print"},{"value":"1557-945X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,10,26]]},"assertion":[{"value":"2018-09-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-07-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2020-10-26","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}