On Parameterized Verification Over Tree Topologies

Romain Delpy; Anca Muscholl; Grégoire Sutre

On Parameterized Verification Over Tree Topologies

计算机科学中的逻辑 2026-06-25 v1 形式语言与自动机理论

作者: Romain Delpy , Anca Muscholl , Grégoire Sutre

摘要

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).

引用

@article{arxiv.2606.27172,
  title  = {On Parameterized Verification Over Tree Topologies},
  author = {Romain Delpy and Anca Muscholl and Grégoire Sutre},
  journal= {arXiv preprint arXiv:2606.27172},
  year   = {2026}
}

备注

Full version of the paper with the same title and authors to appear in the proceedings of CONCUR 2026