A geometric approach to bisimulation and verification of hybrid systems

被引:0
|
作者
Broucke, M [1 ]
机构
[1] Univ Calif Berkeley, Dept Elect Engn & Comp Sci, Berkeley, CA 94720 USA
来源
关键词
D O I
暂无
中图分类号
TP [自动化技术、计算机技术];
学科分类号
0812 ;
摘要
An approximate verification method for hybrid systems in which sets of the automaton are over-approximated, while leaving the vector fields intact, is presented. The method is based on a geometrically-inspired approach, using tangential and transversal foliations, to obtain bisimulations. Exterior differential systems provide a natural setting to obtain an analytical representation of the bisimulation, and to obtain the bisimulation under parallel composition. We define the symbolic execution theory and give applications to coordinated aircraft and robots.
引用
收藏
页码:61 / 75
页数:15
相关论文
共 50 条
  • [41] On the formal verification of hybrid systems
    Guéguen, H
    Zaytoon, J
    [J]. CONTROL ENGINEERING PRACTICE, 2004, 12 (10) : 1253 - 1267
  • [42] Dynamic verification of hybrid systems
    Pakulin, Nikolay
    [J]. 2013 TOOLS & METHODS OF PROGRAM ANALYSIS (TMPA 2013), 2013, : 71 - 77
  • [43] Approach to systems verification
    [J]. Bevier, William R., 1600, (05):
  • [44] EXISTENCE AND VERIFICATION FOR DECENTRALIZED NONDETERMINISTIC DISCRETE-EVENT SYSTEMS UNDER BISIMULATION EQUIVALENCE
    Liu, Fuchun
    Zhao, Rui
    Tan, Taizhe
    Zhang, Qiansheng
    [J]. ASIAN JOURNAL OF CONTROL, 2016, 18 (05) : 1679 - 1687
  • [45] Discrete Abstraction for a Class of Stochastic Hybrid Systems Based on Bounded Bisimulation
    Kobayashi, Koichi
    Fukui, Yasuhito
    Hiraishi, Kunihiko
    [J]. IEICE TRANSACTIONS ON FUNDAMENTALS OF ELECTRONICS COMMUNICATIONS AND COMPUTER SCIENCES, 2014, E97A (02) : 459 - 467
  • [46] Diagnosability Verification Using Compositional Branching Bisimulation
    Noori-Hosseini, Mona
    Lennartson, Bengt
    [J]. 2016 13TH INTERNATIONAL WORKSHOP ON DISCRETE EVENT SYSTEMS (WODES), 2016, : 245 - 250
  • [47] A COMPOSITIONAL PROTOCOL VERIFICATION USING RELATIVIZED BISIMULATION
    LARSEN, KG
    MILNER, R
    [J]. INFORMATION AND COMPUTATION, 1992, 99 (01) : 80 - 108
  • [48] Verification of Diagnosability Based on Compositional Branching Bisimulation
    Noori-Hosseini, Mona
    Lennartson, Bengt
    [J]. 2014 IEEE EMERGING TECHNOLOGY AND FACTORY AUTOMATION (ETFA), 2014,
  • [49] Combining a computer science and control theory approach lo the verification of hybrid systems
    Huuck, R
    Lakhnech, Y
    Urbina, L
    Engel, S
    Kowalewski, S
    Preussig, J
    [J]. PROCEEDINGS OF THE JOINT WORKSHOP ON PARALLEL AND DISTRIBUTED REAL-TIME SYSTEMS: FIFTH INTERNATIONAL WORKSHOP ON PARALLEL AND DISTRIBUTED REAL-TIME SYSTEMS (WPDRTS) AND THE THIRD WORKSHOP ON OBJECT-ORIENTED REAL-TIME SYSTEMS (OORTS), 1997, : 222 - 227
  • [50] Bisimulation of dynamical systems
    van der Schaft, A
    [J]. HYBRID SYSTEMS: COMPUTATION AND CONTROL, PROCEEDINGS, 2004, 2993 : 555 - 569