We study timed systems in which some timing features are unknown parameters. Parametric timed automata (PTAs) are a classical formalism for such systems but for which most interesting problems are undecidable. Notably, the parametric reachability emptiness problem, i.e., the emptiness of the parameter valuations set allowing to reach some given discrete state, is undecidable. Lower-bound/upper-bound parametric timed automata (L/U-PTAs) achieve decidability for reachability properties by enforcing a separation of parameters used as upper bounds in the automaton constraints, and those used as lower bounds. In this paper, we first study reachability. We exhibit a subclass of PTAs (namely integer-points PTAs) with bounded rational-valued parameters for which the parametric reachability emptiness problem is decidable. Using this class, we present further results improving the boundary between decidability and undecidability for PTAs and their subclasses such as L/U-PTAs. We then study liveness. We prove that: (1) the existence of at least one parameter valuation for which there exists an infinite run in an L/U-PTA is PSPACE-complete; (2) the existence of a parameter valuation such that the system has a deadlock is however undecidable; (3) the problem of the existence of a valuation for which a run remains in a given set of locations exhibits a very thin border between decidability and undecidability.
翻译:我们研究一些时间性特征为未知参数的定时系统。 参数定时自动自动数据(PTAs)是这类系统的一种典型形式主义,但最有趣的问题是不可减退的。 值得注意的是, 偏差性可达性问题, 即设定的参数估值能够达到某种给定离散状态的参数值的空虚性是不可减退的。 受限制/ 上限参数定时自动数据( L/ U- PTAs) 达到可达性( 达标性) 的可达性( 达标性), 其方法是对作为自定义限制上限使用的参数和作为较低界限使用的参数进行区分。 在本文中, 我们首先研究可达性。 我们展示了具有约束性合理值参数的 PTA( 整数点 PTAs) 子类( 参数值的空虚度) 。 使用这一类,我们进一步展示了PTA( U) 及其子类( L- PTAs) 的不可变的不可变错性之间的界限和不可变错度 。 我们随后研究了LPPPA 的精确性参数的存在。