Abstract
Metric Temporal Logic (MTL) is a real-time extension of Linear Temporal Logic that was proposed fifteen years ago and has since been extensively studied. Since the early 1990s, it has been widely believed that some very small fragments of MTL are undecidable (i.e., have undecidable satisfiability and model-checking problems). We recently showed that, on the contrary, some substantial and important fragments of MTL are decidable [19,20]. However, until now the question of the decidability of full MTL over infinite timed words remained open.
In this paper, we settle the question negatively. The proof of undecidability relies on a surprisingly strong connection between MTL and a particular class of faulty Turing machines, namely ‘insertion channel machines with emptiness-testing’.
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
Abdulla, P., Jonsson, B.: Undecidable verification problems with unreliable channels. Inf. Comput. 130, 71–90 (1996)
Abdulla, P.A., Deneux, J., Ouaknine, J., Worrell, J.: Decidability and complexity results for timed automata via channel machines. In: Caires, L., Italiano, G.F., Monteiro, L., Palamidessi, C., Yung, M. (eds.) ICALP 2005. LNCS, vol. 3580, Springer, Heidelberg (2005)
Alur, R., Dill, D.: A theory of timed automata. Theor. Comput. Sci. 126, 183–235 (1994)
Alur, R., Feder, T., Henzinger, T.A.: The benefits of relaxing punctuality. J. ACM 43, 116–146 (1996)
Alur, R., Henzinger, T.A.: Logics and models of real time: A survey. In: Huizing, C., de Bakker, J.W., Rozenberg, G., de Roever, W.-P. (eds.) REX 1991. LNCS, vol. 600, Springer, Heidelberg (1992)
Alur, R., Henzinger, T.A.: Real-time logics: Complexity and expressiveness. Inf. Comput. 104, 35–77 (1993)
Alur, R., Henzinger, T.A.: A really temporal logic. J. ACM 41, 181–204 (1994)
Brand, D., Zafiropulo, P.: On communicating finite-state machines. J. ACM 30(2), 323–342 (1983)
Cécé, G., Finkel, A., Iyer, S.P.: Unreliable channels are easier to verify than perfect channels. Inf. Comput. 124, 20–31 (1996)
Finkel, A., Schnoebelen, P.: Well-structured transition systems everywhere! Theor. Comput. Sci. 256(1-2), 63–92 (2001)
Henzinger, T.A.: The Temporal Specification and Verification of Real-Time Systems. PhD thesis, Stanford University, Tech. rep. STAN-CS-91-1380 (1991)
Henzinger, T.A.: It’s about time: Real-time logics reviewed. In: Sangiorgi, D., de Simone, R. (eds.) CONCUR 1998. LNCS, vol. 1466, Springer, Heidelberg (1998)
Henzinger, T.A., Manna, Z., Pnueli, A.: What good are digital clocks? In: Kuich, W. (ed.) ICALP 1992. LNCS, vol. 623, Springer, Heidelberg (1992)
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, Springer, Heidelberg (1998)
Hirshfeld, Y., Rabinovich, A.: Logics for real time: Decidability and complexity. Fundam. Inform. 62(1), 1–28 (2004)
Koymans, R.: Specifying real-time properties with metric temporal logic. Real-time Systems 2(4), 255–299 (1990)
Lasota, S., Walukiewicz, I.: Personal communication (2005)
Lasota, S., Walukiewicz, I.: Alternating timed automata. In: Sassone, V. (ed.) FOSSACS 2005. LNCS, vol. 3441, Springer, Heidelberg (2005)
Ouaknine, J., Worrell, J.: On the decidability of metric temporal logic. In: Proc. LICS, IEEE Press, Los Alamitos (2005)
Ouaknine, J., Worrell, J.: Safety metric temporal logic is fully decidable (submitted 2005)
Raskin, J.-F., Schobbens, P.-Y.: State-clock logic: A decidable real-time logic. In: Maler, O. (ed.) HART 1997. LNCS, vol. 1201, Springer, Heidelberg (1997)
Schneider, K.: Verification of Reactive Systems. Springer, Heidelberg (1997)
Schnoebelen, P.: Verifying lossy channel systems has nonprimitive recursive complexity. Inf. Process. Lett. 83(5), 251–261 (2002)
Wilke, T.: Specifying timed state sequences in powerful decidable logics and timed automata. In: Langmaack, H., de Roever, W.-P., Vytopil, J. (eds.) FTRTFT 1994 and ProCoS 1994. LNCS, vol. 863, Springer, Heidelberg (1994)
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
Ouaknine, J., Worrell, J. (2006). On Metric Temporal Logic and Faulty Turing Machines. In: Aceto, L., Ingólfsdóttir, A. (eds) Foundations of Software Science and Computation Structures. FoSSaCS 2006. Lecture Notes in Computer Science, vol 3921. Springer, Berlin, Heidelberg. https://doi.org/10.1007/11690634_15
Download citation
DOI: https://doi.org/10.1007/11690634_15
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-33045-5
Online ISBN: 978-3-540-33046-2
eBook Packages: Computer ScienceComputer Science (R0)