Metric temporal logic (MTL) is one of the most prominent specification
formalisms for real-time systems. Over infinite timed words, full MTL
is undecidable, but satisfiability for a syntactially defined safety
fragment, called safety MTL, was proved decidable several years
ago. Satisfiability for safety MTL is also known to be equivalent to a
fair termination problem for a class of channel machines with
insertion errors. However, hitherto its precise computational
complexity has remained elusive, with only a non-elementary lower
bound.
Via another equivalent problem, namely termination for a class of
rational relations, we show that satisfiability for safety MTL is
ACKERMANN-complete, i.e., among the easiest non-primitive recursive
problems. This is surprising since decidability was originally
established using Higman's Lemma, suggesting a much higher
non-multiply recursive complexity.
ACM TOCL 17(3), 2016. 27 pages.
PDF
© 2016 ACM.