Concurrency theorems for non-linear rewriting theories

DOI10.1007/978-3-030-78946-6_1MaRDI QIDQ2117255zbMATH OpenOpenAlexFDO

Authors Nicolas Behr, Russ Harmer, Jean Krivine

Publication date 21 March 2022

Full work available at URL https://arxiv.org/abs/2105.02842

Grammars and rewriting systems (68Q42) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Abstract: Sesqui-pushout (SqPO) rewriting along non-linear rules and for monic matches is well-known to permit the modeling of fusing and cloning of vertices and edges, yet to date, no construction of a suitable concurrency theorem was available. The lack of such a theorem, in turn, rendered compositional reasoning for such rewriting systems largely infeasible. We develop in this paper a suitable concurrency theorem for non-linear SqPO-rewriting in categories that are quasi-topoi (subsuming the example of adhesive categories) and with matches required to be regular monomorphisms of the given category. Our construction reveals an interesting "backpropagation effect" in computing rule compositions. We derive in addition a concurrency theorem for non-linear double pushout (DPO) rewriting in rm-adhesive categories. Our results open non-linear SqPO and DPO semantics to the rich static analysis techniques available from concurrency, rule algebra and tracelet theory.

Recommendations

Cites work

Cited in

(20)

Describes a project that uses

Uses Software

AGREE

This page was built for publication: Concurrency theorems for non-linear rewriting theories

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2117255)