Skip to main content
SpringerLink
Log in

EXPSPACE-Complete Variant of Countdown Games, and Simulation on Succinct One-Counter Nets

  • Conference paper
  • First Online:
Reachability Problems (RP 2018)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 11123))

Included in the following conference series:

Abstract

We answer an open complexity question for simulation preorder of succinct one-counter nets (i.e., one-counter automata with no zero tests where counter increments and decrements are integers written in binary), by showing that all relations between bisimulation equivalence and simulation preorder are EXPSPACE-hard for these nets. We describe a reduction from reachability games whose EXPSPACE-completeness in the case of succinct one-counter nets was shown by Hunter [RP 2015], by using other results. We also provide a direct self-contained EXPSPACE-completeness proof for a special case of such reachability games, namely for a modification of countdown games that were shown EXPTIME-complete by Jurdzinski, Sproston, Laroussinie (LMCS 2008); in our modification the initial counter value is not given but is freely chosen by the first player.

This research has been supported by Grant No. 18-11193S, Grant Agency of the Czech Rep. (P. Jančar and P. Osička), and by Grant No. SP2018/172, VŠB-Techn. Univ. Ostrava (Z. Sawa).

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 EPUB and 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

References

  1. Abdulla, P.A., Čerāns, K.: Simulation is decidable for one-counter nets. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 253–268. Springer, Heidelberg (1998). https://doi.org/10.1007/BFb0055627

    Chapter  Google Scholar 

  2. Böhm, S., Göller, S., Jančar, P.: Equivalence of deterministic one-counter automata is NL-complete. In: STOC 2013, pp. 131–140. ACM (2013)

    Google Scholar 

  3. Böhm, S., Göller, S., Jančar, P.: Bisimulation equivalence and regularity for real-time one-counter automata. J. Comput. Syst. Sci. 80(4), 720–743 (2014). Preliminary versions appeared at CONCUR 2010 and MFCS 2011

    Article  MathSciNet  Google Scholar 

  4. Chandra, A.K., Kozen, D., Stockmeyer, L.J.: Alternation. J. ACM 28(1), 114–133 (1981)

    Article  MathSciNet  Google Scholar 

  5. Demri, S., Lazić, R., Sangnier, A.: Model checking freeze LTL over one-counter automata. In: Amadio, R. (ed.) FoSSaCS 2008. LNCS, vol. 4962, pp. 490–504. Springer, Heidelberg (2008). https://doi.org/10.1007/978-3-540-78499-9_34

    Chapter  Google Scholar 

  6. Göller, S., Haase, C., Ouaknine, J., Worrell, J.: Model checking succinct and parametric one-counter automata. In: Abramsky, S., Gavoille, C., Kirchner, C., Meyer auf der Heide, F., Spirakis, P.G. (eds.) ICALP 2010 Part II. LNCS, vol. 6199, pp. 575–586. Springer, Heidelberg (2010). https://doi.org/10.1007/978-3-642-14162-1_48

    Chapter  MATH  Google Scholar 

  7. Göller, S., Lohrey, M.: Branching-time model checking of one-counter processes. In: STACS 2010. LIPIcs, vol. 5, pp. 405–416. Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik (2010)

    Google Scholar 

  8. Göller, S., Mayr, R., To, A.W.: On the computational complexity of verifying one-counter processes. In: LICS 2009, pp. 235–244. IEEE Computer Society (2009)

    Google Scholar 

  9. Haase, C., Kreutzer, S., Ouaknine, J., Worrell, J.: Reachability in succinct and parametric one-counter automata. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 369–383. Springer, Heidelberg (2009). https://doi.org/10.1007/978-3-642-04081-8_25

    Chapter  Google Scholar 

  10. Hofman, P., Lasota, S., Mayr, R., Totzke, P.: Simulation problems over one-counter nets. Log. Methods Comput. Sci. 12(1), 46 pp. (2016). Preliminary versions appeared at FSTTCS 2013, LICS 2013, and in Totzke’s Ph.D. thesis (2014)

    Google Scholar 

  11. Hunter, P.: Reachability in succinct one-counter games. In: Bojańczyk, M., Lasota, S., Potapov, I. (eds.) RP 2015. LNCS, vol. 9328, pp. 37–49. Springer, Cham (2015). https://doi.org/10.1007/978-3-319-24537-9_5

    Chapter  MATH  Google Scholar 

  12. Jančar, P., Kučera, A., Moller, F.: Simulation and bisimulation over one-counter processes. In: Reichel, H., Tison, S. (eds.) STACS 2000. LNCS, vol. 1770, pp. 334–345. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-46541-3_28

    Chapter  Google Scholar 

  13. Jančar, P., Kučera, A., Moller, F., Sawa, Z.: DP lower bounds for equivalence-checking and model-checking of one-counter automata. Inf. Comput. 188(1), 1–19 (2004)

    Article  MathSciNet  Google Scholar 

  14. Jančar, P., Moller, F., Sawa, Z.: Simulation problems for one-counter machine. In: Pavelka, J., Tel, G., Bartošek, M. (eds.) SOFSEM 1999. LNCS, vol. 1725, pp. 404–413. Springer, Heidelberg (1999). https://doi.org/10.1007/3-540-47849-3_28

    Chapter  Google Scholar 

  15. Jančar, P., Sawa, Z.: A note on emptiness for alternating finite automata with a one-letter alphabet. Inf. Process. Lett. 104(5), 164–167 (2007)

    Article  MathSciNet  Google Scholar 

  16. Jančar, P., Srba, J.: Undecidability of bisimilarity by defender’s forcing. J. ACM 55(1), 5:1–5:26 (2008)

    Article  MathSciNet  Google Scholar 

  17. Jurdzinski, M., Sproston, J., Laroussinie, F.: Model checking probabilistic timed automata with one or two clocks. Log. Methods Comput. Sci. 4(3), 28 pp. (2008)

    Google Scholar 

  18. Kiefer, S.: BPA bisimilarity is EXPTIME-hard. Inf. Process. Lett. 113(4), 101–106 (2013)

    Article  MathSciNet  Google Scholar 

  19. Kučera, A.: Efficient verification algorithms for one-counter processes. In: Montanari, U., Rolim, J.D.P., Welzl, E. (eds.) ICALP 2000. LNCS, vol. 1853, pp. 317–328. Springer, Heidelberg (2000). https://doi.org/10.1007/3-540-45022-X_28

    Chapter  Google Scholar 

  20. Mayr, R.: Undecidability of weak bisimulation equivalence for 1-counter processes. In: Baeten, J.C.M., Lenstra, J.K., Parrow, J., Woeginger, G.J. (eds.) ICALP 2003. LNCS, vol. 2719, pp. 570–583. Springer, Heidelberg (2003). https://doi.org/10.1007/3-540-45061-0_46

    Chapter  Google Scholar 

  21. Reichert, J.: On the complexity of counter reachability games. Fundam. Inform. 143(3–4), 415–436 (2016)

    Article  MathSciNet  Google Scholar 

  22. Serre, O.: Parity games played on transition graphs of one-counter processes. In: Aceto, L., Ingólfsdóttir, A. (eds.) FoSSaCS 2006. LNCS, vol. 3921, pp. 337–351. Springer, Heidelberg (2006). https://doi.org/10.1007/11690634_23

    Chapter  Google Scholar 

  23. Srba, J.: Beyond language equivalence on visibly pushdown automata. Log. Methods Comput. Sci. 5(1), 22 pp. (2009)

    Google Scholar 

  24. Valiant, L.G., Paterson, M.: Deterministic one-counter automata. J. Comput. Syst. Sci. 10(3), 340–350 (1975)

    Article  MathSciNet  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. Department of Computer Science, Faculty of Science, Palacký University Olomouc, Olomouc, Czechia

    Petr Jančar & Petr Osička

  2. Department of Computer Science, FEI, Technical University of Ostrava, Ostrava, Czechia

    Zdeněk Sawa

Authors
  1. Petr Jančar
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Petr Osička
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Zdeněk Sawa
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Petr Jančar .

Editor information

Editors and Affiliations

  1. University of Liverpool, Liverpool, UK

    Igor Potapov

  2. Aix-Marseille University, Marseille, France

    Pierre-Alain Reynier

Rights and permissions

Reprints and permissions

Copyright information

© 2018 Springer Nature Switzerland AG

About this paper

Check for updates. Verify currency and authenticity via CrossMark

Cite this paper

Jančar, P., Osička, P., Sawa, Z. (2018). EXPSPACE-Complete Variant of Countdown Games, and Simulation on Succinct One-Counter Nets. In: Potapov, I., Reynier, PA. (eds) Reachability Problems. RP 2018. Lecture Notes in Computer Science(), vol 11123. Springer, Cham. https://doi.org/10.1007/978-3-030-00250-3_5

Download citation

  • DOI: https://doi.org/10.1007/978-3-030-00250-3_5

  • Published:

  • Publisher Name: Springer, Cham

  • Print ISBN: 978-3-030-00249-7

  • Online ISBN: 978-3-030-00250-3

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation