Hostname: page-component-586b7cd67f-rdxmf Total loading time: 0 Render date: 2024-11-29T00:21:42.033Z Has data issue: false hasContentIssue false
  • English
  • Français

A hierarchy of reverse bisimulations on stable configuration structures

Published online by Cambridge University Press:  28 February 2012

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

Abstract

Van Glabbeek and Goltz (and later Fecher) have investigated the relationships between various equivalences on stable configuration structures, including interleaving bisimulation (IB), step bisimulation (SB), pomset bisimulation and hereditary history-preserving (H-H) bisimulation. Since H-H bisimulation may be characterised by the use of reverse as well as forward transitions, it is of interest to investigate these and other forms of bisimulations where both forward and reverse transitions are allowed. Bednarczyk asked whether SB with reverse steps is as strong as H-H bisimulation. We answer this question negatively. We give various characterisations of SB with reverse steps, showing that forward steps do not add power. We strengthen Bednarczyk's result that, in the absence of auto-concurrency, reverse IB is as strong as H-H bisimulation, by showing that we need only exclude auto-concurrent events at the same depth in the configuration.

We consider several other forms of observations of reversible behaviour and define a wide range of bisimulations by mixing the forward and reverse observations. We investigate the power of these bisimulations and represent the relationships between them as a hierarchy with IB at the bottom and H-H at the top.

Type
Paper
Information
Mathematical Structures in Computer Science , Volume 22 , Special Issue 2: Express '09, Ice '09 and Sos '09 , April 2012 , pp. 333 - 372
Copyright
Copyright © Cambridge University Press 2012

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.)

References

Abramsky, S. (1987) Observation equivalence as a testing equivalence. Theoretical Computer Science 53 225–241.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.Google 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
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, IEEE Computer Society Press 118–129.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-Holland 105–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. (2004) Decidability and Coincidence of Equivalences for Concurrency, Ph.D. thesis, University of Edinburgh.Google Scholar
Fröschle, S. B. and Lasota, S. (2005) Decomposition and complexity of hereditary history preserving bisimulation on BPP. In: Proceedings of CONCUR 2005. Springer-Verlag Lecture Notes in Computer Science 3653 263–277.CrossRefGoogle Scholar
van Glabbeek, R. J. (1996) History preserving process graphs. Draft, 20 June 1996. (Available at http://boole.stanford.edu/~rvg/pub/history.draft.dvi.)Google Scholar
van Glabbeek, R. J. and Goltz, U. (1989) Partial order semantics for refinement of actions – neither necessary nor always sufficient but appropriate when used with care. Bulletin of the EATCS 38 154–163.Google 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.Google 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
Joyal, A., Nielsen, M. and Winskel, G. (1996) Bisimulation from open maps. Information and Computation 127 (2)164–185.Google Scholar
Jurdziński, M., Nielsen, M. and Srba, J. (2003) Undecidability of domino games and hhp-bisimilarity. Information and Computation 184 (2)343–368.Google Scholar
Milner, R. (1989) Communication and Concurrency, Prentice-Hall.Google Scholar
Nielsen, M. and Clausen, C. (1994) Bisimulation, games and logic. In: Results and Trends in Theoretical Computer Science. Springer-Verlag Lecture Notes in Computer Science 812 289–306.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.Google Scholar
Phillips, I. C. C. and Ulidowski, I. (2007a) Reversibility and models for concurrency. In: Hennessy, M. C. B. and van Glabbeek, R. (eds.) Proceedings of Fourth International Workshop on Structural Operational Semantics (SOS 2007). Electronic Notes in Theoretical Computer Science 192 (1)93–108.CrossRefGoogle Scholar
Phillips, I. C. C. and Ulidowski, I. (2007b) Reversing algebraic process calculi. Journal of Logic and Algebraic Programming 73 (1-2)70–96.CrossRefGoogle Scholar
Phillips, I. C. C. and Ulidowski, I. (2010) Reverse bisimulations on stable configuration structures. In: Klin, B. and Sobociński, P. (eds.) Proceedings of Sixth International Workshop on Structural Operational Semantics (SOS 2009). Electronic Proceedings in Theoretical Computer Science 18 62–76.CrossRefGoogle 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.Google Scholar
Rabinovich, A. and Trakhtenbrot, B. A. (1988) Behavior structures and nets. Fundamenta Informaticae 11 (4)357–403.CrossRefGoogle Scholar
Winskel, G. (1987) Event structures. In: Advances in Petri Nets 1986. Springer-Verlag Lecture Notes in Computer Science 255 325–392.Google Scholar