无穷状态系统等价性验证

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

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.