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 条
  • [31] Time-Staging Enhancement of Hybrid System Falsification
    Ernst, Gidon
    Hasuo, Ichiro
    Zhang, Zhenya
    Sedwards, Sean
    ELECTRONIC PROCEEDINGS IN THEORETICAL COMPUTER SCIENCE, 2021, (361): : 25 - 43
  • [32] Linear Hybrid System Falsification through Local Search
    Abbas, Houssam
    Fainekos, Georgios
    AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, 2011, 6996 : 503 - 510
  • [33] Taming past LTL and flat counter systems
    Demri, Stephane
    Dhar, Amit Kumar
    Sangnier, Arnaud
    INFORMATION AND COMPUTATION, 2015, 242 : 306 - 339
  • [34] Safety Barrier Certificates for Stochastic Hybrid Systems
    Lavaei, Abolfazl
    Soudjani, Sadegh
    Frazzoli, Emilio
    2022 AMERICAN CONTROL CONFERENCE, ACC, 2022, : 880 - 885
  • [35] Featured Transition Systems: Foundations for Verifying Variability-Intensive Systems and Their Application to LTL Model Checking
    Classen, Andreas
    Cordy, Maxime
    Schobbens, Pierre-Yves
    Heymans, Patrick
    Legay, Axel
    Raskin, Jean-Francois
    IEEE TRANSACTIONS ON SOFTWARE ENGINEERING, 2013, 39 (08) : 1069 - 1089
  • [36] Measurability and Safety Verification for Stochastic Hybrid Systems
    Fraenzle, Martin
    Hahn, Ernst Moritz
    Hermanns, Holger
    Wolovick, Nicolas
    Zhang, Lijun
    HSCC 11: PROCEEDINGS OF THE 14TH INTERNATIONAL CONFERENCE ON HYBRID SYSTEMS: COMPUTATION AND CONTROL, 2011, : 43 - 52
  • [37] Safety Properties of Hybrid System Product Lines
    Diemert, Simon
    Millet, Laure
    Joyce, Jeff
    2020 14TH ANNUAL IEEE INTERNATIONAL SYSTEMS CONFERENCE (SYSCON2020), 2020,
  • [38] A Robustness-Based Confidence Measure for Hybrid System Falsification
    Takisaka, Toru
    Zhang, Zhenya
    Arcaini, Paolo
    Hasuo, Ichiro
    IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2023, 42 (05) : 1718 - 1731
  • [39] On decidability of LTL model checking for process rewrite systems
    Bozzelli, Laura
    Kretinsky, Mojmir
    Rehak, Vojtech
    Strejcek, Jan
    ACTA INFORMATICA, 2009, 46 (01) : 1 - 28
  • [40] Model checking LTL with regular valuations for pushdown systems
    Esparza, J
    Kucera, A
    Schwoon, S
    INFORMATION AND COMPUTATION, 2003, 186 (02) : 355 - 376
12345