Skip to main content
SpringerLink
Log in

Deciding true concurrency equivalences on finite safe nets (preliminary report)

  • Conference paper
  • First Online:
Book cover Automata, Languages and Programming (ICALP 1993)

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

Included in the following conference series:

Abstract

We show that the pomset-trace equivalence problem for finite safe Petri Nets is decidable, and is in fact complete for EXPSPACE. We also show that history-preserving bisimulation between such nets is complete for DEXPTIME, settling a question left open by Vogler. Our decision procedures are based on establishing correspondences between bounded-size partial orders of transition firings, from which the upper bounds follow immediately. Lower bounds follow by reduction of corresponding interleaving (language) equivalence problems with known complexity. Our methods also yield tight complexity bounds for several other true concurrency equivalences. The results are independent of the presence of hidden transitions.

Supported by the AT&T GRPW Fellowship and ONR grant No. N00014-83-K-0125.

Supported by ONR grant No. N00014-83-K-0125.

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

Access this chapter

Log in via an institution

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. C. Alvarez, B. J., J. Gabarro, and M. Santa. Parallel complexity in the design and analysis of concurrent systems. In Proceedings of PARLE '91, Volume 505 of the Lecture Notes in Computer Science, pages 288–303, 1991.

    Google Scholar 

  2. E. Best, R. Devillers, A. Kiehn, and L. Pomello. Concurrent bisimulations in Petri Nets. Acta Inf., 28:231–264, 1991.

    Google Scholar 

  3. G. Boudol and I. Castellani. On the semantics of concurrency: Partial orders and transition systems. In Proceedings of TAPSOFT '87, Volume 249 of the Lecture Notes in Computer Science, pages 123–137, 1987.

    Google Scholar 

  4. S. D. Brookes, C. A. R. Hoare, and A. W. Roscoe. A theory of communicating sequential processes. J. ACM, 31(3):560–599, July 1984.

    Google Scholar 

  5. S. D. Brookes and A. W. Roscoe. An improved failures model for communicating processes. In Seminar on Concurrency, Volume 197 of Lecture Notes in Computer Science, pages 281–305, 1984.

    Google Scholar 

  6. R. Devillers. Maximality preserving bisimulation. Theor. Comput. Sci., 102(1):165–184, Aug. 1992.

    Google Scholar 

  7. J. E. Hopcroft and J. D. Ullman. Introduction to automata theory, languages, and computation. Addison-Wesley, 1979.

    Google Scholar 

  8. L. Jategaonkar and A. R. Meyer. Testing equivalence for Petri nets with action refinement. In Proceedings of CONCUR '92, Volume 630 of the Lecture Notes in Computer Science, pages 17–31, 1992.

    Google Scholar 

  9. L. Jategaonkar and A. R. Meyer. Self-synchronization of concurrent processes. To appear in the Proceedings of LICS, 1993.

    Google Scholar 

  10. P. Kannelakis and S. Smolka. CCS expressions, finite state processes, and three problems of equivalence. Inf. Comput., 86(1):43–68, 1990.

    Google Scholar 

  11. A. J. Mayer and L. J. Stockmeyer. The complexity of word problems — this time with interleaving. Technical report, IBM Research Division, Almaden Research Center, San Jose, CA, Sept. 1992.

    Google Scholar 

  12. R. Milner. Communication and Concurrency. Series in Computer Science. Prentice-Hall, Inc., 1989.

    Google Scholar 

  13. A. Rabinovich. Checking equivalences between concurrent systems of finite agents. In Proceedings of ICALP '92, Volume 379 of the Lecture Series in Computer Science, pages 696–707, 1992.

    Google Scholar 

  14. A. Rabinovich and B. Trakhtenbrot. Behavior structures and nets of processes. Fundamenta Informaticae, 11(4):357–404, 1988.

    Google Scholar 

  15. L. Stockmeyer, Jan. 1992. Unpublished notes.

    Google Scholar 

  16. D. Taubner and W. Vogler. Step failures semantics and a complete proof system. Acta Inf., 27(2):125–156, Nov. 1989.

    Google Scholar 

  17. R. van Glabbeek and U. Goltz. Equivalence notions for concurrent systems and refinement of actions. In Proceedings of MFCS '89, Volume 379 of the Lecture Series in Computer Science, pages 237–248, 1989.

    Google Scholar 

  18. R. van Glabbeek and F. Vaandrager. Petri net models for algebraic theories of concurrency. In Proceedings of PARLE '87, Volume 259 of the Lecture Notes in Computer Science, pages 224–242, 1987.

    Google Scholar 

  19. W. Vogler. Bisimulation and action refinement. In Proceedings of STACS '91, Volume 480 of the Lecture Notes in Computer Science, pages 309–321, 1991.

    Google Scholar 

  20. W. Vogler. Bisimulation and action refinement. Technical report, Technische Universität München, 1991.

    Google Scholar 

  21. W. Vogler. Deciding history preserving bisimulation. In Proceedings of ICALP '91, Volume 510 of the Lecture Notes in Computer Science, pages 495–505, 1991.

    Google Scholar 

  22. W. Vogler. Failures semantics based on interval semiwords is a congruence for refinement. Distributed Computing, 4:139–162, 1991.

    Google Scholar 

  23. W. Vogler. Is partial order semantics necessary for action refinement? Technical report, Technische Universität München, 1991.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. MIT Laboratory for Computer Science, 02139, Cambridge, MA

    Lalita Jategaonkar & Albert Meyer

Authors
  1. Lalita Jategaonkar
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Albert Meyer
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Andrzej Lingas Rolf Karlsson Svante Carlsson

Rights and permissions

Reprints and permissions

Copyright information

© 1993 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Jategaonkar, L., Meyer, A. (1993). Deciding true concurrency equivalences on finite safe nets (preliminary report). In: Lingas, A., Karlsson, R., Carlsson, S. (eds) Automata, Languages and Programming. ICALP 1993. Lecture Notes in Computer Science, vol 700. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-56939-1_99

Download citation

  • DOI: https://doi.org/10.1007/3-540-56939-1_99

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-56939-8

  • Online ISBN: 978-3-540-47826-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation