Abstract
Like most models used in model-checking, timed automata are an idealized mathematical model used for representing systems with strong timing requirements. In such mathematical models, properties can be violated, due to unlikely (sequences of) events. We propose two new semantics for the satisfaction of LTL formulas, one based on probabilities, and the other one based on topology, to rule out these sequences. We prove that the two semantics are equivalent and lead to a PSPACE-Complete model-checking problem for LTL over finite executions.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Alur, R., Courcoubetis, C., Dill, D.: Model-checking for probabilistic real-time systems. In: Leach Albert, J., Monien, B., Rodríguez-Artalejo, M. (eds.) Automata, Languages and Programming. LNCS, vol. 510, pp. 115–126. Springer, Heidelberg (1991)
Alur, R., Courcoubetis, C., Dill, D.: Verifying automata specifications of probabilistic real-time systems. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) Real-Time: Theory in Practice. LNCS, vol. 600, pp. 28–44. Springer, Heidelberg (1992)
Alur, R., Dill, D.: A theory of timed automata. Theoretical Comp. Sci. 126(2), 183–235 (1994)
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)
Baier, C., Bertrand, N., Bouyer, P., Brihaye, Th., Größer, M.: Probabilistic and topological semantics for timed automata. Research Report LSV–07–26, LSV, ENS de Cachan, France (2007)
Bouyer, P., Markey, N., Reynier, P.-A.: Robust model-checking of timed automata. In: Correa, J.R., Hevia, A., Kiwi, M. (eds.) LATIN 2006. LNCS, vol. 3887, pp. 238–249. Springer, Heidelberg (2006)
De Wulf, M., Doyen, L., Markey, N., Raskin, J.-F.: Robustness and implementability of timed automata. In: Lakhnech, Y., Yovine, S. (eds.) FORMATS 2004 and FTRTFT 2004. LNCS, vol. 3253, pp. 118–133. Springer, Heidelberg (2004)
De Wulf, M., Doyen, L., Raskin, J.-F.: Almost ASAP semantics: From timed models to timed implementations. In: Alur, R., Pappas, G.J. (eds.) HSCC 2004. LNCS, vol. 2993, pp. 296–310. Springer, Heidelberg (2004)
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)
Henzinger, Th.A., Majumdar, R., Raskin, J.-F.: A classification of symbolic transition systems. ACM Transactions on Computational Logic 6(1), 1–32 (2005)
Henzinger, Th.A., Raskin, J.-F.: Robust undecidability of timed and hybrid systems. In: Lynch, N.A., Krogh, B.H. (eds.) HSCC 2000. LNCS, vol. 1790, pp. 145–159. Springer, Heidelberg (2000)
Munkres, J.R.: Topology, 2nd edn. Prentice-Hall, Englewood Cliffs (2000)
Oxtoby, J.C.: The Banach-Mazur game and Banach category theorem. Annals of Mathematical Studies 39, 159–163 (1957)
Pnueli, A.: The temporal logic of programs. In: Proc. 18th Ann. Symp. Foundations of Computer Science (FOCS 1977), pp. 46–57. IEEE Comp. Soc. Press, Los Alamitos (1977)
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)
Sproston, J.: Model checking for probabilistic timed systems. In: Baier, C., Haverkort, B., Hermanns, H., Katoen, J.-P., Siegle, M. (eds.) Validation of Stochastic Systems. LNCS, vol. 2925, pp. 189–229. Springer, Heidelberg (2004)
Varacca, D., Völzer, H.: Temporal logics and model checking for fairly correct systems. In: Varacca, D. (ed.) Proc. 21st Ann. Symp. Logic in Computer Science (LICS 2006), pp. 389–398. IEEE Comp. Soc. Press, Los Alamitos (2006)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2007 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Baier, C., Bertrand, N., Bouyer, P., Brihaye, T., Größer, M. (2007). Probabilistic and Topological Semantics for Timed Automata. In: Arvind, V., Prasad, S. (eds) FSTTCS 2007: Foundations of Software Technology and Theoretical Computer Science. FSTTCS 2007. Lecture Notes in Computer Science, vol 4855. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-77050-3_15
Download citation
DOI: https://doi.org/10.1007/978-3-540-77050-3_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-77049-7
Online ISBN: 978-3-540-77050-3
eBook Packages: Computer ScienceComputer Science (R0)