Abstract
We investigate the difference between two well-known notions of independence bisimilarity, history-preserving bisimulation and hereditary history-preserving bisimulation. We characterise the difference between the two bisimulations in trace-theoretical terms, advocating the view that the first is (just) a bisimulation for causality, while the second is a bisimulation for concurrency. We explore the frontier zone between the two notions by defining a hierarchy of bounded backtracking bisimulations. Our goal is to provide a stepping stone for the solution to the intriguing open problem of whether hereditary history-preserving bisimulation is decidable or not. We prove that each of the bounded bisimulations is decidable. However, we also prove that the hierarchy is strict. This rules out the possibility that decidability of the general problem follows directly from the special case. Finally, we give a non trivial reduction solving the general problem for a restricted class of systems and give pointers towards a full answer.
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
Laboratory for Foundations of Computer Science.
Basic Research in Computer Science, Centre of the Danish National Research Foundation. Part of this work was done while the second author was at LFCS.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
M. Bednarczyk. Hereditary history preserving bisimulation or what is the power of the future perfect in program logics. Technical report, Polish Acad. of Sciences, Gdansk, 1991.
E. Best, R. Devillers, A. Kiehn, and L. Pomello. Concurrent bisimulations in Petri nets. Acta Inform., 28(3):231–264, 1991.
A. Cheng. Reasoning About Concurrent Computational Systems. PhD thesis, BRICS, Dep. of Computer Science, University of Aarhus, 1996.
A. Cheng and M. Nielsen. Open maps (at) work. Research Series RS-95-23, BRICS, Dep. of Computer Science, University of Aarhus, Apr. 1995.
P. Degano, R. De Nicola, and U. Montanari. Partial orderings descriptions and observations of nondeterministic concurrent processes. In Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, volume 354 of LNCS, pages 438–466, 1989.
S. Fröschle. On the decidability problem of strong history-preserving bisimulation. Progress Report, 1998.
S. Fröschle and T. T. Hildebrandt. On plain and hereditary history-preserving bisimulation. Technical Report RS-99-4, BRICS, Dep. of Computer Science, University of Aarhus, 1999.
L. Jategaonkar and A. R. Meyer. Deciding true concurrency equivalences on safe, finite nets. Theor. Comp. Sci., 154(1):107–143, 1996.
A. Joyal, M. Nielsen, and G. Winskel. Bisimulation from open maps. Inform. and Comput., 127(2):164–185, 1996.
U. Montanari and M. Pistore. Minimal transition systems for history-preserving bisimulation. In STACS’ 97, volume 1200 of LNCS, pages 413–425. Springer, 1997.
M. Mukund and P. S. Thiagarajan. Linear time temporal logics over Mazurkiewicz traces. In POMIV’ 96, volume 29 of DIMACS, pages 171–201. AMS, 1997.
M. Nielsen and C. Clausen. Bisimulations, games and logic. Technical Report RS-94-6, BRICS, Dep. of Computer Science, University of Aarhus, April 1994.
A. Rabinovich and B. A. Trakhtenbrot. Behavior structures and nets. Fund. Inform., 11(4):357–403, 1988.
R. van Glabbeek and U. Goltz. Equivalence notions for concurrent systems and refinement of actions. In MFCS’ 89, volume 379 of LNCS, pages 237–248. Springer, 1989.
R. van Glabbeek and U. Goltz. Refinement of actions and equivalence notions for concurrent systems, 1998. http://theory.stanford.edu/rvg/abstracts.html.
W. Vogler. Deciding history preserving bisimilarity. In Automata, languages and programming’ 91, volume 510 of LNCS, pages 495–505. Springer, 1991.
W. Vogler. Bisimulation and action refinement. Theor. Comp. Sci., 114(1):173–200, 1993.
W. Vogler. Generalized OM-bisimulation. Inform. and Comput., 118(1):38–47, 1995.
G. Winskel and M. Nielsen. Models for concurrency. In Handbook of logic in computer science, Vol. 4, Oxford Sci. Publ., pages 1–148. Oxford Univ. Press, New York, 1995.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Fröschle, S.B., Hildebrandt, T.T. (1999). On Plain and Hereditary History-Preserving Bisimulation. In: Kutyłowski, M., Pacholski, L., Wierzbicki, T. (eds) Mathematical Foundations of Computer Science 1999. MFCS 1999. Lecture Notes in Computer Science, vol 1672. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48340-3_32
Download citation
DOI: https://doi.org/10.1007/3-540-48340-3_32
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66408-6
Online ISBN: 978-3-540-48340-3
eBook Packages: Springer Book Archive