Greatest solutions of equations in $\text{CLL}_R$ and its application

TL;DR

This paper investigates the solutions of equations in the process calculus $ ext{CLL}_R$, proving the maximality of certain solutions and encoding a fragment of action-based CTL within it.

Contribution

It establishes the maximal solutions for guarded equations in $ ext{CLL}_R$ and demonstrates how a fragment of action-based CTL can be encoded in this calculus.

Findings

Proved that strongly guarded equations have largest solutions in $ ext{CLL}_R$.

Successfully encoded a fragment of action-based CTL in $ ext{CLL}_R$.

Enhanced understanding of solution structures and expressiveness of $ ext{CLL}_R$.

Abstract

This paper explores the process calculus $\text{CLL}_R$ furtherly. First, we prove that for any equation $X=_{RS} t_X$ such that $X$ is strongly guarded in $t_X$, $\langle X|X=t_X \rangle$ is the largest solution w.r.t $\sqsubseteq_{RS}$. Second, we encode a fragment of action-based CTL in $\text{CLL}_R$.