摘要
本文提出消除π-演算中无卫递归的公理,证明了将该公理加入到正则π-演算受卫递归子集上的证明系统后。
Axioms for removing unguarded recursions in the π calculus are proposed. It is shown that these two axioms are sound with respect to bisimulation equivalence, and are sufficient to reduce any unguarded recursively defined processes into guarded forms. Hence, by adding these axioms to the proof systems for guarded regular π calculus, complete proof systems for the whole regular π calculus are obtained.
出处
《软件学报》
EI
CSCD
北大核心
1997年第5期321-326,共6页
Journal of Software
基金
国家自然科学基金
中国科学院"九五"基础性研究重点项目
关键词
进程代数
Π-演算
互模拟
证明系统
无卫递归
Process algebras, π calculus, bisimulation, recursive, processes, proof systems.