Model checking of hybrid systems: From reachability towards stability

被引：0
|
作者：
Podelski, A [1 ]
Wagner, S [1 ]
机构：
[1] Max Planck Inst Informat, Saarbrucken, Germany
来源：
HYBRID SYSTEMS: COMPUTATION AND CONTROL, PROCEEDINGS | 2006年 / 3927卷
关键词：
D O I：
暂无
中图分类号：
TP [自动化技术、计算机技术];
学科分类号：
0812 ;
摘要：
We call a hybrid system stable if every trajectory inevitably ends up in a given region. Our notion of stability deviates from classical definitions in control theory. In this paper, we present a model checking algorithm for stability in the new sense. The idea of the algorithm is to reduce the stability proof for the whole system to a set of (smaller) proofs for several one-mode systems.
引用
收藏
页码：507 / 521
页数：15
相关论文
共 50 条
  • [31] The image computation problem in hybrid systems model checking
    Platzer, Andre
    Clarke, Edmund M.
    HYBRID SYSTEMS: COMPUTATION AND CONTROL, PROCEEDINGS, 2007, 4416 : 473 - +
  • [32] Directed Model Checking for Fast Abstract Reachability Analysis
    Lee, Nakwon
    Kim, Yunho
    Kim, Moonzoo
    Ryu, Duksan
    Baik, Jongmoon
    IEEE ACCESS, 2021, 9 : 158738 - 158750
  • [33] Model Checking of Hybrid Systems Using Shallow Synchronization
    Bu, Lei
    Cimatti, Alessandro
    Li, Xuandong
    Mover, Sergio
    Tonetta, Stefano
    FORMAL TECHNIQUES FOR DISTRIBUTED SYSTEMS, PROCEEDINGS, 2010, 6117 : 155 - +
  • [34] HyLTL : a temporal logic for model checking hybrid systems
    Bresolin, Davide
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2013, (124): : 73 - 84
  • [35] Proofs about folklore: Why model checking = reachability?
    Choe, K.
    Eo, H.
    O, S.
    Shilov, N. V.
    Yi, K.
    MATHEMATICAL LOGIC IN ASIA, 2006, : 41 - +
  • [36] 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
  • [37] Research on state reachability in planning based on model checking
    Wen, Zhong-Hua
    Huang, Wei
    Liu, Ren-Ren
    Jiang, Yun-Fei
    Jisuanji Xuebao/Chinese Journal of Computers, 2012, 35 (08): : 1634 - 1643
  • [38] An Improvement in Decomposed Reachability Analysis for Symbolic Model Checking
    Donataccio, Nicholas
    Zheng, Hao
    2010 IEEE INTERNATIONAL HIGH LEVEL DESIGN VALIDATION AND TEST WORKSHOP (HLDVT), 2010, : 50 - 57
  • [39] Stability and reachability analysis of a hybrid model of luminescence in the marine bacterium Vibrio fischeri
    Belta, C
    Schug, J
    Dang, T
    Kumar, V
    Pappas, GJ
    Rubin, H
    Dunlap, P
    PROCEEDINGS OF THE 40TH IEEE CONFERENCE ON DECISION AND CONTROL, VOLS 1-5, 2001, : 869 - 874
  • [40] Checking Bounded Reachability in Asynchronous Systems by Symbolic Event Tracing
    Dubrovin, Jori
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, PROCEEDINGS, 2010, 5944 : 146 - 162
12345