Browse wiki
From MurrayWiki
Synthesis of Switching Protocols from Temporal Logic Specifications 
Abstract 
We propose formal means for synthesizing s … 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 highlevel 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) underapproximations and overapproximations (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 underapproximation can be formulated as a model checking problem, whereas that for an overapproximation can be transformed into a twoplayer game. Both of these formulations are amenable to efficient, offtheshelf 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. g to possibly adversarial external events. +


Authors  Jun Liu, Necmiye Ozay, Ufuk Topcu and Richard M. Murray + 
Funding  CorrectbyConstruction Synthesis of Control Protocols for Aerospace Systems + 
ID  2011p + 
Source  Submitted, 2012 American Control Conference + 
Tag  lotm12acc + 
Title  Synthesis of Switching Protocols from Temporal Logic Specifications + 
Type  Conference Paper + 
Categories  Papers 
Modification date This property is a special property in this wiki.

15 May 2016 06:15:56 + 
URL This property is a special property in this wiki.

http://www.cds.caltech.edu/~murray/preprints/lotm12acc_s.pdf + 
hide properties that link here 
Synthesis of Switching Protocols from Temporal Logic Specifications +  Title 
