Skip to main content
SpringerLink
Log in
Book cover

International Workshop on Reachability Problems

RP 2010: Reachability Problems pp 51–75Cite as

Lossy Counter Machines Decidability Cheat Sheet

  • Conference paper

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

Abstract

Lossy counter machines (LCM’s) are a variant of Minsky counter machines based on weak (or unreliable) counters in the sense that they can decrease nondeterministically and without notification. This model, introduced by R. Mayr [TCS 297:337-354 (2003)], is not yet very well known, even though it has already proven useful for establishing hardness results.

In this paper we survey the basic theory of LCM’s and their verification problems, with a focus on the decidability/undecidability divide.

Work supported by the Agence Nationale de la Recherche, grant ANR-06-SETIN-001.

This is a preview of subscription content, 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 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

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Abdulla, P.A., Baier, C., Purushothaman Iyer, S., Jonsson, B.: Simulating perfect channels with probabilistic lossy channels. Information and Computation 197(1–2), 22–40 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  2. Abdulla, P.A., Ben Henda, N., de Alfaro, L., Mayr, R., Sandberg, S.: Stochastic games with lossy channels. In: Amadio, R.M. (ed.) FOSSACS 2008. LNCS, vol. 4962, pp. 35–49. Springer, Heidelberg (2008)

    Chapter  Google Scholar 

  3. Abdulla, P.A., Bertrand, N., Rabinovich, A., Schnoebelen, P.: Verification of probabilistic systems with faulty communication. Information and Computation 202(2), 141–165 (2005)

    Article  MATH  MathSciNet  Google Scholar 

  4. Abdulla, P.A., Bouajjani, A., d’Orso, J.: Monotonic and downward closed games. Journal of Logic and Computation 18(1), 153–169 (2008)

    Article  MATH  MathSciNet  Google Scholar 

  5. Abdulla, P.A., Čerāns, K., Jonsson, B., Tsay, Y.-K.: Algorithmic analysis of programs with well quasi-ordered domains. Information and Computation 160(1/2), 109–127 (2000)

    Article  MATH  MathSciNet  Google Scholar 

  6. Abdulla, P.A., Jonsson, B.: Undecidable verification problems for programs with unreliable channels. Information and Computation 130(1), 71–90 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  7. Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. Information and Computation 127(2), 91–101 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  8. Abdulla, P.A., Kindahl, M.: Decidability of simulation and bisimulation between lossy channel systems and finite state systems. In: Lee, I., Smolka, S.A. (eds.) CONCUR 1995. LNCS, vol. 962, pp. 333–347. Springer, Heidelberg (1995)

    Google Scholar 

  9. Baier, C., Bertrand, N., Schnoebelen, P.: On computing fixpoints in well-structured regular model checking, with applications to lossy channel systems. In: Hermann, M., Voronkov, A. (eds.) LPAR 2006. LNCS (LNAI), vol. 4246, pp. 347–361. Springer, Heidelberg (2006)

    Chapter  Google Scholar 

  10. Baier, C., Bertrand, N., Schnoebelen, P.: Verifying nondeterministic probabilistic channel systems against ω-regular linear-time properties. ACM Trans. Computational Logic 9(1) (2007)

    Google Scholar 

  11. Bouajjani, A., Mayr, R.: Model checking lossy vector addition systems. In: Meinel, C., Tison, S. (eds.) STACS 1999. LNCS, vol. 1563, pp. 323–333. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  12. Browne, M.C., Clarke, E.M., Grumberg, O.: Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science 59(1–2), 115–131 (1988)

    Article  MATH  MathSciNet  Google Scholar 

  13. Bukart, O., Caucal, D., Moller, F., Steffen, B.: Verification on infinite structures. In: Bergstra, J.A., Ponse, A., Smolka, S.A. (eds.) Handbook of Process Algebra, ch. 9, pp. 545–623. Elsevier, Amsterdam (2001)

    Chapter  Google Scholar 

  14. Cardoza, E., Lipton, R., Meyer, A.R.: Exponential space complete problems for Petri nets and commutative subgroups. In: Proc. STOC ’76, pp. 50–54. ACM Press, New York (1976)

    Google Scholar 

  15. Cécé, G., Finkel, A., Purushothaman Iyer, S.: Unreliable channels are easier to verify than perfect channels. Information and Computation 124(1), 20–31 (1996)

    Article  MATH  MathSciNet  Google Scholar 

  16. Chambart, P., Schnoebelen, P.: Computing blocker sets for the Regular Post Embedding Problem. In: Proc. DLT 2010. LNCS. Springer, Heidelberg (to appear, 2010)

    Google Scholar 

  17. Clote, P.: On the finite containment problem for Petri nets. Theoretical Computer Science 43(1), 99–105 (1986)

    Article  MATH  MathSciNet  Google Scholar 

  18. Demri, S.: Linear-time temporal logics with Presburger constraints: An overview. J. Applied Non-Classical Logics 16(3-4), 311–347 (2006)

    Article  MATH  MathSciNet  Google Scholar 

  19. Demri, S., Lazić, R.: LTL with the freeze quantifier and register automata. In: Proc. LICS 2006, pp. 17–26. IEEE Computer Society Press, Los Alamitos (2006)

    Google Scholar 

  20. Dufourd, C., Finkel, A., Schnoebelen, P.: Reset nets between decidability and undecidability. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 103–115. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

  21. Dufourd, C., Jančar, P., Schnoebelen, P.: Boundedness of reset P/T nets. In: Wiedermann, J., Van Emde Boas, P., Nielsen, M. (eds.) ICALP 1999. LNCS, vol. 1644, pp. 301–310. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  22. Emerson, E.A.: Temporal and modal logic. In: van Leeuwen, J. (ed.) Handbook of Theoretical Computer Science, ch. 16, vol. B, pp. 995–1072. Elsevier, Amsterdam (1990)

    Google Scholar 

  23. Figueira, D., Figueira, S., Schmitz, S., Schnoebelen, P.: Ackermann and primitive-recursive upper bounds with Dickson’s lemma (2010) (in preparation)

    Google Scholar 

  24. Figueira, D., Segoufin, L.: Future-looking logics on data words and trees. In: Královič, R., Niwiński, D. (eds.) MFCS 2009. LNCS, vol. 5734, pp. 331–343. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

  25. Finkel, A.: A generalization of the procedure of Karp and Miller to well structured transition systems. In: Ottmann, T. (ed.) ICALP 1987. LNCS, vol. 267, pp. 499–508. Springer, Heidelberg (1987)

    Google Scholar 

  26. Finkel, A.: Reduction and covering of infinite reachability trees. Information and Computation 89(2), 144–179 (1990)

    Article  MATH  MathSciNet  Google Scholar 

  27. Finkel, A., Goubault-Larrecq, J.: Forward analysis for WSTS, part I: Completions. In: Proc. STACS 2009. Leibniz International Proceedings in Informatics, vol. 3, pp. 433–444. Leibniz-Zentrum für Informatik (2009)

    Google Scholar 

  28. Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theoretical Computer Science 256(1–2), 63–92 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  29. Henzinger, T.A., Majumdar, R., Raskin, J.-F.: A classification of symbolic transition systems. ACM Trans. Computational Logic 6(1), 1–32 (2005)

    Article  MathSciNet  Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  31. Jančar, P., Kučera, A., Mayr, R.: Deciding bisimulation-like equivalences with finite-state processes. Theoretical Computer Science 258(1–2), 409–433 (2001)

    MATH  MathSciNet  Google Scholar 

  32. Jurdziński, M., Lazić, R.: Alternation-free modal mu-calculus for data trees. In: Proc. LICS 2007, pp. 131–140. IEEE Comp. Soc. Press, Los Alamitos (2007)

    Google Scholar 

  33. Kracht, M.: A new proof of a theorem by Ginsburg and Spanier. Dept. Linguistics, UCLA (December 2002) (manuscript)

    Google Scholar 

  34. Kruskal, J.B.: The theory of well-quasi-ordering: A frequently discovered concept. Journal of Combinatorial Theory, Series A 13(3), 297–305 (1972)

    Article  MATH  MathSciNet  Google Scholar 

  35. Kučera, A., Schnoebelen, P.: A general approach to comparing infinite-state systems with their finite-state specifications. Theoretical Computer Science 358(2–3), 315–333 (2006)

    MATH  MathSciNet  Google Scholar 

  36. van Leeuwen, J.: A partial solution to the reachability-problem for vector-addition systems. In: Proc. STOC ’74, pp. 303–309. ACM Press, New York (1974)

    Google Scholar 

  37. Leroux, J., Point, G.: TaPAS: The Talence Presburger Arithmetic Suite. In: Kowalewski, S., Philippou, A. (eds.) Proc. TACAS 2009. LNCS, vol. 5505, pp. 182–185. Springer, Heidelberg (2009)

    Google Scholar 

  38. Mayr, R.: Undecidable problems in unreliable computations. In: Gonnet, G.H., Viola, A. (eds.) LATIN 2000. LNCS, vol. 1776, pp. 377–386. Springer, Heidelberg (2000)

    Chapter  Google Scholar 

  39. Mayr, R.: Undecidable problems in unreliable computations. Theoretical Computer Science 297(1–3), 337–354 (2003)

    Article  MATH  MathSciNet  Google Scholar 

  40. McAloon, K.: Petri nets and large finite sets. Theoretical Computer Science 32(1–2), 173–183 (1984)

    Article  MATH  MathSciNet  Google Scholar 

  41. Raskin, J.-F., Samuelides, M., Van Begin, L.: Games for counting abstractions. In: Proc. AVoCS 2004. Electronic Notes in Theor. Comp. Sci, vol. 128(6), pp. 69–85. Elsevier Science, Amsterdam (2005)

    Google Scholar 

  42. Schnoebelen, P.: Bisimulation and other undecidable equivalences for lossy channel systems. In: Kobayashi, N., Pierce, B.C. (eds.) TACS 2001. LNCS, vol. 2215, pp. 385–399. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  43. Schnoebelen, P.: Verifying lossy channel systems has nonprimitive recursive complexity. Information Processing Letters 83(5), 251–261 (2002)

    Article  MATH  MathSciNet  Google Scholar 

  44. Schnoebelen, P.: Revisiting Ackermann-Hardness for Lossy Counter Machines and Reset Petri Nets. In: Hliněny, P., Kučera, A. (eds.) MFCS 2010. LNCS, vol. 6281, pp. 616–628. Springer, Heidelberg (2010)

    Google Scholar 

  45. Sifakis, J.: A unified approach for studying the properties of transitions systems. Theoretical Computer Science 18, 227–258 (1982)

    Article  MATH  MathSciNet  Google Scholar 

  46. Tan, T.: On pebble automata for data languages with decidable emptiness problem. In: Královič, R., Niwiński, D. (eds.) MFCS 2009. LNCS, vol. 5734, pp. 712–723. Springer, Heidelberg (2009)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LSV, ENS Cachan, CNRS, 61, av. Pdt. Wilson, F-94230, Cachan, France

    Philippe Schnoebelen

Authors
  1. Philippe Schnoebelen
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculty of Informatics, Masaryk University, Botanická 68a, 60200, Brno, Czech Republic

    Antonín Kučera

  2. Department of Computer Science, University of Liverpool, Ashton Building, L69 3BX, Liverpool, England

    Igor Potapov

Rights and permissions

Reprints and permissions

Copyright information

© 2010 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Schnoebelen, P. (2010). Lossy Counter Machines Decidability Cheat Sheet. In: Kučera, A., Potapov, I. (eds) Reachability Problems. RP 2010. Lecture Notes in Computer Science, vol 6227. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-15349-5_4

Download citation

  • DOI: https://doi.org/10.1007/978-3-642-15349-5_4

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-642-15348-8

  • Online ISBN: 978-3-642-15349-5

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation