无穷状态系统等价性验证

Equality checking on infinite state systems plays a crucial role both in theory and in formal method. The project aims to attack some open problems concerning equality checking on models defined in terms of process rewriting system. The decidability of the branching bisimilarity on epsilon-popping PDA will be investigated, and the completeness issue of the strong bisimilarity on BPA and the complexity of the branching bisimilarity on nBPP will be studied. The principal technical tool we apply is bisimulation tree method we have recently proposed.

无限状态系统的等价性验证既具理论意义，也在形式化方法中有广泛应用。本项目旨在研究有关用进程重写系统定义的若干模型上的等价关系可判定性的若干公开问题。主要考察epsilon-popping PDA的分支互模拟的可判定性、BPA上强互模拟的完备性和nBPP上分支互模拟的复杂性。使用的主要技术是申请人最近提出的互模拟树证明方法。

本研究项目主要取得了四方面进展：.1..开展了交互理论的基础性研究，提出了交互模型假设，证明了现有的一大类模型满足该假定，为进程模型分类和进程度的研究打下了基础。.2..研究了概率模型定义方法，提出了统一的构造概率模型的方法，并提出了研究概率模型语义的统一方法，为概率进程模型研究中的诸多问题提出了一个解决方案。.3..研究了非确定计算的结构，给出了非确定计算谱系的一个公式刻画。.4..证明了带内部动作的无限状态PDA的等价性验证是可判定的，并给出了验证算法。