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 条
  • [11] Falsification of combined invariance and reachability specifications in hybrid control systems
    Rawlings, Blake C.
    Ydstie, B. Erik
    DISCRETE EVENT DYNAMIC SYSTEMS-THEORY AND APPLICATIONS, 2017, 27 (02): : 463 - 479
  • [12] Guaranteed termination in the verification of LTL properties of non-linear robust discrete time hybrid systems
    Damm, Werner
    Pinto, Guilherme
    Ratschan, Stefan
    INTERNATIONAL JOURNAL OF FOUNDATIONS OF COMPUTER SCIENCE, 2007, 18 (01) : 63 - 86
  • [13] Fast Falsification of Hybrid Systems Using Probabilistically Adaptive Input
    Ernst, Gidon
    Sedwards, Sean
    Zhang, Zhenya
    Hasuo, Ichiro
    QUANTITATIVE EVALUATION OF SYSTEMS (QEST 2019), 2019, 11785 : 165 - 181
  • [14] Falsification of combined invariance and reachability specifications in hybrid control systems
    Blake C. Rawlings
    B. Erik Ydstie
    Discrete Event Dynamic Systems, 2017, 27 : 463 - 479
  • [15] Certifying the LTL Formula p Until q in Hybrid Systems
    Han, Hyejin
    Maghenem, Mohamed
    Sanfelice, Ricardo G.
    IEEE TRANSACTIONS ON AUTOMATIC CONTROL, 2023, 68 (07) : 4451 - 4458
  • [16] Probabilistic Temporal Logic Falsification of Cyber-Physical Systems
    Abbas, Houssam
    Fainekos, Georgios
    Sankaranarayanan, Sriram
    Ivancic, Franjo
    Gupta, Aarti
    ACM TRANSACTIONS ON EMBEDDED COMPUTING SYSTEMS, 2013, 12
  • [17] Verifying Safety and Persistence Properties of Hybrid Systems Using Flowpipes and Continuous Invariants
    Sogokon, Andrew
    Jackson, Paul B.
    Johnson, Taylor T.
    NASA FORMAL METHODS (NFM 2017), 2017, 10227 : 194 - 211
  • [18] S-TALIRO: A Tool for Temporal Logic Falsification for Hybrid Systems
    Annapureddy, Yashwanth
    Liu, Che
    Fainekos, Georgios
    Sankaranarayanan, Sriram
    TOOLS AND ALGORITHMS FOR THE CONSTRUCTION AND ANALYSIS OF SYSTEMS, 2011, 6605 : 254 - +
  • [19] A JAG extension for verifying LTL properties on B event systems
    Groslambert, Julien
    B 2007: Formal Specification and Development in B, Proceedings, 2007, 4355 : 262 - 265
  • [20] Safety verification and reachability analysis for hybrid systems
    Gueguen, Herve
    Lefebvre, Marie-Anne
    Zaytoon, Janan
    Nasri, Othman
    ANNUAL REVIEWS IN CONTROL, 2009, 33 (01) : 25 - 36
12345