Document Open Access Logo

Branching in Well-Structured Transition Systems (Invited Talk)

Author Sylvain Schmitz

PDF
Thumbnail PDF

File

LIPIcs.CSL.2021.3.pdf
  • Filesize: 295 kB
  • 3 pages

Document Identifiers

Author Details

Sylvain Schmitz
  • Université de Paris, CNRS, IRIF, France
  • IUF, Paris, France

Funding

http://bravas.labri.fr/

Acknowledgements

The presentation is based on joint work with Ranko Lazić.

Cite AsGet BibTex

Sylvain Schmitz. Branching in Well-Structured Transition Systems (Invited Talk). In 29th EACSL Annual Conference on Computer Science Logic (CSL 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 183, pp. 3:1-3:3, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)
https://doi.org/10.4230/LIPIcs.CSL.2021.3

Abstract

The framework of well-structured transition systems has been highly successful in providing generic algorithms to show the decidability of verification problems for infinite-state systems. In some of these applications, the executions in the system at hand are actually trees, and need to be "lifted" to executions over sets of configurations in order to fit in the framework. The downside of this approach is that we might lose precision when analysing the computational complexity of the algorithms, compared to reasoning over branching executions.

Subject Classification

ACM Subject Classification
  • Theory of computation → Computational complexity and cryptography
  • Theory of computation → Program reasoning
  • Theory of computation → Verification by model checking
Keywords
  • fast-growing complexity
  • well-structured transition system

Metrics

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

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: https://doi.org/10.1006/inco.1999.2843.
  2. Sergio Abriola, Santiago Figueira, and Gabriel Senno. Linearizing well-quasi orders and bounding the length of bad sequences. Theoretical Computer Science, 603:3-22, 2015. URL: https://doi.org/10.1016/j.tcs.2015.07.012.
  3. A. R. Balasubramanian. Complexity of controlled bad sequences over finite sets of ℕ^d. In Proceedings of LICS 2020. ACM, 2020. URL: https://doi.org/10.1145/3373718.3394753.
  4. 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: https://doi.org/10.1007/978-3-662-49630-5_16.
  5. Stéphane Demri and Ranko Lazić. LTL with the freeze quantifier and register automata. ACM Transactions on Computational Logic, 10(3):16, 2009. URL: https://doi.org/10.1145/1507244.1507246.
  6. Diego Figueira. Alternating register automata on finite words and trees. Logical Methods in Computer Science, 8(1), 2012. URL: https://doi.org/10.2168/LMCS-8(1:22)2012.
  7. 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: https://doi.org/10.1109/LICS.2011.39.
  8. Diego Figueira and Luc Segoufin. Future-looking logics on data words and trees. In Proceedings of MFCS '09, volume 5734 of Lecture Notes in Computer Science, pages 331-343. Springer, 2009. URL: https://doi.org/10.1007/978-3-642-03816-7_29.
  9. Diego Figueira and Luc Segoufin. Bottom-up automata on data trees and vertical XPath. Logical Methods in Computer Science, 13(4), 2017. URL: https://doi.org/10.23638/LMCS-13(4:5)2017.
  10. Alain Finkel and Philippe Schnoebelen. Well-structured transition systems everywhere! Theoretical Computer Science, 256(1-2):63-92, 2001. URL: https://doi.org/10.1016/S0304-3975(00)00102-X.
  11. Christoph Haase, Sylvain Schmitz, and Philippe Schnoebelen. The power of priority channel systems. Logical Methods in Computer Science, 10(4):4:1-4:39, December 2014. URL: https://doi.org/10.2168/LMCS-10(4:4)2014.
  12. 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 Press, 2012. URL: https://doi.org/10.1109/LICS.2012.46.
  13. Petr Jančar. A note on well quasi-orderings for powersets. Information Processing Letters, 72(5-6):155-160, 1999. URL: https://doi.org/10.1016/S0020-0190(99)00149-0.
  14. Marcin Jurdziński and Ranko Lazić. Alternating automata on data trees and XPath satisfiability. ACM Transactions on Computational Logic, 12(3), 2011. URL: https://doi.org/10.1145/1929954.1929956.
  15. 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: https://doi.org/10.1007/978-3-642-37075-5_18.
  16. 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: https://doi.org/10.1016/0097-3165(72)90063-5.
  17. 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: https://doi.org/10.1145/2733375.
  18. Ranko Lazić and Sylvain Schmitz. The ideal view on Rackoff’s coverability technique. Information and Computation, 2020. In press. URL: https://doi.org/10.1016/j.ic.2020.104582.
  19. Alberto Marcone. Fine analysis of the quasi-orderings on the power set. Order, 18(4):339-347, 2001. URL: https://doi.org/10.1023/A:1013952225669.
  20. Jacques Riche and Robert K. Meyer. Kripke, Belnap, Urquhart and relevant decidability & complexity. In Proceedings of CSL 1998, volume 1584 of Lecture Notes in Computer Science, pages 224-240. Springer, 1999. URL: https://doi.org/10.1007/10703163_16.
  21. Fernando Rosa-Velardo. Ordinal recursive complexity of unordered data nets. Information and Computation, 254(1):41-58, 2017. URL: https://doi.org/10.1016/j.ic.2017.02.002.
  22. Sylvain Schmitz. Algorithmic Complexity of Well-Quasi-Orders. Habilitation thesis, École Normale Supérieure Paris-Saclay, 2017. URL: http://tel.archives-ouvertes.fr/tel-01663266.
  23. Sylvain Schmitz. The parametric complexity of lossy counter machines. In Proceedings of ICALP 2019, volume 132 of Leibniz International Proceedings in Informatics, pages 129:1-129:15. LZI, 2019. URL: https://doi.org/10.4230/LIPIcs.ICALP.2019.129.
  24. 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: https://doi.org/10.1007/978-3-642-22012-8_35.
  25. Alasdair Urquhart. The complexity of decision procedures in relevance logic II. Journal of Symbolic Logic, 64(4):1774-1802, 1999. URL: https://doi.org/10.2307/2586811.
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-2024 Schloss Dagstuhl – LZI GmbH Imprint Privacy Contact