Compositional Synthesis with Parametric Reactive Controllers
Compositional Synthesis with Parametric Reactive Controllers
复制标题
参数反应控制器的组合综合
DOI：
10.1145/2883817.2883842
复制
发表时间：
2016
期刊：
影响因子：
--
通讯作者：
U. Topcu
中科院分区：
文献类型：
--
作者：
R. Alur;Salar Moarref;U. Topcu
反应合成的雄心勃勃的目标是自动合成正确的结构控制器从高层次的规格，最近引起了系统设计和控制的显着关注。在实践中，复杂的系统往往不是从零开始构建的，而是从一组现有的构建模块开始构建的。例如，在机器人运动规划中，机器人通常具有多个预定义的运动基元，可以选择和组合这些运动基元以执行高级目标。在本文中，我们提出了一种新的基于参数和反应控制器库的综合框架。参数允许我们在许多综合问题中利用对称性。控制器的反应性考虑到环境可能是动态的和潜在的对抗性的。我们首先展示了这些控制器可以自动构建由用户指定的参数目标，形成一个库的参数和反应控制器。然后，我们给出了一个合成算法，选择和实例化控制器从图书馆，以满足给定的线性时序逻辑目标。我们象征性地实现我们的算法，并通过将其应用于自动驾驶汽车的案例研究来说明我们的方法的潜力。
Reactive synthesis with the ambitious goal of automatically synthesizing correct-by-construction controllers from high-level specifications, has recently attracted significant attention in system design and control. In practice, complex systems are often not constructed from scratch but from a set of existing building blocks. For example in robot motion planning, a robot usually has a number of predefined motion primitives that can be selected and composed to enforce a high-level objective. In this paper, we propose a novel framework for synthesis from a library of parametric and reactive controllers. Parameters allow us to take advantage of the symmetry in many synthesis problems. Reactivity of the controllers takes into account that the environment may be dynamic and potentially adversarial. We first show how these controllers can be automatically constructed from parametric objectives specified by the user to form a library of parametric and reactive controllers. We then give a synthesis algorithm that selects and instantiates controllers from the library in order to satisfy a given linear temporal logic objective. We implement our algorithms symbolically and illustrate the potential of our method by applying it to an autonomous vehicle case study.