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 条

[41] PDF: Path-Oriented, Derivative-Free Approach for Safety Falsification of Nonlinear and Nondeterministic CPS
Wang, Jiawan
Bu, Lei
Xing, Shaopeng
Li, Xuandong
IEEE TRANSACTIONS ON COMPUTER-AIDED DESIGN OF INTEGRATED CIRCUITS AND SYSTEMS, 2022, 41 (02) : 238 - 251
[42] Verification and Control of Hybrid Systems Under Safety Requirements
Lucia, W.
Famularo, D.
Franze, G.
Furfaro, A.
IFAC PAPERSONLINE, 2018, 51 (25): : 61 - 66
[43] Managing LTL Properties in Event-B Refinement
Schneider, Steve
Treharne, Helen
Wehrheim, Heike
Williams, David M.
INTEGRATED FORMAL METHODS, IFM 2014, 2014, 8739 : 221 - 237
[44] Reducing DNN Properties to Enable Falsification with Adversarial Attacks
Shriver, David
Elbaum, Sebastian
Dwyer, Matthew B.
2021 IEEE/ACM 43RD INTERNATIONAL CONFERENCE ON SOFTWARE ENGINEERING (ICSE 2021), 2021, : 275 - 287
[45] Constraining Counterexamples in Hybrid System Falsification: Penalty-Based Approaches
Zhang, Zhenya
Arcaini, Paolo
Hasuo, Ichiro
NASA FORMAL METHODS (NFM 2020), 2020, 12229 : 401 - 419
[46] Multi-armed Bandits for Boolean Connectives in Hybrid System Falsification
Zhang, Zhenya
Hasuo, Ichiro
Arcaini, Paolo
COMPUTER AIDED VERIFICATION, CAV 2019, PT I, 2019, 11561 : 401 - 420
[47] Organising LTL monitors over distributed systems with a global clock
Colombo, Christian
Falcone, Ylies
FORMAL METHODS IN SYSTEM DESIGN, 2016, 49 (1-2) : 109 - 158
[48] Approximate Safety Properties in Metric Transition Systems
Qian, Junyan
Shi, Fan
Cai, Yong
Pan, Haiyu
IEEE TRANSACTIONS ON RELIABILITY, 2022, 71 (01) : 221 - 234
[49] How to model and prove hybrid systems with KeYmaera: a tutorial on safety
Quesel, Jan-David
Mitsch, Stefan
Loos, Sarah
Arechiga, Nikos
Platzer, Andre
INTERNATIONAL JOURNAL ON SOFTWARE TOOLS FOR TECHNOLOGY TRANSFER, 2016, 18 (01) : 67 - 91
[50] Extracting counterexamples induced by safety violation in linear hybrid systems
Goyal, Manish
Duggirala, Parasara Sridhar
AUTOMATICA, 2020, 117

← 1 2 3 4 5 →