  Metric Interval Temporal Logic (MITL) is a well studied real-time, temporal
logic that has decidable satisfiability and model checking problems. The
decision procedures for MITL rely on the automata theoretic approach, where
logic formulas are translated into equivalent timed automata. Since timed
automata are not closed under complementation, decision procedures for MITL
first convert a formula into negated normal form before translating to a timed
automaton. We show that, unfortunately, these 20-year-old procedures are
incorrect, because they rely on an incorrect semantics of the R operator. We
present the right semantics of R and give new, correct decision procedures for
MITL. We show that both satisfiability and model checking for MITL are
EXPSPACE-complete, as was previously claimed. We also identify a fragment of
MITL that we call MITL_{WI} that is richer than MITL_{0,\infty}, for which we
show that both satisfiability and model checking are PSPACE-complete. Many of
our results have been formally proved in PVS.
