Context-Free-Language Reachability for Almost-Commuting Transition Systems

on YouTube ↗23m

" summary

Proves that the Parikh-image machinery extends to an almost-commuting monoid, giving a polynomial-time procedure that produces a Presburger formula describing the semi-linear image of an unfolded context-free language; applies that formula to compute CFL-reachability for a new class of infinite-state transition systems. The method unfolds the grammar (blowup bounded by a finite decomposition), takes the Parikh image, and returns sound, computable reachability summaries used as a practical backend for abstraction-based analyses.

AI-written summary · about

" chapters (12)

1. 0:00Interprocedural program analysis
2. 1:07Context-free languages
3. 3:34Reachability relations
4. 7:27Transition systems and monoids
5. 8:51Limitations of commutative systems
6. 9:55Almost commuting systems
7. 12:24Unfolding languages for analysis
8. 13:29Equivalence of program traces
9. 15:39Reachability from prerick images
10. 17:46Analyzability of systems
11. 18:28Applications and future
12. 18:53Q&A