A reachability-based technique for idle speed control synthesis

The goal of this paper is to demonstrate the application of the algorithmic analysis of hybrid systems to idle speed control. This problem can be formulated as to design a safety hybrid controller. In principle, such controllers can be derived from the maximal invariant set. It is, however, hard to compute this set for a nonlinear hybrid system with both continuous control and disturbance inputs. We propose to use a class of piecewise constant control functions, which allows to develop an effective synthesis algorithm based on reachability computations. In addition, we show how assume-guarantee reasoning from automatic verification can be used to reduce the computational complexity.