2013/05/27 by Madnani, Khushraj, Krishna, Shankara Narayanan, Pandya, Paritosh K.
#FOS: Computer and information sciences #Logic in Computer Science (cs.LO)
paper · doi:10.48550/arxiv.1305.6137
Metric Temporal Logic, \mtlfull is amongst the most studied real-time logics. It exhibits considerable diversity in expressiveness and decidability properties based on the permitted set of modalities and the nature of time interval constraints I. \oomitThe classical results of Alur and Henzinger showed that \mtlfull is undecidable where as \mitl which uses only non-singular intervals NS is decidable. In a surprizing result, Ouaknine and Worrell showed that the satisfiability of \mtl is decidable over finite pointwise models, albeit with NPR decision complexity, whereas it remains undecidable for infinite pointwise models or for continuous time. In this paper, we sharpen the decidability results by showing that the satisfiability of \mtlsns (where NS denotes non-singular intervals) is also decidable over finite pointwise strictly monotonic time. We give a satisfiability preserving reduction from the logic \mtlsns to decidable logic \mtl of Ouaknine and Worrell using the technique of temporal projections. We also investigate the decidability of unary fragment \mtlfullunary (a question posed by A. Rabinovich) and show that \mtlfut over continuous time as well as \mtlfullunary over finite pointwise time are both undecidable. Moreover, MTLpw[\futI] over finite pointwise models already has NPR lower bound for satisfiability checking. We also compare the expressive powers of some of these fragments using the technique of EF games for MTL.