Abstract
Formal verification of timed systems is well understood, but their implementation is still challenging. Raskin et al. have recently brought out a model of parameterized timed automata in which the transitions might be slightly delayed or expedited. This model is used to prove that a timed system is implementable with respect to a safety property, by proving that the parameterized model robustly satisfies the safety property. We extend here the notion of implementability to the broader class of linear-time properties, and provide PSPSACE algorithms for the robust model-checking of Büchi-like and LTL properties. We also show how those algorithms can be adapted in order to verify bounded-response-time properties.
Work supported by ACI “Sécurité Informatique” CORTOS (Control and Observation of Real-Time Open Systems), a program of the French Ministry of research.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsPreview
Unable to display preview. Download preview PDF.
References
Altisen, K., Tripakis, S.: Implementation of timed automata: An issue of semantics or modeling? In: Pettersson, P., Yi, W. (eds.) FORMATS 2005. LNCS, vol. 3829, pp. 273–288. Springer, Heidelberg (2005)
Alur, R., Dill, D.: A theory of timed automata. Theoretical Computer Science 126(2), 183–235 (1994)
Alur, R., Henzinger, T.A.: Real-time logics: Complexity and expressiveness. Information and Computation 104(1), 35–77 (1993)
Alur, R., La Torre, S., Madhusudan, P.: Perturbed timed automata. In: Morari, M., Thiele, L. (eds.) HSCC 2005. LNCS, vol. 3414, pp. 70–85. Springer, Heidelberg (2005)
Behrmann, G., Fehnker, A., Hune, T., Larsen, K.G., Pettersson, P., Romijn, J., Vaandrager, F.: Minimum-cost reachability for priced timed automata. In: Di Benedetto, M.D., Sangiovanni-Vincentelli, A.L. (eds.) HSCC 2001. LNCS, vol. 2034, pp. 147–161. Springer, Heidelberg (2001)
Bouyer, P., Markey, N., Reynier, P.-A.: Robust model-checking of timed automata. Tech. Report LSV-05-08, LSV, ENS Cachan, France (2005)
Bozga, M., Daws, C., Maler, O., Olivero, A., Tripakis, S., Yovine, S.: Kronos: a model-checking tool for real-time systems. In: Y. Vardi, M. (ed.) CAV 1998. LNCS, vol. 1427, pp. 546–550. Springer, Heidelberg (1998)
Cassez, F., Henzinger, T.A., Raskin, J.-F.: A comparison of control problems for timed and hybrid systems. In: Tomlin, C.J., Greenstreet, M.R. (eds.) HSCC 2002. LNCS, vol. 2289, pp. 134–148. Springer, Heidelberg (2002)
De Wulf, M., Doyen, L., Markey, N., Raskin, J.-F.: Robustness and implementability of timed automata. Tech. Report 2004.30, Centre Fédéré en Vérification, Belgium (December 2005); Revised version
De Wulf, M., Doyen, L., Raskin, J.-F.: Almost ASAP semantics: From timed models to timed implementations. Formal Aspects of Computing 17(3), 319–341 (2005)
Gupta, V., Henzinger, T.A., Jagadeesan, R.: Robust timed automata. In: Maler, O. (ed.) HART 1997. LNCS, vol. 1201, pp. 331–345. Springer, Heidelberg (1997)
Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Systems 2(4), 255–299 (1990)
Larsen, K.G., Pettersson, P., Yi, W.: Uppaal in a nutshell. Journal of Software Tools for Technology Transfer 1(1–2), 134–152 (1997)
Ouaknine, J., Worrell, J.B.: Revisiting digitization, robustness and decidability for timed automata. In: Proc. 18th Ann. Symp. Logic in Computer Science (LICS 2003), pp. 198–207. IEEE Comp. Soc. Press, Los Alamitos (2003)
Ouaknine, J., Worrell, J.B.: On the decidability of metric temporal logic. In: Proc. 19th Ann. Symp. Logic in Computer Science (LICS 2005), pp. 188–197. IEEE Comp. Soc. Press, Los Alamitos (2005)
Puri, A.: Dynamical properties of timed automata. In: Ravn, A.P., Rischel, H. (eds.) FTRTFT 1998. LNCS, vol. 1486, pp. 210–227. Springer, Heidelberg (1998)
Raskin, J.-F.: Logics, Automata and Classical Theories for Deciding Real-Time. PhD thesis, University of Namur, Namur, Belgium (1999)
Wolper, P., Vardi, M.Y., Sistla, A.P.: Reasoning about infinite computation paths. In: Proc. 24th Ann. Symp. Foundations of Computer Science (FOCS 1983), pp. 185–194. IEEE Comp. Soc. Press, Los Alamitos (1983)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2006 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bouyer, P., Markey, N., Reynier, PA. (2006). Robust Model-Checking of Linear-Time Properties in Timed Automata. In: Correa, J.R., Hevia, A., Kiwi, M. (eds) LATIN 2006: Theoretical Informatics. LATIN 2006. Lecture Notes in Computer Science, vol 3887. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11682462_25
Download citation
DOI: https://doi.org/10.1007/11682462_25
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-32755-4
Online ISBN: 978-3-540-32756-1
eBook Packages: Computer ScienceComputer Science (R0)