Falsification of LTL Safety Properties in Hybrid Systems

被引：0
作者：
Plaku, Erion [1 ]
Kavraki, Lydia E. [1 ]
Vardi, Moshe Y. [1 ]
机构：
[1] Rice Univ, Dept Comp Sci, Houston, TX 77005 USA
来源：
TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, PROCEEDINGS | 2009年 / 5505卷
关键词：
MODEL CHECKING; VERIFICATION; REACHABILITY; COVERAGE;
D O I：
暂无
中图分类号：
TP301 [理论、方法];
学科分类号：
081202 ;
摘要：
This paper develops a novel computational method for the falsification of safety properties specified by syntactically safe linear temporal logic (LTL) formulas phi for hybrid systems with general nonlinear dynamics and input controls. The method is based on an effective combination of robot motion planning and model checking. Experiments on a hybrid robotic system benchmark with nonlinear dynamics show significant speedup over related work. The experiments also indicate significant speedup when using minimized DFA instead of non-minimized NFA, as obtained by standard tools, for representing the violating prefixes of phi.
引用
收藏
页码：368 / 382
页数：15
相关论文
共 50 条
  • [21] Two-Layered Falsification of Hybrid Systems Guided by Monte Carlo Tree Search
    Zhang, Zhenya
    Ernst, Gidon
    Sedwards, Sean
    Arcaini, Paolo
    Hasuo, Ichiro
    IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2018, 37 (11) : 2894 - 2905
  • [22] Verification of the safety and attainability of hybrid systems: State of the art
    Nasri, Othman
    Lefebvre, Marie-Anne
    Guéguen, Hervé
    Zaytoon, Junan
    Journal Europeen des Systemes Automatises, 2007, 41 (7-8): : 855 - 883
  • [23] Hybrid Parallel Model Checking of Hybrid LTL on Hybrid State Space Representation
    Klai, Kais
    Abid, Chiheb Ameur
    Arias, Jaime
    Evangelista, Sami
    VERIFICATION AND EVALUATION OF COMPUTER AND COMMUNICATION SYSTEMS (VECOS 2021), 2022, 13187 : 27 - 42
  • [24] On the Effectiveness of Signal Rescaling in Hybrid System Falsification
    Zhang, Zhenya
    Lyu, Deyun
    Arcaini, Paolo
    Ma, Lei
    Hasuo, Ichiro
    Zhao, Jianjun
    NASA FORMAL METHODS (NFM 2021), 2021, 12673 : 392 - 399
  • [25] Verification of LTL on B event systems
    Groslambert, Julien
    B 2007: Formal Specification and Development in B, Proceedings, 2007, 4355 : 109 - 124
  • [26] Safety Verification for Probabilistic Hybrid Systems
    Zhang, Lijun
    She, Zhikun
    Ratschan, Stefan
    Hermanns, Holger
    Hahn, Ernst Moritz
    COMPUTER AIDED VERIFICATION, PROCEEDINGS, 2010, 6174 : 196 - 211
  • [27] Verifying Safety and Persistence in Hybrid Systems Using Flowpipes and Continuous Invariants
    Sogokon, Andrew
    Jackson, Paul B.
    Johnson, Taylor T.
    JOURNAL OF AUTOMATED REASONING, 2019, 63 (04) : 1005 - 1029
  • [28] Spread the Work: Multi-threaded Safety Analysis for Hybrid Systems
    Schupp, Stefan
    Abraham, Erika
    SOFTWARE ENGINEERING AND FORMAL METHODS, SEFM 2018, 2018, 10886 : 89 - 104
  • [29] Exact Safety Verification of Hybrid Systems Based on Bilinear SOS Representation
    Yang, Zhengfeng
    Lin, Wang
    Wu, Min
    ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS, 2015, 14 (01)
  • [30] Hybrid Tools for Hybrid Systems - Proving Stability and Safety at Once
    Moehlmann, Eike
    Hagemann, Willem
    Theel, Oliver
    FORMAL MODELING AND ANALYSIS OF TIMED SYSTEMS (FORMATS 2015), 2015, 9268 : 222 - 239
12345