Abstract
We study the complexity of model-checking Petri Nets w.r.t. the prepositional 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.
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
P. Abdulla and B. Jonsson. Verifying programs with unreliable channels. Information and Computation, 127:91–101, 1996.
I. Borosh and L. Treybis. Bounds on positive integral solutions of linear Diophantine equations. Proc. Amer. Math Soc., 55:299–304, 1976.
Søren Christensen. Decidability and Decomposition in Process Algebras. PhD thesis, University of Edinburgh, 1993.
M. Dam. Fixed points of Büchi automata. In R. Shyamasundar, editor, Foundations of Software Technology and Theoretical Computer Science, volume 652 of Lecture Notes in Computer Science, pages 39–50. Springer-Verlag, 1992.
J. Esparza. On the decidability of model checking for several mu-calculi and petri nets. In CAAP: Colloquium on Trees in Algebra and Programming. LNCS 787, Springer-Verlag, 1994.
J. Esparza. More infinite results. In Steffen and Margaria, editors, Infinity: International Workshop on Verification of Infinite State Systems, Tech. Report MIP-9614, Univ. Passau, 1996.
J. Esparza and A. Kiehn. On the model checking problem for branching time logics and basic parallel processes. In CAV'95. LNCS 939, 1995.
R. Lipton. The reachability problem requires exponential space. Technical Report 62, Department of Computer Science, Yale University, January 1976.
Faron Moller. Infinite results. In CONCUR: 7th International Conference on Concurrency Theory, volume 1119. LNCS, Springer-Verlag, 1996.
D. Park. Concurrency and Automata on Infinite Sequences. In 5th GI-Conference on Theoretical Computer Science. 1981. LNCS 104.
A. Pnueli. The Temporal Logic of Programs. In FOCS'77. IEEE, 1977.
Charles Rackoff. The covering and boundedness problems for vector addition systems. Theoretical Computer Science, 6(2):223–231, April 1978.
Louis E. Rosier and Hsu-Chun Yen. A multiparameter analysis of the boundedness problem for vector addition systems. Journal of Computer and System Sciences, 32(1):105–135, February 1986.
S. Safra. On the complexity of ω-automata. In 29th Annual Symposium on Foundations of Computer Science, pages 319–327, White Plains, New York, 24–26 October 1988. IEEE.
W. J. Savitch. Relational between nondeterministic and deterministic tape complexity. Journal of Computer and System Sciences, 4:177–192, 1970.
M. Y. Vardi. A temporal fixpoint calculus. In ACM-SIGPLAN ACM-SIGACT, editor, Conference Record of the 15th Annual ACM Symposium on Principels of Programming Languages (POPL '88), pages 250–259, San Diego, CA, USA, January 1988. ACM Press.
M. Y. Vardi. An automata-theoretic approach to linear temporal logic (banff'94). Lecture Notes in Computer Science, 1043, 1996.
Moshe Y. Vardi and Pierre Wolper. Reasoning about infinite computations. Information and Computation, 115(1):1–37, 15 November 1994.
P. Wolper. Temporal Logic Can Be More Expressive. Information and Control, 56, 1983.
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 1997 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Habermehl, P. (1997). On the complexity of the linear-time μ-calculus for Petri Nets. In: Azéma, P., Balbo, G. (eds) Application and Theory of Petri Nets 1997. ICATPN 1997. Lecture Notes in Computer Science, vol 1248. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-63139-9_32
Download citation
DOI: https://doi.org/10.1007/3-540-63139-9_32
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-63139-2
Online ISBN: 978-3-540-69187-7
eBook Packages: Springer Book Archive