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) 系统, 因此, 我们获取了我们的自动分析并测试系统。

0
下载
关闭预览

相关内容

iOS 8 提供的应用间和应用跟系统的功能交互特性。
  • Today (iOS and OS X): widgets for the Today view of Notification Center
  • Share (iOS and OS X): post content to web services or share content with others
  • Actions (iOS and OS X): app extensions to view or manipulate inside another app
  • Photo Editing (iOS): edit a photo or video in Apple's Photos app with extensions from a third-party apps
  • Finder Sync (OS X): remote file storage in the Finder with support for Finder content annotation
  • Storage Provider (iOS): an interface between files inside an app and other apps on a user's device
  • Custom Keyboard (iOS): system-wide alternative keyboards

Source: iOS 8 Extensions: Apple’s Plan for a Powerful App Ecosystem
【经典书】算法C语言实现,Algorithms in C. 672页pdf
专知会员服务
81+阅读 · 2020年8月13日
Linux导论,Introduction to Linux,96页ppt
专知会员服务
77+阅读 · 2020年7月26日
Fariz Darari简明《博弈论Game Theory》介绍,35页ppt
专知会员服务
109+阅读 · 2020年5月15日
已删除
将门创投
6+阅读 · 2019年1月11日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
【泡泡一分钟】ProbFlow:联合光流和不确定性估计
泡泡机器人SLAM
3+阅读 · 2018年10月26日
Arxiv
0+阅读 · 2021年7月20日
Arxiv
0+阅读 · 2021年7月16日
VIP会员
相关资讯
已删除
将门创投
6+阅读 · 2019年1月11日
A Technical Overview of AI & ML in 2018 & Trends for 2019
待字闺中
16+阅读 · 2018年12月24日
【泡泡一分钟】ProbFlow:联合光流和不确定性估计
泡泡机器人SLAM
3+阅读 · 2018年10月26日
Top
微信扫码咨询专知VIP会员