A Robust Theory of Series Parallel Graphs
Rajeev Alur, Caleb Stanford, Christopher Watson
Abstract
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 𝑛 states and 𝑘 counting complexity to a deterministic automaton with 2 𝑛 2 states and 𝑘𝑛 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.
Ask about this paper
Your agent reads all of it.
Lune indexed this paper to the last equation, along with the top-tier papers that cite it. Ask a question and the answer quotes them.
Your agent calls
Luneget_paper_fulltext
Free to start. No credit card required.
Terminal
Install the CLIlune papers fulltext da613232-4c1f-49e6-866f-75faf50a7056Cited by top-tier papers1
Ask how each one uses itBuilds on1
Related papers
- Ramsey Quantifiers over Automatic Structures: Complexity and Applications to VerificationPascal Bergsträßer, Moses Ganardi, Anthony W. Lin, Georg ZetzscheLICS 2022 · 3 citations
- Low Rank MSOMikolaj Bojanczyk, Michal Pilipczuk, Wojciech Przybyszewski, Marek Sokolowski et al.LICS 2026
- Stream TypesJoseph W. Cutler, Christopher Watson, Emeka Nkurumeh, Phillip Hilliard et al.PLDI 2024 · 7 citations
- Reasoning About Data Trees Using CHCsMarco Faella, Gennaro ParlatoCAV 2022 · 6 citations
- Functional Meaning for Parallel StreamingNick Rioux, Steve ZdancewicPLDI 2025 · 1 citation
