Zeno, Hercules and the Hydra: Safety Metric Temporal Logic is ACKERMANN-complete

Ranko Lazic, Joël Ouaknine, and James Worrell

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.

Imprint / Data Protection