Computing reachability relations in timed automata

被引:11
|
作者
Dima, C [1 ]
机构
[1] Verimag, F-38610 Gieres, France
关键词
D O I
10.1109/LICS.2002.1029827
中图分类号
TP31 [计算机软件];
学科分类号
081202 ; 0835 ;
摘要
We give an algorithmic calculus of the reachability relations on clock values defined by timed automata. Our approach is a modular one, by computing unions, compositions and reflexive-transitive closure (star) of "atomic" relations. The essential tool is a new representation technique for n-clock relations - the 2n-automata - and our strategy is to show the closure under union, composition and star of the class of 2n-automata that represent reachability relations in timed automata.
引用
下载
收藏
页码:177 / 186
页数:10
相关论文
共 50 条
  • [31] A Refined Algorithm for Reachability Analysis of Updatable Timed Automata
    Fang, Bingbing
    Li, Guoqiang
    Fang, Ling
    Xiang, Jianwen
    2015 IEEE INTERNATIONAL CONFERENCE ON SOFTWARE QUALITY, RELIABILITY AND SECURITY - COMPANION (QRS-C 2015), 2015, : 230 - 236
  • [32] Configuration reachability analysis of synchronized recursive timed automata
    Uezato Y.
    Minamide Y.
    2018, Japan Society for Software Science and Technology (35) : 140 - 168
  • [33] Pareto Optimal Reachability Analysis for Simple Priced Timed Automata
    Zhang, Zhengkui
    Nielsen, Brian
    Larsen, Kim Guldstrand
    Nies, Gilles
    Stenger, Marvin
    Hermanns, Holger
    FORMAL METHODS AND SOFTWARE ENGINEERING, ICFEM 2017, 2017, 10610 : 481 - 495
  • [34] Robust Reachability in Timed Automata: A Game-Based Approach
    Bouyer, Patricia
    Markey, Nicolas
    Sankur, Ocan
    AUTOMATA, LANGUAGES, AND PROGRAMMING, ICALP 2012, PT II, 2012, 7392 : 128 - 140
  • [35] Reachability-time games on timed automata - (Extended abstract)
    Jurdzinski, Marcin
    Trivedi, Ashutosh
    AUTOMATA, LANGUAGES AND PROGRAMMING, PROCEEDINGS, 2007, 4596 : 838 - +
  • [36] Pushdown timed automata: a binary reachability characterization and safety verification
    Zhe, D
    THEORETICAL COMPUTER SCIENCE, 2003, 302 (1-3) : 93 - 121
  • [37] Optimal-reachability and control for acyclic weighted timed automata
    La Torre, Salvatore
    Mukhopadhyay, Supratik
    Murano, Aniello
    IFIP Advances in Information and Communication Technology, 2002, 96 : 485 - 497
  • [38] Revisiting Bounded Reachability Analysis of Timed Automata Based on MILP
    Ober, Iulian
    FORMAL METHODS FOR INDUSTRIAL CRITICAL SYSTEMS, FMICS 2018, 2018, 11119 : 269 - 283
  • [39] Improvements in SAT-based reachability analysis for timed automata
    Zbrzezny, A
    FUNDAMENTA INFORMATICAE, 2004, 60 (1-4) : 417 - 434
  • [40] Optimal-reachability and control for acyclic weighted timed automata
    La Torre, S
    Mukhopadhyay, S
    Murano, A
    FOUNDATIONS OF INFORMATION TECHNOLOGY IN THE ERA OF NETWORK AND MOBILE COMPUTING, 2002, 96 : 485 - 497