A partial order method for the verification of time Petri nets

  • I. Virbitskaite
  • E. Pokozy
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1684)


The intention of the paper is to develop an efficient model checker for real time systems represented by safe time Petri nets and the real time branching time temporal logic TCTL. Our method is based on the idea of, (1), using the known region graph technique [1] to construct a finite representation of the state-space of a time Petri net and, (2), further reducing the size of this representation by exploiting the net concurrency. To show the correctness of the reduction we introduce a notion of a timed stuttering equivalence. Some experimental results which demonstrate the efficiency of the method are also given.


Partial Order Model Check Time Assignment Region Graph Labelling Algorithm 
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.


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Alur R., Courcoubetis C., Dill D. Model-checking for real-time systems. Proc. 5th IEEE LICS (1990) 414–425.Google Scholar
  2. 2.
    Alur, R., Dill, D.: The theory of timed automata. Theoretical Computer Science 126 (1994) 183–235.zbMATHCrossRefMathSciNetGoogle Scholar
  3. 3.
    Bengtsson, J., Jonsson, B., Lilius, J., Yi, W. Partial order reductions for timed systems. Proc. CONCUR’98 (1998) 485–496.Google Scholar
  4. 4.
    Best, E., Grahlmann, B.: PEP — more than a Petri net tool. Lecture Notes in Computer Science1055 (1996) 397–401.Google Scholar
  5. 5.
    Browne, M.C., Clarke, E.M., Grumberg, O.: Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science59 (1988) 115–131.CrossRefMathSciNetzbMATHGoogle Scholar
  6. 6.
    Burch, J.R., Clarke, E.M., McMillan, L., Dill, D., Hwang, J.: Symbolic model checking: 1020 and beyond. Proc. 5th IEEE LICS (1990) 428–439.Google Scholar
  7. 7.
    Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finitestate systems using temporal logic specifications. ACM TOPLAS8(2) (1986) 244–263.zbMATHCrossRefGoogle Scholar
  8. 8.
    Emersen, E., Sistla, A.: Symmetry and model checking. Lecture Notes in Computer Science697 (1993) 463–478.Google Scholar
  9. 9.
    J. Esparza. Model Checking Using Net Unfoldings. Science of Computer Programming, 23:151–195, 1994.CrossRefMathSciNetGoogle Scholar
  10. 10.
    Gerth, R., Kuiper, R., Peled, D., Penczek, W.: A partial order approach to branching time logic model-checking. Proc. 3rd Israel Symposium on Theory of Computing and Systems (1994).Google Scholar
  11. 11.
    Godefroid, P.: Partial-order methods for the verification of concurrent systems. An approach for state-explosion problem. Lecture Notes in Computer Science1032 (1996) 143 p.Google Scholar
  12. 12.
    Henzinger, T.A., Manna, Z., Pnueli, A.: Timed transition systems. Lecture Notes in Computer Science600 (1991) 226–251.Google Scholar
  13. 13.
    Lilius, J.Efficient state space search for time Petri nets. Proc. MFCS’98Workshop on Concurrency, August 1998, Brno (Czech Republic), FIMU Report Series, FIMU RS-98-06 (1998) 123–130.Google Scholar
  14. 14.
    Merlin, P., Faber, D.J.: Recoverability of communication protocols. IEEE Trans. of Communication24(9) (1976) 1036–1043.zbMATHCrossRefGoogle Scholar
  15. 15.
    McMilan, K.: Using unfolding to avoid the state explosion problem in the verification of asynchronous circuits. Lecture Notes in Computer Science663 (1992) 164–177.Google Scholar
  16. 16.
    Pagani F.: Partial orders and verification of real-time systems Lecture Notes in Computer Science1135 (1996) 327–346.Google Scholar
  17. 17.
    Roux, J-L., Berthomieu, B.: Verification of local area network protocol with Tine, a software package for time Petri nets. Proc. 7th European Workshop on Application and Theory of Petri Nets (1986) 183–205.Google Scholar
  18. 18.
    Valmari, A.: A stubborn attack on state explosion. Lecture Notes in Computer Science535 (1990).Google Scholar
  19. 19.
    Yoneda, T., Shibayama, A., Schlingloff, B.H., Clarke, E.M.: Efficient verification of parallel real-time systems. Lecture Notes in Computer Science697 (1993) 321–333.Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 1999

Authors and Affiliations

  • I. Virbitskaite
    • 1
  • E. Pokozy
    • 1
  1. 1.Siberian Division of the Russian Academy of SciencesInstitute of Informatics SystemsNovosibirskRussia

Personalised recommendations