]> 2026-06-29T09:50:02+00:00 Synthesis of Switching Protocols from Temporal Logic Specifications 0 en We propose formal means for synthesizing switching protocols that determine the sequence in which the modes of a switched system are activated to satisfy certain high-level specifications in linear temporal logic. The synthesized protocols are robust against exogenous disturbances on the continuous dynamics. Two types of finite tran- sition systems, namely (deterministic) under-approximations and over-approximations (potentially with nondeterministic transitions), that abstract the behavior of the underlying continuous dynamics are defined. In particular, we show that the discrete synthesis problem for an under-approximation can be formulated as a model checking problem, whereas that for an over-approximation can be transformed into a two-player game. Both of these formulations are amenable to efficient, off-the-shelf software 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 nonlinear switched system. Moreover, the proposed framework can be straightforwardly extended to accommodate specifications that require reacting to possibly adversarial external events. Jun Liu, Necmiye Ozay, Ufuk Topcu and Richard M. Murray 2011p Submitted, 2012 American Control Conference lotm12-acc Conference Paper 2016-05-15T06:15:56Z 2457523.7610648 Synthesis of Switching Protocols from Temporal Logic Specifications Title 102 en Title