Document Open Access Logo

The Parametric Complexity of Lossy Counter Machines (Track B: Automata, Logic, Semantics, and Theory of Programming)

Author Sylvain Schmitz

PDF
Thumbnail PDF

File

LIPIcs.ICALP.2019.129.pdf
  • Filesize: 0.59 MB
  • 15 pages

Document Identifiers

Author Details

Sylvain Schmitz
  • LSV, ENS Paris Saclay & CNRS, Université Paris-Saclay, France
  • IUF, France

Funding

http://projects.lsv.fr/prodaq/, http://bravas.labri.fr/

Acknowledgements

I thank Philippe Schnoebelen for his comments on a preliminary draft.

Cite AsGet BibTex

Sylvain Schmitz. The Parametric Complexity of Lossy Counter Machines (Track B: Automata, Logic, Semantics, and Theory of Programming). In 46th International Colloquium on Automata, Languages, and Programming (ICALP 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 132, pp. 129:1-129:15, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2019)
https://doi.org/10.4230/LIPIcs.ICALP.2019.129

Abstract

The reachability problem in lossy counter machines is the best-known ACKERMANN-complete problem and has been used to establish most of the ACKERMANN-hardness statements in the literature. This hides however a complexity gap when the number of counters is fixed. We close this gap and prove F_d-completeness for machines with d counters, which provides the first known uncontrived problems complete for the fast-growing complexity classes at levels 3 < d < omega. We develop for this an approach through antichain factorisations of bad sequences and analysing the length of controlled antichains.

Subject Classification

ACM Subject Classification
  • Theory of computation → Computational complexity and cryptography
Keywords
  • Counter machine
  • well-structured system
  • well-quasi-order
  • antichain
  • fast-growing complexity

Metrics

  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    0
    PDF Downloads
    0
    Metadata Views

Related Versions

References

  1. Parosh A. Abdulla, Karlis Čerāns, Bengt Jonsson, and Yih-Kuen Tsay. Algorithmic analysis of programs with well quasi-ordered domains. Information and Computation, 160(1-2):109-127, 2000. URL: http://dx.doi.org/10.1006/inco.1999.2843.
  2. Parosh A. Abdulla and Bengt Jonsson. Verifying programs with unreliable channels. Information and Computation, 127(2):91-101, 1996. URL: http://dx.doi.org/10.1006/inco.1996.0053.
  3. Sergio Abriola, Santiago Figueira, and Gabriel Senno. Linearizing well-quasi orders and bounding the length of bad sequences. tcs, 603:3-22, 2015. URL: http://dx.doi.org/10.1016/j.tcs.2015.07.012.
  4. Roberto M. Amadio and Charles Meyssonnier. On Decidability of the Control Reachability Problem in the Asynchronous π-calculus. Nordic Journal of Computing, 9(2):70-101, 2002. Google Scholar
  5. André Arnold and M. Latteux. Récursivité et cones rationnels fermés par intersection. CALCOLO, 15(4):381-394, 1978. URL: http://dx.doi.org/10.1007/BF02576519.
  6. Pierre Chambart and Philippe Schnoebelen. The Ordinal Recursive Complexity of Lossy Channel Systems. In Proceedings of LICS 2008, pages 205-216. IEEE, 2008. URL: http://dx.doi.org/10.1109/LICS.2008.47.
  7. E. Adam Cichoń and Elias Tahhan Bittar. Ordinal Recursive Bounds for Higman’s Theorem. tcs, 201(1-2):63-84, 1998. URL: http://dx.doi.org/10.1016/S0304-3975(97)00009-1.
  8. Peter Clote. On the finite containment problem for Petri nets. tcs, 43:99-105, 1986. URL: http://dx.doi.org/10.1016/0304-3975(86)90169-6.
  9. Dick H. J. de Jongh and Rohit Parikh. Well-partial orderings and hierarchies. Indagationes Mathematicae, 39(3):195-207, 1977. URL: http://dx.doi.org/10.1016/1385-7258(77)90067-1.
  10. Normann Decker and Daniel Thoma. On Freeze LTL with Ordered Attributes. In Proceedings of FoSSaCS 2016, volume 9634 of Lecture Notes in Computer Science, pages 269-284. Springer, 2016. URL: http://dx.doi.org/10.1007/978-3-662-49630-5_16.
  11. Stéphane Demri and Ranko Lazić. LTL with the freeze quantifier and register automata. ACM Transactions on Computational Logic, 10(3):16:1-16:30, 2009. URL: http://dx.doi.org/10.1145/1507244.1507246.
  12. Leonard Eugene Dickson. Finiteness of the odd perfect and primitive abundant numbers with n distinct prime factors. American Journal of Mathematics, 35(4):413-422, 1913. URL: http://dx.doi.org/10.2307/2370405.
  13. Mirna Džamonja, Sylvain Schmitz, and Philippe Schnoebelen. On Ordinal Invariants in Well Quasi Orders and Finite Antichain Orders. In Monika Seisenberger, Peter Schuster, and Andreas Weiermann, editors, Well-Quasi Orders in Computation, Logic, Language and Reasoning, Trends in Logic. Springer, 2019. To appear. URL: https://arxiv.org/abs/1711.00428.
  14. Diego Figueira, Santiago Figueira, Sylvain Schmitz, and Philippe Schnoebelen. Ackermannian and primitive-recursive bounds with Dickson’s Lemma. In Proceedings of LICS 2011, pages 269-278. IEEE, 2011. URL: http://dx.doi.org/10.1109/LICS.2011.39.
  15. Diego Figueira and Luc Segoufin. Future-looking logics on data words and trees. In Proceedings of MFCS 2009, volume 5734 of Lecture Notes in Computer Science, pages 331-343. Springer, 2009. URL: http://dx.doi.org/10.1007/978-3-642-03816-7_29.
  16. Alain Finkel and Philippe Schnoebelen. Well-Structured Transition Systems Everywhere! tcs, 256(1-2):63-92, 2001. URL: http://dx.doi.org/10.1016/S0304-3975(00)00102-X.
  17. Radu Grigore and Nikos Tzevelekos. History-Register Automata. Logical Methods in Computer Science, 12(1):7:1-7:32, 2016. URL: http://dx.doi.org/10.2168/LMCS-12(1:7)2016.
  18. Christoph Haase, Sylvain Schmitz, and Philippe Schnoebelen. The Power of Priority Channel Systems. Logical Methods in Computer Science, 10(4):4:1-4:39, 2014. URL: http://dx.doi.org/10.2168/LMCS-10(4:4)2014.
  19. Serge Haddad, Sylvain Schmitz, and Philippe Schnoebelen. The Ordinal Recursive Complexity of Timed-Arc Petri Nets, Data Nets, and Other Enriched Nets. In Proceedings of LICS 2012, pages 355-364. IEEE, 2012. URL: http://dx.doi.org/10.1109/LICS.2012.46.
  20. Matthew Hague. Senescent Ground Tree Rewriting Systems. In Proceedings of CSL-LICS 2014, pages 48:1-48:10. ACM, 2014. URL: http://dx.doi.org/10.1145/2603088.2603112.
  21. Graham Higman. Ordering by divisibility in abstract algebras. Proceedings of the London Mathematical Society, 3(2):326-336, 1952. URL: http://dx.doi.org/10.1112/plms/s3-2.1.326.
  22. Piotr Hofman and Patrick Totzke. Trace Inclusion for One-Counter Nets Revisited. tcs, 735:50-63, 2018. URL: http://dx.doi.org/10.1016/j.tcs.2017.05.009.
  23. Rodney R. Howell, Louis E. Rosier, Dung T. Huynh, and Hsu-Chun Yen. Some complexity bounds for problems concerning finite and 2-dimensional vector addition systems with states. tcs, 46:107-140, 1986. URL: http://dx.doi.org/10.1016/0304-3975(86)90026-5.
  24. Petr Jančar and Sylvain Schmitz. Bisimulation Equivalence of First-Order Grammars is ACKERMANN-Complete. In Proceedings of LICS 2019. IEEE, 2019. To appear. URL: https://arxiv.org/abs/1901.07170.
  25. Prateek Karandikar and Sylvain Schmitz. The Parametric Ordinal-Recursive Complexity of Post Embedding Problems. In Proceedings of FoSSaCS 2013, volume 7794 of Lecture Notes in Computer Science, pages 273-288. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-642-37075-5_18.
  26. Joseph B. Kruskal. The theory of well-quasi-ordering: A frequently discovered concept. Journal of Combinatorial Theory, Series A, 13(3):297-305, 1972. URL: http://dx.doi.org/10.1016/0097-3165(72)90063-5.
  27. Ranko Lazić, Joël O. Ouaknine, and James B. Worrell. Zeno, Hercules and the Hydra: Safety Metric Temporal Logic is ACKERMANN-complete. ACM Transactions on Computational Logic, 17(3), 2016. URL: http://dx.doi.org/10.1145/2874774.
  28. Ranko Lazić and Sylvain Schmitz. Non-Elementary Complexities for Branching VASS, MELL, and Extensions. ACM Transactions on Computational Logic, 16(3):20:1-20:30, 2015. URL: http://dx.doi.org/10.1145/2733375.
  29. Ranko Lazić and Sylvain Schmitz. The Complexity of Coverability in ν-Petri Nets. In Proceedings of LICS 2016, pages 467-476. ACM, 2016. URL: http://dx.doi.org/10.1145/2933575.2933593.
  30. Martin H. Löb and Stanley S. Wainer. Hierarchies of number theoretic functions, I. Archiv für Mathematische Logik und Grundlagenforschung, 13:39-51, 1970. URL: http://dx.doi.org/10.1007/BF01967649.
  31. Ernst W. Mayr and Albert R. Meyer. The Complexity of the Finite Containment Problem for Petri Nets. J. ACM, 28(3):561-576, 1981. URL: http://dx.doi.org/10.1145/322261.322271.
  32. Richard Mayr. Undecidable problems in unreliable computations. tcs, 297(1-3):337-354, 2003. URL: http://dx.doi.org/10.1016/S0304-3975(02)00646-1.
  33. Kenneth McAloon. Petri nets and large finite sets. Theor. Comput. Sci., 32(1-2):173-183, 1984. URL: http://dx.doi.org/10.1016/0304-3975(84)90029-X.
  34. Robin Milner. Operational and Algebraic Semantics of Concurrent Processes. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, chapter 19, pages 1201-1242. Elsevier, 1990. URL: http://dx.doi.org/10.1016/B978-0-444-88074-1.50024-X.
  35. Angelo Montanari, Gabriele Puppis, and Pietro Sala. Maximal Decidable Fragments of Halpern and Shoham’s Modal Logic of Intervals. In Proceedings of ICALP 2010, volume 6199 of Lecture Notes in Computer Science, pages 345-356. Springer, 2010. URL: http://dx.doi.org/10.1007/978-3-642-14162-1_29.
  36. Guillermo A. Pérez. The Fixed Initial Credit Problem for Partial-Observation Energy Games is ACK-complete. ipl, 118:91-99, 2017. URL: http://dx.doi.org/10.1016/j.ipl.2016.10.005.
  37. Fernando Rosa-Velardo. Ordinal recursive complexity of unordered data nets. Information and Computation, 254(1):41-58, 2017. URL: http://dx.doi.org/10.1016/j.ic.2017.02.002.
  38. Sylvain Schmitz. Complexity Hierarchies Beyond ELEMENTARY. ACM Transactions on Computation Theory, 8(1):3:1-3:36, 2016. URL: http://dx.doi.org/10.1145/2858784.
  39. Sylvain Schmitz. Algorithmic Complexity of Well-Quasi-Orders. Habilitation thesis, École Normale Supérieure Paris-Saclay, 2017. URL: https://tel.archives-ouvertes.fr/tel-01663266.
  40. Sylvain Schmitz and Philippe Schnoebelen. Multiply-Recursive Upper Bounds with Higman’s Lemma. In Proceedings of ICALP 2011, volume 6756 of Lecture Notes in Computer Science, pages 441-452. Springer, 2011. URL: http://dx.doi.org/10.1007/978-3-642-22012-8_35.
  41. Sylvain Schmitz and Philippe Schnoebelen. Algorithmic Aspects of WQO Theory. Lecture notes, 2012. URL: http://cel.archives-ouvertes.fr/cel-00727025.
  42. Sylvain Schmitz and Philippe Schnoebelen. The Power of Well-Structured Systems. In Proceedings of Concur 2013, volume 8052 of Lecture Notes in Computer Science, pages 5-24. Springer, 2013. URL: http://dx.doi.org/10.1007/978-3-642-40184-8_2.
  43. Philippe Schnoebelen. Verifying Lossy Channel Systems has Nonprimitive Recursive Complexity. Inf. Process. Lett., 83(5):251-261, 2002. URL: http://dx.doi.org/10.1016/S0020-0190(01)00337-4.
  44. Philippe Schnoebelen. Lossy Counter Machines Decidability Cheat Sheet. In Proceedings of RP 2010, volume 6227 of Lecture Notes in Computer Science, pages 51-75. Springer, 2010. URL: http://dx.doi.org/10.1007/978-3-642-15349-5_4.
  45. Philippe Schnoebelen. Revisiting Ackermann-Hardness for Lossy Counter Machines and Reset Petri Nets. In Proceedings of MFCS 2010, volume 6281 of Lecture Notes in Computer Science, pages 616-628. Springer, 2010. URL: http://dx.doi.org/10.1007/978-3-642-15155-2_54.
  46. Helmut Schwichtenberg and Stanley S. Wainer. Proofs and Computation. Perspectives in Logic. Cambridge University Press, 2012. Google Scholar
  47. Alasdair Urquhart. The Complexity of Decision Procedures In Relevance Logic II. Journal of Symbolic Logic, 64(4):1774-1802, 1999. URL: http://dx.doi.org/10.2307/2586811.
  48. Stanley S. Wainer. Ordinal recursion, and a refinement of the extended Grzegorczyk hierarchy. Journal of Symbolic Logic, 37(2):281-292, 1972. URL: http://dx.doi.org/10.2307/2272973.
  49. Andreas Weiermann. Complexity bounds for some finite forms of Kruskal’s Theorem. Journal of Symbolic Computation, 18(5):463-488, 1994. URL: http://dx.doi.org/10.1006/jsco.1994.1059.
Questions / Remarks / Feedback
X

Feedback for Dagstuhl Publishing


Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail
© 2023 Schloss Dagstuhl - LZI GmbH Imprint Privacy Contact