Unguardedness mostly means many solutions

A widely accepted method to specify (possibly infinite) behaviour is to define it as the solution, in some process algebra, of a recursive specification, i.e., a system of recursive equations over the fundamental operations of the process algebra. The method only works if the recursive specification has a unique solution in the process algebra; it is well-known that guardedness is a sufficient requirement on a recursive specification to guarantee a unique solution in any of the standard process algebras.In this paper we investigate to what extent guardedness is also a necessary requirement to ensure unique solutions. We prove a theorem to the effect that all unguarded recursive specifications over have infinitely many solutions in the standard models for . In contrast, we observe that there exist recursive specifications over , necessarily involving parallel composition, that have a unique solution, or finitely many solutions in the standard models for .