On unary fragments of MTL and TPTL over timed words

Abstract

Real time logics such as Metric Temporal Logic, MTL and Timed Propositional Temporal Logic (TPTL) exhibit considerable diversity in expressiveness and decidability properties based on the permitted set of modalities, the nature of time interval constraints and restriction on models. We study the expressiveness and decidability properties of various unary fragments of MTL incorporating strict as well as non-strict modalities. We show that, from the point of view of expressive power, (Formula Presented), in pointwise semantics. We also sharpen the decidability results by showing that, in the pointwise semantics, (Formula Presented) (which is the least expressive amongst the unary fragments considered) already has non-primitive-recursive complexity and is (Formula Presented)-hard for satisfiability checking over finite timed words, and that (Formula Presented) is undecidable and (Formula Presented)-hard. Next we explore, in the pointwise models, the decidability of (Formula Presented) (unary TPTL) and show that 2-variables unary TPTL has undecidable satisfiability, while the single variable fragment (Formula Presented) incorporating even the most expressive operator Usoperator is decidable over finite timed words. We provide a comprehensive picture of the decidability and expressiveness properties of unary fragments of TPTL and MTL over pointwise time.