把不确定性用半环来描述的计算模型、理论及其应用研究

Uncertainty is a pervasive phenomenon in real world. The mathematical treatment of the uncertainty is a center of modern science. This project aims to deepen the study a kind of computation models involing a variety of uncertainty-weighted automata and their applications. Weighted automata are the most extensive computation model concerning uncertainty. Combinned with category theory, this project will provide a new appraoch to study weighted automata which is called the "reduction" theory and method. By the "reduction" method, one can reduce one kind of weighted automata into another kind of weighted automata using different semirings as weights. Then the structure and property of the weighted automata can be further characterized, and the approximation and optimization of weighted automata with different weights can be obtained. Using the "reduction" method, the project will study the state minimization of fuzzy (weighted) automata based on conjugate relation. By introducing the lattice-valued topology on weighted automata, this project will also study the Stone-type duality of weighted automata, which will give an equaitional theroy of weighted automata. The Stone-type duality of weighted automata will be useful to the study of decidability of weighted autoamta such as the equality and the inclusion relations between two weighted automata, and the minimization of weighted automata. This project will furher study the formal power series characterization of the weghted Turing machines. Using formal power series, we will provide an algebraic approach to the complexity theory of Turing machines. Also, we will make explicit the super computing power and the universalty of weighted Turing machine. As an application of the above study on weighted automata, we will develop a new theory of model checking involving uncertainty based on muti-valued logic or modeled by possibility measure.

不确定性是现实世界普遍存在的现象，不确定性的数学处理是现代科学的一个中心内容。本项目旨在研究把不确定性用半环来描述的计算模型：加权自动机。后者是当前计算理论研究中针对不确定性现象最为广泛的计算模型。结合范畴论本项目将提供研究加权自动机的新方法："归约"理论与方法，针对不同半环通过自动机的归约来对自动机的结构和性质给出进一步的刻画，并研究针对半环的加权自动机的逼近和优化结果；研究模糊（加权）自动机的基于共轭关系的状态最小化问题；引入加权自动机的格值拓扑结构，利用格上拓扑学的结论研究加权自动机的Stone型对偶，进而探讨加权自动机诸如语言相等、包含和极小化等基本问题的可判定性。研究加权图灵机的形式幂级数刻画问题，进一步研究加权图灵机的形式幂级数对图灵机本身的复杂性的反映，研究加权图灵机的超级计算能力以及通用性。作为应用，我们将针对多值与基于可能性测度的模型检测问题给出新的理论结果和检测算法。

基于半环的计算模型与理论研究是当前不确定环境下计算理论的主流研究方向。本项目在此取得系统成果，并将成果应用于量化模型检测领域。通过对形式幂级数的商、剩余商的研究，揭示了加权自动机的极小化构造。通过巧妙的构造，给出了通用加权自动机的完整结构，对加权自动机的状态极小化提供了新的研究视角。开展了加权自动机的互模拟以及极小化的研究，并特别研究了模糊自动机的近似互模拟关系，给出了求解模糊自动机极大近似互模拟关系的完整算法，系统研究了模糊自动机的近似极小化问题。初步建立了模糊正则语言的拓扑对偶理论，开辟了研究加权自动机的拓扑对偶方法。项目还完成了加权图灵机的相关理论研究，取得了一般的研究成果。作为上述理论的应用，项目较为系统地开展了基于可能性测度的模型检测方法研究，建立了基于模糊Buchi自动机的可能性线性时序逻辑(GPoLTL)的模型检测理论，建立了基于可能性计算树逻辑(GPoCTL)的模型检测理论，证明了基于可能性测度的计算树逻辑从表达能力上较经典计算树逻辑要强，从而基于可能性测度的时序逻辑可以在模糊系统的建模与验证方面发挥更大的作用。项目开展了量子计算与量子信息的理论研究，特别在量子程序的形式化研究以及量子程序的验证技术方面开展了较好的工作。针对相干性的度量问题进行了相关的研究，在有限维系统下，证明用保真度作为距离度量来量化相干性时，保真度不满足强单调的约束条件，同时，给定某些约束条件，迹范数可以作为量化相干性的度量。在无限维系统下，通过增加一个新的约束条件，证明相对熵仍然可以作为相干性的度量。这些结果部分回答了M. B. Plenio等人提出的公开问题。在开放环境下，提出基于逻辑的量子检测技术,并用于验证量子程序的终止问题和量子游走的概率特性。该项目丰富了不确定环境下的计算理论，所取得的成果具有较大的国际影响，处于国际领先地位，部分成果形成专著《模糊计算理论》。该项目共发表各类论文90余篇，其中SCI源论文28篇，部分成果获得教育部自然科学奖。