Formal Methods for Dynamical Systems
Formal Methods for Dynamical Systems
复制标题
动力系统的形式化方法
DOI：
--
复制
发表时间：
2012
期刊：
影响因子：
--
通讯作者：
C. Belta
中科院分区：
文献类型：
--
作者：
C. Belta
在控制理论中，物理过程的“复杂”模型，如微分方程系统，通常是根据“简单”规范，如稳定性和集合不变性来检查的。在形式化方法中，“丰富的”规范，如语言和时间逻辑公式，与软件程序和数字电路的“简单”模型（如有限转换图）进行核对。随着网络物理和安全关键系统的发展和集成，越来越需要计算工具来从丰富的时间逻辑规范中验证和控制复杂系统。即使对于非常简单的无限空间连续和混合系统，形式验证和综合问题也证明是不可判定的。然而，近年来，可证明正确但保守的方法受到了很多关注，其中动力系统的性质满足是通过系统的有限过近似（抽象）的性质满足来暗示的。一些类别的系统允许从时间逻辑规范计算有效的验证和控制进行审查。对于连续、离散时间线性系统和连续时间多线性系统，证明了有限抽象只能通过多面体运算来构造。通过使用来自模型检查和自动机游戏的技术，这允许根据状态变量中的线性谓词的线性时间逻辑（LTL）公式给出的规范进行验证和控制。对于离散线性系统和切换线性系统，建立了李雅普诺夫函数的存在性与有限双模拟之间的联系。最后，将最优性和正确性要求结合在模型预测方法中以生成离散时间线性系统的控制策略。这些计算工具的有用性通过各种例子来说明，例如合成生物学中的生物电路的验证和合成以及机器人中的运动规划和控制。
In control theory, "complex" models of physical processes, such as systems of differential equations, are usually checked against "simple" specifications, such as stability and set invariance. In formal methods, "rich" specifications, such as languages and formulae of temporal logics, are checked against "simple" models of software programs and digital circuits, such as finite transition graphs. With the development and integration of cyber physical and safety critical systems, there is an increasing need for computational tools for verification and control of complex systems from rich, temporal logic specifications. The formal verification and synthesis problems have been shown to be undecidable even for very simple classes of infinitespace continuous and hybrid systems. However, provably correct but conservative approaches, in which the satisfaction of a property by a dynamical system is implied by the satisfaction of the property by a finite over-approximation (abstraction) of the system, have received a lot of attention in recent years. Some classes of systems allowing for computationally efficient verification and control from temporal logic specifications are reviewed. For continuous and discrete-time linear systems and continuous-time multi-linear systems, it is shown that finite abstractions can be constructed through polyhedral operations only. By using techniques from model checking and automata games, this allows for verification and control from specifications given as Linear Temporal Logic (LTL) formulae over linear predicates in the state variables. A connection between the existence of Lyapunov functions and finite bisimulations is established for discrete-time linear and switched linear systems. Finally, optimality and correctness requirements are combined in a model predictive approach to generate control strategies for discrete-time linear systems. The usefulness of these computational tools is illustrated with various examples such as verification and synthesis of biological circuits in synthetic biology and motion planning and control in robotics.