A Caltech Library Service

Synthesis of Switching Protocols from Temporal Logic Specifications

Liu, Jun and Ozay, Necmiye and Topcu, Ufuk and Murray, Richard M. (2011) Synthesis of Switching Protocols from Temporal Logic Specifications. California Institute of Technology , Pasadena, CA. (Unpublished)

See Usage Policy.


Use this Persistent URL to link to this item:


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 transition systems, namely under- and over-approximations, 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. Finally, these results are illustrated using three examples from different application domains.

Item Type:Report or Paper (Technical Report)
Murray, Richard M.0000-0002-5785-7481
Additional Information:This work was supported in part by the NSERC of Canada, the FCRP consortium through the Multiscale Systems Center (MuSyC), and the Boeing Corporation.
Group:Control and Dynamical Systems Technical Reports
Subject Keywords:Hybrid systems, switching protocols, formal synthesis, linear temporal logic, model checking, temporal logic games
Record Number:CaltechCDSTR:2011.006
Persistent URL:
Usage Policy:You are granted permission for individual, educational, research and non-commercial reproduction, distribution, display and performance of this work in any format.
ID Code:28146
Deposited By: Imported from CaltechCDSTR
Deposited On:19 Sep 2011
Last Modified:03 Oct 2019 03:29

Repository Staff Only: item control page