The principles of ambient calculus revisited

The paper presents a foundational analysis of the class of ambient calculi focussing on the spatial structures of the processes they can describe. We propose sound correct set-theoretical models for different types of ambient calculi (involving recursion, denumerable parallel composition, etc) by using special types of coalgebras - labelled flat systems of equations of set theory. These models help to understand the spatiality of the ambient processes and provide a set-theoretical description of the structural congruence. Consistently with the model, we extend the classical structural congruence, the extension proving that P|P|P|...=(recX.X|P)=(recX|X|X|...|X|P), if X does not appear free in P. In Ambient Calculus the space has a decisive influence in the behavior of a process. Consequently, replication cannot simulate recursion because the processes involving replication have always a finite or denumerable class of active actions, while there are recursive ambient processes having infinite non-denumerable active actions due to a possibly non-wellfounded spatial structure. Still recursion can successfully describe any process involving replication. Thus we propose the most expressive Recursive Ambient Calculus, interpreting replication as recursion. Using the set-theoretical model for this calculus, we construct a propositional temporal logic on top of it able to describe properties of the processes. Our logic works similarly with wellfounded and non-wellfounded processes.