Unique fixpoint induction for message-passing process calculi. (English) Zbl 0998.68089

Hennessy, M.; Lin, H.; Rathke, J.

Sci. Comput. Program. 41, No. 3, 241-275 (2001).

Summary: We present a proof system for message-passing process calculi with recursion. The key inference 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.

MSC:

68Q85

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)

Keywords:

proof system; message-passing process calculi with recursion

Software:

Coq