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) deciding 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) 达到可达性特征的可变性, 其方法是对作为自定义限制上限使用的参数和作为较低界限使用的参数进行分离。 在本文中, 我们首先研究可达性问题。 我们展示了一个具有约束性合理值参数的 PTAs( 指整数点 PTAs) 子类( 参数的空闲置值) 。 使用这一类, 我们进一步展示了PTAs及其子类( 如L/ U- PTAs ) 的不可变性与不可变的不可变性之间界线之间的界限。 我们随后研究一个运行性参数 。