Abstract
Broadcast networks are a formalism of distributed computation that allow one to model networks of identical nodes communicating through message broadcasts over a communication topology that does not change over the course of executions. The parameterized verification problem for these networks amounts to proving correctness of a property for any number of nodes, and on all executions. Dually speaking, this problem asks for the existence of an execution of the broadcast network that violates a given property. One specific instance of parameterized verification is the coverability problem which asks whether there is an execution of the network in which some node reaches a given state of the broadcast protocol. This problem was proven to be undecidable by Delzanno, Sangnier and Zavattaro (CONCUR 2010). In the same paper, the authors also prove that, if we additionally assume that the underlying communication topology has a bound on the longest path, then the coverability problem becomes decidable.
In this paper, we provide complexity results for the above problem and prove that the coverability problem for boundedpath topologies is 𝐅_ε₀complete, where 𝐅_ε₀ is a class in the fastgrowing hierarchy of complexity classes. This solves an open problem of Hasse, Schmitz and Schnoebelen (LMCS, Vol 10, Issue 4).
BibTeX  Entry
@InProceedings{balasubramanian:LIPIcs.FSTTCS.2021.35,
author = {Balasubramanian, A. R.},
title = {{Complexity of Coverability in Bounded Path Broadcast Networks}},
booktitle = {41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021)},
pages = {35:135:16},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {9783959772150},
ISSN = {18688969},
year = {2021},
volume = {213},
editor = {Boja\'{n}czy, Miko{\l}aj and Chekuri, Chandra},
publisher = {Schloss Dagstuhl  LeibnizZentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2021/15546},
URN = {urn:nbn:de:0030drops155466},
doi = {10.4230/LIPIcs.FSTTCS.2021.35},
annote = {Keywords: Parameterized verification, Bounded path networks, Fastgrowing complexity classes}
}
Keywords: 

Parameterized verification, Bounded path networks, Fastgrowing complexity classes 
Collection: 

41st IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science (FSTTCS 2021) 
Issue Date: 

2021 
Date of publication: 

29.11.2021 