文章基本信息

标题：Backward Reachability Analysis for Timed Automata with Data Variables
本地全文：下载
作者：Rebeka Farkas ; Tamás Tóth ; Ákos Hajdu 等
期刊名称：Electronic Communications of the EASST
电子版ISSN：1863-2122
出版年度：2019
卷号：76
页码：1-21
DOI：10.14279/tuj.eceasst.76.1076
出版社：European Association of Software Science and Technology (EASST)
摘要：Efficient techniques for reachability analysis of timed automata are zone-based methods that explore the reachable state space from the initial state, and SMT-based methods that perform backward search from the target states. It is also possible to perform backward exploration based on zones, but calculating predecessor states for systems with data variables is computationally expensive, prohibiting the successful application of this approach so far. In this paper we overcome this limitation by combining zone-based backward exploration with the weakest precondition operation for data variables. This combination allows us to handle diagonal constraints efficiently as opposed to zone-based forward search where most approaches require additional operations to ensure correctness. We demonstrate the applicability and compare the efficiency of the algorithm to existing forward exploration approaches by measurements performed on industrial case studies. Although the large number of states often prevents successful verification, we show that data variables can be efficienlty handled by the weakest precondition operation. This way our new approach complements existing techniques.
关键词：timed automata; reachability analysis; backward exploration; weakest precondition