Formal Methods for Control Synthesis: An Optimization Perspective
Formal Methods for Control Synthesis: An Optimization Perspective
复制标题
控制综合的形式化方法：优化视角
DOI：
--
复制
发表时间：
2019
期刊：
影响因子：
--
通讯作者：
Sadra Sadraddini
中科院分区：
文献类型：
--
作者：
C. Belta;Sadra Sadraddini
在控制理论中，复杂的动力学，例如（非线性）微分方程组，主要是为了实现稳定性而进行控制。这一基本属性可以与期望的操作点或规定的轨迹相关，通常与最优性相关，这需要最小化沿着稳定系统的轨迹的一定成本。在形式验证（模型检查）中，简单的系统（例如对计算机程序或数字电路进行建模的有限状态转换图）会根据作为时序逻辑公式给出的丰富规范进行检查。形式综合问题的目标是根据时序逻辑规范综合或控制有限系统，最近引起了越来越多的关注。在本文中，我们回顾了关于最优控制和形式综合之间联系的一些最新结果。具体来说，我们关注以下问题：给定动态系统的成本和正确性时间逻辑规范，生成满足规范的最优控制策略。我们首先提供基于自动机的方法的简短概述，其中系统的动态被映射到有限抽象，然后使用与规范相对应的自动机进行控制。然后，我们提供一类方法的详细概述，这些方法依赖于将规范和动态映射到优化问题的约束。我们讨论了这两种方法的优点和局限性，并提出了未来研究的方向。
In control theory, complicated dynamics such as systems of (nonlinear) differential equations are controlled mostly to achieve stability. This fundamental property, which can be with respect to a desired operating point or a prescribed trajectory, is often linked with optimality, which requires minimizing a certain cost along the trajectories of a stable system. In formal verification (model checking), simple systems, such as finite-state transition graphs that model computer programs or digital circuits, are checked against rich specifications given as formulas of temporal logics. The formal synthesis problem, in which the goal is to synthesize or control a finite system from a temporal logic specification, has recently received increased interest. In this article, we review some recent results on the connection between optimal control and formal synthesis. Specifically, we focus on the following problem: Given a cost and a correctness temporal logic specification for a dynamical system, generate an optimal control strategy that satisfies the specification. We first provide a short overview of automata-based methods, in which the dynamics of the system are mapped to a finite abstraction that is then controlled using an automaton corresponding to the specification. We then provide a detailed overview of a class of methods that rely on mapping the specification and the dynamics to constraints of an optimization problem. We discuss advantages and limitations of these two types of approaches and suggest directions for future research.