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 [OW05,OW06]. 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'.
Proceedings of FOSSACS 06, LNCS 3921, 2006. 14 pages.
PostScript /
PDF
© 2006
Springer-Verlag.