Skip to main content
Springer Nature Link
Log in

Robust safety of timed automata

  • Published:
Formal Methods in System Design Aims and scope Submit manuscript

Abstract

Timed automata are governed by an idealized semantics that assumes a perfectly precise behavior of the clocks. The traditional semantics is not robust because the slightest perturbation in the timing of actions may lead to completely different behaviors of the automaton. Following several recent works, we consider a relaxation of this semantics, in which guards on transitions are widened by Δ>0 and clocks can drift by ε>0. The relaxed semantics encompasses the imprecisions that are inevitably present in an implementation of a timed automaton, due to the finite precision of digital clocks.

We solve the safety verification problem for this robust semantics: given a timed automaton and a set of bad states, our algorithm decides if there exist positive values for the parameters Δ and ε such that the timed automaton never enters the bad states under the relaxed semantics.

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

Access this article

Log in via an institution

Subscribe and save

Springer+ Basic
$34.99 /Month
  • Get 10 units per month
  • Download Article/Chapter or eBook
  • 1 Unit = 1 Article or 1 Chapter
  • Cancel anytime
Subscribe now

Buy Now

Price excludes VAT (USA)
Tax calculation will be finalised during checkout.

Instant access to the full article PDF.

Institutional subscriptions

Similar content being viewed by others

References

  1. Annichini A, Asarin E, Bouajjani A (2000) Symbolic techniques for parametric reasoning about counter and clock systems. In: Proc 12th int conf computer aided verification (CAV 2000), pp 419–434

  2. Asarin E, Bouajjani A (2001) Perturbed Turing machines and hybrid systems. In: Proc 16th annual symposium on logic in computer science (LICS). IEEE Comput Soc, Los Alamitos, pp 269–278

    Chapter  Google Scholar 

  3. Alur R, Courcoubetis C, Dill DL, Halbwachs N, Wong-Toi H (1992) An implementation of three algorithms for timing verification based on automata emptiness. In: Proc 13th IEEE real-time systems symposium. IEEE Comput Soc, Los Alamitos, pp 157–166

    Google Scholar 

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

    Article  MATH  MathSciNet  Google Scholar 

  5. Amnell T, Fersman E, Mokrushin L, Pettersson P, Yi W (2002) Times: A tool for modelling and implementation of embedded systems. In: Katoen J-P, Stevens P (eds) Proc 8th int conference tools and algorithms for the construction and analysis of systems (TACAS’02). Lecture notes in computer science, vol 2280. Springer, Berlin, pp 460–464

    Chapter  Google Scholar 

  6. Amnell T, Fersman E, Pettersson P, Sun H, Yi W (2003) Code synthesis for timed automata. Nord J Comput 9

  7. Alur R, Ivancic F, Kim J, Lee I, Sokolsky O (2003) Generating embedded software from hierarchical hybrid models. In: Proc 2003 conf languages, compilers, and tools for embedded systems (LCTES’03), pp 171–182

  8. Alur R, La Torre S, Madhusudan P (2005) Perturbed timed automata. In: Proc 8th int workshop hybrid systems: computation and control (HSCC’05). Lecture notes in computer science, vol 3414. Springer, Berlin, pp 70–85

    Google Scholar 

  9. Asarin E, Maler O, Pnueli A, Sifakis J (1998) Controller synthesis for timed automata. In: Proc system structure and control. Elsevier, Amsterdam

    Google Scholar 

  10. Agrawal M, Thiagarajan PS (2004) Lazy rectangular hybrid automata. In: Proc of HSCC 04: Hybrid systems—computation and control. Lecture notes in computer science, vol 2993. Springer, Berlin, pp 1–15

    Google Scholar 

  11. Altisen K, Tripakis S (2005) Implementation of timed automata: an issue of semantics or modeling? In: Proc 3rd int conf formal modelling and analysis of timed systems (FORMATS’05). Lecture notes in computer science. Springer, Berlin

    Google Scholar 

  12. Bouyer P, Chevalier F (2005) On conciseness of extensions of timed automata. J Autom Lang Comb 10(4):393–405

    MATH  MathSciNet  Google Scholar 

  13. Behrmann G, David A, Larsen KG, Håkansson J, Pettersson P, Yi W, Hendriks M (2006) Uppaal 4.0. In: QEST, pp 125–126

  14. Berthomieu B, Menasche M (1983) An enumerative approach for analyzing time Petri nets. In: Mason REA (ed) Information processing 83—Proceedings of the 9th IFIP world computer congress, September 1983. North-Holland/IFIP, pp 41–46

  15. Bouyer P, Markey N, Reynier P-A (2006) Robust model-checking of linear-time properties in timed automata. In: Correa JR, Hevia A, Kiwi M (eds) Proceedings of the 7th Latin American symposium on theoretical informatics (LATIN’06). Lecture Notes in Computer Science, vol 3887. Springer, Berlin, pp 238–249

    Google Scholar 

  16. Bouyer P, Markey N, Reynier P-A (2008) Robust analysis of timed automata via channel machines. In: Amadio R (ed) Proceedings of the 11th international conference on foundations of software science and computation structures (FoSSaCS’08), Budapest, Hungary, March–April 2008. Lecture notes in computer science, vol 4962. Springer, Berlin, pp 157–171

    Google Scholar 

  17. Clarke E, Grumberg O, Peled D (1999) Model checking. MIT Press, Cambridge

    Google Scholar 

  18. Chaochen Z, Hoare CAR, Ravn AP (1991) A calculus of durations. Inf Process Lett 40(5):269–276

    Article  MATH  MathSciNet  Google Scholar 

  19. Cassez F, Henzinger TA, Raskin J-F (2002) A comparison of control problems for timed and hybrid systems. In: Proc 5th int workshop hybrid systems: computation and control (HSCC’02). Lecture notes in computer science, vol 2289. Springer, Berlin, pp 134–148

    Chapter  Google Scholar 

  20. Chaochen Z, Hansen MR, Sestoft P (1993) Decidability and undecidability results for duration calculus. In: In proc of STACS 93: symposium on theoretical aspects of computer science. Lecture notes in computer science, vol 665. Springer, Berlin, pp 58–68

    Google Scholar 

  21. Courcoubetis C, Yannakakis M (1991) Minimum and maximum delay problems in real-time systems. In: Proc 3rd int workshop computer aided verification (CAV’91). Lecture notes in computer science, vol 575. Springer, Berlin, pp 399–409

    Google Scholar 

  22. De Wulf M, Doyen L, Markey N, Raskin J-F (2004) Robustness and implementability of timed automata. In: Lakhnech Y, Yovine S (eds) Proceedings of the joint conferences formal modelling and analysis of timed systems (FORMATS’04) and formal techniques in real-time and fault-tolerant systems (FTRTFT’04), Grenoble, France, September 2004. Lecture notes in computer science, vol 3253. Springer, Berlin, pp 118–133

    Google Scholar 

  23. De Wulf M, Doyen L, Raskin J-F (2005) Almost ASAP semantics: from timed models to timed implementations. Form Asp Comput 17(3):319–341

    Article  MATH  Google Scholar 

  24. Dierks H (1999) Specification and verification of polling real-time systems. PhD thesis, University of Oldenburg

  25. Dierks H (2001) PLC-automata: a new class of implementable real-time automata. Theor Comput Sci 253(1):61–93

    Article  MATH  MathSciNet  Google Scholar 

  26. Dill D (1990) Timing assumptions and verification of finite-state concurrent systems. In: Proc 1st int workshop automatic verification methods for finite state systems (CAV’89). Lecture notes in computer science, vol 407. Springer, Berlin, pp 197–212

    Google Scholar 

  27. Dima C (2007) Dynamical properties of timed automata revisited. In: Proc of FORMATS 07: formal modeling and analysis of timed systems. Lecture notes in computer science, vol 4763. Springer, Berlin, pp 130–146

    Chapter  Google Scholar 

  28. Daws C, Kordy P (2006) Symbolic robustness analysis of timed automata. In: Proc of FORMATS 06: formal modeling and analysis of timed systems. Lecture notes in computer science, vol 4202. Springer, Berlin, pp 143–155

    Chapter  Google Scholar 

  29. Fränzle M (1999) Analysis of hybrid systems: an ounce of realism can save an infinity of states. In: CSL. Lecture notes in computer science, vol 1683. Springer, Berlin, pp 126–140

    Google Scholar 

  30. Gupta V, Henzinger TA, Jagadeesan R (1997) Robust timed automata. In: Maler O (ed) Proc int workshop hybrid and real-time systems (HART’97). Lecture notes in computer science, vol 1201. Springer, Berlin, pp 331–345

    Chapter  Google Scholar 

  31. Henzinger TA, Kirsch CM, Sanvido MA, Pree W (2003) From control models to real-time code using giotto. IEEE Control Syst Mag 23(1):50–64

    Article  Google Scholar 

  32. Henzinger TA, Nicollin X, Sifakis J, Yovine S (1992) Symbolic model checking for real-time systems. In: Proc 7th annual symposium logic in computer science (LICS’92). IEEE Comput Soc, Los Alamitos, pp 394–406

    Google Scholar 

  33. Hune T, Romijn J, Stoelinga M, Vaandrager FW (2001) Linear parametric model checking of timed automata. In: Proc 7th int conf tools and algorithms for construction and analysis of systems (TACAS’01), pp 189–203

  34. Milner R (1980) A calculus of communicating systems. Lecture notes in computer science, vol 92. Springer, Berlin

    MATH  Google Scholar 

  35. Maler O, Pnueli A, Sifakis J (1995) On the synthesis of discrete controllers for timed systems (an extended abstract). In: STACS, pp 229–242

  36. Puri A (1998) Dynamical properties of timed automata. In: Proc 5th int symposium formal techniques in real-time and fault-tolerant systems (FTRTFT’98). Lecture notes in computer science, vol 1486. Springer, Berlin, pp 210–227

    Chapter  Google Scholar 

  37. Puri A (2000) Dynamical properties of timed automata. Discrete Event Dyn Syst 10(1–2):87–113

    Article  MATH  MathSciNet  Google Scholar 

  38. Swaminathan M, Fränzle M (2007) A symbolic decision procedure for robust safety of timed systems. In: Proceedings of the 14th international symposium on temporal representation and reasoning (TIME’07). IEEE Comput Soc, Los Alamitos, p 192

    Chapter  Google Scholar 

  39. Yovine S (1996) Model checking timed automata. In: European educational forum: school on embedded systems, pp 114–152

Download references

Author information

Authors and Affiliations

  1. Dépt Informatique, Université Libre de Bruxelles (ULB), Campus de la Plaine, Bd du Triomphe CP 212, 1050, Brussels, Belgium

    Martin De Wulf & Jean-François Raskin

  2. École Polytechnique Fédérale de Lausanne (EPFL), Station 14, 1015, Lausanne, Switzerland

    Laurent Doyen

  3. Laboratoire Spécification & Vérification (LSV), ENS Cachan & CNRS, 61 av. Pdt Wilson, 94230, Cachan, France

    Nicolas Markey

Authors
  1. Martin De Wulf
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Laurent Doyen
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Nicolas Markey
    View author publications

    You can also search for this author in PubMed Google Scholar

  4. Jean-François Raskin
    View author publications

    You can also search for this author in PubMed Google Scholar

Corresponding author

Correspondence to Laurent Doyen.

Additional information

This research was supported by the Belgian FNRS grant 2.4530.02 of the FRFC project “Centre Fédéré en Vérification” and by the project “MoVES”, an Interuniversity Attraction Poles Programme of the Belgian Federal Government.

Rights and permissions

Reprints and permissions

About this article

Cite this article

De Wulf, M., Doyen, L., Markey, N. et al. Robust safety of timed automata. Form Methods Syst Des 33, 45–84 (2008). https://doi.org/10.1007/s10703-008-0056-7

Download citation

  • Published:

  • Issue Date:

  • DOI: https://doi.org/10.1007/s10703-008-0056-7

Keywords

Search

Navigation