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

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 results of this project would explore the inherent relationship between control systems and their finite abstractions which offers the theoretical basis for the formal design of these systems, and solve the problem of the design of controller for infinite state control systems with disturbances.

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

本项目完成了计划书中基于近似行为等价理论的控制系统形式化设计方面的研究，并新增了混成规范理论方面的研究。具体论述如下: 控制系统的形式化设计方面，本项目基于近似交替互模拟的逻辑特征，在时序逻辑规范上引入了“弱化”转换函数和“强化”转换函数。这两个函数用于刻画控制系统与其有限抽象分别受控满足的规范间的关系。进而，利用“弱化”转换函数提出了一种方法用于构造控制系统的控制器使其受控近似满足给定规范；利用“强化”转换函数，另一种用于构造使原系统严格满足规范的控制器的方法被提出了。本项目还分析比较了上述两种方法与文献中已有的方法，指出了各自的优缺点和适用范围。最后给出了仿真实验说明上述两种方法的有效性并展示了这些方法的不同适用范围。在近似行为等价理论的研究中，本项目为(eta,alpha)-互模拟建立了分层刻画，揭示了越晚出现的差异越不重要这种折扣思想，并基于(eta,alpha)-互模拟的分层刻画给出了一种该互模拟的判定算法。本项目还提供了一个简单的例子用于说明(eta,alpha)-互模拟及其判定算法在描述实现与规范间关系上的应用。在混成规范理论研究方面，本项目在进程演算系统CLLR中研究了解的唯一性和公理化问题，给出例子说明了在进程演算系统CLLR中递归等式的解一般不唯一，并证明了当递归变元是强有卫时，递归项是递归等式的最大解；证明了预备模拟概念是一个前同余关系，并为其建立了公理系统。本项目还将Patrick Maier关于直觉主义线性时序逻辑的研究扩张到了计算树逻辑中，基于完全树和非完全树构成的集合提出了一种直觉主义解释的计算树逻辑，在此逻辑框架中研究了安全性和活性及其相关性质，并为直觉主义计算树逻辑公式建立了分解定理。