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 条
  • [21] Dara: Hybrid Model Checking of Distributed Systems
    Anand, Vaastav
    ESEC/FSE'18: PROCEEDINGS OF THE 2018 26TH ACM JOINT MEETING ON EUROPEAN SOFTWARE ENGINEERING CONFERENCE AND SYMPOSIUM ON THE FOUNDATIONS OF SOFTWARE ENGINEERING, 2018, : 977 - 979
  • [22] Towards efficient partition refinement for checking reachability in timed automata
    Pólrola, A
    Penczek, W
    Szreter, M
    FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS, 2003, 2791 : 2 - 17
  • [23] Reachability for Continuous and Hybrid Systems
    Maler, Oded
    REACHABILITY PROBLEMS, PROCEEDINGS, 2009, 5797 : 24 - 25
  • [24] Discrete reachability of hybrid systems
    Lunze, J
    Nixdorf, B
    INTERNATIONAL JOURNAL OF CONTROL, 2003, 76 (14) : 1453 - 1468
  • [25] Reachability of a class of hybrid systems
    Wang, YJ
    Xie, GM
    Nang, L
    2003 IEEE INTERNATIONAL CONFERENCE ON SYSTEMS, MAN AND CYBERNETICS, VOLS 1-5, CONFERENCE PROCEEDINGS, 2003, : 312 - 316
  • [26] Necessary and Sufficient Conditions of Reachability for a Model of Multidimensional Hybrid Systems
    Prepelita, Valeriu
    PROCEEDINGS OF THE 8TH WSEAS INTERNATIONAL CONFERENCE ON SYSTEMS THEORY AND SCIENTIFIC COMPUTATION (ISTAC'08), 2008, : 247 - 254
  • [27] Optimizing bounded model checking for linear hybrid systems
    Abrahám, E
    Becker, B
    Klaedtke, F
    Steffen, M
    VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, PROCEEDINGS, 2005, 3385 : 396 - 412
  • [28] Model Checking the Quantitative μ-Calculus on Linear Hybrid Systems
    Fischer, Diana
    Kaiser, Lukasz
    AUTOMATA, LANGUAGES AND PROGRAMMING, ICALP, PT II, 2011, 6756 : 404 - 415
  • [29] MODEL CHECKING THE QUANTITATIVE μ-CALCULUS ON LINEAR HYBRID SYSTEMS
    Fischer, Diana
    Kaiser, Lukasz
    LOGICAL METHODS IN COMPUTER SCIENCE, 2012, 8 (03)
  • [30] Selective search in bounded model checking of reachability properties
    Szreter, M
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, PROCEEDINGS, 2005, 3707 : 159 - 173
12345