Bounded Model Checking of Hybrid Systems for Control

被引：8

作者：

Kwon, YoungMin ^{[1
]}

Kim, Eunhee ^{[2
]}

机构：

[1] Microsoft Corp, Redmond, WA 98052 USA

[2] 2e Consulting Corp, Seoul 151038, South Korea

来源：

IEEE TRANSACTIONS ON AUTOMATIC CONTROL | 2015年 / 60卷 / 11期

关键词：

Automatic control; hybrid system; linear temporal logic for control (LTLC); model checking; predictive control; TEMPORAL LOGIC;

D O I：

10.1109/TAC.2015.2417839

中图分类号：

TP [自动化技术、计算机技术];

学科分类号：

0812 ;

摘要：

A bounded LTL model checking algorithm to check the properties of hybrid systems is presented. The proposed algorithm can also be applied to control systems as counterexamples of a negated goal contain information to achieve the original goal. This approach is different than existing abstraction-based techniques. While many of the latter approaches build a control strategy after partitioning a state space, the proposed approach constructs a necessary set of constraints and computes a possibly optimal control input on the fly. The bounded LTL semantics of this paper is more expressive than those of bounded reachability: in addition to the finite computation paths that the reachability checkers can handle, the proposed algorithm can check infinite paths ending with a loop. Furthermore, the LTL operators provide a convenient and expressive way of writing complicated specifications.

引用

页码：2961 / 2976

页数：16

共 50 条

[1] Bounded model checking of hybrid dynamical systems
Giorgetti, Nicolo
Pappas, George J.
Beraporad, Alberto
[J]. 2005 44th IEEE Conference on Decision and Control & European Control Conference, Vols 1-8, 2005, : 672 - 677
[2] Optimizing bounded model checking for linear hybrid systems
Abrahám, E
Becker, B
Klaedtke, F
Steffen, M
[J]. VERIFICATION, MODEL CHECKING, AND ABSTRACT INTERPRETATION, PROCEEDINGS, 2005, 3385 : 396 - 412
[3] Bounded STL Model Checking for Hybrid Systems (Invited Talk)
Bae, Kyungmin
[J]. PROCEEDINGS OF THE 9TH ACM SIGPLAN INTERNATIONAL WORKSHOP ON FORMAL TECHNIQUES FOR SAFETY-CRITICAL SYSTEMS, FTSCS 2023, 2023, : 1 - 1
[4] Efficient Proof Engines for Bounded Model Checking of Hybrid Systems
Franzle, Martin
Herde, Christian
[J]. ELECTRONIC NOTES IN THEORETICAL COMPUTER SCIENCE, 2005, 133 : 119 - 137
[5] HySAT:: An efficient proof engine for bounded model checking of hybrid systems
Fraenzle, Martin
Herde, Christian
[J]. FORMAL METHODS IN SYSTEM DESIGN, 2007, 30 (03) : 179 - 198
[6] CEGAR based bounded model checking of discrete time hybrid systems
Mari, Federico
Tronci, Enrico
[J]. HYBRID SYSTEMS: COMPUTATION AND CONTROL, PROCEEDINGS, 2007, 4416 : 399 - +
[7] HySAT: An efficient proof engine for bounded model checking of hybrid systems
Martin Fränzle
Christian Herde
[J]. Formal Methods in System Design, 2007, 30 : 179 - 198
[8] Bounded model checking for timed systems
Audemard, G
Cimatti, A
Kornilowicz, A
Sebastiani, R
[J]. FORMAL TECHNIQUE FOR NETWORKED AND DISTRIBUTED SYSTEMS - FORTE 2002, PROCEEDINGS, 2002, 2529 : 243 - 259
[9] Application of symbolic and bounded model checking to the verification of logic control systems
Loeis, Kingliana
Younis, Mohammed Bani
Frey, Georg
[J]. ETFA 2005: 10TH IEEE INTERNATIONAL CONFERENCE ON EMERGING TECHNOLOGIES AND FACTORY AUTOMATION, VOL 1, PTS 1 AND 2, PROCEEDINGS, 2005, : 247 - 250
[10] Bounded model checking of infinite state systems
Tobias Schuele
Klaus Schneider
[J]. Formal Methods in System Design, 2007, 30 : 51 - 81

← 1 2 3 4 5 →