On parameterized verification over tree topologies
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 2-EXPSPACE-complete (both for arbitrary depth).