{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,11]],"date-time":"2026-01-11T19:36:49Z","timestamp":1768160209200,"version":"3.49.0"},"reference-count":30,"publisher":"Association for Computing Machinery (ACM)","issue":"4","license":[{"start":{"date-parts":[[2014,7,1]],"date-time":"2014-07-01T00:00:00Z","timestamp":1404172800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100003407","name":"Ministero dell'Istruzione, dell'Universit\u00e0 e della Ricerca","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100003407","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["J. ACM"],"published-print":{"date-parts":[[2014,7]]},"abstract":"<jats:p>We propose a logic for true concurrency whose formulae predicate about events in computations and their causal dependencies. The induced logical equivalence is hereditary history-preserving bisimilarity, and fragments of the logic can be identified which correspond to other true concurrent behavioural equivalences in the literature: step, pomset and history-preserving bisimilarity. Standard Hennessy-Milner logic, and thus (interleaving) bisimilarity, is also recovered as a fragment. We also propose an extension of the logic with fixpoint operators, thus allowing to describe causal and concurrency properties of infinite computations. This work contributes to a rational presentation of the true concurrent spectrum and to a deeper understanding of the relations between the involved behavioural equivalences.<\/jats:p>","DOI":"10.1145\/2629638","type":"journal-article","created":{"date-parts":[[2014,8,12]],"date-time":"2014-08-12T13:53:48Z","timestamp":1407851628000},"page":"1-36","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":27,"title":["A Logic for True Concurrency"],"prefix":"10.1145","volume":"61","author":[{"given":"Paolo","family":"Baldan","sequence":"first","affiliation":[{"name":"University of Padova"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Silvia","family":"Crafa","sequence":"additional","affiliation":[{"name":"University of Padova"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2014,7]]},"reference":[{"key":"e_1_2_1_1_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of CONCUR\u201910, Paul Gastin and Fran\u00e7ois Laroussinie, Eds.","author":"Baldan Paolo","unstructured":"Paolo Baldan and Silvia Crafa . 2010. A logic for true concurrency . In Proceedings of CONCUR\u201910, Paul Gastin and Fran\u00e7ois Laroussinie, Eds. , Lecture Notes in Computer Science , vol. 6269 , Springer , Berlin , 147--161. Paolo Baldan and Silvia Crafa. 2010. A logic for true concurrency. In Proceedings of CONCUR\u201910, Paul Gastin and Fran\u00e7ois Laroussinie, Eds., Lecture Notes in Computer Science, vol. 6269, Springer, Berlin, 147--161."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF01178506"},{"key":"e_1_2_1_4_1","first-page":"102","article-title":"Independence-friendly modal logic and True Concurrency","volume":"9","author":"Bradfield Julian","year":"2002","unstructured":"Julian Bradfield and Sibylle B. Fr\u00f6schle . 2002 . Independence-friendly modal logic and True Concurrency . Nord. J. Comput. 9 , 1 (2002), 102 -- 117 . Julian Bradfield and Sibylle B. Fr\u00f6schle. 2002. Independence-friendly modal logic and True Concurrency. Nord. J. Comput. 9, 1 (2002), 102--117.","journal-title":"Nord. J. Comput."},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1007\/11538363_25"},{"key":"e_1_2_1_6_1","volume-title":"Handbook of Modal Logic, Patrick Blackburn, Johan van Benthem","author":"Bradfield Julian","unstructured":"Julian Bradfield and Colin Stirling . 2006. Modal mu-calculi . In Handbook of Modal Logic, Patrick Blackburn, Johan van Benthem , and Franck Wolter, Eds., Elsevier , Amsterdam, The Netherlands, 721--756. Julian Bradfield and Colin Stirling. 2006. Modal mu-calculi. In Handbook of Modal Logic, Patrick Blackburn, Johan van Benthem, and Franck Wolter, Eds., Elsevier, Amsterdam, The Netherlands, 721--756."},{"key":"e_1_2_1_7_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of PARLE\u201992, Daniel Etiemble and Jean-Claude Syre, Eds.","author":"Cherief Ferroudja","unstructured":"Ferroudja Cherief . 1992. Back and forth bisimulations on prime event structures . In Proceedings of PARLE\u201992, Daniel Etiemble and Jean-Claude Syre, Eds. , Lecture Notes in Computer Science , vol. 605 , Springer , Berlin , 843--858. Ferroudja Cherief. 1992. Back and forth bisimulations on prime event structures. In Proceedings of PARLE\u201992, Daniel Etiemble and Jean-Claude Syre, Eds., Lecture Notes in Computer Science, vol. 605, Springer, Berlin, 843--858."},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0072"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.5555\/646738.701963"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/111662.111685"},{"key":"e_1_2_1_11_1","series-title":"Lecture Notes in Computer Science","volume-title":"Rocco De Nicola, and Ugo Montanari","author":"Degano Pierpaolo","year":"1988","unstructured":"Pierpaolo Degano , Rocco De Nicola, and Ugo Montanari . 1988 . Partial orderings descriptions and observations of nondeterministic concurrent processes. In REX Workshop, Jaco W. de Bakker, Willem P. de Roever, and Grzegorz Rozenberg, Eds., Lecture Notes in Computer Science , vol. 354 , Springer , Berlin, 438--466. Pierpaolo Degano, Rocco De Nicola, and Ugo Montanari. 1988. Partial orderings descriptions and observations of nondeterministic concurrent processes. In REX Workshop, Jaco W. de Bakker, Willem P. de Roever, and Grzegorz Rozenberg, Eds., Lecture Notes in Computer Science, vol. 354, Springer, Berlin, 438--466."},{"key":"e_1_2_1_12_1","series-title":"Lecture Notes in Computer Science","volume-title":"Hildebrandt","author":"Fr\u00f6schle Sibylle B.","year":"1999","unstructured":"Sibylle B. Fr\u00f6schle and Thomas T . Hildebrandt . 1999 . On plain and hereditary history-preserving bisimulation. In Proceedings of MFCS\u201999, Miroslaw Kutylowski, Leszek Pacholski, and Tomasz Wierzbicki, Eds., Lecture Notes in Computer Science , vol. 1672 , Springer , Berlin, 354--365. Sibylle B. Fr\u00f6schle and Thomas T. Hildebrandt. 1999. On plain and hereditary history-preserving bisimulation. In Proceedings of MFCS\u201999, Miroslaw Kutylowski, Leszek Pacholski, and Tomasz Wierzbicki, Eds., Lecture Notes in Computer Science, vol. 1672, Springer, Berlin, 354--365."},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.scico.2004.08.002"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/3266641.3266652"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04081-8_24"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2455.2460"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(85)80025-5"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0057"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00064-6"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/646512.695493"},{"key":"e_1_2_1_22_1","first-page":"221","article-title":"Games and logics for a noninterleaving bisimulation","volume":"2","author":"Nielsen Mogens","year":"1995","unstructured":"Mogens Nielsen and Christian Clausen . 1995 . Games and logics for a noninterleaving bisimulation . Nord. J. Comput. 2 , 2, 221 -- 249 . Mogens Nielsen and Christian Clausen. 1995. Games and logics for a noninterleaving bisimulation. Nord. J. Comput. 2, 2, 221--249.","journal-title":"Nord. J. Comput."},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(81)90112-2"},{"key":"e_1_2_1_24_1","volume-title":"Time and Logic: A Computational Approach, Leonard Bolc and Andrzej Sza\u0142as","author":"Penczek Wojciech","unstructured":"Wojciech Penczek . 1995. Branching time and partial order in temporal logics . In Time and Logic: A Computational Approach, Leonard Bolc and Andrzej Sza\u0142as , Eds., UCL Press , London, UK , 179--228. Wojciech Penczek. 1995. Branching time and partial order in temporal logics. In Time and Logic: A Computational Approach, Leonard Bolc and Andrzej Sza\u0142as, Eds., UCL Press, London, UK, 179--228."},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.18.5"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.64.8"},{"key":"e_1_2_1_28_1","first-page":"357","article-title":"Behaviour structures and nets","volume":"11","author":"Rabinovich Alexander","year":"1988","unstructured":"Alexander M.. Rabinovich and Boris A. Trakhtenbrot . 1988 . Behaviour structures and nets . Fund. Inf. 11 , 357 -- 404 . Alexander M.. Rabinovich and Boris A. Trakhtenbrot. 1988. Behaviour structures and nets. Fund. Inf. 11, 357--404.","journal-title":"Fund. Inf."},{"key":"e_1_2_1_29_1","volume-title":"Handbook of Process Algebra, Jan A","author":"van Glabbeek Rob J.","unstructured":"Rob J. van Glabbeek . 2001. The linear time -- branching time spectrum I: The semantics of concrete, sequential processes . In Handbook of Process Algebra, Jan A . Bergstra, Alban Ponse, and Scott A. Smolka, Eds., Elsevier , Amsterdam, The Netherlands, 3--99. Rob J. van Glabbeek. 2001. The linear time -- branching time spectrum I: The semantics of concrete, sequential processes. In Handbook of Process Algebra, Jan A. Bergstra, Alban Ponse, and Scott A. Smolka, Eds., Elsevier, Amsterdam, The Netherlands, 3--99."},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/s002360000041"},{"key":"e_1_2_1_31_1","series-title":"Lecture Notes in Computer Science","volume-title":"Proceedings of ICALP\u201991, Javier Leach Albert, Burkhard Monien, and Mario Rodr\u00edguez-Artalejo, Eds.","author":"Vogler Walter","unstructured":"Walter Vogler . 1991. Deciding history preserving bisimilarity . In Proceedings of ICALP\u201991, Javier Leach Albert, Burkhard Monien, and Mario Rodr\u00edguez-Artalejo, Eds. , Lecture Notes in Computer Science , vol. 510 , Springer , Berlin , 495--505. Walter Vogler. 1991. Deciding history preserving bisimilarity. In Proceedings of ICALP\u201991, Javier Leach Albert, Burkhard Monien, and Mario Rodr\u00edguez-Artalejo, Eds., Lecture Notes in Computer Science, vol. 510, Springer, Berlin, 495--505."},{"key":"e_1_2_1_32_1","series-title":"Lecture Notes in Computer Science","volume-title":"Petri Nets: Applications and Relationships to Other Models of Concurrency, Wilfried Brauer, Wolfgang Reisig, and Grzegorz Rozenberg, Eds.","author":"Winskel Glynn","unstructured":"Glynn Winskel . 1987. Event structures . In Petri Nets: Applications and Relationships to Other Models of Concurrency, Wilfried Brauer, Wolfgang Reisig, and Grzegorz Rozenberg, Eds. , Lecture Notes in Computer Science , vol. 255 , Springer , Berlin , 325--392. Glynn Winskel. 1987. Event structures. In Petri Nets: Applications and Relationships to Other Models of Concurrency, Wilfried Brauer, Wolfgang Reisig, and Grzegorz Rozenberg, Eds., Lecture Notes in Computer Science, vol. 255, Springer, Berlin, 325--392."},{"key":"e_1_2_1_33_1","volume-title":"Handbook of logic in Computer Science","author":"Winskel Glynn","unstructured":"Glynn Winskel and Mogens Nielsen . 1995. Models for concurrency . In Samson Abramsky, Dov M. Gabbay, and Thomas S. E. Maibaum, Eds., Handbook of logic in Computer Science , vol. 4 , Clarendon Press , Oxford, UK . Glynn Winskel and Mogens Nielsen. 1995. Models for concurrency. In Samson Abramsky, Dov M. Gabbay, and Thomas S. E. Maibaum, Eds., Handbook of logic in Computer Science, vol. 4, Clarendon Press, Oxford, UK."}],"container-title":["Journal of the ACM"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2629638","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2629638","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T06:13:30Z","timestamp":1750227210000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2629638"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2014,7]]},"references-count":30,"journal-issue":{"issue":"4","published-print":{"date-parts":[[2014,7]]}},"alternative-id":["10.1145\/2629638"],"URL":"https:\/\/doi.org\/10.1145\/2629638","relation":{},"ISSN":["0004-5411","1557-735X"],"issn-type":[{"value":"0004-5411","type":"print"},{"value":"1557-735X","type":"electronic"}],"subject":[],"published":{"date-parts":[[2014,7]]},"assertion":[{"value":"2011-10-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-04-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2014-07-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}