On the Decidability and Complexity of Some Fragments of Metric Temporal\n Logic

Metric Temporal Logic, $\\mtlfull$ is amongst the most studied real-time\nlogics. It exhibits considerable diversity in expressiveness and decidability\nproperties based on the permitted set of modalities and the nature of time\ninterval constraints $I$. \\oomit{The classical results of Alur and Henzinger\nshowed that $\\mtlfull$ is undecidable where as $\\mitl$ which uses only\nnon-singular intervals $NS$ is decidable. In a surprizing result, Ouaknine and\nWorrell showed that the satisfiability of $\\mtl$ is decidable over finite\npointwise models, albeit with NPR decision complexity, whereas it remains\nundecidable for infinite pointwise models or for continuous time.} In this\npaper, we sharpen the decidability results by showing that the satisfiability\nof $\\mtlsns$ (where $NS$ denotes non-singular intervals) is also decidable over\nfinite pointwise strictly monotonic time. We give a satisfiability preserving\nreduction from the logic $\\mtlsns$ to decidable logic $\\mtl$ of Ouaknine and\nWorrell using the technique of temporal projections. We also investigate the\ndecidability of unary fragment $\\mtlfullunary$ (a question posed by A.\nRabinovich) and show that $\\mtlfut$ over continuous time as well as\n$\\mtlfullunary$ over finite pointwise time are both undecidable. Moreover,\n$\\mathsf{MTL}^{pw}[\\fut_I]$ over finite pointwise models already has NPR lower\nbound for satisfiability checking. We also compare the expressive powers of\nsome of these fragments using the technique of EF games for $\\mathsf{MTL}$.\n