Skip to main content
SpringerLink
Log in

Simulation is decidable for one-counter nets

Extended abstract

  • Conference paper
  • First Online:
CONCUR'98 Concurrency Theory (CONCUR 1998)

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

Included in the following conference series:

Abstract

We prove that the simulation preorder is decidable for the class of one-counter nets. A one-counter net consists of a finite-state machine operating on a variable (counter) which ranges over the natural numbers. Each transition can increase or decrease the value of the counter. A transition may not be performed if this implies that the value of the counter becomes negative. The class of one-counter nets is computationally equivalent to the class of Petri nets with one unbounded place, and to the class of pushdown automata where the stack alphabet is restricted to one symbol. To our knowledge, this is the first result in the literature which gives a positive answer to the decidability of simulation preorder between pairs of processes in a class whose elements are neither finite-state nor allow finite partitioning of their state spaces.

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. Parosh Aziz Abdulla and Bengt Jonsson. Verifying programs with unreliable channels. In Proc. 8th IEEE Int. Symp. on Logic in Computer Science, pages 160–170, 1993.

    Google Scholar 

  2. J.C.M. Baeten, J.A. Bergstra, and J.W. Klop. Decidability of bisimulation equivalence for processes generating context-free languages. Journal of the ACM, (40):653–682, 1993.

    Google Scholar 

  3. S. Christensen, Y. Hirshfeld, and F. Moller. Bisimulation equivalence is decidable for basic parallel processes. In Proc. CONCUR '93, Theories of Concurrency: Unification and Extension, pages 143–157, 1993.

    Google Scholar 

  4. S. Christensen, H. Hüttel, and C. Stirling. Bisimulation equivalence is decidable for all context-free processes. In W. R. Cleaveland, editor, Proc. CONCUR '92, Theories of Concurrency: Unification and Extension, pages 138–147, 1992.

    Google Scholar 

  5. J. Esparza. Petri nets, commutative context-free grammers, and basic parallel processes. In Proc. Fundementals of Computation Theory, number 965 in Lecture Notes in Computer Science, pages 221–232, 1995.

    MathSciNet  Google Scholar 

  6. J.F. Groote and H. Hüttel. Undecidable equivelences for basic process algebra. Information and Computation, 1994.

    Google Scholar 

  7. P. Jančar. Undecidability of bisimilarity for Petri nets and related problem. Theoretical Computer Science, (148):281–301, 1995.

    Google Scholar 

  8. P. Jančar. Bisimulation equivalence is decidable for one-counter processes. In Proc. ICALP '97, pages 549–559, 1997.

    Google Scholar 

  9. P. Jančar and J. Esparza. Deciding finiteness of petri nets up to bisimulation. In Proc. ICALP '96, number 1099 in Lecture Notes in Computer Science, pages 478–489, 1996.

    Google Scholar 

  10. P. Jančar and F. Moller. Checking regular properties of Petri nets. In Proc. CONCUR '95, 6th Int. Conf. on Concurrency Theory, pages 348–362, 1995.

    Google Scholar 

  11. Mats Kindahl. Results on decidability of simulation and bisimulation for lossy channel systems. Technical Report 91, Department of Computer Systems, Uppsala University, May 1997. Licentiate Thesis.

    Google Scholar 

  12. C. Stirling. Local model checking games. In Proc. CONCUR '95, 6th Int. Conf. on Concurrency Theory, volume 962 of Lecture Notes in Computer Science, pages 1–11. Springer Verlag, 1995.

    Google Scholar 

  13. C. Stirling. Decidability of bisimulation equivalence for normed pushdown processes. In Proc. CONCUR '96, 7th Int. Conf. on Concurrency Theory, volume 1119 of Lecture Notes in Computer Science, pages 217–232. Springer Verlag, 1996.

    Google Scholar 

  14. W. Thomas. On the synthesis of strategies in infinite games. In STACS 95, volume 900 of Lect. Notes in Comput. Sci., pages 1–13. Springer-Verlag, 1995.

    Google Scholar 

Download references

Author information

Authors and Affiliations

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

    Parosh Aziz Abdulla

  2. Institute of Mathematics and Computer Science, University of Latvia, Latvia

    Karlis Čerāns

Authors
  1. Parosh Aziz Abdulla
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Karlis Čerāns
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Davide Sangiorgi Robert de Simone

Rights and permissions

Reprints and permissions

Copyright information

© 1998 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Abdulla, P.A., Čerāns, K. (1998). Simulation is decidable for one-counter nets. In: Sangiorgi, D., de Simone, R. (eds) CONCUR'98 Concurrency Theory. CONCUR 1998. Lecture Notes in Computer Science, vol 1466. Springer, Berlin, Heidelberg. https://doi.org/10.1007/BFb0055627

Download citation

  • DOI: https://doi.org/10.1007/BFb0055627

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

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

  • Online ISBN: 978-3-540-68455-8

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation