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.
Similar content being viewed by others
References
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
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
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
Alur R, Dill DL (1994) A theory of timed automata. Theor Comput Sci 126(2):183–235
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
Amnell T, Fersman E, Pettersson P, Sun H, Yi W (2003) Code synthesis for timed automata. Nord J Comput 9
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
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
Asarin E, Maler O, Pnueli A, Sifakis J (1998) Controller synthesis for timed automata. In: Proc system structure and control. Elsevier, Amsterdam
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
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
Bouyer P, Chevalier F (2005) On conciseness of extensions of timed automata. J Autom Lang Comb 10(4):393–405
Behrmann G, David A, Larsen KG, Håkansson J, Pettersson P, Yi W, Hendriks M (2006) Uppaal 4.0. In: QEST, pp 125–126
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
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
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
Clarke E, Grumberg O, Peled D (1999) Model checking. MIT Press, Cambridge
Chaochen Z, Hoare CAR, Ravn AP (1991) A calculus of durations. Inf Process Lett 40(5):269–276
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
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
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
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
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
Dierks H (1999) Specification and verification of polling real-time systems. PhD thesis, University of Oldenburg
Dierks H (2001) PLC-automata: a new class of implementable real-time automata. Theor Comput Sci 253(1):61–93
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
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
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
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
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
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
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
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
Milner R (1980) A calculus of communicating systems. Lecture notes in computer science, vol 92. Springer, Berlin
Maler O, Pnueli A, Sifakis J (1995) On the synthesis of discrete controllers for timed systems (an extended abstract). In: STACS, pp 229–242
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
Puri A (2000) Dynamical properties of timed automata. Discrete Event Dyn Syst 10(1–2):87–113
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
Yovine S (1996) Model checking timed automata. In: European educational forum: school on embedded systems, pp 114–152
Author information
Authors and Affiliations
Corresponding author
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
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
Published:
Issue Date:
DOI: https://doi.org/10.1007/s10703-008-0056-7