Abstract
We introduce the Clock-Aware Linear Temporal Logic (CA-LTL) for expressing linear time properties of timed automata, and show how to apply the standard automata-based approach of Vardi and Wolper to check for the validity of a CA-LTL formula over the continuous-time semantics of a timed automaton. Our model checking procedure employs zone-based abstraction and a new concept of the so called ultraregions. We also show that the Timed Büchi Automaton Emptiness problem is not the problem that the intended automata-based approach to CA-LTL model checking is reduced to. Finally, we give the necessary proofs of correctness, some hints for an efficient implementation, and preliminary experimental evaluation of our technique.
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.
Similar content being viewed by others
References
Clarke, E., Grumberg, O., Peled, D.: Model Checking. MIT Press (1999)
Alur, R., Dill, D.L.: A Theory of Timed Automata. Theor. Comput. Sci. 126(2), 183–235 (1994)
Daws, C., Tripakis, S.: Model Checking of Real-Time Reachability Properties Using Abstractions. In: Steffen, B. (ed.) TACAS 1998. LNCS, vol. 1384, pp. 313–329. Springer, Heidelberg (1998)
Behrmann, G., David, A., Larsen, K.G., Müller, O., Pettersson, P., Yi, W.: Uppaal - present and future. In: Proc. of 40th IEEE Conference on Decision and Control. IEEE Computer Society Press (2001)
Tripakis, S.: Checking timed Büchi Automata Emptiness on Simulation Graphs. TOCL 10(3) (2009)
Li, G.: Checking Timed Büchi Automata Emptiness Using LU-Abstractions. In: Ouaknine, J., Vaandrager, F.W. (eds.) FORMATS 2009. LNCS, vol. 5813, pp. 228–242. Springer, Heidelberg (2009)
Laarman, A., Olesen, M.C., Dalsgaard, A.E., Larsen, K.G., van de Pol, J.: Multi-core Emptiness Checking of Timed Büchi Automata Using Inclusion Abstraction. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 968–983. Springer, Heidelberg (2013)
Vardi, M., Wolper, P.: An automata-theoretic approach to automatic program verification (preliminary report). In: Proceedings, Symposium on Logic in Computer Science (LICS 1986), pp. 332–344. IEEE Computer Society (1986)
Bezděk, P., Beneš, N., Havel, V., Barnat, J., Černá, I.: On clock-aware ltl properties of timed automata. Technical report FIMU-RS-2014-04, Faculty of Informatics, Masaryk University, Brno (2014)
Alur, R., Henzinger, T.A.: A really temporal logic. Journal of the ACM (JACM) 41(1), 181–203 (1994)
Koymans, R.: Specifying real-time properties with metric temporal logic. Real-time Systems 2(4), 255–299 (1990)
Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43(1), 116–146 (1996)
Ostroff, J.S.: Temporal logic for real-time systems, vol. 40. Cambridge Univ. Press (1989)
Harel, E., Lichtenstein, O., Pnueli, A.: Explicit clock temporal logic. In: Proceedings of the Fifth Annual IEEE Symposium on e Logic in Computer Science, LICS 1990, pp. 402–413. IEEE (1990)
Demri, S., D‘Souza, D.: An automata-theoretic approach to constraint LTL. Information and Computation 205(3), 380–415 (2007)
Li, G., Tang, Z.: Modelling real-time systems with continuous-time temporal logic. In: George, C.W., Miao, H. (eds.) ICFEM 2002. LNCS, vol. 2495, pp. 231–236. Springer, Heidelberg (2002)
Alur, R., Madhusudan, P.: Decision problems for timed automata: A survey. In: Bernardo, M., Corradini, F. (eds.) SFM-RT 2004. LNCS, vol. 3185, pp. 1–24. Springer, Heidelberg (2004)
Baier, C., Katoen, J.P.: Principles of Model Checking. Representation and Mind Series. The MIT Press (2008)
Alur, R., Courcoubetis, C., Dill, D.: Model-checking for real-time systems. In: Proceedings of the Fifth Annual IEEE Symposium on e Logic in Computer Science, LICS 1990, pp. 414–425. IEEE (1990)
Tripakis, S.: Checking timed Büchi automata emptiness on simulation graphs. ACM Transactions on Computational Logic (TOCL) 10(3), 15 (2009)
Dill, D.L.: Timing assumptions and verification of finite-state concurrent systems. In: Automatic Verification Methods for Finite State Systems, pp. 197–212. Springer (1990)
Bengtsson, J.E., Yi, W.: Timed automata: Semantics, algorithms and tools. In: Desel, J., Reisig, W., Rozenberg, G. (eds.) Lectures on Concurrency and Petri Nets. LNCS, vol. 3098, pp. 87–124. Springer, Heidelberg (2004)
Pettersson, P.: Modelling and verification of real-time systems using timed automata: theory and practice, Citeseer (1999)
Bouyer, P.: Forward analysis of updatable timed automata. Formal Methods in System Design 24(3), 281–320 (2004)
Herbreteau, F., Srivathsan, B., Walukiewicz, I.: Efficient Emptiness Check for Timed Büchi Automata (Extended version). CoRR abs/1104.1540 (2011)
Tripakis, S., Yovine, S.: Analysis of timed systems using time-abstracting bisimulations. Formal Methods in System Design 18(1), 25–68 (2001)
Barnat, J., Brim, L., Havel, V., Havlíček, J., Kriho, J., Lenčo, M., Ročkai, P., Štill, V., Weiser, J.: DiVinE 3.0 – An Explicit-State Model Checker for Multithreaded C & C++ Programs. In: Sharygina, N., Veith, H. (eds.) CAV 2013. LNCS, vol. 8044, pp. 863–868. Springer, Heidelberg (2013)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Bezděk, P., Beneš, N., Havel, V., Barnat, J., Černá, I. (2014). On Clock-Aware LTL Properties of Timed Automata. In: Ciobanu, G., Méry, D. (eds) Theoretical Aspects of Computing – ICTAC 2014. ICTAC 2014. Lecture Notes in Computer Science, vol 8687. Springer, Cham. https://doi.org/10.1007/978-3-319-10882-7_4
Download citation
DOI: https://doi.org/10.1007/978-3-319-10882-7_4
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-10881-0
Online ISBN: 978-3-319-10882-7
eBook Packages: Computer ScienceComputer Science (R0)