Abstract
Metric Interval Temporal Logic (MITL) is a popular formalism for expressing real-time specifications. This logic achieves decidability by restricting the precision of timing constraints, in particular, by banning so-called punctual specifications. In this paper we introduce a significantly more expressive logic that can express a wide variety of punctual specifications, but whose model-checking problem has the same complexity as that of MITL. We conclude that for model checking the most commonly occurring specifications, such as invariance and bounded response, punctuality can be accommodated at no cost.
Access provided by Autonomous University of Puebla. Download to read the full chapter text
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Alur, R., Dill, D.: A theory of timed automata. TCS 126(2), 183–235 (1994)
Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. of the ACM 43(1), 116–146 (1996)
Alur, R., Henzinger, T.A.: Logics and models of real time: A survey. In: Real-Time: Theory in Practice, Proc. REX Workshop 1991. LNCS, vol. 600, pp. 74–106. Springer, Heidelberg (1992)
Alur, R., Henzinger, T.A.: Real-time logics: Complexity and expressiveness. Inf. & Comp. 104(1), 35–77 (1993)
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)
Bouyer, P., Markey, N., Ouaknine, J., Worrell, J.: The cost of punctuality. In: Proc. 22nd Ann. IEEE Symp. Logic in Computer Science (LICS 2007), pp. 109–118. IEEE, Los Alamitos (2007)
Comon, H., Cortier, V.: Flatness is not a weakness. In: Clote, P.G., Schwichtenberg, H. (eds.) CSL 2000. LNCS, vol. 1862, pp. 262–276. Springer, Heidelberg (2000)
Demri, S., Lazić, R., Nowak, D.: On the freeze quantifier in constraint LTL: Decidability and complexity. Inf. & Comp. 205(1), 2–24 (2007)
Henzinger, T.A.: It’s about time: Real-time logics reviewed. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, pp. 439–454. Springer, Heidelberg (1998)
Henzinger, T.A., Raskin, J.-F., Schobbens, P.-Y.: The regular real-time languages. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) ICALP 1998. LNCS, vol. 1443, pp. 580–591. Springer, Heidelberg (1998)
Hirshfeld, Y., Rabinovich, A.: Timer formulas and decidable metric temporal logic. Inf. & Comp. 198(2), 148–178 (2005)
Koymans, R.: Specifying real-time properties with metric temporal logic. Real-Time Systems 2(4), 255–299 (1990)
Lichtenstein, O., Pnueli, A., Zuck, L.D.: The glory of the past. In: Proc. Conference on Logics of Programs. LNCS, vol. 193, pp. 413–424. Springer, Heidelberg (1985)
Lutz, C., Walther, D., Wolter, F.: Quantitative temporal logics over the reals: PSPACE and below. Inf. & Comp. 205(1), 99–123 (2007)
Maler, O., Nickovic, D., Pnueli, A.: From MITL to timed automata. In: Asarin, E., Bouyer, P. (eds.) FORMATS 2006. LNCS, vol. 4202, pp. 274–289. Springer, Heidelberg (2006)
Ouaknine, J., Worrell, J.: On metric temporal logic and faulty Turing machines. In: Aceto, L., Ingólfsdóttir, A. (eds.) FOSSACS 2006 and ETAPS 2006. LNCS, vol. 3921, pp. 217–230. Springer, Heidelberg (2006)
Raskin, J.-F.: Logics, Automata and Classical Theories for Deciding Real-Time. PhD thesis, Université de Namur, Belgium (1999)
Reynolds, M.: The complexity of the temporal logic over the reals(submitted 2004)
Wolper, P.: Constructing automata from temporal logic formulas: A tutorial. In: European Educational Forum: School on Formal Methods and Performance Analysis. LNCS, vol. 2090, pp. 261–277. Springer, Heidelberg (2000)
Author information
Authors and Affiliations
Editor information
Rights and permissions
Copyright information
© 2008 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Bouyer, P., Markey, N., Ouaknine, J., Worrell, J. (2008). On Expressiveness and Complexity in Real-Time Model Checking. In: Aceto, L., Damgård, I., Goldberg, L.A., Halldórsson, M.M., Ingólfsdóttir, A., Walukiewicz, I. (eds) Automata, Languages and Programming. ICALP 2008. Lecture Notes in Computer Science, vol 5126. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-70583-3_11
Download citation
DOI: https://doi.org/10.1007/978-3-540-70583-3_11
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-70582-6
Online ISBN: 978-3-540-70583-3
eBook Packages: Computer ScienceComputer Science (R0)