Reachability results for timed automata with unbounded data structures

被引：2
|
作者：
Lanotte, Ruggero [1 ]
Maggiolo-Schettini, Andrea [2 ]
Troina, Angelo [3 ]
机构：
[1] Univ Insubria, Dipartimento Informat & Comunicaz, I-22100 Como, Italy
[2] Univ Pisa, Dipartimento Informat, I-56127 Pisa, Italy
[3] Univ Turin, Dipartimento Informat, I-10149 Turin, Italy
来源：
ACTA INFORMATICA | 2010年 / 47卷 / 5-6期
关键词：
VERIFICATION; PROTOCOLS; SYSTEMS;
D O I：
10.1007/s00236-010-0121-8
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
Systems of Data Management Timed Automata (SDMTAs) are networks of communicating timed automata with structures to store messages and functions to manipulate them. We prove the decidability of the reachability problem for a subclass of SDMTAs which assumes an unbounded knowledge, and we analyze the expressiveness of the model and the considered subclass. In particular, while SDMTAs can simulate a Turing machine, and hence the reachability problem is in general undecidable, the subclass for which reachability is decidable, when endowed with a concept of recognized language, accepts languages that are not regular. As an application, we model and analyze a variation of the Yahalom protocol.
引用
收藏
页码：279 / 311
页数：33
相关论文
共 50 条
  • [1] Reachability results for timed automata with unbounded data structures
    Ruggero Lanotte
    Andrea Maggiolo-Schettini
    Angelo Troina
    [J]. Acta Informatica, 2010, 47 : 279 - 311
  • [2] VERIFICATION FOR TIMED AUTOMATA EXTENDED WITH UNBOUNDED DISCRETE DATA STRUCTURES
    Quaas, Karin
    [J]. LOGICAL METHODS IN COMPUTER SCIENCE, 2015, 11 (03)
  • [3] Revisiting Reachability in Timed Automata
    Quaas, Karin
    Shirmohammadi, Mahsa
    Worrell, James
    [J]. 2017 32ND ANNUAL ACM/IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE (LICS), 2017,
  • [4] Improved Undecidability Results for Reachability Games on Recursive Timed Automata
    Krishna, Shankara Narayanan
    Manasa, Lakshmi
    Trivedi, Ashutosh
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2014, (161): : 245 - 259
  • [5] Distributed reachability analysis in timed automata
    Behrmann G.
    [J]. International Journal on Software Tools for Technology Transfer, 2005, 7 (1) : 19 - 30
  • [6] Computing reachability relations in timed automata
    Dima, C
    [J]. 17TH ANNUAL IEEE SYMPOSIUM ON LOGIC IN COMPUTER SCIENCE, PROCEEDINGS, 2002, : 177 - 186
  • [7] The power of reachability testing for timed automata
    Aceto, L
    Bouyer, P
    Burgueño, A
    Larsen, KG
    [J]. FOUNDATIONS OF SOFTWARE TECHNOLOGY AND THEORETICAL COMPUTER SCIENCE, 1998, 1530 : 245 - 256
  • [8] Reachability relations of timed pushdown automata
    Clemente, Lorenzo
    Lasota, Slawomir
    [J]. JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 2021, 117 : 202 - 241
  • [9] Approximate reachability analysis of timed automata
    Balarin, F
    [J]. 17TH IEEE REAL-TIME SYSTEMS SYMPOSIUM, PROCEEDINGS, 1996, : 52 - 61
  • [10] Reachability Probabilities in Markovian Timed Automata
    Chen, Taolue
    Han, Tingting
    Katoen, Joost-Pieter
    Mereacre, Alexandru
    [J]. 2011 50TH IEEE CONFERENCE ON DECISION AND CONTROL AND EUROPEAN CONTROL CONFERENCE (CDC-ECC), 2011, : 7075 - 7080
12345