论文标题
具有一个参数的两参数定时自动机中的可及性是expspace complete
Reachability in two-parametric timed automata with one parameter is EXPSPACE-complete
论文作者
论文摘要
参数定时自动机（PTA）是定时自动机的扩展，其中可以将时钟与参数进行比较。可及性问题要求将参数分配到非阴性整数中，以便在基础定时自动机中保持可及性。 PTA的可及性问题早已不可确定，已经超过了三个参数时钟。 几年前，Bundala和Ouaknine证明，对于两个参数时钟和一个参数，可及性问题是可以决定的，并且还显示了复杂性类Pspace^nexp的下限。我们的主要结果是，具有一个参数的两参数定时自动机的可及性问题是expspace complete。我们的贡献是两个方面。 对于Expspace下限，我们利用复杂性理论的深层结果，即Expspace的序列化表征（基于Barrington的定理），以及中文代表中数字的logspace翻译到二进制表示。 对于expspace上限，我们基于Bundala和Ouaknine引起的次要调整，在两个参数的一个参数Automata（POCA）上对PTA进行了仔细的指数时间缩短，一个参数单式自动机（POCA）在一个参数上逐渐减少了一个参数的一个参数次数。我们提供了一系列技术，将POCA的虚拟运行划分为几个精心选择的子集，使我们能够证明仅考虑指数级的参数值足够。这使我们能够在两个参数时钟和一个参数上显示PTA唯一参数的值的双指数上限。我们希望我们的技术的扩展最终导致使用两个参数时钟（并任意许多参数）在参数定时自动机中长期存在的可及性问题的确定性。
Parametric timed automata (PTA) are an extension of timed automata in which clocks can be compared against parameters. The reachability problem asks for the existence of an assignment of the parameters to the non-negative integers such that reachability holds in the underlying timed automaton. The reachability problem for PTA is long known to be undecidable, already over three parametric clocks. A few years ago, Bundala and Ouaknine proved that for PTA over two parametric clocks and one parameter the reachability problem is decidable and also showed a lower bound for the complexity class PSPACE^NEXP. Our main result is that the reachability problem for two-parametric timed automata with one parameter is EXPSPACE-complete. Our contribution is two-fold. For the EXPSPACE lower bound we make use of deep results from complexity theory, namely a serializability characterization of EXPSPACE (based on Barrington's Theorem) and a logspace translation of numbers in chinese remainder representation to binary representation. For the EXPSPACE upper bound, we give a careful exponential time reduction from PTA over two parametric clocks and one parameter to a slight subclass of parametric one-counter automata (POCA) over one parameter based on a minor adjustment of a construction due to Bundala and Ouaknine. We provide a series of techniques to partition a fictitious run of a POCA into several carefully chosen subruns that allow us to prove that it is sufficient to consider a parameter value of exponential magnitude only. This allows us to show a doubly-exponential upper bound on the value of the only parameter of a PTA over two parametric clocks and one parameter. We hope that extensions of our techniques lead to finally establishing decidability of the long-standing open problem of reachability in parametric timed automata with two parametric clocks (and arbitrarily many parameters).
