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
EXPSPACE-Complete.
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.
PostScript /
PDF
© 2007 IEEE Computer Society Press.