Incremental synthesis of switching protocols via abstraction refinement

We consider the problem of synthesizing switching protocols that regulate the modes of a switched system in order to guarantee that the trajectories of the system satisfy certain high-level specifications. In particular, we develop a computational framework for incremental synthesis of switching protocols. Augmented finite transition systems are used as abstract representations of continuous dynamics. Inspired by counter-example guided abstraction refinement procedures for hybrid system verification, we start with a coarse abstraction and gradually refine it according to preorder relations on augmented finite transition systems. At each iteration, the proposed procedure can produce either a switching protocol that ensures the satisfaction of the specification, a certificate for nonexistence of such a protocol, or a refinement suggestion together with a partial solution to be used in the next iteration. Although the procedure is not guaranteed to terminate in general, we illustrate its practical applicability with two simple examples.