ON THE IMPLEMENTATION OF CONCURRENT CALCULI IN NET CALCULI - 2 CASE-STUDIES

Concurrent calculi, such as CCS, are defined in terms of labelled tran sition system; similarly, here we introduce the notion of net (or dist ributed) calculus, which is defined through a place/transition Petri n et. As a first case study, a simple calculus of nets, called SCONE, is proposed, Relationships between SCONE and the subset of CCS without r estriction and relabelling, called RCCS, are studied by showing that R CCS can be implemented in SCONE through a suitable mapping from the tr ansition system for RCCS to net for SCONE. In particular, the complex CCS operation of global choice is implemented in terms of the SCONE fi ner grained operation of local choice, making explicit the fact that c ertain CCS transition are implemented as SCONE computations to be exec uted atomically. The result is a finite net implementation for RCCS ag ents. By making the quotient of the RCCS transition system w.r.t. the implementation mapping, we induce a truly concurrent semantics for RCC S. The second case study is then concerned with an extension dealing w ith restriction and relabelling. The resulting net calculus, called SC ONE(+), is exploited as an implementation language for full CCS. The t ruly concurrent semantics induced by the implementation mapping is pro ved to coincide with the so-called ''permutation-of-transitions'' sema tics.