*For the most recent entries see the
Petri Nets Newsletter.*

## On the Complexity of the Linear-Time µ-Calculus for Petri Nets.

Habermehl, Peter
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.

*Do you need a refined search? Try our search engine
which allows complex field-based queries.*
*Back to the Petri Nets Bibliography*