In an influential paper titled "The Benefits of Relaxing
Punctuality" (JACM 1996), Alur, Feder, and Henzinger introduced
Metric Interval Temporal Logic (MITL) as a fragment of the
real-time logic Metric Temporal Logic (MTL) in which exact or
punctual timing constraints are banned. Their main result showed that
model checking and satisfiability for MITL are both
Until recently, it was widely believed that admitting even the simplest punctual specifications in any linear-time temporal logic would automatically lead to undecidability. Although this was recently disproved, until now no punctual fragment of MTL was known to have even primitive recursive complexity (with certain decidable fragments having provably non-primitive recursive complexity).
In this paper we identify a 'co-flat' subset of MTL that is capable of expressing a large class of punctual specifications and for which model checking (although not satisfiability) has no complexity cost over MITL. Our logic is moreover qualitatively different from MITL in that it can express properties that are not timed-regular. Correspondingly, our decision procedures do not involve translating formulas into finite-state automata, but rather into certain kinds of reversal-bounded Turing machines. Using this translation we show that the model checking problem for our logic is EXPSPACE-Complete.
Proceedings of LICS 07, 2007. 10 pages.
© 2007 IEEE Computer Society Press.