The Unary Fragments of Metric Interval Temporal Logic: Bounded versus Lower bound Constraints (Full Version)

We study two unary fragments of the well-known metric interval temporal logic MITL[UI,SI] that was originally proposed by Alur and Henzinger, and we pin down their expressiveness as well as satisfaction complexities. We show that MITL[F_inf,P_inf] which has unary modalities with only lower-bound constraints is (surprisingly) expressively complete for Partially Ordered 2-Way Deterministic Timed Automata (po2DTA) and the reduction from logic to automaton gives us its NP-complete satisfiability. We also show that the fragment MITL[Fb,Pb] having unary modalities with only bounded intervals has nexptime-complete satisfiability. But strangely, MITL[Fb,Pb] is strictly less expressive than MITL[F_inf,P_inf]. We provide a comprehensive picture of the decidability and expressiveness of various unary fragments of MITL.