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

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.