Logic-Based Design and Synthesis of Controllers for Hybrid Systems
Jennifer M. Davoren, Tinne De Moor · 2000
In this paper, we formulate and solve a quite general class of hybrid controller synthesis problems. The plant consists of a finite number of continuous systems, given by di#erential equations over a common state space; the controller steers the plant state by determining when to discretely switch between the various di#erential equations; and the closed-loop trajectories correspond to those of (a subclass of) the widely accepted hybrid automaton model. In addition to the well-studied classes of safety (reachability or invariance) and liveness (non-blocking and non-Zeno) performance specifications, we deal with a general class of active behavioural specifications, requiring that trajectories traverse in prescribed sequences through the blocks of a given finite partition of the plant state space. We give an abstract algorithm which solves this controller synthesis problem for arbitrary di#erential equations with unique solutions, and give an analytic proof of finite terminat...