# The Tile Model

In this paper we introduce a model for a wide class of computational
systems, whose behaviour can be described by certain rewriting rules.
We gathered our inspiration both from the world of term rewriting, in
particular from the {\em rewriting logic} framework \cite{Mes92}, and of
concurrency theory: among the others, the
{\em structured operational semantics} \cite{Plo81}, the {\em context systems}
\cite{LX90} and the {\em structured transition systems} \cite {CM92}
approaches.
Our model recollects many properties of these sources: first, it provides
a compositional way to describe both the states and the sequences of
transitions performed by a given system, stressing their distributed nature.
Second, a suitable notion of typed proof allows to take into account also
those formalisms relying on the notions of {\em synchronization} and
{\em side-effects} to determine the actual behaviour of a system.
Finally, an equivalence relation over sequences of transitions is defined,
equipping the system under analysis with a concurrent
semantics, where each equivalence class denotes a family of
``computationally equivalent'' behaviours, intended to correspond to the
execution of the same set of (causally unrelated) events.
As a further abstraction step, our model is conveniently represented using
double-categories: its operational semantics is recovered with a free
construction, by means of a suitable adjunction.