Hostname: page-component-599cfd5f84-z6fpd Total loading time: 0 Render date: 2025-01-07T06:50:23.220Z Has data issue: false hasContentIssue false
  • English
  • Français

Event Identifier Logic†

Published online by Cambridge University Press:  27 September 2013

IAIN PHILLIPS  and
IREK ULIDOWSKI
IAIN PHILLIPS
Affiliation:
Department of Computing, Imperial College London, 180 Queen's Gate, London SW7 2AZ, United Kingdom Email: [email protected]
IREK ULIDOWSKI
Affiliation:
Department of Computer Science, University of Leicester, University Road, Leicester LE1 7RH, United Kingdom Email: [email protected]
Get access Rights & Permissions [Opens in a new window]

Abstract

In this paper we introduce Event Identifier Logic (EIL), which extends Hennessy–Milner logic by the addition of:

  1. (1) reverse as well as forward modalities; and

  2. (2) identifiers to keep track of events.

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.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 24 , Issue 2 , April 2014 , e240204
Copyright
Copyright © Cambridge University Press 2013 

Access options

Get access to the full version of this content by using one of the access options below. (Log in options will check for institutional or personal access. Content may require purchase if you do not have access.)

Footnotes

†

This paper was originally submitted for inclusion in the forthcoming EXPRESS 2011 Special Issue of Mathematical Structures in Computer Science. It was accepted, and the revised (final) version was sent in November 2012. Subsequently, in April 2013, in view of the extra time required to handle other articles in the Special Issue, the Guest Editors very kindly agreed to the article being published separately in the Journal to avoid further delay in publication.

References

Aceto, L., Ingólfsdóttir, A. and Sack, J. (2009) Characteristic formulae for fixed-point semantics: A general framework. In: Proceedings 16th International Workshop on Expressiveness in Concurrency, EXPRESS 2009. Electronic Proceedings in Theoretical Computer Science 8 1–15.CrossRefGoogle Scholar
Baldan, P. and Crafa, S. (2010) A logic for true concurrency. In: Proceedings of 21st International Conference on Concurrency Theory, CONCUR 2010. Springer-Verlag Lecture Notes in Computer Science 6269 147–161.CrossRefGoogle Scholar
Baldan, P. and Crafa, S. (2011) A logic for true concurrency. CoRR, abs/1110.4094.Google Scholar
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ńsk.Google Scholar
Boudol, G. and Castellani, I. (1987) On the semantics of concurrency: partial orders and transition systems. In: Proceedings of TAPSOFT '87. Springer-Verlag Lecture Notes in Computer Science 249 123–137.CrossRefGoogle Scholar
Cherief, F. (1992) Back and forth bisimulations on prime event structures. In: Proceedings of PARLE '92. Springer-Verlag Lecture Notes in Computer Science 605 843–858.Google Scholar
Degano, P., De Nicola, R. and Montanari, U. (1987) Observational equivalences for concurrency models. In: Wirsing, M. (ed.) Formal Descriptions of Programming Concepts – III, Proceedings of the 3rd IFIP WG 2.2 Conference, North-Holland105–129.Google Scholar
De Nicola, R. and Ferrari, G. L. (1990) Observational logics and concurrency models. In: Proceedings of 10th Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 1990. Springer-Verlag Lecture Notes in Computer Science 472 301–315.Google Scholar
De Nicola, R., Montanari, U. and Vaandrager, F. (1990) Back and forth bisimulations. In: Proceedings of CONCUR '90, Theories of Concurrency: Unification and Extension. Springer-Verlag Lecture Notes in Computer Science 458 152–165.CrossRefGoogle Scholar
De Nicola, R. and Vaandrager, F. (1990) Three logics for branching bisimulation (extended abstract). In: Proceedings, Fifth Annual IEEE Symposium on Logic in Computer Science, LICS 1990, IEEE Computer Society Press 118–129.Google Scholar
Fecher, H. (2004) A completed hierarchy of true concurrent equivalences. Information Processing Letters 89 (5)261–265.CrossRefGoogle Scholar
Fröschle, S. B. (1999) Decidability of plain and hereditary history-preserving bisimilarity for BPP. In: Proceedings of 6th International Workshop on Expressiveness in Concurrency, EXPRESS '99. Electronic Notes in Theoretical Computer Science 27 85–106.CrossRefGoogle Scholar
Fröschle, S. B. (2005) Composition and decomposition in true-concurrency. In: Foundations of Software Science and Computational Structures, 8th International Conference, FOSSACS 2005. Springer-Verlag Lecture Notes in Computer Science 3441 333–347.CrossRefGoogle Scholar
Fröschle, S. B. and Lasota, S. (2005) Decomposition and complexity of hereditary history preserving bisimulation on BPP. In: Proceedings of 16th International Conference on Concurrency Theory, CONCUR 2005. Springer-Verlag Lecture Notes in Computer Science 3653 263–277.CrossRefGoogle Scholar
van Glabbeek, R. J. and Goltz, U. (2001) Refinement of actions and equivalence notions for concurrent systems. Acta Informatica 37 (4/5)229–327.CrossRefGoogle Scholar
van Glabbeek, R. J. and Plotkin, G. D. (1995) Configuration structures. In: Proceedings of 10th Annual IEEE Symposium on Logic in Computer Science, LICS 1995, IEEE Computer Society Press 199–209.Google Scholar
van Glabbeek, R. J. and Plotkin, G. D. (2009) Configuration structures, event structures and Petri nets. Theoretical Computer Science 410 (41)4111–4159.CrossRefGoogle Scholar
van Glabbeek, R. J. and Vaandrager, F. W. (1997) The difference between splitting in n and n+1. Information and Computation 136 (2)109–142.CrossRefGoogle Scholar
Goltz, U., Kuiper, R. and Penczek, W. (1992) Propositional temporal logics and equivalences. In: Proceedings of 3rd International Conference on Concurrency Theory, CONCUR '92. Springer-Verlag Lecture Notes in Computer Science 630 222–236.CrossRefGoogle Scholar
Graf, S. and Sifakis, J. (1986) A modal characterization of observational congruence on finite terms of CCS. Information and Control 68 (1–3)125–145.CrossRefGoogle Scholar
Gutierrez, J. (2009) Logics and bisimulation games for concurrency, causality and conflict. In: Proceedings of the 12th International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2009. Springer-Verlag Lecture Notes in Computer Science 5504 48–62.CrossRefGoogle Scholar
Gutierrez, J. and Bradfield, J. C. (2009) Model-checking games for fixpoint logics with partial order models. In: Proceedings of the 20th International Conference on Concurrency Theory, CONCUR 2009. Springer-Verlag Lecture Notes in Computer Science 5710 354–368.CrossRefGoogle Scholar
Hennessy, M. C. B. and Milner, R. (1985) Algebraic laws for nondeterminism and concurrency. Journal of the Association for Computing Machinery 32 (1)137–161.CrossRefGoogle Scholar
Hennessy, M. C. B. and Stirling, C. (1985) The power of the future perfect in program logics. Information and Control 67 23–52.CrossRefGoogle Scholar
Joyal, A., Nielsen, M. and Winskel, G. (1996) Bisimulation from open maps. Information and Computation 127 (2)164–185.CrossRefGoogle Scholar
Jurdzinski, M., Nielsen, M. and Srba, J. (2003) Undecidability of domino games and HHP-bisimilarity. Information and Computation 184 (2)343–368.CrossRefGoogle Scholar
Laroussinie, F., Pinchinat, S. and Schnoebelen, Ph. (1995) Translations between modal logics of reactive systems. Theoretical Computer Science 140 (1)53–71.CrossRefGoogle Scholar
Laroussinie, F. and Schnoebelen, Ph. (1995) A hierarchy of temporal logics with past. Theoretical Computer Science 148 303–324.CrossRefGoogle Scholar
Mukund, M. and Thiagarajan, P. S. (1992) A logical characterization of well branching event structures. Theoretical Computer Science 96 (1)35–72.CrossRefGoogle Scholar
Nielsen, M. and Clausen, C. (1994a) Bisimulation for models in concurrency. In: Proceedings of 5th International Conference on Concurrency Theory, CONCUR '94. Springer-Verlag Lecture Notes in Computer Science 836 385–400.Google Scholar
Nielsen, M. and Clausen, C. (1994b) Bisimulation, games, and logic. In: Results and Trends in Theoretical Computer Science. Springer-Verlag Lecture Notes in Computer Science 812 289–306.CrossRefGoogle Scholar
Nielsen, M. and Clausen, C. (1995) Games and logics for a noninterleaving bisimulation. Nordic Journal of Computing 2 (2)221–249.Google Scholar
Nielsen, M., Plotkin, G. D. and Winskel, G. (1981) Petri nets, event structures and domains, part I. Theoretical Computer Science 13 85–108.CrossRefGoogle Scholar
Penczek, W. (1995) Branching time and partial order in temporal logics. In: Time and Logic: A Computational Approach, UCL Press Ltd 179–228.Google Scholar
Phillips, I. C. C. and Ulidowski, I. (2006) Reversing algebraic process calculi. In: Proceedings of Ninth International Conference on Foundations of Software Science and Computation Structures, FOSSACS 2006. Springer-Verlag Lecture Notes in Computer Science 3921 246–260.CrossRefGoogle Scholar
Phillips, I. C. C. and Ulidowski, I. (2007) Reversing algebraic process calculi. Journal of Logic and Algebraic Programming 73 (1–2)70–96.CrossRefGoogle Scholar
Phillips, I. C. C. and Ulidowski, I. (2011) A logic with reverse modalities for history-preserving bisimulations. In: Proceedings of Eighteenth International Workshop on Expressiveness in Concurrency, EXPRESS 2011. Electronic Proceedings in Theoretical Computer Science 64 104–118.CrossRefGoogle Scholar
Phillips, I. C. C. and Ulidowski, I. (2012) A hierarchy of reverse bisimulations on stable configuration structures. Mathematical Structures in Computer Science 22 333–372.CrossRefGoogle Scholar
Pinchinat, S., Laroussinie, F. and Schnoebelen, Ph. (1994) Logical characterizations of truly concurrent bisimulation. Technical Report 114, Grenoble.Google Scholar
Pomello, L. (1986) Some equivalence notions for concurrent systems – An overview. In: Advances in Petri Nets 1985. Springer-Verlag Lecture Notes in Computer Science 222 381–400.CrossRefGoogle Scholar
Rabinovich, A. and Trakhtenbrot, B. A. (1988) Behavior structures and nets. Fundamenta Informaticae 11 (4)357–403.CrossRefGoogle Scholar
Steffen, B. and Ingólfsdóttir, A. (1994) Characteristic formulae for processes with divergence. Information and Computation 110 (1)149–163.CrossRefGoogle Scholar
Winskel, G. (1987) Event structures. In: Advances in Petri Nets 1986. Springer-Verlag Lecture Notes in Computer Science 255 325–392.CrossRefGoogle Scholar