基于不确定测度的定量时序逻辑的表示与可判定性研究

The verification of function correctness and performance satisfiability of complex information system is an important aspect of credibility of information systems. Quantitative temporal logic can represent both the properties of function and the properties of performance of information system, and the verification of these properties can be reduced to the decidability of quantitative temporal logic. Therefore, it is a challenge problem to devise one kind of quantitative temporal logic such that it can represent both the properties of function and the properties of performance of information system, and it is decidable. This project will study the representation and decidability of quantitative temporal logic based on uncertainty measures, then the new approach can be inferred such that the function and performance of information system can be represented by the corresponding quantitative temporal logic, and function correctness and performance satisfiability of information system can be tackled using the decidability of quantitative temporal logic. In the concrete, quantitative temporal logic with quantitative domain as an evaluation monoid will be defined, and then the expressiveness of the corresponding quantitative temporal logic will be studied. This kind of quantitative temporal logic will be the universal form of quantitative temporal logic. By devising some methods of transforming a quantitative temporal logic formula into a weighted automaton or transforming a quantitative temporal logic formula into a soft constraint problem solving, this project will study systematically the representation and decidability of quantitative temporal logic based on measure theory under uncertainty environment. Using the above theory, the approximate abstraction method of quantitative model checking will be investigated, and the state reduction method based on approximate equivalence will be studied. This will provide us a method to design a quantitative temporal logic which is both expressible and decidable. Then the theory of model checking will be enriched. For the application of the method provided by this project, some quantitative model checking auxiliary tools will be devised and case study on some standard information systems will be given.

信息系统的功能正确性验证和性能可满足性验证是信息系统正确运行的重要保障。定量时序逻辑可以表示信息系统的功能和性能性质，而这些性质的验证可以归结为定量时序逻辑的可判定性。那么，如何设计一种定量时序逻辑，使其既具有较强的表达能力，又是可判定的，这是目前信息系统从理论层面亟需解决的关键性问题。本项目将研究基于不确定测度的定量时序逻辑的表示和可判定性，以期提供信息系统功能正确性和性能可满足性验证新方法。在理论方面，拟给出定量论域取为赋值幺半群的定量时序逻辑，提供定量时序逻辑的通用形式；拟研究将定量时序逻辑公式转化为加权自动机或软约束问题的方法，进而系统研究不确定环境下基于测度论的定量时序逻辑的表示和可判定性的基本理论；基于该理论，研究基于模型检测验证方法的逼近抽象理论，以提供定量的模型检测新方法，并设计验证辅助工具。在应用方面，将本项目提供的方法和辅助工具应用于智能交通等几个典型信息系统。

定量时序逻辑及其对应的模型检测是信息系统功能正确性和性能可满足性验证的重要的理论和方法，是当前时序逻辑及其对应模型检测的主流研究方向。本项目在此取得系统成果。完成了基于可能性测度的时序逻辑及其对应的模型检测方法；完成了格值时序逻辑及其对应的模型检测方法；提出基于自动机约简和约束问题求解的方法并用于对应模型检测的状态简化；在量子信息的度量方面开展了系统的研究。具体地，定义基于可能性测度的线性时序逻辑的并讨论了其表达能力，基于模糊矩阵运算、不动点技术巧妙地给出线性时序性质的验证方法，形成可能性时序逻辑模型检测的特征。通过引入时间加权函数给出模糊时态的语义，定义了含模糊时间的模糊时态词的可能性线性时序逻辑与计算树逻辑，证明了其较强的表达能力；基于模糊矩阵运算和模糊Buchi自动机给出了对应的模型检测算法。系统研究了不确定型模糊Kripke结构的计算树逻辑的模型检测，证明了对应问题的可判定性，给出了该问题在对数时间内的算法。在格值线性时序逻辑方面通过引入基于剩余类布尔型蕴含的多值线性时序性质，基于格值自动机定义了系统满足线性性质的程度。完成了基于格值可能性测度的格值计算树逻辑定义，讨论了其表达能力，以及对应的模型检测算法，克服了已有时序逻辑在表达性方面的一些缺陷，并证明了该逻辑相较经典计算树逻辑和多值计算树逻辑的更强的表达能力，并通过模糊矩阵运算、不动点算法给出对应模型检测算法，形成了完整的理论框架。通过医疗系统、智能系统等设计模型检测器并实现了上述算法。针对上述定量模型检测，提出利用格值自动机和约束问题求解简化对应的模型状态。特别地，我们提出了基于相似性度量的模糊自动机的状态近似逼近等价的全新方法，并研究了状态逼近等价下的自动机状态极小化简化方法。进一步，基于语言的近似等价的概念给出模糊语言的一个无穷谱系，对模糊自动机可近似表达的系统进行了深入的研究，得到了完备的结果。在约束问题求解方面，探讨了约束满足问题的三类易处理类并给出对应算法。在量子不确定系统、量子相干性度量方面开展了较为系统的研究，在量子信息的度量及其作为资源在信息处理与量子计算方面形成了系统的成果。该项目提出了新型定量时序逻辑及其模型检测理论，所取得的成果具有较大的国际影响。该项目共发表各类论文70余篇，其中SCI源论文57篇，部分成果获得陕西省教育厅自然科学奖。