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

TL;DR

This paper provides a complete set of axioms for a specific behavioral preorder in finite processes within the process calculus CLL_R, enhancing understanding of process interactions without recursion.

Contribution

It introduces a ground-complete axiomatization for the ready simulation preorder in CLL_R, including axioms for operator interactions, which was previously unestablished.

Findings

Axiomatization is ground-complete for the preorder.

Includes axioms for process and logical operator interactions.

Applicable to non-recursive processes in CLL_R.

Abstract

In the framework of logic labelled transition system, a variant of weak ready simulation has been presented by L\"{u}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.