Zeno, Hercules and the Hydra: Downward Rational Termination Is Ackermannian

Ranko Lazic ( University of Warwick )

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 its safety fragment was proved decidable several years ago by Ouaknine and Worrell. The problem is also known to be equivalent to a fair termination problem for a class of channel machines with insertion errors. However, the complexity has remained elusive, except for 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 not primitive recursive, yet is Ackermannian, i.e., among the simplest non-primitive recursive problems. This is surprising since decidability was originally established using Higman's Lemma, suggesting a much higher non-multiply recursive complexity.

This is joint work with Ouaknine and Worrell.