Revisiting Decidability and Optimum Reachability for Multi-Priced Timed Automata
Revisiting Decidability and Optimum Reachability for Multi-Priced Timed Automata
复制标题
重新审视多价定时自动机的可判定性和最佳可达性
DOI：
--
复制
发表时间：
2009
期刊：
影响因子：
--
通讯作者：
M. Swaminathan
中科院分区：
文献类型：
--
作者：
M. Fränzle;M. Swaminathan
我们研究了多价定时自动机（MPTA）的最佳可达性问题，它承认边缘和位置的正成本和负成本，从而缩小了 Bouyer 等人的结果之间的差距。 （2007）以及拉森和拉斯穆森（2008）。我们的贡献如下：（1）我们表明，即使是具有正成本和负成本的 MPTA 也无法解决位置可达性问题，前提是成本受到有限预算的影响，即运行上超出预算的底层多价转换系统 (MPTS) 的路径被认为是不可行的。这种不可判定性结果源自使用此类 MPTA 的秒表自动机编码，并且适用于具有少至两个成本变量的 MPTA，甚至在获取边缘时不产生任何成本时也是如此。 (2) 然后，我们限制 MPTA，使得底层 MPTS 的每个可行的准循环路径都会产生最小的绝对成本。在这种情况下，位置可达性问题被证明是可判定的，并且对于具有正成本和负成本以及有界预算的 MPTA 来说，最优成本是可计算的。这些结果源自将最佳可达性问题简化为线性约束系统的解，该线性约束系统表示有限数量的有界长度的可行路径上的路径条件。
We investigate the optimum reachability problem for Multi-Priced Timed Automata (MPTA) that admit both positive and negative costs on edges and locations, thus bridging the gap between the results of Bouyer et al. (2007) and of Larsen and Rasmussen (2008). Our contributions are the following: (1) We show that even the location reachability problem is undecidable for MPTA equipped with both positive and negative costs, provided the costs are subject to a bounded budget, in the sense that paths of the underlying Multi-Priced Transition System (MPTS) that operationally exceed the budget are considered as not being viable. This undecidability result follows from an encoding of Stop-Watch Automata using such MPTA, and applies to MPTA with as few as two cost variables, and even when no costs are incurred upon taking edges. (2) We then restrict the MPTA such that each viable quasi-cyclic path of the underlying MPTS incurs a minimum absolute cost. Under such a condition, the location reachability problem is shown to be decidable and the optimum cost is shown to be computable for MPTA with positive and negative costs and a bounded budget. These results follow from a reduction of the optimum reachability problem to the solution of a linear constraint system representing the path conditions over a finite number of viable paths of bounded length.