Skip to main content
SpringerLink
Log in

Checking regular properties of Petri nets

  • Session: Decidability Results
  • Conference paper
  • First Online:
CONCUR '95: Concurrency Theory (CONCUR 1995)

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

Included in the following conference series:

Abstract

In this paper we consider the problem of comparing an arbitrary Petri net against one whose places may contain only a bounded number of tokens (that is, against a regular behaviour), with respect to trace set inclusion and equivalence, as well as simulation and bisimulation. In contrast to the known result that language equivalence is undecidable, we find that all of the above are in fact decidable. We furthermore demonstrate that it is undecidable whether a given Petri net is either trace equivalent or simulation equivalent to any (unspecified) bounded net.

The first author is supported by the Grant Agency of the Czech Republic, Grant No. 201/93/2123; and also received partial support from Esprit Network EXPRESS in order to visit the Swedish Institute of Computer Science, during which time the research reported here was carried out.

The second author is supported by Esprit Basic Research Action No. 7166, “CONCUR2”.

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. Abdulla, P., K. Čerāns, P. Jančar, and F. Moller. One counter Petri nets vs bounded Petri nets. Research Report, 1995.

    Google Scholar 

  2. Christensen, S., Y. Hirshfeld, and F. Moller. Bisimulation is decidable for basic parallel processes. In E. Best (editor), Proceedings of CONCUR'93: Concurrency Theory, Lecture Notes in Computer Science 715, pp143–157, Springer-Verlag, 1993.

    Google Scholar 

  3. Dickson, L.E. Finiteness of the odd perfect and primitive abundant numbers with distinct factors. American Journal of Mathematics 35, pp413–422, 1913.

    Google Scholar 

  4. Ginsburg, S., and E. Spanier. Semigroups, Presburger formulas, and languages. Pacific Journal of Mathematics 16, pp285–296, 1966.

    Google Scholar 

  5. van Glabbeek, R.J. The linear time — branching time spectrum. In J.C.M. Baeten, and J.W. Klop (editors), Proceedings of CONCUR'90: Concurrency Theory, Lecture Notes in Computer Science 458, pp278–297, Springer-Verlag, 1990.

    Google Scholar 

  6. Higman, H. Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society 3(2), pp326–336, 1952.

    Google Scholar 

  7. Hirshfeld, Y. Petri nets and the equivalence problem. In E. Börger, Y. Gurevich, and K. Meinke (editors), Proceedings of CSL'93: Computer Science Logic, Lecture Notes in Computer Science 832, pp165–174, Springer-Verlag, 1994.

    Google Scholar 

  8. Hopcroft, J.E., and J.D. Ullman. Introduction to Automata Theory, Languages, and Computation. Addison Wesley, 1979.

    Google Scholar 

  9. Hüttel, H. Undecidable equivalences for basic parallel processes. In R.K. Shyamasundar (editor), Proceedings of FSTTCS'93: Foundations of Software Technology and Theoretical Computer Science, Lecture Notes in Computer Science 761, Springer-Verlag, 1993.

    Google Scholar 

  10. Jančar, P. Undecidability of bisimilarity for Petri nets and some related problems. Journal of Theoretical Computer Science (to appear). (A preliminary version appears in P. Enjalbert, E.W. Mayr and K.W. Wagner (editors), Proceedings of STACS'94: Symposium on Theoretical Aspects of Computer Science, Lecture Notes in Computer Science 775, pp581–592, Springer-Verlag, 1994.)

    Google Scholar 

  11. Jančar, P. Decidability questions for equivalences on Petri nets. Czech Habilitation Thesis. Masaryk University, Brno. (Submitted April 1995.)

    Google Scholar 

  12. Karp, R., and R. Miller. Parallel program schemata. Journal of Computer and System Sciences 3, pp167–195, 1969.

    Google Scholar 

  13. Mauw, S., and H. Mulder. Regularity of BPA-systems is decidable. In B. Jonsson and J. Parrow (editors), Proceedings of CONCUR'94: Concurrency Theory, Lecture Notes in Computer Science 836, pp34–47, Springer-Verlag, 1993.

    Google Scholar 

  14. Mayr, E. An algorithm for the general Petri net reachability problem. SIAM Journal of Computing 13, pp441–460, 1984.

    Article  Google Scholar 

  15. Mazurkiewicz, A. Trace theory. In W. Brauer, W. Reisig, and G. Rozenberg (editors), Petri Nets: Applications and Relationships to Other Models of Concurrency, Lecture Notes in Computer Science 255, pp279–324, Springer-Verlag, 1987.

    Google Scholar 

  16. Milner, R. Communication and Concurrency. Prentice Hall, 1989.

    Google Scholar 

  17. Minsky, M. Computation: Finite and Infinite Machines. Prentice Hall, 1967.

    Google Scholar 

  18. Peterson, J.L. Petri Net Theory and the Modeling of Systems. Prentice Hall, 1981.

    Google Scholar 

  19. Stirling, C. Local model checking games. Department of Computer Science Research Report, University of Edinburgh, 1995.

    Google Scholar 

  20. Valk, R., and G. Vidal-Naquet. Petri nets and regular languages. Journal of Computer and System Sciences 23(3), pp299–325, 1981.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, University of Ostrava, Dvořákova 7, 701 00, Ostrava 1, Czech Republic

    Petr Jančar

  2. Swedish Institute of Computer Science, Box 1263, 164 28, Kista, Sweden

    Faron Moller

Authors
  1. Petr Jančar
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Faron Moller
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Insup Lee Scott A. Smolka

Rights and permissions

Reprints and permissions

Copyright information

© 1995 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Jančar, P., Moller, F. (1995). Checking regular properties of Petri nets. In: Lee, I., Smolka, S.A. (eds) CONCUR '95: Concurrency Theory. CONCUR 1995. Lecture Notes in Computer Science, vol 962. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-60218-6_26

Download citation

  • DOI: https://doi.org/10.1007/3-540-60218-6_26

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-60218-7

  • Online ISBN: 978-3-540-44738-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation