{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,1,11]],"date-time":"2026-01-11T19:36:53Z","timestamp":1768160213457,"version":"3.49.0"},"reference-count":43,"publisher":"Cambridge University Press (CUP)","issue":"2","license":[{"start":{"date-parts":[[2013,9,27]],"date-time":"2013-09-27T00:00:00Z","timestamp":1380240000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/www.cambridge.org\/core\/terms"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":["Math. Struct. Comp. Sci."],"published-print":{"date-parts":[[2014,4]]},"abstract":"<jats:p>In this paper we introduce Event Identifier Logic (EIL), which extends Hennessy\u2013Milner logic by the addition of:<jats:list list-type=\"number\"><jats:list-item><jats:label>(1)<\/jats:label><jats:p>reverse as well as forward modalities; and<\/jats:p><\/jats:list-item><jats:list-item><jats:label>(2)<\/jats:label><jats:p>identifiers to keep track of events.<\/jats:p><\/jats:list-item><\/jats:list>We show that this logic corresponds to hereditary history-preserving (HH) bisimulation equivalence within a particular true-concurrency model, namely, stable configuration structures. We also show how natural sublogics of EIL correspond to coarser equivalences. In particular, we provide logical characterisations of weak-history- preserving (WH) and history-preserving (H) bisimulation. Logics corresponding to HH and H bisimulation have been given previously, but none, as far as we are aware, corresponding to WH bisimulation (when autoconcurrency is allowed). We also present characteristic formulas that characterise individual structures with respect to history-preserving equivalences.<\/jats:p>","DOI":"10.1017\/s0960129513000510","type":"journal-article","created":{"date-parts":[[2013,9,27]],"date-time":"2013-09-27T13:53:12Z","timestamp":1380289992000},"source":"Crossref","is-referenced-by-count":18,"title":["Event Identifier Logic"],"prefix":"10.1017","volume":"24","author":[{"given":"IAIN","family":"PHILLIPS","sequence":"first","affiliation":[]},{"given":"IREK","family":"ULIDOWSKI","sequence":"additional","affiliation":[]}],"member":"56","published-online":{"date-parts":[[2013,9,27]]},"reference":[{"key":"S0960129513000510_ref43","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-17906-2_31"},{"key":"S0960129513000510_ref42","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1994.1028"},{"key":"S0960129513000510_ref40","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0016222"},{"key":"S0960129513000510_ref36","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlap.2006.11.002"},{"key":"S0960129513000510_ref35","doi-asserted-by":"publisher","DOI":"10.1007\/11690634_17"},{"key":"S0960129513000510_ref34","first-page":"179","volume-title":"Time and Logic: A Computational Approach","author":"Penczek","year":"1995"},{"key":"S0960129513000510_ref33","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(81)90112-2"},{"key":"S0960129513000510_ref31","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-58131-6_54"},{"key":"S0960129513000510_ref27","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(94)00204-V"},{"key":"S0960129513000510_ref24","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(85)80025-5"},{"key":"S0960129513000510_ref23","doi-asserted-by":"publisher","DOI":"10.1145\/2455.2460"},{"key":"S0960129513000510_ref21","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00596-1_5"},{"key":"S0960129513000510_ref16","first-page":"199","volume-title":"Proceedings of 10th Annual IEEE Symposium on Logic in Computer Science, LICS 1995","author":"van Glabbeek","year":"1995"},{"key":"S0960129513000510_ref12","doi-asserted-by":"publisher","DOI":"10.1016\/S1571-0661(05)80297-X"},{"key":"S0960129513000510_ref26","doi-asserted-by":"publisher","DOI":"10.1016\/S0890-5401(03)00064-6"},{"key":"S0960129513000510_ref22","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-04081-8_24"},{"key":"S0960129513000510_ref11","doi-asserted-by":"publisher","DOI":"10.1016\/j.ipl.2003.11.008"},{"key":"S0960129513000510_ref7","first-page":"105","volume-title":"Formal Descriptions of Programming Concepts \u2013 III, Proceedings of the 3rd IFIP WG 2.2 Conference","author":"Degano","year":"1987"},{"key":"S0960129513000510_ref5","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-17660-8_52"},{"key":"S0960129513000510_ref20","doi-asserted-by":"publisher","DOI":"10.1016\/S0019-9958(86)80031-6"},{"key":"S0960129513000510_ref4","unstructured":"Bednarczyk M. A. (1991) Hereditary history preserving bisimulations or what is the power of the future perfect in program logics. Technical report, Institute of Computer Science, Polish Academy of Sciences, Gda\u0144sk."},{"key":"S0960129513000510_ref2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-15375-4_11"},{"key":"S0960129513000510_ref32","first-page":"221","article-title":"Games and logics for a noninterleaving bisimulation.","volume":"2","author":"Nielsen","year":"1995","journal-title":"Nordic Journal of Computing"},{"key":"S0960129513000510_ref37","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.64.8"},{"key":"S0960129513000510_ref3","unstructured":"Baldan P. and Crafa S. (2011) A logic for true concurrency. CoRR, abs\/1110.4094."},{"key":"S0960129513000510_ref39","unstructured":"Pinchinat S. , Laroussinie F. and Schnoebelen Ph. (1994) Logical characterizations of truly concurrent bisimulation. Technical Report 114, Grenoble."},{"key":"S0960129513000510_ref28","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(95)00035-U"},{"key":"S0960129513000510_ref10","first-page":"118","volume-title":"Proceedings, Fifth Annual IEEE Symposium on Logic in Computer Science, LICS 1990","author":"De Nicola","year":"1990"},{"key":"S0960129513000510_ref9","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0039058"},{"key":"S0960129513000510_ref14","doi-asserted-by":"publisher","DOI":"10.1007\/11539452_22"},{"key":"S0960129513000510_ref15","doi-asserted-by":"publisher","DOI":"10.1007\/s002360000041"},{"key":"S0960129513000510_ref30","first-page":"385","article-title":"Bisimulation for models in concurrency. In: Proceedings of 5th International Conference on Concurrency Theory, CONCUR '94.","volume":"836","author":"Nielsen","year":"1994","journal-title":"Springer-Verlag Lecture Notes in Computer Science"},{"key":"S0960129513000510_ref6","first-page":"843","article-title":"Back and forth bisimulations on prime event structures. In: Proceedings of PARLE '92.","volume":"605","author":"Cherief","year":"1992","journal-title":"Springer-Verlag Lecture Notes in Computer Science"},{"key":"S0960129513000510_ref25","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0057"},{"key":"S0960129513000510_ref19","doi-asserted-by":"publisher","DOI":"10.1007\/BFb0084794"},{"key":"S0960129513000510_ref18","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1997.2634"},{"key":"S0960129513000510_ref41","doi-asserted-by":"crossref","first-page":"357","DOI":"10.3233\/FI-1988-11404","article-title":"Behavior structures and nets.","volume":"11","author":"Rabinovich","year":"1988","journal-title":"Fundamenta Informaticae"},{"key":"S0960129513000510_ref8","first-page":"301","article-title":"Observational logics and concurrency models. In: Proceedings of 10th Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 1990.","volume":"472","author":"De Nicola","year":"1990","journal-title":"Springer-Verlag Lecture Notes in Computer Science"},{"key":"S0960129513000510_ref29","doi-asserted-by":"publisher","DOI":"10.1016\/0304-3975(92)90181-E"},{"key":"S0960129513000510_ref1","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.8.1"},{"key":"S0960129513000510_ref13","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-31982-5_21"},{"key":"S0960129513000510_ref38","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129511000429"},{"key":"S0960129513000510_ref17","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2009.06.014"}],"container-title":["Mathematical Structures in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/www.cambridge.org\/core\/services\/aop-cambridge-core\/content\/view\/S0960129513000510","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2022,3,7]],"date-time":"2022-03-07T00:46:40Z","timestamp":1646614000000},"score":1,"resource":{"primary":{"URL":"https:\/\/www.cambridge.org\/core\/product\/identifier\/S0960129513000510\/type\/journal_article"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,9,27]]},"references-count":43,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2014,4]]}},"alternative-id":["S0960129513000510"],"URL":"https:\/\/doi.org\/10.1017\/s0960129513000510","relation":{},"ISSN":["0960-1295","1469-8072"],"issn-type":[{"value":"0960-1295","type":"print"},{"value":"1469-8072","type":"electronic"}],"subject":[],"published":{"date-parts":[[2013,9,27]]},"article-number":"e240204"}}