无限状态CCS进程的等价验证问题研究

CCS, an abstract computational model proposed by Milner, can depict concurrent systems and infinite state systems. It has been widely studied and a great deal of results have been throughout many fields, such as expressiveness, behavioral equivalence, program language, program analysis and information security etc. However, verification of equivalences on infinite state processes are still not studied systematically. This proposal focuses on eight problems of verification on infinite state processes of CCS disallowing the restriction operator. It does not only improve understanding the theory of CCS, but also benifit the formal analysis and verification of concurrent programs and large-scale systems. In this propposal, the decidability of equivalence checking of branching/weak bisimilarity are established by introducing tableau systems and decomposition properties for CCS disallowing the restriction operator, and a sound and complete axiom system is proposed respectively for branching/weak bisimilarity on infinite state processes of CCS disallowing the restriction operator. The decidability of regularities of strong/branching/weak bisimilarity are proved by be reduced to the one of the corresponding equivalence checking. They can be used to deduce that the finitenesses are decidable.

CCS是由Milner提出用于描述并发系统的抽象计算模型，具备描述无限状态系统的能力。30多年来，相关研究已经涉及表达能力、行为等价、程序语言、程序分析和信息安全等多个理论和应用领域，但在无限状态进程的等价验证方面仍有待深入。课题拟研究不考虑受限操作子时无限状态CCS进程的等价验证相关问题，有助于理解CCS的理论性质，而且还能运用于并发程序以及大规模系统的形式化分析与验证。首先通过良定义序性质建立适合分支互模拟和弱互模拟的Tableau系统，并据此证明相应等价性问题的可判定性；接着给出两种互模拟关系的可靠完备的公理系统；然后将强互模拟/分支互模拟/弱互模拟的正则性问题规约为相应的等价性问题，证明正则性问题的可判定性，并由此推导出有限性问题是可判定的。

CCS是描述并发系统的抽象计算模型，具备描述无限状态系统的能力。其相关研究已经涉及多种变体、表达能力、行为等价、程序语言等多个领域。关于其变体的理论结果研究也有很多，但随着研究的深入，显现出两个问题：1）针对不同的关注点，如算子、通道的使用方式等，演化出更多的变体，这些变体的性质仍未可知；2）已有研究缺乏一个统一有效的理论体系，甚至会得到相矛盾的结果。我们针对这两个问题，在模型独立的交互理论框架下对四类演化变体展开研究。首先给出两类扩展变体关于绝对等价的外部刻画，进一步给出了它们在有限状态项上的可靠完备的证明系统；另外两类变体由于缺乏有效的控制机制，其等价关系尚有待进一步研究。通过对可计算模型的编码实现，根据完备性公理，证明四类变体都是交互完备的，即其无限状态进程间的等价关系是不可判定的；给出了三类演化变体间不相容的相对表达能力结果。随着对等价关系理论的深入认识，基于轨迹等价理论提出新技术应用于并发程序测试领域。