Incremental Synthesis of Switching Protocols via Abstraction Refinement

P. Nilsson and N. Ozay
Proc. 53rd IEEE Conference on Decision and Control (CDC) 2014.

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 switch- ing 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.