A Compositional Approach to Reactive Games under Temporal Logic Specifications
A Compositional Approach to Reactive Games under Temporal Logic Specifications
复制标题
时间逻辑规范下反应式博弈的组合方法
DOI：
--
复制
发表时间：
2018
期刊：
影响因子：
--
通讯作者：
Jie Fu
中科院分区：
文献类型：
--
作者：
A. Kulkarni;Jie Fu
我们研究具有线性时序逻辑（LTL）规范的反应式游戏控制器的组合综合问题。反应式游戏是可控系统与其不受控制的动态环境之间交互的抽象。在复杂规格下对此类系统进行集中控制设计的计算成本可能很高。相反，组合方法旨在通过为其组件子规范组合解决方案来合成复杂规范的控制器。这缓解了可扩展性问题，并具有模块化和灵活的优点。本文使用组合方法分两步解决了反应式游戏合成问题。首先，我们使用随机许可策略的概念将策略综合问题简化为仅识别受控代理针对不受控环境的获胜区域。然后，我们利用 LTL 公式固有的组合性质，将两个子游戏的独立计算的获胜区域组合成组合游戏获胜区域的超集。我们利用基本集合运算来构造这个超集。最后，我们引入了一种迭代算法来从超集中提取精确的获胜区域。我们证明了所提出方法的正确性，并使用玩具问题和机器人运动规划示例来说明解决方案。
We study the problem of compositional synthesis of controllers for reactive games with linear temporal logic (LTL) specifications. A reactive game is an abstraction of the interaction between a controllable system and its uncontrolled and dynamic environment. A centralized control design for such systems under complex specifications can be computationally expensive. Instead, a compositional approach aims to synthesize a controller for a complex specification by composing the solutions for its component sub-specifications. This mitigates the issue of scalability and has the advantages of being modular and flexible. This paper solves the problem of reactive game synthesis using the compositional approach in two steps. First, we use the notion of randomized permissive strategy to reduce the strategy synthesis problem to that of identifying only the winning region for the controlled agent against the uncontrolled environment. Then, we exploit the inherent compositional nature of LTL formulas to compose the independently computed winning regions of two sub-games into a superset of the composed-game winning region. We make use of elementary set operations to construct this superset. Finally, we introduce an iterative algorithm to extract the exact winning region from the superset. We prove the correctness of our proposed method and illustrate the solution using a toy-problem and a robot motion planning example.