On infinite guarded recursive specifications in process algebra

TL;DR

This paper extends the completeness proof of ACP with guarded recursion to include general infinite recursive specifications, beyond the previously restricted finite or linear cases.

Contribution

It broadens the completeness result to encompass all guarded recursive specifications, including infinite and non-linear cases.

Findings

Completeness proof now applies to general infinite guarded recursive specifications.

Extends previous results limited to finite or linear recursive specifications.

Enhances the theoretical foundation of process algebra with guarded recursion.

Abstract

In most presentations of ACP with guarded recursion, recursive specifications are finite or infinite sets of recursion equations of which the right-hand sides are guarded terms. The completeness with respect to bisimulation equivalence of the axioms of ACP with guarded recursion has only been proved for the special case where recursive specifications are finite sets of recursion equations of which the right-hand sides are guarded terms of a restricted form known as linear terms. In this note, we widen this completeness result to the general case.