A Generalized Concurrent Rule Construction for Double-Pushout Rewriting

TL;DR

This paper introduces generalized concurrent rules in double-pushout graph rewriting, allowing for more flexible rule composition by preserving elements deleted and created across rules, extending the existing concurrency theorem.

Contribution

It proposes a new class of generalized concurrent rules within the double-pushout framework, broadening the scope of rule composition and concurrency results.

Findings

Introduces generalized concurrent rules (GCRs) that preserve elements across rules.

Establishes a Generalized Concurrency Theorem for GCRs.

Positions GCRs within the existing double-pushout rewriting framework.

Abstract

Double-pushout rewriting is an established categorical approach to the rule-based transformation of graphs and graph-like objects. One of its standard results is the construction of concurrent rules and the Concurrency Theorem pertaining to it: The sequential application of two rules can equivalently be replaced by the application of a concurrent rule and vice versa. We extend and generalize this result by introducing generalized concurrent rules (GCRs). Their distinguishing property is that they allow identifying and preserving elements that are deleted by their first underlying rule and created by the second one. We position this new kind of composition of rules among the existing ones and obtain a Generalized Concurrency Theorem for it. We conduct our work in the same generic framework in which the Concurrency Theorem has been presented, namely double-pushout rewriting in M-adhesive categories via rules equipped with application conditions.