Precise Robustness Analysis of Time Petri Nets with Inhibitor Arcs

  • Étienne André
  • Giuseppe Pellegrino
  • Laure Petrucci
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 8053)


Quantifying the robustness of a real-time system consists in measuring the maximum extension of the timing delays such that the system still satisfies its specification. In this work, we introduce a more precise notion of robustness, measuring the allowed variability of the timing delays in their neighbourhood. We consider here the formalism of time Petri nets extended with inhibitor arcs. We use the inverse method, initially defined for timed automata. Its output, in the form of a parametric linear constraint relating all timing delays, allows the designer to identify the delays allowing the least variability. We also exhibit a condition and a construction for rendering robust a non-robust system.


Time Petri nets Quantitative robustness Parameter synthesis 


Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.


  1. 1.
    Akshay, S., Hélouët, L., Jard, C., Lime, D., Roux, O.H.: Robustness of time petri nets under architectural constraints. In: Jurdziński, M., Ničković, D. (eds.) FORMATS 2012. LNCS, vol. 7595, pp. 11–26. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  2. 2.
    Akshay, S., Hélouët, L., Jard, C., Reynier, P.-A.: Robustness of time Petri nets under guard enlargement. In: Finkel, A., Leroux, J., Potapov, I. (eds.) RP 2012. LNCS, vol. 7550, pp. 92–106. Springer, Heidelberg (2012)CrossRefGoogle 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.
    André, É., Soulat, R.: The Inverse Method. FOCUS Series in Computer Engineering and Information Technology. ISTE Ltd and John Wiley & Sons Inc. (2013)Google Scholar
  5. 5.
    Bouyer, P., Larsen, K.G., Markey, N., Sankur, O., Thrane, C.: Timed automata can always be made implementable. In: Katoen, J.-P., König, B. (eds.) CONCUR 2011. LNCS, vol. 6901, pp. 76–91. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  6. 6.
    Bouyer, P., Markey, N., Sankur, O.: Robust reachability in timed automata: A game-based approach. In: Czumaj, A., Mehlhorn, K., Pitts, A., Wattenhofer, R. (eds.) ICALP 2012, Part II. LNCS, vol. 7392, pp. 128–140. Springer, Heidelberg (2012)CrossRefGoogle Scholar
  7. 7.
    Fribourg, L., Kühne, U.: Parametric verification and test coverage for hybrid automata using the inverse method. IJFCS 24(2), 233–249 (2013)Google Scholar
  8. 8.
    Jaubert, R., Reynier, P.-A.: Quantitative robustness analysis of flat timed automata. In: Hofmann, M. (ed.) FOSSACS 2011. LNCS, vol. 6604, pp. 229–244. Springer, Heidelberg (2011)CrossRefGoogle Scholar
  9. 9.
    Markey, N.: Robustness in real-time systems. In: SIES, pp. 28–34. IEEE Computer Society Press (2011)Google Scholar
  10. 10.
    Merlin, P.M.: A study of the recoverability of computing systems. PhD thesis, University of California, Irvine, CA, USA (1974)Google Scholar
  11. 11.
    Sankur, O.: Shrinktech: A tool for the robustness analysis of timed automata. In: CAV. LNCS. Springer (to appear, 2013)Google Scholar
  12. 12.
    Traonouez, L.-M.: A parametric counterexample refinement approach for robust timed specifications. In: FIT. EPTCS, vol. 87, pp. 17–33 (2012)Google Scholar
  13. 13.
    Traonouez, L.-M., Lime, D., Roux, O.H.: Parametric model-checking of stopwatch Petri nets. Journal of Universal Computer Science 15(17), 3273–3304 (2009)MathSciNetzbMATHGoogle Scholar

Copyright information

© Springer-Verlag Berlin Heidelberg 2013

Authors and Affiliations

  • Étienne André
    • 1
  • Giuseppe Pellegrino
    • 1
  • Laure Petrucci
    • 1
  1. 1.Sorbonne Paris Cité, LIPNUniversité Paris 13VilletaneuseFrance

Personalised recommendations