Safety metric temporal logic is fully decidable

Abstract. Metric Temporal Logic (MTL) is a widely-studied real-time extension of Linear Temporal Logic. In this paper we consider a frag-ment of MTL, called Safety MTL, capable of expressing properties such as invariance and time-bounded response. Our main result is that the satis ability problem for Safety MTL is decidable. This is the rst posi-tive decidability result for MTL over timed!-words that does not involve restricting the precision of the timing constraints, or the granularity of the semantics; the proof heavily uses the techniques of innite-state ver-i cation. Combining this result with some of our previous work, we con-clude that Safety MTL is fully decidable in that its satisability, model checking, and renement problems are all decidable.