Region-Based Analysis of Hybrid Petri Nets with a Single General One-Shot Transition

  • Hamed Ghasemieh
  • Anne Remke
  • Boudewijn Haverkort
  • Marco Gribaudo
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 7595)


Recently, hybrid Petri nets with a single general one-shot transition (HPnGs) have been introduced together with an algorithm to analyze their underlying state space using a conditioning/deconditioning approach. In this paper we propose a considerably more efficient algorithm for analysing HPnGs. The proposed algorithm maps the underlying state-space onto a plane for all possible firing times of the general transition s and for all possible systems times t. The key idea of the proposed method is that instead of dealing with infinitely many points in the t-s-plane, we can partition the state space into several regions, such that all points inside one region are associated with the same system state. To compute the probability to be in a specific system state at time τ, it suffices to find all regions intersecting the line t = τ and decondition the firing time over the intersections. This partitioning results in a considerable speed-up and provides more accurate results. A scalable case study illustrates the efficiency gain with respect to the previous algorithm.


System State General Transition Occurrence Time Deterministic Region Time Automaton 
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., Halbwachs, N., Henzinger, T., Yovine, S., Ho, P.H., Nicollin, X., Olivero, A., Sifakis, J.: The algorithmic analysis of hybrid systems. Theoretical Computer Science 138, 3–34 (1995)MathSciNetzbMATHCrossRefGoogle Scholar
  2. 2.
    Alur, R., Courcoubetis, C., Henzinger, T.: Hybrid automata: An algorithmic approach to the specification and verification of hybrid systems. Hybrid Systems 736, 209–229 (1993)MathSciNetCrossRefGoogle Scholar
  3. 3.
    Alur, R., Dill, D.L.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)MathSciNetzbMATHCrossRefGoogle Scholar
  4. 4.
    Asarin, E., Maler, O.: Reachability analysis of dynamical systems having piecewise-constant derivatives. Theoretical Computer Science 138(1), 35–65 (1995)MathSciNetzbMATHCrossRefGoogle Scholar
  5. 5.
    Berthomieu, B.: Modeling and verification of time dependent systems using time Petri nets. IEEE Transactions on Software Engineering 17(3), 259–273 (1991)MathSciNetCrossRefGoogle Scholar
  6. 6.
    David, R., Alla, H.: Discrete, Continuous, and Hybrid Petri Nets, 2nd edn. Springer (2010)Google Scholar
  7. 7.
    Ghasemieh, H., Remke, A., Haverkort, B., Gribaudo, M.: Region-based analysis of hybrid Petri nets with a single general one-shot transition: extended version. Technical report, University of Twente (2012),
  8. 8.
    Gribaudo, M., Remke, A.: Hybrid Petri Nets with General One-Shot Transitions for Dependability Evaluation of Fluid Critical Infrastructures. In: 2010 IEEE 12th International Symposium on High Assurance Systems Engineering, pp. 84–93. IEEE CS Press (November 2010)Google Scholar
  9. 9.
    Gribaudo, M., Remke, A.: Hybrid petri nets with general one-shot transitions: model evolution. Technical report, University of Twente (2010),
  10. 10.
    Kartson, D., Balbo, G., Donatelli, S., Franceschinis, G., Conte, G.: Modelling with Generalized Stochastic Petri Nets, 1st edn. John Wiley & Sons, Inc. (1994)Google Scholar
  11. 11.
    Vicario, E.: Static analysis and dynamic steering of time-dependent systems. IEEE Transactions on Software Engineering 27(8), 728–748 (2001)CrossRefGoogle Scholar
  12. 12.
    Vicario, E., Sassoli, L., Carnevali, L.: Using stochastic state classes in quantitative evaluation of dense-time reactive systems. IEEE Transactions on Software Engineering 35(5), 703–719 (2009)CrossRefGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2012

Authors and Affiliations

  • Hamed Ghasemieh
    • 1
  • Anne Remke
    • 1
  • Boudewijn Haverkort
    • 1
    • 2
  • Marco Gribaudo
    • 3
  1. 1.Design and Analysis of Communication SystemsUniversity of TwenteThe Netherlands
  2. 2.Embedded System InstituteEindhovenThe Netherlands
  3. 3.Dipartimento Di Elettronica E InformazioneIngegneria dell’InformazioneItaly

Personalised recommendations