控制系统形式化设计中逻辑特征应用的研究

项目名称： 控制系统形式化设计中逻辑特征应用的研究

项目编号： No.11426136

项目类型： 专项基金项目

立项/批准年度： 2015

项目学科： 数理科学和化学

项目作者： 张晋津

作者单位： 南京审计学院

项目金额： 3万元

中文摘要： 近年来，近似行为等价理论在形式化方法和控制论领域均是研究热点，它为利用形式化方法解决控制系统的分析和设计问题提供了有效途径。本项目以近似行为等价的逻辑特征为理论基石，旨在解决带扰动控制系统形式化设计中遇到的若干问题，并提出基于有限抽象构造带扰动控制系统控制器的方案。主要研究内容包括：（1）描述带扰动控制系统与其近似有限抽象分别可控满足的逻辑规范间的关系；（2）提出一种控制策略算法，该算法用于求解使带扰动控制系统的有限抽象满足时序逻辑规范的控制策略；（3）在系统的有限抽象的控制策略存在的条件下，证明使原系统满足规范的控制器存在并给出构造方法；（4）基于上述工作给出两种适用于不同要求的带扰动控制系统形式化设计方法。 本项目的研究意义在于展现带扰动控制系统与其有限抽象之间的内在联系，为此类系统的形式设计提供理论依据，并解决状态无限的带扰动控制系统的控制器设计问题。

中文关键词： 形式化方法；反馈控制；时序逻辑；进程代数；计算树逻辑

英文摘要： Recently, the theory of approximate behavioral equivalence becomes a research focus in the areas of both formal method and control theory. It offers an available avenue for adopting formal methods to deal with the analysis and design of control systems. Due to logical characterization of approximate behavioral equivalence, this project aims to deal with the problems of the formal design of control systems with disturbances, and then provide approaches for constructing controllers of control systems with disturbances based on their finite abstractions. Main research topics of this project include: (1) To describe the relation between the logical specifications satisfied by control systems and their approximate finite abstractions under control, (2) To provide a control strategy algorithm which may be used to find control strategies of finite abstractions of control systems with disturbances so that finite abstractions satisfy the given temporal logical specifications under such control, (3) To prove the existence of controllers of control systems based on the control strategies of finite abstractions and to provide methods for constructing such controllers, (4) based on the above work, to offer two methodologies of the formal design of control systems with disturbances which fit different requirements. The result

英文关键词： formal methods；feedback control；temporal logic；process algebra；computation tree logic