进程理论中的否定结果研究

项目名称： 进程理论中的否定结果研究

项目编号： No.61472239

项目类型： 面上项目

立项/批准年度： 2015

项目学科： 自动化技术、计算机技术

项目作者： 傅育熙

作者单位： 上海交通大学

项目金额： 80万元

中文摘要： 否定结果在数学、数理逻辑、计算机科学中扮演着重要角色。在进程理论中，否定结果能推进进程理论向深度发展。本申请项目拟探索进程理论中有重要意义的否定结果，主要考察两个方面：一、研究进程表达能力的否定结果，即证明一个模型的表达能力不比另一个强，或两个模型的表达能力不一致等结果。表达能力的否定结果是建立现有模型之间关系图的关键步骤。二、研究不可有限公理化问题，主要研究有限状态进程上等价关系的不可有限公理化问题，这里有限公理化是指不使用规不动点归纳的完备系统。不可有限公理化方面的结论不仅对设计验证系统有实际应用，而且对模型设计和算子选择具有指导意义。本申请项目的意义在于通过探索具有重要意义的否定结果，推进进程理论证明技术和低层理论的研究，加快进程理论的深度研究以及对模型无关的核心理论的探讨。

中文关键词： 进程理论；否定结果；表达能力；公理化

英文摘要： Negative results play a crucial role in mathematics, logic and computer science. In process theory, negative results help reveal the depth of the theory. The project aims to investigate some negative results in process theory. Two aspects will be studied. Firstly we attempt to prove some negative results on expressiveness. By showing that one model is not as expressive as another, or that two models are incompatible with each other in terms of expressiveness, we advance our understanding of process theory in particular and concurrency theory in general. Secondly we look at the non-axiomatisability issue of the finite states, focusing mainly on equational systems without using the fixpoint induction. Results obtained in this direction are useful to the construction of verification systems. It is expected that the techniques developed in this have wide applications in process theory.

英文关键词： Process theory;Negative results;Expressiveness;Axiomatization