Abstract
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.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
G. Berthelot. Checking properties of nets using transformations. In Advances in Petri Nets, LNCS 222, pages 19–40. Springer-Verlag, 1985.
J. C. Corbett. Evaluating Deadlock Detection Methods, 1994.
J. M. Colom and M. Silva. Improving the Linearly Based Characterization of P/T Nets. In Advances in Petri Nets, LNCS 483, pages 113–145. Springer-Verlag, 1990.
J. Desel and J. Esparza. Free Choice Petri Nets. Cambridge University Press, 1995.
J. Esparza and K. Heljanko. A new Unfolding Approach to LTL Model Checking. In ICALP’00, LNCS 1853, pages 475–486. Springer-Verlag, 2000.
J. Esparza and K. Heljanko. Implementing LTL Model Checking with Net Unfoldings. Accepted paper for SPIN’01, 2001.
J. Esparza and C. Schröter. Net Reductions for LTL Model-Checking. Full version, available at ftp://131.159.22.8/pub/theory/schroete/reduct.ps.gz, 2001.
M. Heiner and P. Deusen. Petri net based qualitative analysis-A case study. Technical report I-08/1995. Brandenburg Technische Universität Cottbus, 1995, 1995.
H. Hellwagner. Scalable Readers/Writers Synchronization on Shared-Memory Machines. Esprit P5404 (GP MIMD), Working Paper, 1993.
K. Heljanko. Unfsmodels 0.9. Available at http://www.tcs.hut.fi/kepa/experiments/spin2001/, 2001.
C. Lewerentz and T. Lindner. Formal Development of Reactive Systems: Case Study Production Cell. LNCS 891. Springer-Verlag, 1995.
A. J. Martin. Self-timed FIFO: An exercise in compiling programs into VLSI circuits. In From HDL Descriptions to Guruanteed Correct Circuit Designs, pages 133–153. Elsevier Science Publishers, 1986.
K. L. McMillan. Using Unfoldings to Avoid the State Explosion Problem in the Verification of Asynchronous Circuits. In CAV’92, LNCS 663, pages 164–174. Springer-Verlag, 1992.
D. Poitrenaud and J. F. Pradat-Peyre. Pre-and Post-agglomerations for LTL Model Checking. In ICATPN’00, LNCS 1825, pages 387–408. Springer-Verlag, 2000.
Pastor, O. Roig, J. Cortadella, and R. M. Badia. Petri Net Analysis Using Boolean Manipulation. In ATPN’94, LNCS 815, pages 416–435. Springer-Verlag, 1994.
O. Roig, J. Cortadella, and E. Pastor. Verification of Asynchronous Circuits by BDD-based Model Checking of Petri Nets. In ATPN’95, LNCS 935, pages 374–391. Springer-Verlag, 1995.
W. Reisig. Petri Nets. Volume 4 of the EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1985.
S. Römer. Theorie und Praxis der Netzentfaltungen als Grundlage für die Verifikation nebenläufiger Systeme. PhD thesis, Tech. Univ. München, 2000.
M. Y. Vardi. An automata theoretic approach to linear temporal logic. In Logics for Concurrency: Structure versus Automata, LNCS 1043, pages 238–265. Springer-Verlag, 1996.
F. Wallner. Model checking LTL using net unfoldings. In CAV’98, LNCS 1427, pages 207–218. Springer-Verlag, 1998.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Esparza, J., Schröter, C. (2001). Net Reductions for LTL Model-Checking. In: Margaria, T., Melham, T. (eds) Correct Hardware Design and Verification Methods. CHARME 2001. Lecture Notes in Computer Science, vol 2144. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44798-9_25
Download citation
DOI: https://doi.org/10.1007/3-540-44798-9_25
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42541-0
Online ISBN: 978-3-540-44798-6
eBook Packages: Springer Book Archive