Switching protocol synthesis for temporal logic specifications

We consider the problem of synthesizing a robust switching controller for nonlinear hybrid systems to guarantee that the trajectories of the system satisfy a high level specification expressed in linear temporal logic. Two different types of finite transition systems, namely under-approximations and over-approximations, that abstract the behavior of the underlying continuous dynamical system are defined. Using these finite abstractions, it is possible to leverage tools from logic and automata theory to synthesize discrete mode sequences or strategies. In particular, we show that the discrete synthesis problem for an under-approximation can be reformulated as a model checking problem and that for an over-approximation can be transformed into a two-player game, which can then be solved by using off-the-shelf tools. By construction, existence of a discrete switching strategy for the discrete synthesis problem guarantees the existence of a continuous switching protocol for the continuous synthesis problem, which can be implemented at the continuous level to ensure the correctness of the trajectories for the nonlinear hybrid system. Moreover, in the case of over-approximations, it is shown that one can easily accommodate specifications that require reacting to possibly adversarial external events within the same framework.