Synthesizing Switching Logic to Minimize Long-Run Cost
Given a multi-modal dynamical system, optimal switching logic synthesis involves generating the conditions for switching between the system modes such that the resulting hybrid system satisfies a quantitative specification. The authors formalize and solve the problem of optimal switching logic synthesis for quantitative specifications over long run behavior. Each trajectory of the system, and each state of the system, is associated with a cost. The goal is to synthesize a system that minimizes this cost from each initial state. The paper generalizes earlier work on synthesis for safety as safety specifications can be encoded as quantitative specifications.