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