Unique fixpoint induction for message-passing process calculi

摘要

We present a proof system for message-passing process calculi with recursion. The key infer- ence rule to deal with recursive processes is a version of Unique Fixpoint Induction for process abstractions. We prove that the proof system is sound and also complete for guarded regular message-passing processes. We also show that the system is incomplete for unguarded processes and discuss more powerful extensions with inductive inference rules.