Using Zone Graph Method for Computing the State Space of a Time Petri Net

  • Guillaume Gardey
  • Olivier H. Roux
  • Olivier F. Roux
Part of the Lecture Notes in Computer Science book series (LNCS, volume 2791)


Presently, the method to verify quantitative time properties on Time Petri Nets is the use of observers. The state space is then computed to test the reachability of a given marking. The main method to compute the state space of a Time Petri Net has been introduced by Berthomieu and Diaz. It is known as the “state class method”. We present in this paper a new efficient method to compute the state space of a bounded Time Petri Net as a marking graph, based on the region graph method used for Timed Automaton. The algorithm is proved to be exact with respect to the reachability of a marking and it computes a graph which nodes are exactly the reachable markings of the Time Petri Net. The tool implemented computes faster than Tina, a tool for constructing the state space using classes, and allows to test on-the-fly the reachability of a given marking.


Time Petri Nets Zone State Space Reachability Analysis Verification 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. [AD94]
    Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)zbMATHCrossRefMathSciNetGoogle Scholar
  2. [AJ01]
    Abdulla, P.A., Jonsson, B.: Ensuring completeness of symbolic verification methods for infinite-state systems. Theoretical Computer Science 256, 145–167 (2001)zbMATHCrossRefMathSciNetGoogle Scholar
  3. [AN01]
    Abdulla, P.A., Nylén, A.: Timed petri nets and bqos. In: Colom, J.-M., Koutny, M. (eds.) ICATPN 2001. LNCS, vol. 2075, pp. 53–72. Springer, Heidelberg (2001)CrossRefGoogle Scholar
  4. [BC02]
    Boniol, F., Carcenac, F.: Une étude de cas pour la vérification formelle de propriétés temporelles. In: FAC 2002 (March 2002),
  5. [BD91]
    Berthomieu, B., Diaz, M.: Modeling and verification of time dependent systems using time petri nets. IEEE transactions on software engineering 17(3), 259–273 (1991)CrossRefMathSciNetGoogle Scholar
  6. [BDFP00]
    Bouyer, P., Dufourd, C., Fleury, E., Petit, A.: Are timed automata updatable? In: Emerson, E.A., Sistla, A.P. (eds.) CAV 2000. LNCS, vol. 1855, pp. 464–479. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  7. [Bou02]
    Bouyer, P.: Timed automata may cause some troubles. Technical report, LSV (July 2002)Google Scholar
  8. [Bou03]
    Bouyer, P.: Unteamable timed automata! In: Alt, H., Habib, M. (eds.) STACS 2003. LNCS, vol. 2607, pp. 620–631. Springer, Heidelberg (2003)CrossRefGoogle Scholar
  9. [BV]
    Berthomieu, B., Vernadat, F.: Tina,
  10. [BV03]
    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)CrossRefGoogle Scholar
  11. [CEP00]
    Cortes, L.A., Eles, P., Peng, Z.: Verification of embedded systems using a petri net based representation. In: 13th International Symposium on System Synthesis (ISSS 2000), Madrid, Spain, September 2000, pp. 149–155 (2000)Google Scholar
  12. [CR03]
    Cassez, F., Roux, O.H.: Traduction structurelle des réseaux de petri temporels vers les automates temporisés. In: 4ieme Colloque Francophone sur la Modélisation des Systèmes Réactifs (MSR 2003), Metz, France (October 2003)Google Scholar
  13. [dFRA00]
    de Frutos Escrig, D., Ruiz, V.V., Alonso, O.M.: Decidability of properties of timed-arc petri nets. In: Nielsen, M., Simpson, D. (eds.) ICATPN 2000. LNCS, vol. 1825, pp. 187–206. Springer, Heidelberg (2000)CrossRefGoogle Scholar
  14. [DS94]
    Diaz, M., Senac, P.: Time stream petri nets: a model for timed multimedia information. In: Valette, R. (ed.) ICATPN 1994. LNCS, vol. 815, pp. 219–238. Springer, Heidelberg (1994)Google Scholar
  15. [FS98]
    Finkel, A., Schnoebelen, P.: Fundamental structures in wellstructured infinite transitions systems. In: Lucchesi, C.L., Moura, A.V. (eds.) LATIN 1998. LNCS, vol. 1380, pp. 102–118. Springer, Heidelberg (1998)CrossRefGoogle Scholar
  16. [KDC96]
    Khasa, W., Denat, J.-P., Collart-Dutilleul, S.: P-Time Petri Nets for manufacturing systems. In: International Workshop on Discrete Event Systems, WODES 1996, August 1996, pp. 94–102, Edinburgh, U.K. (1996)Google Scholar
  17. [Lil99]
    Lilius, J.: Efficient state space search for time petri nets. In: MFCS Workshop on Concurrency 1998. ENTCS, vol. 18, Elsevier, Amsterdam (1999)Google Scholar
  18. [LPY97]
    Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. International Journal on Software Tools for Technology Transfer 1(1–2), 134–152 (1997), zbMATHGoogle Scholar
  19. [LR03]
    Lime, D., Roux, O.H.: State class timed automaton of a time petri net. In: The 10th International Workshop on Petri Nets and Performance Models (PNPM 2003), IEEE Computer Society, Los Alamitos (2003) (to appear)Google Scholar
  20. [Men82]
    Menasche, M.: Analyse des réseaux de Petri temporisés et application aux systèmes distribués. PhD thesis, Université Paul Sabatier, Toulouse, France (1982)Google Scholar
  21. [Mer74]
    Merlin, P.M.: A study of the recoverability of computing systems. PhD thesis, Department of Information and Computer Science, University of California, Irvine, CA (1974)Google Scholar
  22. [OY97]
    Okawa, Y., Yoneda, T.: Symbolic ctl model checking of time petri nets. In: Technica, S. (ed.) Electronics and Communications in Japan, vol. 80, pp. 11–20 (1997)Google Scholar
  23. [Pop91]
    Popova, L.: On time petri nets. Journal Information Processing and Cybernetics, EIK 27(4), 227–244 (1991)zbMATHGoogle Scholar
  24. [Ram74]
    Ramchandani, C.: Analysis of asynchronous concurrent systems by timed Petri nets. PhD thesis, Massachusetts Institute of Technology, Cambridge, MA, Project MAC Report MAC-TR-120 (1974)Google Scholar
  25. [RM94]
    Rokicki, T.G., Myers, C.J.: Automatic verification of timed circuits. In: Dill, D.L. (ed.) CAV 1994. LNCS, vol. 818, pp. 468–480. Springer, Heidelberg (1994)Google Scholar
  26. [Rok93]
    Rokicki, T.G.: Representing an Modeling Circuits. PhD thesis, Stanford University (1993)Google Scholar
  27. [Rom00]
    Romeo. A tool for Time Petri Nets Analysis (2000),
  28. [SA01]
    Sava, A.T., Alla, H.: Commande par supervision des systemes à évènements discrets temporisées. In: Modélisation des syst‘emes réactifs (MSR 2001), pp. 71–86 (2001)Google Scholar
  29. [TST97]
    Toussaint, J., Simonot-Lion, F., Thomesse, J.-P.: Time constraint verifications methods based time petri nets. In: 6th Workshop on Future Trends in Distributed Computing Systems (FTDCS 1997), pp. 262–267, Tunis, Tunisia (1997)Google Scholar
  30. [Yov97]
    Yovine, S.: Kronos: A verification tool for real-time systems. International Journal of Software Tools for Technology Transfer 1(1–2), 123–133 (1997), zbMATHCrossRefGoogle Scholar
  31. [YR98]
    Yoneda, T., Ryuba, H.: Ctl model checking of time petri nets using geometric regions. IEICE Transactions on Information and Systems E99-D(3), 297–396 (1998)Google Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2004

Authors and Affiliations

  • Guillaume Gardey
    • 1
  • Olivier H. Roux
    • 1
  • Olivier F. Roux
    • 1
  1. 1.IRCCyN (Institut de Recherche en Communication et Cybernétique de Nantes)NANTES cedex 3France

Personalised recommendations