The Cost of Punctuality

In an influential paper titled “The Benefits of Relaxing Punctuality” [2], 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. Ou...

• Type: Conference
• Year: 2007
• Where: LICS
• Authors: Patricia Bouyer, Nicolas Markey, Joël Ouaknine, James Worrell
• Keywords: Computer Science, LICS 2007, Model Checking, Punctual, Temporal Logic