| 摘要: |
| 本文提出消除π－演算中无卫递归的公理，证明了将该公理加入到正则π－演算受卫递归子集上的证明系统后，所得到的证明系统在π－演算全体正则子集上关于互模拟等价的可靠性和完备性. |
| 关键词: 进程代数 π－演算 互模拟 递归进程 证明系统 |
| DOI： |
| 分类号: |
| 基金项目:本文研究得到国家自然科学基金,中国科学院“九五”基础性研究重点项目资助. |
|
| ON REMOVING UNGUARDED RECURSIONS IN THE π CALCULUS |
|
LIN Huimin
|
| Abstract: |
| 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. |
| Key words: Process algebras π calculus bisimulation recursive processes proof systems. |
