Synthesis of Switching Protocols from Temporal Logic Specifications
Synthesis of Switching Protocols from Temporal Logic Specifications
复制标题
从时间逻辑规范综合切换协议
DOI：
--
复制
发表时间：
2011
期刊：
影响因子：
--
通讯作者：
R. Murray
中科院分区：
文献类型：
--
作者：
Jun Liu;N. Ozay;U. Topcu;R. Murray
我们提出了用于综合切换协议的正式方法，该协议确定切换系统的模式被激活的顺序，以满足线性时序逻辑中的某些高级规范。合成的协议对于连续动态的外源干扰具有鲁棒性。定义了两种类型的有限过渡系统，即欠近似和过近似，它们抽象了底层连续动态的行为。特别是，我们证明了欠近似的离散综合问题可以表述为模型检查问题，而过近似的离散综合问题可以转化为两人游戏。这两种表述都适用于高效、现成的软件工具。通过构造，离散综合问题的离散切换策略的存在保证了连续综合问题的连续切换协议的存在，该协议可以在连续级别上实现，以保证非线性切换系统的正确性。此外，所提出的框架可以直接扩展以适应需要对可能的敌对外部事件做出反应的规范。最后，使用来自不同应用领域的三个示例来说明这些结果。
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.