Tiles for Concurrent and Located Calculi
Gian-Luigi Ferrari, Ugo Montanari · Electronic Notes in Theoretical Computer Science · 1997
When concurrency is a primitive notion, models of process calculi usually include commuting diamonds and observations of causality links or of abstract locations. However it is still debatable if the existing approaches are natural, or rather if they are an ad hoc addition to the more basic interleaving semantics. In the paper a treatment of concurrent process calculi is proposed where the same operational and abstract concurrent semantics described in the literature now descend from general, uniform notions. More precisely we introduce a tile-based semantics for located CCS and we show it consistent with the ordinary concurrent (via permutation of transitions) and bisimilarity based location semantics. Tiles are rewrite rules with side effects, reminiscent of both Plotkin SOS and Meseguer rewriting logic rules. We argue that the tile model is particularly well suited for defining directly operational and abstract semantics of concurrent process calculi in a compositional style.