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.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
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)
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)
Abdulla, P.A., Bertrand, N., Rabinovich, A., Schnoebelen, P.: Verification of probabilistic systems with faulty communication. Information and Computation 202(2), 141–165 (2005)
Abdulla, P.A., Bouajjani, A., d’Orso, J.: Monotonic and downward closed games. Journal of Logic and Computation 18(1), 153–169 (2008)
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)
Abdulla, P.A., Jonsson, B.: Undecidable verification problems for programs with unreliable channels. Information and Computation 130(1), 71–90 (1996)
Abdulla, P.A., Jonsson, B.: Verifying programs with unreliable channels. Information and Computation 127(2), 91–101 (1996)
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)
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)
Baier, C., Bertrand, N., Schnoebelen, P.: Verifying nondeterministic probabilistic channel systems against ω-regular linear-time properties. ACM Trans. Computational Logic 9(1) (2007)
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)
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)
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)
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)
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)
Chambart, P., Schnoebelen, P.: Computing blocker sets for the Regular Post Embedding Problem. In: Proc. DLT 2010. LNCS. Springer, Heidelberg (to appear, 2010)
Clote, P.: On the finite containment problem for Petri nets. Theoretical Computer Science 43(1), 99–105 (1986)
Demri, S.: Linear-time temporal logics with Presburger constraints: An overview. J. Applied Non-Classical Logics 16(3-4), 311–347 (2006)
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)
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)
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)
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)
Figueira, D., Figueira, S., Schmitz, S., Schnoebelen, P.: Ackermann and primitive-recursive upper bounds with Dickson’s lemma (2010) (in preparation)
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)
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)
Finkel, A.: Reduction and covering of infinite reachability trees. Information and Computation 89(2), 144–179 (1990)
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)
Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theoretical Computer Science 256(1–2), 63–92 (2001)
Henzinger, T.A., Majumdar, R., Raskin, J.-F.: A classification of symbolic transition systems. ACM Trans. Computational Logic 6(1), 1–32 (2005)
Jančar, P.: Undecidability of bisimilarity for Petri nets and some related problems. Theoretical Computer Science 148(2), 281–301 (1995)
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)
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)
Kracht, M.: A new proof of a theorem by Ginsburg and Spanier. Dept. Linguistics, UCLA (December 2002) (manuscript)
Kruskal, J.B.: The theory of well-quasi-ordering: A frequently discovered concept. Journal of Combinatorial Theory, Series A 13(3), 297–305 (1972)
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)
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)
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)
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)
Mayr, R.: Undecidable problems in unreliable computations. Theoretical Computer Science 297(1–3), 337–354 (2003)
McAloon, K.: Petri nets and large finite sets. Theoretical Computer Science 32(1–2), 173–183 (1984)
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)
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)
Schnoebelen, P.: Verifying lossy channel systems has nonprimitive recursive complexity. Information Processing Letters 83(5), 251–261 (2002)
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)
Sifakis, J.: A unified approach for studying the properties of transitions systems. Theoretical Computer Science 18, 227–258 (1982)
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)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights 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)