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 条
  • [1] Verification of continuous dynamical systems by timed automata
    Sloth, Christoffer
    Wisniewski, Rafael
    FORMAL METHODS IN SYSTEM DESIGN, 2011, 39 (01) : 47 - 82
  • [2] Abstraction of Dynamical Systems by Timed Automata
    Wisniewski, Rafael
    Sloth, Christoffer
    MODELING IDENTIFICATION AND CONTROL, 2011, 32 (02) : 79 - 90
  • [3] Approximating continuous systems by timed automata
    Maler, Oded
    Batt, Gregory
    FORMAL METHODS IN SYSTEMS BIOLOGY, 2008, 5054 : 77 - +
  • [4] Complete abstractions of dynamical systems by timed automata
    Sloth, Christoffer
    Wisniewski, Rafael
    NONLINEAR ANALYSIS-HYBRID SYSTEMS, 2013, 7 (01) : 80 - 100
  • [5] On the timed automata-based verification of Ravenscar systems
    Ober, Iulian
    Halbwachs, Nicolas
    RELIABLE SOFTWARE TECHNOLOGIES - ADA-EUROPE 2008, 2008, 5026 : 30 - +
  • [6] Dynamical properties of timed automata
    Puri, A
    FORMAL TECHNIQUES IN REAL-TIME AND FAULT-TOLERANT SYSTEMS, 1998, 1486 : 210 - 227
  • [7] Dynamical properties of timed automata
    Puri, A
    DISCRETE EVENT DYNAMIC SYSTEMS-THEORY AND APPLICATIONS, 2000, 10 (1-2): : 87 - 113
  • [8] Dynamical Properties of Timed Automata
    Anuj Puri
    Discrete Event Dynamic Systems, 2000, 10 : 87 - 113
  • [9] Dynamical properties of timed automata revisited
    Dima, Catalin
    FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, 2007, 4763 : 130 - 146
  • [10] Improvements for the symbolic verification of timed automata
    Yan, Rongjie
    Li, Guangyuan
    Zhang, Wenliang
    Peng, Yunquan
    FORMAL TECHNIQUES FOR NETWORKED AND DISTRIBUTED SYSTEMS - FORTE 2007, 2007, 4574 : 196 - +
12345