Bounded Model Checking of Hybrid Systems for Control

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-bas...

Full description

Saved in:
Bibliographic Details
Published in:IEEE transactions on automatic control 2015-11, Vol.60 (11), p.2961-2976
Main Authors: Kwon, YoungMin, Kim, Eunhee
Format: Article
Language:English
Subjects:
Algorithms
Automata
Automatic Control
Checkers
Construction
Control systems
Drugs
Equations
Hybrid System
Hybrid systems
Linear Temporal Logic for Control
LTLC
Mathematical analysis
Mathematical model
Model checking
Predictive Control
Specifications
Strategy
Switches
Trajectory
Citations: Items that this one cites
Items that cite this one
Online Access:Get full text
Tags: Add Tag
No Tags, Be the first to tag this record!
Description
Summary: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.
ISSN:0018-9286
1558-2523
DOI:10.1109/TAC.2015.2417839