On the greatest solution of equations in $\text{CLL}_R$

TL;DR

This paper proves that in the process calculus CLL_R, the recursively defined process < X | X = t_X > is the greatest solution to equations where X is strongly guarded, with respect to ready simulation.

Contribution

It establishes that the recursive process is the greatest solution for strongly guarded equations in CLL_R under ready simulation semantics.

Findings

Recursive process < X | X = t_X > is the greatest solution.

The result applies to equations with strongly guarded variable X.

The proof is based on L"{u}ttgen and Vogler's ready simulation.

Abstract

It is shown that, for any equation $X=_{RS} t_X$ in the LLTS-oriented process calculus $\text{CLL}_R$, if $X$ is strongly guarded in $t_X$, then the recursive term $\langle X|X=t_X \rangle$ is the greatest solution of this equation w.r.t L\"{u}ttgen and Vogler's ready simulation.