Skip to main content
SpringerLink
Log in
Book cover

Transactions on Petri Nets and Other Models of Concurrency X pp 34–54Cite as

Timed Aggregate Graph: A Finite Graph Preserving Event- and State-Based Quantitative Properties of Time Petri Nets

  • Chapter
  • First Online:

Part of the book series: Lecture Notes in Computer Science ((TOPNOC,volume 9410))

Abstract

In this paper, we propose a new finite graph, called Timed Aggregate Graph (TAG), abstracting the behavior of bounded Time Petri Nets (TPN) with strong time semantics. The main feature of this abstract representation compared to existing approaches is the used criterion to encapsulate the elapsing of time within each node of the TAG (called aggregate), and how to maintain the relative differences between the firing times of enabled transitions. We prove that the TAG preserves timed traces and reachable states of the corresponding TPN. Another interesting and novel feature of the TAGs is the possibility of extracting an explicit run from any of its traces. Thus, we supply an algorithm that maps an abstract run of the TAG to an explicit timed trace (involving a relative elapsed time before each fired transition) of the corresponding TPN. Moreover, the fact that the TAG preserves the timed behavior of the corresponding TPN makes it directly usable in order to check both event- and state-based timed properties as well as the Zenoness property. Zenoness is a pathological behavior which violate a fundamental progress requirement for timed systems stating that it should be possible for time to diverge. A TPN is said to be Zeno when it admits a run where an infinity of transitions are fired in a finite amount of time. We give an algorithm allowing to detect the Zenoness of bounded TPNs and compare the size of the TAG to two well known approaches namely the state class graph and the zone-based graph methods.

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   39.99
Price excludes VAT (USA)
  • Available as EPUB and 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

Learn about institutional subscriptions

Notes

  1. 1.

    I thank Olivier H. Roux who supplied this TPN example during our discussions on the TAG approach.

References

  1. Alur, R., Dill, D.L.: A theory of timed automata. Theor. Comput. Sci. 126(2), 183–235 (1994)

    Article  MathSciNet  MATH  Google Scholar 

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

    Article  MathSciNet  Google Scholar 

  3. Berthomieu, B., Menasche, M.: An enumerative approach for analyzing time petri nets. In: IFIP Congress, pp. 41–46 (1983)

    Google Scholar 

  4. Berthomieu, B., Vernadat, F.: State class constructions for branching analysis of time petri nets. In: Garavel, H., Hatcliff, J. (eds.) TACAS 2003. LNCS, vol. 2619, pp. 442–457. Springer, Heidelberg (2003)

    Chapter  Google Scholar 

  5. Berthomieu, B., Vernadat, F.: Time petri nets analysis with TINA. In: QEST, pp. 123–124 (2006)

    Google Scholar 

  6. Boucheneb, H., Gardey, G., Roux, O.H.: TCTL model checking of time petri nets. J. Log. Comput. 19(6), 1509–1540 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  7. Cassez, F., Roux, O.H.: Structural translation from time petri nets to timed automata. Electr. Notes Theor. Comput. Sci. 128(6), 145–160 (2005)

    Article  MATH  Google Scholar 

  8. Cassez, F., Roux, O.H.: Structural translation from time petri nets to timed automata. J. Syst. Softw. 79(10), 1456–1468 (2006)

    Article  MATH  Google Scholar 

  9. Gardey, G., Lime, D., Magnin, M., Roux, O.H.: Romeo: a tool for analyzing time petri nets. In: Etessami, K., Rajamani, S.K. (eds.) CAV 2005. LNCS, vol. 3576, pp. 418–423. Springer, Heidelberg (2005)

    Chapter  Google Scholar 

  10. Gardey, G., Roux, O.H., Roux, O.F.: Using zone graph method for computing the state space of a time petri net. In: Niebert, P., Larsen, K.G. (eds.) FORMATS 2003. LNCS, vol. 2791, pp. 246–259. Springer, Heidelberg (2004)

    Chapter  Google Scholar 

  11. Hadjidj, R., Boucheneb, H.: Improving state class constructions for CTL* model checking of time petri nets. STTT 10(2), 167–184 (2008)

    Article  MATH  Google Scholar 

  12. Hadjidj, R., Boucheneb, H.: On-the-fly TCTL model checking for time petri nets. Theor. Comput. Sci. 410(42), 4241–4261 (2009)

    Article  MathSciNet  MATH  Google Scholar 

  13. Henzinger, T.A., Nicollin, X., Sifakis, J., Yovine, S.: Symbolic model checking for real-time systems. Inf. Comput. 111(2), 193–244 (1994)

    Article  MathSciNet  MATH  Google Scholar 

  14. Klai, K.: On-the-fly model checking of timed properties on time petri nets. In: Proceedings of the International Workshop on Petri Nets and Software Engineering, pp. 35–53 (2014)

    Google Scholar 

  15. Larsen, K.G., Pettersson, P., Yi, W.: Model-checking for real-time systems. In: Reichel, H. (ed.) FCT 1995. LNCS, vol. 965, pp. 62–88. Springer, Heidelberg (1995)

    Chapter  Google Scholar 

  16. Lime, D., Roux, O.H.: Model checking of time petri nets using the state class timed automaton. Discrete Event Dyn. Syst. 16(2), 179–205 (2006)

    Article  MathSciNet  MATH  Google Scholar 

  17. Merlin, P.M., Farber, D.J.: Recoverability of modular systems. Oper. Syst. Rev. 9(3), 51–56 (1975)

    Article  Google Scholar 

  18. Penczek, W., Pólrola, A., Zbrzezny, A.: SAT-based (parametric) reachability for a class of distributed time petri nets. Trans. Petri Nets Other Models Concurrency 4, 72–97 (2010)

    MATH  Google Scholar 

  19. Petri, C.A.: Concepts of net theory. In: MFCS 1973. Mathematical Institute of the Slovak Academy of Sciences (1973)

    Google Scholar 

  20. Pezzè, M., Young, M.: Time petri nets: a primer introduction. In: Tutorial at the Multi-workshop on Formal Methods in Performance Evaluation and Applications (1999)

    Google Scholar 

  21. Ramchandani, C.: Analysis of asynchronous concurrent systems by timed petri nets. Technical report, Cambridge, MA, USA (1974)

    Google Scholar 

  22. Toussaint, J., Simonot-Lion, F., Thomesse, J.: Time constraints verification methods based on time petri nets. In: Proceedings of the 6th IEEE Workshop on Future Trends of Distributed Computer Systems (FTDCS 1997), Tunis, Tunisia, 29–31 October 1997, pp. 262–269 (1997)

    Google Scholar 

  23. Tripakis, S.: Verifying progress in timed systems. In: Katoen, J.-P. (ed.) AMAST-ARTS 1999, ARTS 1999, and AMAST-WS 1999. LNCS, vol. 1601, pp. 299–314. Springer, Heidelberg (1999)

    Chapter  Google Scholar 

  24. Yoneda, T., Ryuba, H.: CTL model checking of time petri nets using geometric regions (1998)

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. LIPN, CNRS UMR 7030, Université Paris 13, Sorbonne Paris Cité, 99 avenue Jean-Baptiste Clément, 93430, Villetaneuse, France

    Kais Klai

Authors
  1. Kais Klai
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Kais Klai .

Editor information

Editors and Affiliations

  1. Newcastle University, Newcastle upon Tyne, United Kingdom

    Maciej Koutny

  2. Lehrgebiet Software Engineering, FernUniversität in Hagen, Hagen, Germany

    Jörg Desel

  3. École Normale Supérieure de Cachan, Cachan, France

    Serge Haddad

Rights and permissions

Reprints and permissions

Copyright information

© 2015 Springer-Verlag Berlin Heidelberg

About this chapter

Cite this chapter

Klai, K. (2015). Timed Aggregate Graph: A Finite Graph Preserving Event- and State-Based Quantitative Properties of Time Petri Nets. In: Koutny, M., Desel, J., Haddad, S. (eds) Transactions on Petri Nets and Other Models of Concurrency X. Lecture Notes in Computer Science(), vol 9410. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-662-48650-4_3

Download citation

  • DOI: https://doi.org/10.1007/978-3-662-48650-4_3

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-662-48649-8

  • Online ISBN: 978-3-662-48650-4

  • eBook Packages: Computer ScienceComputer Science (R0)

Publish with us

Policies and ethics

Search

Navigation