Complexity of Coverability in Depth-Bounded Processes

Abstract

We consider the class of depth-bounded processes in $\pi$-calculus. These processes are the most expressive fragment of $\pi$-calculus, for which verification problems are known to be decidable. The decidability of the coverability problem for this class has been achieved by means of well-quasi orders. (Meyer, IFIP TCS 2008; Wies, Zufferey and Henzinger, FoSSaCS 2010). However, the precise complexity of this problem is not known so far, with only a known EXPSPACE-lower bound. In this paper, we prove that coverability for depth-bounded processes is $\mathbf{F}{\epsilon_0}$-complete, where $\mathbf{F}{\epsilon_0}$ is a class in the fast-growing hierarchy of complexity classes. This solves an open problem mentioned by Haase, Schmitz, and Schnoebelen (LMCS, Vol 10, Issue 4) and also addresses a question raised by Wies, Zufferey and Henzinger (FoSSaCS 2010).

Bio

A. R. Balasubramanian is a Ph.D. student at the Technical University of Munich under Prof. Javier Esparza. His research interests include parameterized systems, well-quasi orders, and verification of infinite-state systems.
Find his website here.