zbMATH — the first resource for mathematics

Unique fixpoint induction for message-passing process calculi. (English) Zbl 0998.68089
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.

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDF BibTeX Cite
Full Text: DOI