Verification of continuous dynamical systems by timed automata

被引：0
|
作者：
Christoffer Sloth
Rafael Wisniewski
机构：
[1] Aalborg University,Department of Computer Science
[2] Aalborg University,Section for Automation & Control
来源：
Formal Methods in System Design | 2011年 / 39卷
关键词：
Timed automata; Verification; Reachability; Lyapunov functions;
D O I：
暂无
中图分类号：
学科分类号：
摘要：
This paper presents a method for abstracting continuous dynamical systems by timed automata. The abstraction is based on partitioning the state space of a dynamical system using positive invariant sets, which form cells that represent locations of a timed automaton. The abstraction is intended to enable formal verification of temporal properties of dynamical systems without simulating any system trajectory, which is currently not possible. Therefore, conditions for obtaining sound, complete, and refinable abstractions are set up.
引用
收藏
页码：47 / 82
页数：35
相关论文
共 50 条
  • [21] Timed-automata abstraction of switched dynamical systems using control invariants
    Bouyer, Patricia
    Markey, Nicolas
    Perrin, Nicolas
    Schlehuber-Caissier, Philipp
    REAL-TIME SYSTEMS, 2017, 53 (03) : 327 - 353
  • [22] Timed-Automata Abstraction of Switched Dynamical Systems Using Control Funnels
    Bouyer, Patricia
    Markey, Nicolas
    Perrin, Nicolas
    Schlehuber-Caissier, Philipp
    FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS (FORMATS 2015), 2015, 9268 : 60 - 75
  • [23] Past pushdown timed automata and safety verification
    Dang, Z
    Bultan, T
    Ibarra, OH
    Kemmerer, RA
    THEORETICAL COMPUTER SCIENCE, 2004, 313 (01) : 57 - 71
  • [24] Static guard analysis in timed automata verification
    Behrmann, G
    Bouyer, P
    Fleury, E
    Larsen, KG
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS, 2003, 2619 : 254 - 270
  • [25] Verification of computation Orchestration via timed automata
    Dong, Jin Song
    Liu, Yang
    Sun, Jun
    Zhang, Xian
    Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics), 2006, 4260 LNCS : 226 - 245
  • [26] Timed Opacity Verification for Switching Output Automata
    Liu, T.
    Seatzu, C.
    Giva, A.
    IFAC PAPERSONLINE, 2024, 58 (01): : 24 - 29
  • [27] Stochastic Games for Verification of Probabilistic Timed Automata
    Kwiatkowska, Marta
    Norman, Gethin
    Parker, David
    FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, PROCEEDINGS, 2009, 5813 : 212 - 227
  • [28] Verification of RabbitMQ with Kerberos Using Timed Automata
    Li, Ran
    Yin, Jiaqi
    Zhu, Huibiao
    Phan Cong Vinh
    MOBILE NETWORKS & APPLICATIONS, 2022, 27 (05): : 2049 - 2067
  • [29] Verification of AUTOSAR Software Architectures with Timed Automata
    Beringer, Steffen
    Wehrheim, Heike
    CRITICAL SYSTEMS: FORMAL METHODS AND AUTOMATED VERIFICATION, 2016, 9933 : 189 - 204
  • [30] Mechanical verification of timed automata: A case study
    Archer, M
    Heitmeyer, C
    1996 IEEE REAL-TIME TECHNOLOGY AND APPLICATIONS SYMPOSIUM, PROCEEDINGS, 1996, : 192 - 203
12345