Sylvain Schmitz and Philippe Schnoebelen

• Area: LoCo
• Level: A
• Week: 2
• Time: 09:00 – 10:30
• Room: D1.01

Abstract

Well-quasi-orderings (wqos) are a fundamental tool in logic and computer science. They provide termination arguments in a large number of decidability (or finiteness, regularity, …) results. In constraint solving, automated deduction, program analysis, and many more fields, wqos usually appear under the guise of specific tools, like Dickson’s Lemma (for tuples of integers), Higman’s Lemma (for words and their subwords), Kruskal’s Tree Theorem and its variants (for finite trees with embeddings), and recently the Robertson-Seymour Theorem (for graphs and their minors). What is not very well known is that wqo-based proofs have an algorithmic content.

The purpose of this course is to provide an introduction to the algorithmic aspects of wqos: to present generic algorithms working on large classes of problems, to introduce the techniques used to prove complexity upper bounds and lower bounds, to explain the use of wqo ideals in algorithms, and provide several applications in logics (e.g. data logics, relevance logic), verification (prominently for well-structured transition systems), and formal languages. Because wqos are in such wide use, we believe this topic to be of relevance to a broad community with interests in complexity theory and decision procedures for logical theories.

Planned Content

1. well-quasi-orders (wqos): examples and characterisations
2. applications of wqos: well-structured transition systems (WSTS), termination proofs, relevance logic
3. complexity: fast-growing complexity, Hardy computations, length function theorems
4. ideals: effective representations and algorithmics
5. applications of ideals: complete WSTS, coverability algorithms

Resources

• lecture notes (100+ pages)
• slides day 1: Basics of wqo theory
• slides day 2: Algorithmic applications of wqos
• slides day 4: Ideals of wqos and their algorithms
• student survey

Additional References

• Blondin, M., Finkel, A., and McKenzie, P., 2014. Handling infinitely branching WSTS.
  In ICALP 2014, volume 8573 of Lecture Notes in Computer Science, pages 13–25.
  doi:10.1007/978-3-662-43951-7_2.
• Figueira, D., 2012. Alternating register automata on finite words and trees. Logical Methods in Computer Science, 8(1):22. doi:10.2168/LMCS-8(1:22)2012.
• Finkel, A. and Schnoebelen, Ph., 2001. Well-structured transition systems everywhere!
  Theoretical Computer Science, 256(1–2):63–92. doi:10.1016/S0304-3975(00)00102-X.
• Lazić, R. and Schmitz, S., 2015. The ideal view on Rackoff’s coverability technique. In
  RP 2015, volume 9328 of Lecture Notes in Computer Science, pages 1–13. Springer.
  doi:10.1007/978-3-319-24537-9_8.
• Milner, E.C., 1985. Basic WQO- and BQO-theory. In Rival, I., editor, Graphs and Order.
  The Role of Graphs in the Theory of Ordered Sets and Its Applications, pages 487–502. doi:10.1007/978-94-009-5315-4_14.
• Podelski, A. and Rybalchenko, A., 2004. Transition invariants. In LICS 2004, pages
  32–41. IEEE. doi:10.1109/LICS.2004.1319598.
• Schmitz, S., 2016. Complexity hierarchies beyond Elementary. ACM Transactions on
  Computation Theory, 8(1):1–36. doi:10.1145/2858784.
• Schmitz, S. and Schnoebelen, Ph., 2011. Multiply-recursive upper bounds with Higman’s Lemma. In ICALP 2011, volume 6756 of Lecture Notes in Computer Science, pages 441–452. Springer. doi:10.1007/978-3-642-22012-8_35.
• Schnoebelen, Ph., 2010a. Revisiting Ackermann-hardness for lossy counter machines
  and reset Petri nets. In MFCS 2010, volume 6281 of Lecture Notes in Computer Science, pages 616–628. Springer. doi:10.1007/978-3-642-15155-2_54.
• Urquhart, A., 1999. The complexity of decision procedures in relevance logic II. Journal
  of Symbolic Logic, 64(4):1774–1802. doi:10.2307/2586811.
• Wainer, S.S., 1972. Ordinal recursion, and a refinement of the extended Grzegorczyk
  hierarchy. Journal of Symbolic Logic, 37(2):281–292. doi:10.2307/2272973.
• Weiermann, A., 1994. Complexity bounds for some finite forms of Kruskal’s Theorem.
  Journal of Symbolic Computation, 18(5):463–488. doi:10.1006/jsco.1994.1059.
• Zetzsche, G., 2015. An approach to computing downward closures. In ICALP 2015,
  volume 9135 of Lecture Notes in Computer Science, pages 440–451. Springer. doi:10.1007/978-3-662-47666-6_35.