On the operational semantics of distributed concurrent systems

A methodology for defining truly concurrent operational semantics of distributed concurrent systems in a compositional way and for obtaining a hierarchy of increasingly abstract descriptions is proposed. All our descriptions at any level of abstraction are consistent by construction: first a very concrete operational semantics, called initial, is defined which fully expresses both the spatial and the internal structure of systems, and the causal dependencies of the actions they perform. From the initial description more abstracts ones are stepwise derived, which in turn define four operational semantics: the distributed, the causal, the multiset and the interleaving ones. All the descriptions have been defined within a fully declarative approach by inducing on the syntactic structure of the involved objects in a merely compositional way.