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

arXiv: https://arxiv.org/abs/1305.3204 · HTML: https://mlsanity.com/paper/1305.3204/

## Key facts

- Cited by 6 papers in the map (data through 14 Oct 2026).
- First posted on arXiv 14 May 2013.

## Built on by (most cited first, 6 of 6)

- [Learning a Large Neighborhood Search Algorithm for Mixed Integer Programs](https://mlsanity.com/paper/2107.10201/) (2021)
- [Efficient Global Robustness Certification of Neural Networks via Interleaving Twin-Network Encoding](https://mlsanity.com/paper/2203.14141/) (2022)
- [Guessing Winning Policies in LTL Synthesis by Semantic Learning](https://mlsanity.com/paper/2305.15109/) (2023)
- [Checking Trustworthiness of Probabilistic Computations in a Typed Natural Deduction System](https://mlsanity.com/paper/2206.12934/) (2022)
- [Monitoring ROS2: from Requirements to Autonomous Robots](https://mlsanity.com/paper/2209.14030/) (2022)
- [A Geometric Method for Improved Uncertainty Estimation in Real-time](https://mlsanity.com/paper/2206.11562/) (2022)

## Abstract (arXiv)

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.