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

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.

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

本项研究取得四项进展。一、否定了此前有关高阶进程演算和一阶pi-演算之间关系的伪命题。我们证明了：一般地，高阶演算无法在一阶pi-演算中得到解释，故高阶进程模型的表达能力不超过一阶pi-演算的结论是错误的。我们还研究了高阶模型的若干变种之间的表达能力关系。二、我们提出了extensional Petri网模型，在该模型中，Petri网是可复合的，这解决了传统Petri网不可复合的问题。三、我们加强了Senizergues获得哥德尔奖的结果，证明了epsilon-pushing nPDA和epsilon-popping PDA均为可判定的。这方面的两篇文章尚在审稿中。最后，我们研究了C-图的计数问题，证明了不确定计算的结构是非常复杂的。这方面的一篇文章也在审稿中。