Abstract   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      BPA        have infinitely many solutions in the standard models for      BPA       . In contrast, we observe that there exist recursive specifications over      PA       , necessarily involving parallel composition, that have a unique solution, or finitely many solutions in the standard models for      PA       .
['Jcm Jos Baeten', 'Sp Bas Luttik']
Unguardedness mostly means many solutions