递归数据传送进程的证明系统

本文提出了递归数据传送进程互模拟的证明系统，并证明了其可靠性和相对于数据推理的完备性，其中关键的推理规则是唯一不动点归纳法，这个结果一方面将Ｍｉｌｎｅｒ关于正则基本ＣＣＳ的公理系统推广到数据传送进程，另一方面将Ｈｅｎｎｅｓｓｙ与Ｌｉｎ关于有穷数据传送进程的证明系统推广到无穷进程。

PROOF SYSTEMS FOR VALUE-PASSING PROCESSES WITH RECURSION

This paper presents inference systems for value-passing process calculi with recursion, and proves their soundness and completeness with respect to lateand early-bisimulation equivalences (relative to data domain reasoning). The key inference rule to deal with recursion is Unique Fixpoint induction. These results on the one hand generalize the complete axiomatization for regular pure-CCS by Mimer to value-passing processes, on the other hand generalize the proof systems for finite value-passing processes by Hennessy and Lin to infinite processes.