DocumentCode :
116171
Title :
Incremental synthesis of switching protocols via abstraction refinement
Author :
Nilsson, Petter ; Ozay, Necmiye
Author_Institution :
Electr. Eng. & Comput. Sci. Dept., Univ. of Michigan, Ann Arbor, MI, USA
fYear :
2014
fDate :
15-17 Dec. 2014
Firstpage :
6246
Lastpage :
6253
Abstract :
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 switching 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.
Keywords :
continuous time systems; control system synthesis; switching systems (control); augmented finite transition systems; counter-example guided abstraction refinement procedure; incremental synthesis; refinement suggestion; switched system regulation; switching protocols; Abstracts; Games; Heuristic algorithms; Protocols; Switched systems; Switches; Trajectory;
fLanguage :
English
Publisher :
ieee
Conference_Titel :
Decision and Control (CDC), 2014 IEEE 53rd Annual Conference on
Conference_Location :
Los Angeles, CA
Print_ISBN :
978-1-4799-7746-8
Type :
conf
DOI :
10.1109/CDC.2014.7040368
Filename :
7040368
Link To Document :
بازگشت