论文标题
参数定时自动机的可及性和可笑性
Reachability and liveness in parametric timed automata
论文作者
论文摘要
我们研究一些定时特征是未知参数的定时系统。参数定时自动机（PTA）是此类系统的古典形式，但最有趣的问题是不可确定的。值得注意的是，参数可达性空虚问题，即允许达到某些离散状态的参数估值的空虚是无法确定的。下限/上限参数定时自动机（L/U-PTA）通过执行自动机约束中用作上限的参数的分离以及用作下限的参数来实现可及性属性。 在本文中，我们首先研究可达性。我们展示了PTA的子类（即整数PTA），其中有有界的有理值参数，该参数可及性问题是可以决定的。使用此类别，我们提出了进一步的结果，以改善PTA及其子类（例如L/U-PTAS）之间的可决定性和不确定性之间的边界。 然后，我们研究LIVENICE。我们证明： （1）确定在L/U-PTA中存在无限运行的至少一个参数估值的存在是Pspace-complete； （2）存在参数估值，使系统的僵局是不可决定的； （3）存在估值的问题，该估值在给定的位置中保持运行的问题表现出可决定性和不确定性之间非常薄的边界。
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.
