Skip to main content

Simulation and Bisimulation over One-Counter Processes

  • Conference paper
  • First Online:
STACS 2000 (STACS 2000)

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

Included in the following conference series:

Abstract

We show an effective construction of (a periodicity description of) the maximal simulation relation for a given one-counter net. Then we demonstrate how to reduce simulation problems over one-counter nets to analogous bisimulation problems over one-counter automata. We use this to demonstrate the decidability of various problems, specifically testing regularity and strong regularity of one-counter nets with respect to simulation equivalence, and testing simulation equivalence between a one-counter net and a deterministic pushdown automaton. Various obvious generalisations of these problems are known to be undecidable.

Partially supported by the Grant Agency of the Czech Republic, grants No. 201/97/0456 and No. 201/00/0400.

Supported by a Research Fellowship granted by the Alexander von Humboldt Foundation and by a Post-Doc grant GA ČR No. 201/98/P046.

Partially supported by TFR grant No. 221-98-103 and Np. 201/97/275.

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

Access this chapter

Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 109.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. P.A. Abdulla and K. Čerāns. Simulation is decidable for one-counter nets. In Proceedings of CONCUR’98, volume 1466 of LNCS, pages 253–268. Springer, 1998.

    Google Scholar 

  2. O. Burkart, D. Caucal, and B. Steffen. Bisimulation collapse and the process taxonomy. In Proceedings of CONCUR’96, volume 1119 of LNCS, pages 247–262. Springer, 1996.

    Google Scholar 

  3. P. Jančar. Bisimulation equivalence is decidable for one-counter processes. In Proceedings of ICALP’97, volume 1256 of LNCS, pages 549–559. Springer, 1997.

    Google Scholar 

  4. P. Jančar and J. Esparza. Deciding finiteness of Petri nets up to bisimilarity. In Proceedings of ICALP’96, volume 1099 of LNCS, pages 478–489. Springer, 1996.

    Google Scholar 

  5. P. Jančar and F. Moller. Checking regular properties of Petri nets. In Proceedings of CONCUR’95, volume 962 of LNCS, pages 348–362. Springer, 1995.

    Google Scholar 

  6. P. Jančar and F. Moller. Simulation of one-counter nets via colouring. In Proceedings of Workshop Journées Systèmes Infinis, LSV-ENS Cachan, pages 1–6, November 1998. (Revised version, Research Report 159, Computing Science Department, Uppsala University, 1999.)

    Google Scholar 

  7. P. Jančar, F. Moller, and Z. Sawa. Simulation problems for one-counter machines. In Proceedings of SOFSEM’99, volume 1725 of LNCS, pages 398–407. Springer, 1999.

    Google Scholar 

  8. A. Kučera. On finite representations of infinite-state behaviours. Information Processing Letters, 70(1):23–30, 1999.

    Article  MATH  MathSciNet  Google Scholar 

  9. A. Kučera and J. Esparza. A logical viewpoint on process-algebraic quotients. In Proceedings of CSL’99, volume 1683 of LNCS, pages 499–514. Springer, 1999.

    Google Scholar 

  10. A. Kučera and R. Mayr. Simulation preorder on simple process algebras. In Proceedings of ICALP’99, volume 1644 of LNCS, pages 503–512. Springer, 1999.

    Google Scholar 

  11. S. Mauw and H. Mulder. Regularity of BPA-systems is decidable. In Proceedings of CONCUR’94, volume 836 of LNCS, pages 34–47. Springer, 1994.

    Google Scholar 

  12. F. Moller. Infinite results. In Proceedings of CONCUR’96, volume 1119 of LNCS, pages 195–216. Springer, 1996.

    Google Scholar 

  13. G. Sénizergues. Decidability of bisimulation equivalence for equational graphs of finite out-degree. In Proceedings of 39th Annual Symposium on Foundations of Computer Science, pages 120–129. IEEE Computer Society Press, 1998.

    Google Scholar 

  14. R.J. van Glabbeek. The linear time — branching time spectrum. In Proceedings of CONCUR’90, volume 458 of LNCS, pages 278–297. Springer, 1990.

    Google Scholar 

Download references

Author information

Authors and Affiliations

Authors

Editor information

Editors and Affiliations

Rights and permissions

Reprints and permissions

Copyright information

© 2000 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Jančar, P., Kučera, A., Moller, F. (2000). Simulation and Bisimulation over One-Counter Processes. In: Reichel, H., Tison, S. (eds) STACS 2000. STACS 2000. Lecture Notes in Computer Science, vol 1770. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-46541-3_28

Download citation

  • DOI: https://doi.org/10.1007/3-540-46541-3_28

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-67141-1

  • Online ISBN: 978-3-540-46541-6

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics