Given the versatility of timed automata a huge body of work has evolved that considers extensions of timed automata. One extension that has received a lot of interest is timed automata with a, possibly unbounded, stack, also called the pushdown timed automata (PDTA) model. While different algorithms have been given for reachability in different variants of this model, most of these results are purely theoretical and do not give rise to efficient implementations. One main reason for this is that none of these algorithms (and the implementations that exist) use the so-called zone-based abstraction, but rely either on the region-abstraction or other approaches, which are significantly harder to implement. In this paper, we show that a naive extension using simulations of the zone based reachability algorithm for the control state reachability problem of timed automata is not sound in the presence of a stack. To understand this better we give an inductive rule based view of the zone reachability algorithm for timed automata. This alternate view allows us to analyze and adapt the rules to also work for pushdown timed automata. We obtain the first zone-based algorithm for PDTA which is terminating, sound and complete. We implement our algorithm in the tool TChecker and perform experiments to show its efficacy, thus leading the way for more practical approaches to the verification of pushdown timed systems.
翻译:根据时间自动自动数据(PDTA) 的多功能性, 一个巨大的工作体已经演变成一个考虑时间自动数据扩展的庞大工作体。 一个兴趣很大的扩展是时间自动数据(Automata), 以及一个(可能没有约束的)堆叠, 也称为自定义数据(PDTA) 模式。 虽然在这个模型的不同变体中给出了不同的算法, 但大多数这些结果都是纯理论性的, 没有带来有效的执行。 其中一个主要原因是, 这些算法( 和现有的执行) 没有使用所谓的基于区域的抽象数据, 但却依赖区域吸附或其他方法, 而这些方法执行起来非常困难。 在本文件中, 我们显示, 使用基于区域的模拟的可达性算法来模拟这个模型的可控制状态问题, 多数是纯理论性的, 并且没有带来有效的执行。 要更好地了解这一点, 我们给出了基于区域可切换规则的基于时间的可达度算法( 以及现有的执行方法) 。 这个替代视图让我们能够分析并调整规则, 也很难执行区域- 将规则用于在关闭时间算法(DBDA) 系统, 因此, 我们获取了我们的自动分析并测试系统。