带量化信息的异构规范与其应用的研究

Logic labelled transition systems and the related process calculus CLLR admit to make use of logic operator and process operator to describe specifications of systems freely. These two heterogeneous specifications possess the advantage of the logic-based and behaviour-based specification approaches. This project aims to solve some problems which are encountered in the foundation of heterogeneous specifications with quantitative data, to explore the application of them in the research on safety and liveness and in the construction of controller. Main research topic of this project include: 1) To solve the problem of the definition of logic operator in logic labelled transition systems and CLLR associated with quantitative data, study the problem of computation of quantitative data in compositional systems, to found heterogeneous specifications with quantitative data. 2) By adopting the approximate equivalences and their preservation with respect to some operators, to provide the definition of safety and liveness, to explore their preservation, and to analyze the syntactic characterization of them. 3) To establish the relationship between heterogeneous specifications with quantitative data satisfied by control systems and their finite abstractions, and to offer two methodologies for constructing the controllers to satisfy different requirements. The results of this project will provide a novel uniform framework for logic-based and behavior-based specification approaches under considering quantitative data. They will present a new perspective for the research on safety and liveness and then illustrate the advantage of the novel framework. They will also solve the problem of the formal design of control systems w.r.t. heterogeneous specifications.

逻辑标记转换系统与相关进程演算CLLR允许自由使用逻辑算子和进程算子描述系统规范，这些异构规范兼顾基于逻辑与基于行为的两类规范方法的优点。本项目旨在解决建立带量化信息的异构规范时遇到的若干问题，探究其在安全性与活性的研究和控制器构造中的应用。主要内容包括：1）解决引入量化信息时逻辑标记转换系统和CLLR中逻辑算子的定义问题，探讨系统组合时量化信息的计算问题，建立带量化信息的异构规范；2）利用近似等价概念与其关于各类算子的保持性，给出安全性与活性的定义并研究其关于算子的保持性，分析安全性与活性的语法特征；3）揭示控制系统与其有限抽象分别满足的带量化信息的异构规范间的关系，给出构造适用于不同要求的控制器的设计方案。本项目的研究意义在于为基于逻辑与基于行为的规范方法在含量化信息的背景下提供新的统一框架；为安全性与活性的研究提供新角度，借此展现新框架的优点；解决关于异构规范的控制器构造问题。

本项目在带量化扰动信息的转换系统框架中给出了一个控制策略算法，该算法可以用于构造带扰动信息的控制系统的控制器，使控制系统在此控制器作用下可以满足线性时序逻辑公式所刻画的规范，从而解决了带量化扰动信息的控制系统的的形式化分析与设计中的控制策略求解问题；讨论了并发加权μ-演算的性质，给出了互模拟量词在标记加权转移系统上的语义，并研究了互模拟量词和并发加权μ－演算上一致性内插定理之间的关系，结合轮替树自动机，引入互模拟量词并证明了一致性内插定理在并发加权μ－演算上成立；为了分析安全性与活性的性质，在已有工作基础上引入了否定词的语义解释，证明了引入后所建立的进程演算符合直觉主义逻辑的公理，从而建立了新的异构规范系统，使得余算子、商算子和部分时序逻辑算子均可以给出相应的行为语义解释，为进程代数与逻辑的研究提供了统一框架，建立了不含递归的CSP与直觉主义逻辑的伽罗瓦连接，从而使进程代数与逻辑之间的关系更容易地揭示出来；探讨了协变-逆变精化模态逻辑及其公理化，扩展精化算子为CC-精化算子，扩展了Bozzelli等人的精化模态逻辑，建立了CC-精化模态逻辑，并且证明了在新的逻辑系统下，互模拟、精化及其他几种模型关系与相关算子均可建立联系。