A Logic for Modular Descriptions of Asynchronous and Synchronized Concurrent Systems
Roberto L. Bruni · Electronic Notes in Theoretical Computer Science · 1998
Tile logic is a framework to reason about the dynamic evolution of concurrent systems in a modular way, and it extends rewriting logic (in the unconditional case) by rewriting synchronization and side effects. The subject of this dissertation concerns some interesting tile models of computation such that the mathematical structures representing configurations (i.e., system states) and effects (i.e., observable actions) have in common some auxiliary structure (e.g., for tupling, projecting, etc.). In particular, two such logics (called process and term tile logic respectively) are fully discussed, where net-process-like and usual term structures are employed. 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 new model 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 proofs are performed. Exploiting the reflective capabilities of the Maude language, such meta-layer is specified in terms of internal strategies. Some detailed examples illustrating the implementation of tile systems for interesting concurrent process calculi conclude the presentation.