A fixpoint approach to finite delay and fairness

AbstractWe introduce a language SCCSσ with a restriction operation on recursion. This involves a relativization of processes to formal environments which can be seen as a simple typing of processes. The fragment SCCSμν of SCCSσ drops explicit typing by introducing both least and greatest fixpoint operators. SCCSμν is expressive enough so that both SCCS and the Finite Delay Calculus of Milner (1982) can be regarded as subcalculi. The delay operators can be defined by εP: = μx.lx + P and δP:= νx.lx + P. Syntactic full abstractness results are proven for fortification and fair bisimilarity. We propose a collection of algebraic laws and induction rules (which imply Milner's fixpoint rule in Milner (1982)) and prove the theory sound for fair bisimilarity and fortification. The theory is strong enough so that it can prove all the laws for the delay operators taken as axioms in the Finite Delay Calculus of Milner. Finally, we sketch a semantics for SCCSσ that is fully abstract for fair bisimilarity and fortification. The semantics is along the lines of Aczel's (1994) and this author's (1997) and it is defined as the largest solution ℘(in the category of classes) of the recursive equation X = ℘(Act × X) × ℘ (Actω)