A generalized concurrent rule construction for double-pushout rewriting: Generalized concurrency theorem and language-preserving rule applications

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. Furthermore, we identify sufficient conditions for language-preserving applications of GCRs when these are computed from rules that belong to a given grammar. 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.