期刊
IEEE TRANSACTIONS ON AUTOMATIC CONTROL
卷 58, 期 7, 页码 1771-1785出版社
IEEE-INST ELECTRICAL ELECTRONICS ENGINEERS INC
DOI: 10.1109/TAC.2013.2246095
关键词
Formal synthesis; hybrid systems; linear temporal logic; switching protocols; temporal logic games
资金
- NSERC of Canada
- FCRP consortium through the Multiscale Systems Center (MuSyC), AFOSR [FA9550-12-1-031]
- Boeing Corporation
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 (LTL). The synthesized protocols are robust against exogenous disturbances on the continuous dynamics and can react to possibly adversarial events (both external and internal). Finite-state approximations that abstract the behavior of the underlying continuous dynamics are defined using finite transition systems. Such approximations allow us to transform the continuous switching synthesis problem into a discrete synthesis problem in the form of a two-player game between the system and the environment, where the winning conditions represent the high-level temporal logic specifications. Restricting to an expressive subclass of LTL formulas, these temporal logic games are amenable to solutions with polynomial-time complexity. By construction, existence of a discrete switching strategy for the discrete synthesis problem guarantees the existence of a switching protocol that can be implemented at the continuous level to ensure the correctness of the nonlinear switched system and to react to the environment at run time.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据