Paper detail

Axiomatizing Lüttgen and Vogler's ready simulation for finite processes in $\text{CLL}_R$

In the framework of logic labelled transition system, a variant of weak ready simulation has been presented by Lüttgen and Vogler. It has been shown that such behavioural preorder is the largest precongruence w.r.t parallel and conjunction composition satisfying desired properties. This paper offers a ground-complete axiomatization for this precongruence over processes containing no recursion in the calculus $\text{CLL}_R$. Compared with usual inference system for process calculus, in addition to axioms about process operators, such system contains a number of axioms to characterize the interaction between process operators and logical operators.