Tile Logic for Synchronized Rewriting of Concurrent Systems

Tile logic is a framework to reason about the dynamic evolution of concurrent systems in a modular way. It extends rewriting logic (in the unconditional case) by adding rewriting synchronization and side effects. This dissertation concerns both theoretical and implementation issues of tile models of computation where the mathematical structures representing configurations (i.e., system states) and observations (i.e., observable actions) rely on the same common auxiliary structure (e.g., for tupling, projecting, etc.). We proceed by considering maybe the simplest tile model (whose configurations and observations are just commutative monoids, and their sequential and parallel compositions coincide) and showing that it yields an original net model, called zero-safe net, which comes equipped with a primitive notion of transition synchronization, which is missing in ordinary Petri nets. The operational and abstract semantics of the model are expressed in the language of Net Theory and also as universal constructions in the language of Category Theory. Then, two original versions of tile logic (called process and term tile logic respectively) are fully discussed, where net-process-like and usual term structures are employed for modelling configurations and observations. The categorical models for the two logics are introduced in terms of suitable classes of double categories. Then, the new model theory of 2EVH-categories is proposed to relate the categorical models of tile logic and rewriting logic. This is particularly important, because rewriting logic is the semantic basis of several language implementation efforts (Cafe, ELAN, Maude), and therefore a conservative mapping of tile logic back into rewriting logic can be useful to get executable specifications of tile systems. The theory required to relate the two logics is presented in partial membership equational logic, a recently developed framework, which is particularly suitable to deal with categorical structures. The comparison yields a correct rewriting implementation of tile logic that uses a meta-layer to make sure that only tile computations are performed. Exploiting the reflective capabilities of the Maude language, such meta-layer is specified in terms of internal strategies. Several detailed examples illustrating the implementation of tile systems for concurrent process calculi conclude the presentation.