Parametric Metric Interval Temporal Logic

We study an extension of the logic MITL with parametric constants. In particular, we define a logic, denoted PMITL (parametric MITL), where the subscripts of the temporal operators are intervals with possibly a parametric end-point. We consider typical decision problems, such as emptiness and universality of the set of parameter valuations under which a given parametric formula is satisfiable, or whether a given parametric timed automaton is a model of a given parametric formula. We show that when each parameter is used with a fixed polarity and only parameter valuations which evaluate parametric intervals to non-singular time intervals are taken into consideration, then the considered problems are decidable and EXPSPACE-complete. We also investigate the computational complexity of these problems for natural fragments of PMITL, and show that in meaningful fragments of the logic they are PSPACE-complete. Finally, we discuss other natural parameterizations of MITL, which indeed lead to undecidability.