Skip to main content
SpringerLink
Log in
Book cover

International Symposium on Fundamentals of Computation Theory

FCT 1999: Fundamentals of Computation Theory pp 547–558Cite as

A partial order method for the verification of time Petri nets

  • Conference paper
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 1684))

Abstract

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.

Article

This work is supported in part by the Russian Ministry of High Education, Grant for Basic Research in Mathematics.

This is a preview of subscription content, log in via an institution.

Chapter
USD   29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD   84.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD   109.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Learn about institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Alur R., Courcoubetis C., Dill D. Model-checking for real-time systems. Proc. 5th IEEE LICS (1990) 414–425.

    Google Scholar 

  2. Alur, R., Dill, D.: The theory of timed automata. Theoretical Computer Science 126 (1994) 183–235.

    Article  MATH  MathSciNet  Google Scholar 

  3. Bengtsson, J., Jonsson, B., Lilius, J., Yi, W. Partial order reductions for timed systems. Proc. CONCUR’98 (1998) 485–496.

    Google Scholar 

  4. Best, E., Grahlmann, B.: PEP — more than a Petri net tool. Lecture Notes in Computer Science1055 (1996) 397–401.

    Google Scholar 

  5. Browne, M.C., Clarke, E.M., Grumberg, O.: Characterizing finite Kripke structures in propositional temporal logic. Theoretical Computer Science59 (1988) 115–131.

    Article  MathSciNet  MATH  Google Scholar 

  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. Clarke, E.M., Emerson, E.A., Sistla, A.P.: Automatic verification of finitestate systems using temporal logic specifications. ACM TOPLAS8(2) (1986) 244–263.

    Article  MATH  Google Scholar 

  8. Emersen, E., Sistla, A.: Symmetry and model checking. Lecture Notes in Computer Science697 (1993) 463–478.

    Google Scholar 

  9. J. Esparza. Model Checking Using Net Unfoldings. Science of Computer Programming, 23:151–195, 1994.

    Article  MathSciNet  Google Scholar 

  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. 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. Henzinger, T.A., Manna, Z., Pnueli, A.: Timed transition systems. Lecture Notes in Computer Science600 (1991) 226–251.

    Google Scholar 

  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. Merlin, P., Faber, D.J.: Recoverability of communication protocols. IEEE Trans. of Communication24(9) (1976) 1036–1043.

    Article  MATH  Google Scholar 

  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. Pagani F.: Partial orders and verification of real-time systems Lecture Notes in Computer Science1135 (1996) 327–346.

    Google Scholar 

  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. Valmari, A.: A stubborn attack on state explosion. Lecture Notes in Computer Science535 (1990).

    Google Scholar 

  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 

Download references

Author information

Authors and Affiliations

  1. Siberian Division of the Russian Academy of Sciences, Institute of Informatics Systems, 6, Acad. Lavrentiev av., 630090, Novosibirsk, Russia

    I. Virbitskaite & E. Pokozy

Authors
  1. I. Virbitskaite
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. E. Pokozy
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Faculty of Computer Science, “A.I.Cuza” University, 6600, Iaşi, Romania

    Gabriel Ciobanu

  2. Institute of Mathematics of the Romanian Academy, P.O. Box 1-764, 70700, Bucharest, Romania

    Gheorghe Păun

Rights and permissions

Reprints and permissions

Copyright information

© 1999 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Virbitskaite, I., Pokozy, E. (1999). A partial order method for the verification of time Petri nets. In: Ciobanu, G., Păun, G. (eds) Fundamentals of Computation Theory. FCT 1999. Lecture Notes in Computer Science, vol 1684. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48321-7_46

Download citation

  • DOI: https://doi.org/10.1007/3-540-48321-7_46

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-66412-3

  • Online ISBN: 978-3-540-48321-2

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation