POPL 2026
Sun 11 - Sat 17 January 2026 Rennes, France
Wed 14 Jan 2026 16:35 - 17:00 at Dortoirs - Decision Procedures Chair(s): Andrés Goens

We extend the scope of context-free-language (CFL) reachability to a new class of infinite-state systems. Parikh's Theorem is a useful tool for solving CFL-reachability problems for transition systems that consist of commuting transition relations. It implies that the image of a context-free language under a homomorphism into a commutative monoid is semi-linear, and that there is a linear-time algorithm for constructing a Presburger arithmetic formula that represents it. However, for many transition systems of interest, transitions do not commute.

In this paper, we introduce almost-commuting transition systems, which pair finite-state control with commutative components, but which are in general not commutative. We extend Parikh's theorem to show that the image of a context-free language under a homomorphism into an \textit{almost-commuting monoid is semi-linear and that there is a polynomial-time algorithm for constructing a Presburger arithmetic formula that represents it. This result yields a general framework for solving CFL-reachability problems over \textit{almost-commuting transition systems}. We describe several examples of systems within this class. Finally, we examine closure properties of almost-commuting monoids that can be used to modularly compose almost-commuting transition systems while remaining in the class.

Wed 14 Jan

Displayed time zone: Brussels, Copenhagen, Madrid, Paris change

16:10 - 17:25
Decision ProceduresPOPL at Dortoirs
Chair(s): Andrés Goens TU Darmstadt
16:10
25m
Talk
Characterizing Sets of Theories That Can Be Disjointly Combined
POPL
Benjamin Przybocki Carnegie Mellon University, Guilherme V. Toledo Bar-Ilan University, Yoni Zohar
DOI
16:35
25m
Talk
Context-Free-Language Reachability for Almost-Commuting Transition Systems
POPL
Nikhil Pimpalkhare Princeton University, Zachary Kincaid Princeton University, Thomas Reps University of Wisconsin-Madison
DOI
17:00
25m
Talk
Determination Problems for Orbit Closures and Matrix Groups
POPL
Rida Ait El Manssour University of Oxford, George Kenison Liverpool John Moores University, Mahsa Shirmohammadi CNRS, Anton Varonka TU Wien, James Worrell University of Oxford
DOI