Parametric metric interval temporal logic

In this paper we focus on the role of parametric constants in real-time temporal logic and introduce the logic PMITL as a parametric extension of MITL. For this logic, we study decision problems which are the analogues of satisfiability, validity and model-checking problems for non-parametric temporal logic. We impose some restrictions on the use of the parameters: each parameter is used with a fixed polarity, parameters can appear only in one of the endpoints of the intervals, parametric linear expressions can be used only as right endpoints of the intervals. We show that, for parameter valuations yielding only non-singular intervals, the considered problems are all decidable and Expspace-complete, such as for the decision problems in MITL. Moreover, we show that if we relax any of the imposed restrictions, the problems become undecidable. We also investigate the computational complexity of these problems for natural fragments of PMITL, and show that for some meaningful fragments they can be solved in polynomial space and are Pspace-complete. Finally, we consider the decision problem of determining the truth of first-order queries over PMITL formulas where the parameters are used as variables that can be existentially or universally quantified. We solve this problem in several cases and exhibit an exponential-space algorithm.