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 条

[1] Falsification of LTL safety properties in hybrid systems
Plaku E.
Kavraki L.E.
Vardi M.Y.
International Journal on Software Tools for Technology Transfer, 2013, 15 (04) : 305 - 320
[2] Falsification of Temporal Properties of Hybrid Systems Using the Cross-Entropy Method
Sankaranarayanan, Sriram
Fainekos, Georgios
HSCC 12: PROCEEDINGS OF THE 15TH ACM INTERNATIONAL CONFERENCE ON HYBRID SYSTEMS: COMPUTATION AND CONTROL, 2012, : 125 - 134
[3] LTL falsification in infinite-state systems
Cimatti, Alessandro
Griggio, Alberto
Magnago, Enrico
INFORMATION AND COMPUTATION, 2022, 289
[4] Monte-Carlo Techniques for Falsification of Temporal Properties of Non-Linear Hybrid Systems
Nghiem, Truong
Sankaranarayanan, Sriram
Fainekos, Georgios
Ivancic, Franjo
Gupta, Aarti
Pappas, George J.
HSSC 10: PROCEEDINGS OF THE 13TH ACM INTERNATIONAL CONFERENCE ON HYBRID SYSTEMS: COMPUTATION AND CONTROL, 2010, : 211 - 220
[5] Automated generation of hybrid automata for multi-rigid-body mechanical systems and its application to the falsification of safety properties
Navarro-Lopez, E. M.
O'Toole, M. D.
MATHEMATICAL AND COMPUTER MODELLING OF DYNAMICAL SYSTEMS, 2018, 24 (01) : 44 - 75
[6] Stochastic Local Search for Falsification of Hybrid Systems
Deshmukh, Jyotirmoy
Jin, Xiaoqing
Kapinski, James
Maler, Oded
AUTOMATED TECHNOLOGY FOR VERIFICATION AND ANALYSIS, ATVA 2015, 2015, 9364 : 500 - 517
[7] Ant Colonies for Temporal Logic Falsification of Hybrid Systems
Annapureddy, Yashwanth Singh Rahul
Fainekos, Georgios E.
IECON 2010: 36TH ANNUAL CONFERENCE OF THE IEEE INDUSTRIAL ELECTRONICS SOCIETY, 2010,
[8] Convergence Proofs for Simulated Annealing Falsification of Safety Properties
Abbas, Houssam
Fainekos, Georgios
2012 50TH ANNUAL ALLERTON CONFERENCE ON COMMUNICATION, CONTROL, AND COMPUTING (ALLERTON), 2012, : 1594 - 1601
[9] Hybrid systems: from verification to falsification by combining motion planning and discrete search
Plaku, Erion
Kavraki, Lydia E.
Vardi, Moshe Y.
FORMAL METHODS IN SYSTEM DESIGN, 2009, 34 (02) : 157 - 182
[10] Falsification of Hybrid Systems Using Adaptive Probabilistic Search
Ernst, Gidon
Sedwards, Sean
Zhang, Zhenya
Hasuo, Ichiro
ACM TRANSACTIONS ON MODELING AND COMPUTER SIMULATION, 2021, 31 (03):

← 1 2 3 4 5 →