Underspecification for a simple process algebra of recursive processes

AbstractThis paper deals with underspecification for process algebras which is relevant in early design stages. We consider a form of underspecification that arises from a situation where at a certain design stage the decision between several options of system behaviour is to be postponed until more information is available. We follow an approach of Veglioni and De Nicola (Lecture Notes in Computer Science 1466 (1998) 179) who propose to interpret the choice operator + of a simple class of finite process terms as underspecification whenever it combines two processes that have some initial action in common, as e.g. in (a.P+b.Q)+(a.R+c.S). In particular, we consider recursive processes and discuss several extensions