The Unary Fragments of Metric Interval Temporal Logic: Bounded versus Lower bound Constraints (Full Version)
Abstract
We study two unary fragments of the well-known metric interval temporal logic MITL[U_I,S_I] 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[F_b,P_b] having unary modalities with only bounded intervals has \nexptime-complete satisfiability. But strangely, MITL[F_b,P_b] 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.
Keywords
Cite
@article{arxiv.1305.3204,
title = {The Unary Fragments of Metric Interval Temporal Logic: Bounded versus Lower bound Constraints (Full Version)},
author = {Paritosh K. Pandya and Simoni S. Shah},
journal= {arXiv preprint arXiv:1305.3204},
year = {2013}
}
Comments
Presented at ATVA, 2012