Net Reductions for LTL Model-Checking

  • Javier Esparza
  • Claus Schröter
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2144)


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.


Model Check Atomic Proposition Reduction Rule Linear Programming Technique Occurrence Sequence 
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.


  1. [Ber85]
    G. Berthelot. Checking properties of nets using transformations. In Advances in Petri Nets, LNCS 222, pages 19–40. Springer-Verlag, 1985.CrossRefGoogle Scholar
  2. [Cor94]
    J. C. Corbett. Evaluating Deadlock Detection Methods, 1994.Google Scholar
  3. [CS90]
    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.Google Scholar
  4. [DE95]
    J. Desel and J. Esparza. Free Choice Petri Nets. Cambridge University Press, 1995.Google Scholar
  5. [EH00]
    J. Esparza and K. Heljanko. A new Unfolding Approach to LTL Model Checking. In ICALP’00, LNCS 1853, pages 475–486. Springer-Verlag, 2000.Google Scholar
  6. [EH01]
    J. Esparza and K. Heljanko. Implementing LTL Model Checking with Net Unfoldings. Accepted paper for SPIN’01, 2001.Google Scholar
  7. [ES01]
    J. Esparza and C. Schröter. Net Reductions for LTL Model-Checking. Full version, available at, 2001.
  8. [HD95]
    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.Google Scholar
  9. [Hel93]
    H. Hellwagner. Scalable Readers/Writers Synchronization on Shared-Memory Machines. Esprit P5404 (GP MIMD), Working Paper, 1993.Google Scholar
  10. [Hel01]
    K. Heljanko. Unfsmodels 0.9. Available at, 2001.
  11. [LL95]
    C. Lewerentz and T. Lindner. Formal Development of Reactive Systems: Case Study Production Cell. LNCS 891. Springer-Verlag, 1995.zbMATHGoogle Scholar
  12. [Mar86]
    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.Google Scholar
  13. [McM92]
    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.Google Scholar
  14. [PPP00]
    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.Google Scholar
  15. [PRCB94]E.
    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.Google Scholar
  16. [RCP95]
    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.Google Scholar
  17. [Rei85]
    W. Reisig. Petri Nets. Volume 4 of the EATCS Monographs on Theoretical Computer Science. Springer-Verlag, 1985.Google Scholar
  18. [Röm00]
    S. Römer. Theorie und Praxis der Netzentfaltungen als Grundlage für die Verifikation nebenläufiger Systeme. PhD thesis, Tech. Univ. München, 2000.Google Scholar
  19. [Var96]
    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.Google Scholar
  20. [Wal98]
    F. Wallner. Model checking LTL using net unfoldings. In CAV’98, LNCS 1427, pages 207–218. Springer-Verlag, 1998.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2001

Authors and Affiliations

  • Javier Esparza
    • 1
  • Claus Schröter
    • 1
  1. 1.Institut für InformatikTechnische Universität MünchenGermany

Personalised recommendations