In: Azéma, P.; Balbo, G.: Lecture Notes in Computer Science, Vol. 1248: 18th International Conference on Application and Theory of Petri Nets, Toulouse, France, June 1997, pages 102-116. Berlin, Germany: Springer-Verlag, June 1997.
Abstract: We study the complexity of model-checking Petri Nets w.r.t. the propositional linear-time µ-calculus. Esparza has shown 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.