Process Creation and Full Sequential Composition in a Name-Passing Calculus

This paper presents a first attempt to formulate a process calculus featuring process creation and sequential composition, instead of the more usual parallel composition and action prefixing, in a setting where mobility is achieved by communicating channel names. We discuss the questions of scope and name binding, raised by the interaction of mobility and sequential composition. Substitution of names is integrated as a syntactic operator in the calculus. Although many aspects necessary to model the combination of process creation, sequential composition and name-passing are taken into account, the setup described in this paper is not yet satisfactory, in that it does not give rise to a useful abstract behavioural equivalence. In particular, the natural notion of bisimulation in our calculus gives rise to a relation that is not a congruence