Model checking of hybrid systems: From reachability towards stability

被引:0
|
作者
Podelski, A [1 ]
Wagner, S [1 ]
机构
[1] Max Planck Inst Informat, Saarbrucken, Germany
关键词
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 条
  • [1] Verifying Cyber-Physical Systems by Combining Software Model Checking with Hybrid Systems Reachability
    Bak, Stanley
    Chaki, Sagar
    [J]. 2016 PROCEEDINGS OF THE INTERNATIONAL CONFERENCE ON EMBEDDED SOFTWARE (EMSOFT), 2016,
  • [2] Model Checking Hybrid Systems
    Clarke, Edmund M.
    Gao, Sicun
    [J]. LEVERAGING APPLICATIONS OF FORMAL METHODS, VERIFICATION AND VALIDATION: SPECIALIZED TECHNIQUES AND APPLICATIONS, PT II, 2014, 8803 : 385 - 386
  • [3] Automatic Synthesis for the Reachability of Process Systems with a Model Checking Algorithm
    Kim, Jinkyung
    Park, Jaedeuk
    Moon, Il
    [J]. INDUSTRIAL & ENGINEERING CHEMISTRY RESEARCH, 2013, 52 (07) : 2613 - 2624
  • [4] Model Checking as A Reachability Problem
    Vardi, Moshe Y.
    [J]. REACHABILITY PROBLEMS, PROCEEDINGS, 2009, 5797 : 35 - 35
  • [5] Composing Reachability Analyses of Hybrid Systems for Safety and Stability
    Bogomolov, Sergiy
    Mitrohin, Corina
    Podelski, Andreas
    [J]. AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, 2010, 6252 : 67 - 81
  • [6] Model checking multirate hybrid systems
    Zhang, Hai-Bin
    Duan, Zhen-Hua
    [J]. Xi'an Dianzi Keji Daxue Xuebao/Journal of Xidian University, 2008, 35 (01): : 60 - 64
  • [7] Towards Checking Parametric Reachability for UML State Machines
    Niewiadomski, Artur
    Penczek, Wojciech
    Szreter, Maciej
    [J]. PERSPECTIVES OF SYSTEMS INFORMATICS, 2010, 5947 : 319 - +
  • [8] Towards Symbolic Model-Based Mutation Testing: Combining Reachability and Refinement Checking
    Aichernig, Bernhard K.
    Joebstl, Elisabeth
    [J]. ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2012, (80): : 88 - 102
  • [9] Checking Algebraic Reachability of Polynomial and Rational Systems
    Nemcova, Jana
    van Schuppen, Jan H.
    [J]. IFAC PAPERSONLINE, 2017, 50 (01): : 12119 - 12124
  • [10] Model checking based on simultaneous reachability analysis
    Karaçali, B
    Tai, KC
    [J]. SPIN MODEL CHECKING AND SOFTWARE VERIFICATION, 2000, 1885 : 34 - 53