Axiomatizing Lüttgen & Vogler's ready simulation for finite processes in CLLR

In the framework of logic labelled transition systems, 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 some desirable properties. This paper offers a ground-complete axiomatization for this precongruence over processes containing no recursion in the calculus CLLRCLLR. Compared with the usual inference systems for process calculi, in addition to axioms about process operators, such system contains a number of axioms to characterize the interaction between process operators and logical operators.