| Summary: | <p>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.</p> <br/> <p>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.</p>
|
|---|