The Complex(ity) Landscape of Checking Infinite Descent
summary
Two new decision procedures for Infinite Descent appear: an automata-based variant that encodes sloped relations so the trace automaton is exponential only in vertex width, and a relation-based approach that adapts Floyd–Warshall with an order-reduced optimization that removes an exponential factor in the vertex width. Parameterized analysis shows a tradeoff between number of vertices and vertex width; a C++ implementation in the Cyclist prover benchmarks real-world and worst-case suites and finds relation-based methods dominate on practical and width-varying cases, while automata methods help in some positive/negative instances.
AI-written summary · about
chapters (13)
- 0:00Infinite descent in cyclic proofs
- 1:54What is infinite descent
- 4:24Sloped graphs for descent
- 6:49Algorithms for checking descent
- 7:33Automaton-based algorithm
- 8:56Relation-based complexity
- 10:40Optimizing relation-based
- 11:03New automaton with sloped relations
- 12:07Order-reduced Floyd-Warshall
- 13:34Complexity tradeoffs
- 13:54Experimental evaluation
- 15:19Summary and conclusions
- 15:41Q&A
related talks
16mCertified Decision Procedures for Width-Independent Bitvector Predicates
01h 02mTheory and Control
18mLanguages with Decidable Learning: A Meta-theorem
17mAn Algebra of Sequential Decision Problems
26mOn the Complexity of Bidirected Interleaved Dyck-Reachability
14mAdequacy for Algebraic Effects Revisited
17mA Better Approximation for Interleaved Dyck Reachability
21mWeighted Context-Free-Language Ordered Binary Decision Diagrams