On the complexity of the linear-time µ-calculus for petri nets

Abstract

We study the complexity of model-checking Petri Nets w.r.t, the propositional linear-time µ-calculus. Esparza has shown in [5] that it is decidable, but the space complexity of his algorithm is exponential in the size of the system and double exponential in the size of the formula. In this paper we show that the complexity in the size of the formula can be reduced to polynomial space. We also prove that this is the best one can do. We also show that for the subclass of BPPs the problem has already the same complexity as for arbitrary nets. Furthermore we obtain the same results for the linear time temporal logic LTL, which is strictly less expressive than the linear-time µ-calculus.