Nicolas Markey

Résumé

In an influential paper titled "The Benefits of Relaxing Punctuality", 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, and is even PSPACE-Complete if timing constraints are encoded in unary.

@inproceedings{lics2007-BMOW,
  author =              {Bouyer, Patricia and Markey, Nicolas and Ouaknine,
                         Jo{\"e}l and Worrell, James},
  title =               {The Cost of Punctuality},
  booktitle =           {{P}roceedings of the 22nd {A}nnual {S}ymposium on
                         {L}ogic in {C}omputer {S}cience ({LICS}'07)},
  acronym =             {{LICS}'07},
  publisher =           {IEEE Comp. Soc. Press},
  pages =               {109-118},
  year =                {2007},
  month =               jul,
  doi =                 {10.1109/LICS.2007.49},
  abstract =            {In an influential paper titled {"}The Benefits of
                         Relaxing Punctuality{"}, 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.\par 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).\par 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, and is even
                         PSPACE-Complete if timing constraints are encoded in
                         unary.},
}