尚未生成 AI 速览(可能缺少 API key 或等待下次运行补跑)。
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 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 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.
DOI 原文 ·
@article{paperbot3915,
title = {Context-Free-Language Reachability for Almost-Commuting Transition Systems},
author = {Nikhil Pimpalkhare and Zachary Kincaid and Thomas Reps},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {POPL},
year = {2026},
doi = {10.1145/3776686}
}