The tile model

The tile model relies on certain rewrite rules with side effects, called tiles, reminiscent of both Plotkin SOS and Meseguer rewriting logic rules. It provides a logic of concurrent systems with conditional state changes and synchronization, and has been shown to be especially useful for defining compositional models of mobile processes and causal and located concurrent systems. The tile model has been used for modelling coordination formalisms equipped with flexible synchronization primitives. The main advantage of the tile approach is the full compositionality of the underlying logic, which is able to handle computations of (nonclosed) system components as they were new rewrite rules specifying complex coordinators. [FM97a,GM97].

Ferrari and Montanari used tiles to give a tile-based semantics for located CCS in [FM97b]. They give a treatment of concurrent process calculi where the same operational and abstract concurrent semantics described in the literature now descend from general, uniform notions. More precisely, a tile-based semantics for located CCS is shown to be consistent with the ordinary concurrent (via permutation of transitions) and bisimilarity based location semantics. The tile model is particularly well suited for defining directly operational and abstract semantics of concurrent process calculi in a compositional style.

[[FM97a]] Ferrari, G., Montanari, U. A Tile-Based Coordination View of Asynchronous $\pi$-calculus, In Proc. MFCS'97, LNCS 1295, 1997.

[[FM97b]] Ferrari, G., Montanari, U. Tiles for Concurrent and Located Calculi. In Proc. EXPRESS'97, ENTCS 7, 1997.

[[GM97]] Gadducci, F. and Montanari, U., The Tile Model. In: Gordon Plotkin, Colin Stirling, and Mads Tofte, Eds., Proof, Language and Interaction: Essays in Honour of Robin Milner, MIT Press, to appear.