Parallelism Theorem and Derived Rules for Parallel Coherent Transformations
This work addresses foundational issues in graph transformation theory, providing incremental theoretical advancements for researchers in formal methods and category theory.
The paper proves an Independent Parallelism Theorem in adhesive HLR categories, establishing a bijective correspondence between sequential and parallel independent direct derivations in the Weak Double-Pushout framework, and shows that derived rules can be extracted from Parallel Coherent Transformations.
An Independent Parallelism Theorem is proven in the theory of adhesive HLR categories. It shows the bijective correspondence between sequential independent and parallel independent direct derivations in the Weak Double-Pushout framework, see [2]. The parallel derivations are expressed by means of Parallel Coherent Transformations (PCTs), hence without assuming the existence of coproducts compatible with M as in the standard Parallelism Theorem. It is aslo shown that a derived rule can be extracted from any PCT, in the sense that to any direct derivation of this rule corresponds a valid PCT.