Skip to main content

Hereditary History Preserving Bisimulation Is Decidable for Trace-Labelled Systems

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2556))

Abstract

Hereditary history preserving bisimulation is a natural extension of bisimulation to the setting of so-called “true” concurrency. Somewhat surprisingly, this extension turns out to be undecidable, in general, for finite-state concurrent systems. In this paper, we show that for a substantial and useful class of finite-state concurrent systems - those whose semantics can be described in terms of Mazurkiewicz traces - hereditary history preserving is decidable.

Partially supported by IFCPAR Project 2102-1 (ACSMV).

This is a preview of subscription content, log in via an institution.

Buying options

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. M.A. Bednarczyk: Hereditary history preserving bisimulation or what is the power of the future perfect in program logics. Technical report, Polish Academy of Sciences, Gdansk (1991).

    Google Scholar 

  2. M.A. Bednarczyk: Categories of asynchronous systems, PhD Thesis, Report 1/88, Computer Science, University of Sussex (1988).

    Google Scholar 

  3. P. Degano, R. de Nicola and U. Montanari: Partial ordering descriptions and observations of nondeterministic concurrent processes, in Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, Springer LNCS 354 (1989) 438–466.

    Chapter  Google Scholar 

  4. V. Diekert and G. Rozenberg (eds), The Book of Traces,World Scientific, Singapore (1995).

    Google Scholar 

  5. S.B. Fröschle and T.T. Hildebrandt: On plain and hereditary history-preserving bisimulation, Proc MFCS’ 99, Springer LNCS 1672 (1999) 354–365.

    Google Scholar 

  6. L. Jategaonkar and A. Meyer: Deciding true concurrency equivalence on safe, finite nets, Theoretical Computer Science, 154(1) (1996) 107–143.

    Article  MATH  MathSciNet  Google Scholar 

  7. A. Joyal, M. Nielsen and G. Winskel: Bisimulation from open maps, Information and Computation, 127(2) (1996) 164–185.

    Article  MATH  MathSciNet  Google Scholar 

  8. M. Jurdzinski and M. Nielsen: Hereditary history preserving bisimilarity is undecidable, in Proc. STACS 2000 Springer LNCS 1770 (2000) 358–369.

    Google Scholar 

  9. K. Lodaya, R. Parikh, R. Ramanujam and P.S. Thiagarajan: A Logical Study of Distributed Transition Systems, Information and Computation 119(1) (1995) 91–118.

    Article  MATH  MathSciNet  Google Scholar 

  10. A. Mazurkiewicz: Basic notions of trace theory, in: J.W. de Bakker, W.P. de Roever, G. Rozenberg (eds.), Linear time, branching time and partial order in logics and models for concurrency, LNCS, 354 (1989) 285–363.

    Chapter  Google Scholar 

  11. R. Milner: Communication and Concurrency, Prentice-Hall, London (1989).

    Google Scholar 

  12. M. Nielsen and C. Clausen: Games and Logics for a Noninterleaving Bisimulation, Nordic Journal of Computing 2(2) (1995) 221–249.

    MATH  MathSciNet  Google Scholar 

  13. D. Park: Concurrency and automata on infinite sequences, in Proc. Theoretical Computer Science: 5th GI Conference, Springer LNCS 104 (1981).

    Google Scholar 

  14. W. Reisig and G. Rozenberg (eds.): Lectures on Petri Nets, Vols I and II Springer LNCS 1492,1493 (1998).

    Google Scholar 

  15. A. Rabinovitch and B.A. Trakhtenbrot: Behavior strucures and nets, Fundamenta Informaticae, 11(4) (1988) 357–403.

    MathSciNet  Google Scholar 

  16. R. van Glabbeek and U. Goltz: Refinement of actions and equivalence notions for concurrent systems, Proc MFCS’ 89, Springer LNCS 379 (1989) 237–248.

    Google Scholar 

  17. G. Winskel and M. Nielsen: Models for concurrency, in S. Abramsky, D. Gabbay and T.S.E. Maibaum, eds, Handbook of Logic in Computer Science, Vol 4, Oxford (1995) 1–148.

    Google Scholar 

  18. W. Zielonka: Notes on finite asynchronous automata, R.A.I.R.O.-Inform. Théor. Appl., 21 (1987) 99–135.

    MATH  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2002 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Mukund, M. (2002). Hereditary History Preserving Bisimulation Is Decidable for Trace-Labelled Systems. In: Agrawal, M., Seth, A. (eds) FST TCS 2002: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2002. Lecture Notes in Computer Science, vol 2556. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-36206-1_26

Download citation

  • DOI: https://doi.org/10.1007/3-540-36206-1_26

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-00225-3

  • Online ISBN: 978-3-540-36206-7

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics