一句话：将 CFL 可达性推广到几乎可交换迁移系统，证明其同态像半线性并给出多项式时间 Presburger 构造。
CFL 可达性常用于程序分析，但已有基于 Parikh 定理的方法仅适用于迁移关系可交换的无限状态系统。本文提出几乎可交换迁移系统，由有限状态控制与可交换分量组成，整体一般不可交换。作者将 Parikh 定理推广到该情形，证明上下文无关语言在到几乎可交换幺半群的同态下的像仍是半线性的，并给出多项式时间构造其 Presburger 算术公式的算法。由此得到求解几乎可交换迁移系统上 CFL 可达性的一般框架，并给出若干实例。最后还研究了几乎可交换幺半群的封闭性质，以支持模块化组合而不离开该类。
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.
@article{PimpalkhareKR26,
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}
}