Sciweavers

Share
CHARME
2001
Springer

Net Reductions for LTL Model-Checking

12 years 4 months ago
Net Reductions for LTL Model-Checking
We present a set of reduction rules for LTL model-checking of 1-safe Petri nets. Our reduction techniques are of two kinds: (1) Linear programming techniques which are based on well-known Petri net techniques like invariants and implicit places, and (2) local net reductions. We show that the conditions for the application of some local net reductions can be weakened if one is interested in LTL model-checking using the approach of [EH00,EH01]. Finally, we present a number of experimental results and show that the model-checking time of a net system can be significantly decreased if it has been preprocessed with our reduction techniques.
Javier Esparza, Claus Schröter
Added 28 Jul 2010
Updated 28 Jul 2010
Type Conference
Year 2001
Where CHARME
Authors Javier Esparza, Claus Schröter
Comments (0)
books