Skip to main content
SpringerLink
Log in

Complete Finite Prefixes of Symbolic Unfoldings of Safe Time Petri Nets

  • Conference paper
Petri Nets and Other Models of Concurrency - ICATPN 2006 (ICATPN 2006)

Part of the book series: Lecture Notes in Computer Science ((LNTCS,volume 4024))

Included in the following conference series:

Abstract

Time Petri nets have proved their interest in modeling real-time concurrent systems. Their usual semantics is defined in term of firing sequences, which can be coded in a (symbolic and global) state graph, computable from a bounded net. An alternative is to consider a “partial order” semantics given in term of processes, which keep explicit the notions of causality and concurrency without computing arbitrary interleavings. In ordinary place/transition bounded nets, it has been shown for many years that the whole set of processes can be finitely represented by a prefix of what is called the “unfolding”. This paper defines such a prefix for safe time Petri nets. It is based on a symbolic unfolding of the net, using a notion of “partial state”.

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

Access this chapter

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 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.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

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Kitai, T., Oguro, Y., Yoneda, T., Mercer, E., Myers, C.: Partial order reduction for timed circuit verification based on a level oriented model. IEICE Trans. E86-D(12), 2601–2611 (2001)

    Google Scholar 

  2. Penczek, W., Pólrola, A.: Abstractions and partial order reductions for checking branching properties of time Petri nets. In: Colom, J.-M., Koutny, M. (eds.) ICATPN 2001. LNCS, vol. 2075, pp. 323–342. Springer, Heidelberg (2001)

    Chapter  Google Scholar 

  3. Chatain, T., Jard, C.: Time Supervision of Concurrent Systems Using Symbolic Unfoldings of Time Petri Nets. In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 196–210. Springer, Heidelberg (2005); Extended version available in INRIA Research Report RR-5706

    Google Scholar 

  4. Aura, T., Lilius, J.: Time processes for time Petri nets. In: Azéma, P., Balbo, G. (eds.) ICATPN 1997. LNCS, vol. 1248, pp. 136–155. Springer, Heidelberg (1997)

    Google Scholar 

  5. Lilius, J.: Efficient state space search for time Petri nets. In: MFCS Workshop on Concurrency 1998. ENTCS, vol. 18. Elsevier, Amsterdam (1999)

    Google Scholar 

  6. McMillan, K.L.: A technique of state space search based on unfolding. Formal Methods in System Design 6(1), 45–65 (1995)

    Article  MATH  MathSciNet  Google Scholar 

  7. Esparza, J., Römer, S., Vogler, W.: An improvement of McMillan’s unfolding algorithm. Formal Methods in System Design 20(3), 285–310 (2002)

    Article  MATH  Google Scholar 

  8. Bieber, B., Fleischhack, H.: Model checking of time Petri nets based on partial order semantics. In: Baeten, J.C.M., Mauw, S. (eds.) CONCUR 1999. LNCS, vol. 1664, pp. 210–225. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  9. Fleischhack, H., Stehno, C.: Computing a finite prefix of a time Petri net. In: Esparza, J., Lakos, C.A. (eds.) ICATPN 2002. LNCS, vol. 2360, pp. 163–181. Springer, Heidelberg (2002)

    Chapter  Google Scholar 

  10. Berthomieu, B., Diaz, M.: Modeling and verification of time dependent systems using time Petri nets. IEEE Trans. Software Eng. 17(3), 259–273 (1991)

    Article  MathSciNet  Google Scholar 

  11. Semenov, A.L., Yakovlev, A.: Verification of asynchronous circuits using time Petri net unfolding. In: DAC, pp. 59–62. ACM Press, New York (1996)

    Google Scholar 

  12. Merlin, P., Farber, D.: Recoverability of communication protocols – implications of a theorical study. IEEE Transactions on Communications 24 (1976)

    Google Scholar 

  13. Engelfriet, J.: Branching processes of Petri nets. Acta Inf. 28(6), 575–591 (1991)

    Article  MATH  MathSciNet  Google Scholar 

  14. Chatain, T., Jard, C.: Symbolic diagnosis of partially observable concurrent systems. In: de Frutos-Escrig, D., Núñez, M. (eds.) FORTE 2004. LNCS, vol. 3235, pp. 326–342. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  15. Best, E.: Structure theory of Petri nets: the free choice hiatus. In: Proceedings of an Advanced Course on Petri Nets: Central Models and Their Properties, Advances in Petri Nets 1986-Part I, London, UK, pp. 168–205. Springer, Heidelberg (1987)

    Chapter  Google Scholar 

  16. Baldan, P., Corradini, A., Montanari, U.: Contextual Petri nets, asymmetric event structures, and processes. Inf. Comput. 171(1), 1–49 (2001)

    Article  MATH  MathSciNet  Google Scholar 

  17. Vogler, W., Semenov, A.L., Yakovlev, A.: Unfolding and finite prefix for nets with read arcs. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 501–516. Springer, Heidelberg (1998)

    Chapter  Google Scholar 

Download references

Author information

Authors and Affiliations

  1. IRISA/INRIA, Campus de Beaulieu, F-35042 cedex, Rennes, France

    Thomas Chatain

  2. IRISA/ENS Cachan-Bretagne, Campus de Ker Lann, F-35170, Bruz, France

    Claude Jard

Authors
  1. Thomas Chatain
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Claude Jard
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Dipartimento di Informatica, Università di Torino, 10149, Torino, Italy

    Susanna Donatelli

  2. School of Computing, National University of Singapore,  

    P. S. Thiagarajan

Rights and permissions

Reprints and permissions

Copyright information

© 2006 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Chatain, T., Jard, C. (2006). Complete Finite Prefixes of Symbolic Unfoldings of Safe Time Petri Nets. In: Donatelli, S., Thiagarajan, P.S. (eds) Petri Nets and Other Models of Concurrency - ICATPN 2006. ICATPN 2006. Lecture Notes in Computer Science, vol 4024. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11767589_8

Download citation

  • DOI: https://doi.org/10.1007/11767589_8

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-34699-9

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

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation