pith. sign in

arxiv: 2606.27172 · v1 · pith:MWUY5BDQnew · submitted 2026-06-25 · 💻 cs.LO · cs.FL

On Parameterized Verification Over Tree Topologies

Romain Delpy , Anca Muscholl , Gr\'egoire Sutre This is my paper

Pith reviewed 2026-06-26 02:11 UTC · model grok-4.3

classification 💻 cs.LO cs.FL
keywords parameterized verificationtree topologiesrendez-vous synchronizationsafety checkingEXPSPACEphasesfast-growing hierarchy
0
0 comments X

The pith

Safety checking for parameterized rendez-vous processes on trees is EXPSPACE-complete when the number of phases is fixed.

A machine-rendered reading of the paper's core claim, the machinery that carries it, and where it could break.

The paper establishes that parameterized verification of finite-state processes communicating by rendez-vous is undecidable on linear topologies but decidable on trees once either tree depth or the number of phases is bounded. A phase counts an alternation between upward and downward synchronizations. With a fixed phase bound the safety problem is EXPSPACE-complete even for trees of unbounded depth; when the phase bound is part of the input the complexity becomes 2EXPSPACE-complete. Bounding depth instead yields complexities located in the fast-growing hierarchy.

Core claim

Over tree topologies the safety problem for parameterized finite-state processes with rendez-vous synchronization is decidable when the number of phases is bounded, with EXPSPACE-complete complexity if the phase bound is fixed and 2EXPSPACE-complete if the bound is variable, both holding for arbitrary tree depth. Bounding the depth of the tree instead places the complexity inside the fast-growing hierarchy.

What carries the argument

The phase bound, which limits alternations between upward and downward rendez-vous synchronizations along tree edges.

If this is right

  • Safety verification remains decidable for trees of arbitrary depth once the phase count is fixed.
  • The decision procedure runs in EXPSPACE when the phase bound is constant and in 2EXPSPACE when the bound is input.
  • Depth-bounded instances have complexity governed by the fast-growing hierarchy.
  • Systems whose communication naturally stays within a small number of up-down alternations become verifiable.

Where Pith is reading between the lines

These are editorial extensions of the paper, not claims the author makes directly.

  • The phase notion may identify a broad class of hierarchical networks whose verification is feasible.
  • Comparable alternation bounds could render verification tractable on other non-linear topologies such as rings.
  • The results supply concrete resource bounds that verification tools for tree-shaped systems could target.

Load-bearing premise

Finite-state processes communicate only by rendez-vous on a tree and the chosen bound on phases or depth is enough to decide safety.

What would settle it

A concrete family of finite-state processes on trees with a fixed phase bound for which any safety-checking algorithm requires more than exponential space.

read the original abstract

Parameterized verification of finite-state processes with rendez-vous synchronization is notoriously undecidable when processes are linearly ordered. In this paper we study two kinds of bounds under which we determine the complexity of safety checking over tree topologies. When bounding the depth we obtain that the complexity is related to the fast growing hierarchy. Our second bound limits the alternations between upwards and downwards synchronizations in the tree (phases), and occurs naturally in many concrete settings. If we fix the number of phases then the complexity of safety checking is EXPSPACE complete, and if the number of phases is part of the input it is 2EXPSPACE complete (both for arbitrary depth).

Editorial analysis

A structured set of objections, weighed in public.

Desk editor's note, referee report, simulated authors' rebuttal, and a circularity audit. Tearing a paper down is the easy half of reading it; the pith above is the substance, this is the friction.

Referee Report

0 major / 2 minor

Summary. The manuscript studies parameterized verification of finite-state processes communicating via rendez-vous synchronization over tree topologies. It introduces two restrictions to recover decidability and complexity: (i) bounding tree depth, under which safety checking complexity is shown to lie in the fast-growing hierarchy, and (ii) bounding the number of phases (alternations between upward and downward synchronizations), under which safety checking is EXPSPACE-complete when the phase bound is fixed and 2EXPSPACE-complete when the phase bound is part of the input (both for arbitrary depth).

Significance. If the stated upper and lower bounds hold, the results supply precise complexity characterizations for a verification problem that is undecidable on linear topologies. The phase bound is noted to arise naturally in concrete systems, and the connection to the fast-growing hierarchy for depth bounds situates the problem within a well-studied hierarchy of computable functions, which is a notable technical contribution.

minor comments (2)
  1. The abstract states that depth-bounded complexity 'is related to the fast growing hierarchy' without indicating the precise level or the form of the reduction; a short clarifying sentence in the introduction would help readers locate the exact result.
  2. The model of rendez-vous on trees is described only at a high level in the abstract; an early section should explicitly define the transition relation and the safety property to make the complexity statements self-contained.

Simulated Author's Rebuttal

0 responses · 0 unresolved

We thank the referee for the positive summary and significance assessment of our work on parameterized verification over tree topologies. The recommendation for minor revision is noted; however, no specific major comments were provided in the report.

Circularity Check

0 steps flagged

No significant circularity detected

full rationale

The paper's complexity results for safety checking (EXPSPACE-complete for fixed phases, 2EXPSPACE-complete when phases are input, and fast-growing-hierarchy dependence under depth bounds) are derived via standard reductions in parameterized verification and automata theory on tree topologies. No self-definitional steps, fitted inputs presented as predictions, or load-bearing self-citations appear in the stated claims or assumptions; the model (finite-state processes, rendez-vous on trees, phase/depth bounds) is explicitly external and sufficient for the decidability results without reducing the central theorems to their own inputs by construction.

Axiom & Free-Parameter Ledger

0 free parameters · 2 axioms · 0 invented entities

The paper relies on standard assumptions from parameterized verification and complexity theory; no new parameters or entities introduced based on the abstract.

axioms (2)
  • domain assumption Rendez-vous synchronization model for finite-state processes on trees.
    Core modeling assumption for the verification problem.
  • standard math Standard complexity theory reductions and completeness proofs.
    Used to establish EXPSPACE and 2EXPSPACE completeness.

pith-pipeline@v0.9.1-grok · 5635 in / 1173 out tokens · 25984 ms · 2026-06-26T02:11:05.033135+00:00 · methodology

discussion (0)

Sign in with ORCID, Apple, or X to comment. Anyone can read and Pith papers without signing in.

Reference graph

Works this paper leans on

14 extracted references · 10 canonical work pages

  1. [1]

    Parameterized tree systems

    1 Parosh Aziz Abdulla, Noomene Ben Henda, Giorgio Delzanno, Frédéric Haziza, and Ahmed Rezine. Parameterized tree systems. In Kenji Suzuki, Teruo Higashino, Keiichi Yasumoto, and Khaled El-Fakih, editors,Formal Techniques for Networked and Distributed Systems - FORTE 2008, 28th IFIP WG 6.1 International Conference, Tokyo, Japan, June 10-13, 2008, Proceedi...

    work page doi:10.1007/978-3-540-68855-6 2008

  2. [2]

    4 Krzysztof R

    URL: https://doi.org/10.1007/s00446-017-0302-6,doi:10.1007/S00446-017-0302-6. 4 Krzysztof R. Apt and Dexter Kozen. Limits for automatic verification of finite-state concurrent systems.Inf. Process. Lett., 22(6):307–309, 1986.doi:10.1016/0020-0190(86)90071-2. 5 A. R. Balasubramanian. Complexity of coverability in depth-bounded processes. In Bartek Klin, Sl...

    work page doi:10.1007/s00446-017-0302-6 1986

  3. [3]

    URL:https://doi.org/10.4230/ LIPIcs.CONCUR.2022.17,doi:10.4230/LIPICS.CONCUR.2022.17. 6 A. R. Balasubramanian, Javier Esparza, and Mikhail A. Raskin. Finding cut-offs in leaderless rendez-vous protocols is easy.Log. Methods Comput. Sci., 19(4),

    work page doi:10.4230/lipics.concur.2022.17 2022

  4. [4]

    org/10.46298/lmcs-19(4:2)2023,doi:10.46298/LMCS-19(4:2)2023

    URL:https://doi. org/10.46298/lmcs-19(4:2)2023,doi:10.46298/LMCS-19(4:2)2023. 7 A.R. Balasubramanian and Franzisco Schmidt. The complexity of nested reset counter systems. In41st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2026, Lisbon, 20-23 July, 2026, LIPIcs. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,

    work page doi:10.46298/lmcs-19(4:2)2023 2023

  5. [5]

    8 Pascal Baumann, Rupak Majumdar, Ramanathan S

    To appear. 8 Pascal Baumann, Rupak Majumdar, Ramanathan S. Thinniyam, and Georg Zetzsche. The complexity of bounded context switching with dynamic thread creation. In Artur Czumaj, Anuj Dawar, and Emanuela Merelli, editors,47th International Colloquium on Automata, Languages, and Programming, ICALP 2020, Saarbrücken, Germany (Virtual Conference), July 8-1...

    2020

  6. [6]

    9 Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, and Josef Widder.Decidability of Parameterized Verification

    URL: https://doi.org/10.4230/LIPIcs.ICALP.2020.111, doi:10.4230/LIPICS.ICALP.2020.111. 9 Roderick Bloem, Swen Jacobs, Ayrat Khalimov, Igor Konnov, Sasha Rubin, Helmut Veith, and Josef Widder.Decidability of Parameterized Verification. Synthesis Lectures on Distributed Computing Theory. Morgan & Claypool Publishers,

    work page doi:10.4230/lipics.icalp.2020.111 2020

  7. [7]

    11 Marius Bozga, Javier Esparza, Radu Iosif, Joseph Sifakis, and Christoph Welzel

    URL: https://doi.org/10.1007/s10009-011-0205-y,doi:10.1007/S10009-011-0205-Y. 11 Marius Bozga, Javier Esparza, Radu Iosif, Joseph Sifakis, and Christoph Welzel. Structural invariants for the verification of systems with parameterized architectures. In Armin Biere and David Parker, editors,Tools and Algorithms for the Construction and Analysis of Systems -...

    work page doi:10.1007/s10009-011-0205-y 2020

  8. [8]

    17 Allen E

    URL: https://arxiv.org/abs/1504.06355,arXiv:1504.06355. 17 Allen E. Emerson and Kedar S. Namjoshi. On reasoning about rings.International Journal of Foundations of Computer Science, 14(04):527–549,

    Pith/arXiv arXiv

  9. [9]

    Keeping a crowd safe: On the complexity of parameterized verification (invited talk)

    18 Javier Esparza. Keeping a crowd safe: On the complexity of parameterized verification (invited talk). In Ernst W. Mayr and Natacha Portier, editors,31st International Symposium on Theoretical Aspects of Computer Science, STACS 2014, Lyon, France, March 5-8, 2014, LIPIcs, pages 1–10. Schloss Dagstuhl - Leibniz-Zentrum für Informatik,

    2014

  10. [10]

    19 Steven M

    URL:https: //doi.org/10.4230/LIPIcs.STACS.2014.1,doi:10.4230/LIPICS.STACS.2014.1. 19 Steven M. German and Prasad A. Sistla. Reasoning about systems with many processes. J. ACM, 39(3):675–735,

    work page doi:10.4230/lipics.stacs.2014.1 2014

  11. [11]

    Phase-bounded broadcast net- works over topologies of communication

    20 Lucie Guillou, Arnaud Sangnier, and Nathalie Sznajder. Phase-bounded broadcast net- works over topologies of communication. In Rupak Majumdar and Alexandra Silva, ed- itors,35th International Conference on Concurrency Theory, CONCUR 2024, Calgary, Canada, September 9-13, 2024, LIPIcs, pages 26:1–26:16. Schloss Dagstuhl - Leibniz- Zentrum für Informatik,

    2024

  12. [12]

    21 Yonit Kesten, Oded Maler, Monica Marcus, Amir Pnueli, and Elad Shahar

    URL: https://doi.org/10.4230/LIPIcs.CONCUR.2024.26, doi:10.4230/LIPICS.CONCUR.2024.26. 21 Yonit Kesten, Oded Maler, Monica Marcus, Amir Pnueli, and Elad Shahar. Symbolic model checking with rich assertional languages.Theor. Comput. Sci., 256(1-2):93–112,

    work page doi:10.4230/lipics.concur.2024.26 2024

  13. [13]

    22 Marvin Künnemann, Filip Mazowiecki, Lia Schütze, Henry Sinclair-Banks, and Karol Wegrzycki

    doi:10.1016/S0304-3975(00)00103-1. 22 Marvin Künnemann, Filip Mazowiecki, Lia Schütze, Henry Sinclair-Banks, and Karol Wegrzycki. Coverability in VASS revisited: Improving Rackoff’s bounds to obtain condi- tional optimality.J. ACM, 72(5):33:1–33:27, 2025.doi:10.1145/3762178. 23 Jérôme Leroux. The reachability problem for Petri nets is not primitive recurs...

    work page doi:10.1016/s0304-3975(00)00103-1 2025

  14. [14]

    25 Richard J

    doi:10.1109/LICS.2019.8785796. 25 Richard J. Lipton. The reachability problem requires exponential space. Technical Report 62, Yale University,

    work page doi:10.1109/lics.2019.8785796 2019