Unguardedness mostly means many solutions

J.C.M. Baeten, S.P. Luttik

Research output: Contribution to journalArticleAcademicpeer-review

4 Citations (Scopus)


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.
Original languageEnglish
Pages (from-to)3090-3100
JournalTheoretical Computer Science
Issue number28
Publication statusPublished - 2011


Dive into the research topics of 'Unguardedness mostly means many solutions'. Together they form a unique fingerprint.

Cite this