Decision Problems for Lower/Upper Bound Parametric Timed Automata

摘要

We investigate a class of parametric timed automata, called lower bound/upper bound (L/U) automata, where each parameter occurs in the timing constraints either as a lower bound or as un upper bound. For such automata, we show that checking if for a parameter valuation (resp., all parameter valuations) there is an infinite accepting run is PsPACE-complete. We extend these results by allowing the specification of constraints on parameters as a linear system. We show that the considered decision problems are still PSPACE-complete, if the lower bound parameters are not compared to the upper bound parameters in the linear system, and are undecidable in general. Finally, we consider a parametric extension of MITL_o.∞, and prove that the related satisfiability and model checking (w.r.t. L/U automata) problems are PSPACE-complete.