For the most recent entries see the Petri Nets Newsletter.

LTL Model Checking for Modular Petri Nets.

Latvala, Timo; Mäkelä, Marko

In: Proceedings of Applications and Theory of Petri Nets 2004: 25th International Conference, ICATPN 2004, Bologna, Italy, June 21-25, 2004, pages 298-311. Volume 3099 of Lecture Notes in Computer Science / Cortadella, Reisig (Eds.) --- Springer-Verlag, September 2004.

Abstract: We consider the problem of model checking modular Petri nets for the linear time logic LTL-X. An algorithm is presented which can use the synchronisation graph from modular analysis as presented by Christensen and Petrucci and perform LTL-X model checking. We have implemented our method in the reachability analyser Maria and performed experiments. As is the case for modular analysis in general, in some cases the gains can be considerable while in other cases the gain is negligible.


Do you need a refined search? Try our search engine which allows complex field-based queries.

Back to the Petri Nets Bibliography