Bounded Treewidth, Multiple Context-Free Grammars, and Downward Closures
summary
Proves that the word languages of MSO-definable bounded-stw = multiple context-free languages by translating bounded-treewidth run graphs to tree automata and then to MCFGs, and gives a Ramsey-based acceleration + annotated projection construction that yields an optimal downward-closure algorithm (succinct automata via fixed-point embeddings and accelerated productions). Shows downward closures are computable efficiently enough that safety for systems with dynamic spawning of bounded-stw processes matches the complexity of sequential recursive-process verification.
AI-written summary · about
chapters (11)
- 0:00Bounded treewidth systems
- 1:48Downward closures importance
- 3:31Bounded tree width examples
- 7:02Multiple context-free grammars
- 9:10Equivalence of models
- 10:14Downward closures for MCGGs
- 13:51Acceleratable components
- 16:39Derivation tree acceleration
- 19:48Ramsey construction succinctness
- 21:55Contributions and results
- 22:45Q&A on parameters
related talks
15mRecursive State Machine Guided Graph Folding for Context-Free Language Reachability
31mFibred Categories of Tree Automata
19mContext-Free Language Reachability via Skewed Tabulation
15mDetecting and explaining (in-)equivalence of context-free grammars
18mLanguages with Decidable Learning: A Meta-theorem
01h 02mTheory and Control
14mFast Client-Driven CFL-Reachability via Regularization-Based Graph Simplification
16mAutomatically Deriving Control-Flow Graph Generators from Operational Semantics