一句话：提出同步串并联图，证明其确定性/非确定性自动机等价于MSO与分级μ演算，并给出确定化与判定过程。
论文引入由顺序与并行复合构造的带标签有向无环图，并研究其上的自动机与逻辑。核心是同步串并联图（SSPG）：并行复合从新源点向汇点引入同步边，使信息传递成为可能，从而实现确定化。作者证明确定性/非确定性接受器表达能力相同，可由一元二阶逻辑（MSO）与分级 μ 演算刻画；语言类对复合封闭，成员、空性与包含问题可判定。SSPG 支持有序带秩与无序不带秩并行，后者带来按状态类型计数的“计数复杂度”。确定化将 n 状态、k 计数复杂度的 NFA 转为 2^{n^2} 状态、k^n 计数复杂度的 DFA，界均紧；非确定性自动机的计数复杂度可限制为 2 而不损失表达力。
Motivated by distributed data processing applications, we introduce a class of labeled directed acyclic graphs constructed using sequential and parallel composition operations, and study automata and logics over them. We show that deterministic and non-deterministic acceptors over such graphs have the same expressive power, which can be equivalently characterized by Monadic Second-Order logic and the graded µ-calculus. We establish closure under composition operations and decision procedures for membership, emptiness, and inclusion. A key feature of our graphs, called synchronized series-parallel graphs (SSPG), is that parallel composition introduces a synchronization edge from the newly introduced source vertex to the sink. The transfer of information enabled by such edges is crucial to the determinization construction, which would not be possible for the traditional definition of series-parallel graphs. SSPGs allow both ordered ranked parallelism and unordered unranked parallelism. The latter feature means that in the corresponding automata, the transition function needs to account for an arbitrary number of predecessors by counting each type of state only up to a specified constant, thus leading to a notion of counting complexity that is distinct from the classical notion of state complexity. The determinization construction translates a nondeterministic automaton with n states and k counting complexity to a deterministic automaton with 2 n 2 states and kn counting complexity, and both these bounds are shown to be tight. Furthermore, for nondeterministic automata a bound of 2 on counting complexity suffices without loss of expressiveness.
@article{paperbot2059,
title = {A Robust Theory of Series Parallel Graphs},
author = {Rajeev Alur and Caleb Stanford and Christopher Watson},
journal = {Proceedings of the ACM on Programming Languages},
volume = {7},
number = {POPL},
year = {2023},
doi = {10.1145/3571230}
}