Skip to main content
SpringerLink
Log in

On the Decidability of Non-Interleaving Process Equivalences

  • Conference paper
CONCUR ’94: Concurrency Theory (CONCUR 1994)

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

Included in the following conference series:

Abstract

We develop decision procedures based on proof tableaux for a number of non-interleaving equivalences over processes. The processes considered are those which can be described in a simple extension of BPP, Basic Parallel Processes, obtained by omitting the restriction operator from COS. Decision procedures are given for both strong and weak versions of causal bisimulation, location equivalence and ST-bisimulation.

This work has been supported by the ARC project An Algebraic Theory for Distributed Systems

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

Access this chapter

Log in via an institution
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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. G. Boudol, I. Castellani, M. Hennessy, and A. Kiehn. A theory of processes with localities. In Proceedings of CONCUR 92.

    Google Scholar 

  2. G. Boudol, I. Castellani, M. Hennessy, and A. Kiehn. Observing localities. Theoretical Computer Science, (114): 31–61, 1993.

    Google Scholar 

  3. I. Castellani and M. Hennessy. Distributed bisimulations. Report 5/87, University of Sussex, 1987. Also in JACM 1989.

    Google Scholar 

  4. S. Christensen. Distributed bisimilarity is decidable for a class of infinite—state systems. In Proceedings of CONCUR 92, number 630 in Lecture Notes in Computer Science, 1992.

    Google Scholar 

  5. S. Christensen. Decidability and Decomposition in Process Algebras. Ph.d. thesis, University of dinburgh, 1993.

    Google Scholar 

  6. S. Christensen, Y. Hirshfeld, and F. Moller. Bisimulation equivalence is decidable for all basic parallel processes. In E. Best, editor, Proceedings of CONCUR 93, number 715 in Lecture Notes in Computer Science, pages 143–157. Springer-Verlag, 1993.

    Google Scholar 

  7. S. Christensen, Y. Hirshfeld, and F. Moller. Decomposability, decidability and axiomatisability for bisimulation equivalence on basic parallel processes. In E. Best, editor, Proceedings of LICS 93. IEEE Computer society Press, 1993.

    Google Scholar 

  8. S. Christensen, H. Hüttel, and C. Stirling. Bisimulation equivalence is decidable for all context-free processes. In Proceedings of CONCUR 92, number 630 in Lecture Notes in Computer Science, pages 138–147. Springer-Verlag, 1992.

    Google Scholar 

  9. R. Cleaveland, J. Parrow, and B. Steffen. A semantics based verification tool for finite state systems. In Proceedings of the 9th International Symposium on Protocol Specification, Testing and Verification, North Holland, 1989.

    Google Scholar 

  10. P. Darondeau and P. Degano. Causal trees. In Proceedings of ICALP 89, number 372 in Lecture Notes in Computer Science, pages 234–248, 1989.

    Google Scholar 

  11. P. Darondeau and P. Degano. Causal trees, interleaving + causality. In I. Guessarian, editor, Semantics of Systems of Concurrent Processes, number 469 in Lecture Notes in Computer Science, pages 239–255, 1990.

    Google Scholar 

  12. P. Degano, R. De Nicola, and U. Montanari. Partial ordering descriptions and observations of nondeterministic concurrent processes. In Proceedings REX School/Workshop on Linear Time, Branching Time and Partial Order in Logics and Models for Concurrency, number 354 in Lecture Notes in Computer Science, pages 438–466, 1989.

    Google Scholar 

  13. Y. Hirshfeld. Petri nets and the equivalence problem. In K. Meinke, editor, Proceedings of CSL„ 1994. to appear.

    Google Scholar 

  14. Y. Janär. Undecidability of bisimilarity and consequences for reachability sets equality and language equivalence. unpublished, 1993.

    Google Scholar 

  15. L. Jategaonkar and A. Meyer. Deciding true concurrency equivalences on finite Petri nets. In A. Lingas, R. Karlsson, and S. Carlsson, editors, Proceedings of ICALP 93„ number 700, pages 519–531, 1993.

    Google Scholar 

  16. A. Kiehn. Comparing locality and causality based equivalences. Acta Informatica, 1994. to appear, Revision of Local and global causes, report TUM-I9132.

    Google Scholar 

  17. M. Lothaire. Combinatorics on Words. Addison-Wesley Publishing Company, 1983.

    Google Scholar 

  18. R. Milner. Communication and Concurrency. Prentice-Hall, 1989.

    Google Scholar 

  19. R. De Simone and D. Vergamimi. Aboard auto. Report RT111, INRIA, 1989.

    Google Scholar 

  20. R.J. van Glabbeek and F.W. Vaandrager. Petri net models for algebraic theories of concurrency. In J.W. de Bakker, A.J. Nijman, and P.C. Treleaven, editors, Proceedings PARLE conference, number 259 in Lecture Notes in Computer Science, pages 224–242. Springer-Verlag, 1987.

    Google Scholar 

  21. W. Vogler. Deciding history preserving bisimilarity. In Proceedings of ICA LP 91, number 510 in Lecture Notes in Computer Science, pages 495–505. Springer-Verlag, 1991.

    Google Scholar 

  22. W. Vogler. Generalized OM-bisimulation. Report TUM-I9113, Technische Universität München, 1991.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Institut für Informatik, TU München, Germany

    Astrid Kiehn

  2. Cognitive and Computing Sciences, University of Sussex, UK

    Matthew Hennessy

Authors
  1. Astrid Kiehn
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Matthew Hennessy
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Systems, Uppsala University, P.O. Box 325, S-751 05, Uppsala, Sweden

    Bengt Jonsson

  2. Swedish Institute of Computer Science, P.O. Box 1262, S-164 28, Kista, Sweden

    Joachim Parrow

Rights and permissions

Reprints and permissions

Copyright information

© 1994 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Kiehn, A., Hennessy, M. (1994). On the Decidability of Non-Interleaving Process Equivalences. In: Jonsson, B., Parrow, J. (eds) CONCUR ’94: Concurrency Theory. CONCUR 1994. Lecture Notes in Computer Science, vol 836. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-48654-1_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-540-48654-1_3

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-58329-5

  • Online ISBN: 978-3-540-48654-1

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation