Computing reachability relations in timed automata

被引：11
|
作者：
Dima, C [1 ]
机构：
[1] Verimag, F-38610 Gieres, France
来源：
17TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS | 2002年
关键词：
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 条
  • [21] Checking reachability properties for timed automata via SAT
    Wozna, B
    Zbrzezny, A
    Penczek, W
    FUNDAMENTA INFORMATICAE, 2003, 55 (02) : 223 - 241
  • [22] Lazy Reachability Checking for Timed Automata Using Interpolants
    Toth, Tamas
    Majzik, Istvan
    FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS (FORMATS 2017), 2017, 10419 : 264 - 280
  • [23] Improving Search Order for Reachability Testing in Timed Automata
    Herbreteau, Frederic
    Thanh-Tung Tran
    FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS (FORMATS 2015), 2015, 9268 : 124 - 139
  • [24] Backward Symbolic Optimal Reachability in Weighted Timed Automata
    Parrot, Remi
    Lime, Didier
    FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, FORMATS 2020, 2020, 12288 : 41 - 57
  • [25] Reachability Preservation Based Parameter Synthesis for Timed Automata
    Andre, Etienne
    Lipari, Giuseppe
    Hoang Gia Nguyen
    Sun, Youcheng
    NASA FORMAL METHODS (NFM 2015), 2015, 9058 : 50 - 65
  • [26] Reachability results for timed automata with unbounded data structures
    Lanotte, Ruggero
    Maggiolo-Schettini, Andrea
    Troina, Angelo
    ACTA INFORMATICA, 2010, 47 (5-6) : 279 - 311
  • [27] Reachability analysis for timed automata using partitioning algorithms
    Pólrola, A
    Penczek, W
    Szreter, M
    FUNDAMENTA INFORMATICAE, 2003, 55 (02) : 203 - 221
  • [28] Model checking via reachability testing for timed automata
    Aceto, L
    Burgueno, A
    Larsen, KG
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 1998, 1384 : 263 - 280
  • [29] Optimal reachability for multi-priced timed automata
    Larsen, Kim Guldstrand
    Rasmussen, Jacob Blum
    THEORETICAL COMPUTER SCIENCE, 2008, 390 (2-3) : 197 - 213
  • [30] Control synthesis for parametric timed automata under reachability
    Gol, Ebru A. Y. D. I. N.
    TURKISH JOURNAL OF ELECTRICAL ENGINEERING AND COMPUTER SCIENCES, 2021, 29 (03) : 1751 - 1764
12345