A logic modular descriptions of asynchronous and synchronized concurrent systems.

*(English)*Zbl 0917.68099
Kirchner, Claude (ed.) et al., International workshop on Rewriting logic and its applications. Abbaye des Prèmontrès at Pont-á-Mousson, France, September 1998. Amsterdam: Elsevier, Electronic Notes in Theoretical Computer Science. 15, electronic paper No. 15 (1998).

Summary: 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 (ie, system states) and effects (ie, observable actions) have in common some auxiliary structure (eg, 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.

For the entire collection see [Zbl 0903.00070].

For the entire collection see [Zbl 0903.00070].

##### MSC:

68Q42 | Grammars and rewriting systems |