LTL Model Checking for Modular Petri Nets

13 years 9 months ago
LTL Model Checking for Modular Petri Nets
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.
Timo Latvala, Marko Mäkelä
Added 30 Jun 2010
Updated 30 Jun 2010
Type Conference
Year 2004
Where APN
Authors Timo Latvala, Marko Mäkelä
Comments (0)