Improving reachability analysis of hybrid automata for engine control

A new approach is presented for computing approximations of the reached sets of linear hybrid automata. First, we present some new theoretical results on termination of a class of reachability algorithms, which includes Botchkarev´s, based on ellipsoidal calculus. The main contribution of the paper is a revised reachability computation that avoids the approximations caused by the union operation in the discretized flow tube estimation. Therefore, the new algorithm may classify as unreachable states that are reachable according to the previous algorithm because of the looser over-approximations introduced by the union operation. We implemented the new reachability algorithm and tested it successfully on a real-life case modeling a hybrid model of a controlled car engine.