LFCS Seminar

The Cost of Punctuality

Joel Ouaknine

Oxford University

4pm Tuesday 24th October 2006
Room 2511, JCMB, King's Buildings

---

Abstract

In an influential paper titled "The Benefits of Relaxing Punctuality" (JACM 1996), Alur, Feder, & Henzinger introduced the logic Metric Interval Temporal Logic (MITL), which is a fragment of the real-time logic Metric Temporal Logic (MTL) in which the time constraints on operators are not allowed to be punctual, i.e., singleton sets. They produced an intricate proof (11 pages) that MITL model checking and satisfiability are decidable - in fact EXPSPACE-COMPLETE. This has led to considerable further work; in the last year alone, both Hirshfeld & Rabinovich, and Maler, Nickovic, & Pnueli, published new and simpler decision procedures for MITL.

An obvious question to ask is, what happens if punctuality is allowed? Until recently, it was widely believed that the faintest presence of punctuality in any linear-time timed temporal logic would automatically lead to undecidability. Although this was recently disproved, until now no decidable punctual fragment of MTL was known to have even primitive recursive complexity (with certain fragments having provably non-primitive recursive complexity!).

Very recently, in joint work with Patricia Bouyer, Nicolas Markey, and James Worrell, we have been able to precisely pinpoint the complexity of the main decidable punctual fragments of MTL. Our complexity bounds involve a connection between MTL formulas and reversal-bounded Turing machines. We will present an overview of these results and how they relate to standard (untimed) verification.