On Meije and SCCS: Infinite sum operators vs. non-guarded definitions (Q789888)

SCCS is an algebraic calculus, due to R. Milner, modelizing concurrent synchronized processes. Its main difference with the latter Meije, from G. Boudol, comes from choice of principal operator for setting processes in parallel: synchronous in the former calculus, asynchronous in the latter. From there two distinct notions of time, global or local, emerge. SCCS global grasp of time made it tend to disfavor so-called unguarded process definitions to the benefit of an infinitary choice operator (infinite indexed sum). Questions of unrestricted, and perhaps non- constructive syntax were then raised. We began studying here how Meije, without infinitary operators but with full use of unguarded, ''instant- ''recursive process definitions, could partially simulate SCCS. For instance Meije's \(x\quad where\quad x=a:0\| x\) corresponds to SCCS's \(fix x.\sum_{i\geq 1}a^ i:0\). We produced affirmative results under constructive assumptions for processes of atomic lifetime. It allowed us to show realisation in Meije from another SCCS operator, restriction on an allowed subset of the action monoid, as soon as this set is ''constructible''. Since the article we showed how every recursively enumerable action-labelled transition system may be realized in Meije (these \(3^{ieme}\) cycle, université Jussieu P. 7, France). It is thus the case for the whole constructive subclass of SCCS.