{'fraction_non_alphanumeric': 0.04707119994628108, 'fraction_numerical': 0.014235512679902411, 'mean_word_length': 4.379003130267277, 'pattern_counts': {'":': 1, '<': 0, '<?xml version=': 0, '>': 0, 'https://': 0, 'lorem ipsum': 0, 'www.': 0, 'xml': 0}, 'pii_count': 0, 'substrings_counts': 0, 'word_list_counts': {'cursed_substrings.json': 6, 'profanity_word_list.json': 0, 'sexual_word_list.json': 0, 'zh_pornsignals.json': 0}}
Sesqui-Pushout Rewriting: Concurrency, Associativity and Rule Algebra Framework

Sesqui-pushout (SqPO) rewriting is a variant of transformations of graph-like and other types of structures that fit into the framework of adhesive categories where deletion in unknown context may be implemented. We provide the first account of a concurrency theorem for this important type of rewriting, and we demonstrate the additional mathematical property of a form of associativity for these theories. Associativity may then be exploited to construct so-called rule algebras (of SqPO type), based upon which in particular a universal framework of continuous-time Markov chains for stochastic SqPO rewriting systems may be realized.


Motivation and relation to previous work
The framework of Sesqui-Pushout (SqPO) rewriting has been introduced relatively recently in [16] as a novel alternative to the pre-existing algebraic graph transformation frameworks known as Double-Pushout (DPO) [26,24,17,34] and Single-Pushout (SPO) rewriting [32,35,38]. In the setting of the rewriting of graph-like structures, the distinguishing feature of the aforementioned DPO-type rewriting is that the deletion of vertices with incident edges is only possible if the incident edges are explicitly deleted via the application of the rewriting rule. In contrast, in both the SqPO and the SPO rewriting setups, "deletion in unknown context" is implementable. Thus for practical applications of rewriting, in particular in view of the modeling of stochastic rewriting systems, the S(q)PO rewriting semantics provide an important additional option for the practitioners, and will thus in particular complement the existing DPO-type associative rewriting and rule algebra framework as introduced in [3,7]. Referring the interested readers to [36] for a recent review and further conceptual details of the three approaches, suffice it here to quote that SqPO and SPO rewriting via linear rules 1 (defined as monic spans) and along monomorphic matches effectively encode the same semantics of rewriting. We chose (by the preceding argument without loss of expressivity) to develop the theory of associative rewriting within the SqPO rather than the SPO setting, since the SqPO framework bears certain close technical similarities to the DPO rewriting framework, which proved crucial in finding a strategy for the highly intricate proofs of the concurrency and associativity theorems presented in this paper. While it is well-known (see e.g. Section 5.1 of [16]) that DPO-and SqPO-type semantics coincide for certain special classes of linear rules (essentially rules that do not delete vertices), and while these cases might provide some valuable crosschecks of technical results to the experts, SqPO-type semantics is in its full generality a considerably more intricate variant of semantics due to its inherent "mixing" of pushouts with final pullback complements. It should further be noted that we must impose a set of additional assumptions on the underlying formation from stochastic rewriting systems via analysis of certain combinatorial relationships (so-called nested commutators) of the infinitesimal generator of the CTMC with the (pattern-counting) observables of the system. It is via these relations that one may in certain cases obtain exact closed-form solutions for such dynamical data (see e.g. Section 6). It would nevertheless be an intriguing avenue for future research to understand better the finer points of the "traditional" stochastic rewriting frameworks (which also feature sophisticated developments in terms of probabilistic model-checking and various types of stochastic logics), and furthermore whether or not rule-algebraic techniques might be of interest also in more general stochastic rewriting semantics such as probabilistic (timed) graph transformations [33,40].
Structure of the paper: In Section 2, some category-theoretical background material is provided. The key results of associativity and concurrency of SqPO rewriting are presented in Section 3, followed by the construction of SqPO-type rule algebras in Section 4. The second part of the paper contains the stochastic mechanics framework (Section 5) as well as a practical application example (Section 6). Technical proofs are situated in the Appendix.

Background: adhesive categories and final pullback complements
We recall some of the elementary definitions and properties related to the notions of adhesive categories, upon which our framework will rely.
We will be exclusively interested in categories that satisfy certain finiteness properties (in order to ensure finiteness of the sets of matches for rule applications and compositions, see Section 3): Definition 2 (Finitary categories [12]). A category C is said to be finitary if every object X ∈ obj(C) has only finitely many subobjects (i.e. if there only exist finitely many monomorphisms Y → X up to isomorphism for every X ∈ obj(C)). For every adhesive category C, the restriction to finite objects of C defines a full subcategory C f in called the finitary restriction of C.
Theorem 1 (Finitary restrictions; [12], Thm. 4.6). The finitary restriction C f in of any adhesive category C is a finitary adhesive category.
Adhesive categories have been introduced and advocated in [34] as a framework for rewriting due to their numerous useful properties, some of which are listed in Appendix A for the reader's convenience. One of the central concepts in the theory of SqPO rewriting is the following: Definition 3 (Final Pullback Complement (FPC); [16,36]). Let C be a category. Given a commutative diagram as in (1) on the right, a pair of morphisms (d, b) is a final pullback complement (FPC) of a pair (c, a) if (i) (a, b) is a pullback of (c, d) (i.e. if the square marked (B) is a pullback square), and (ii) for each collection of morphisms (x, y, z, w) as in (1) on the right, where (x, y) is pullback of (c, z) and where a • w = x, there exists a unique morphism w * with d • w * = z and w * • y = b • w.
For our associative rewriting framework, it will be crucial to work with a category in which (i) FPCs are guaranteed to exist when constructing them for composable pairs of monomorphisms, and (ii) monomorphisms are stable under FPCs, i.e. FPCs of pairs of monomorphisms are given by pairs of monomorphisms. This property is satisfied by adhesive categories (cf. Lemma 3 of Appendix A), yet to the best of our knowledge the question of which more general types of categories possess this property has not yet been investigated to quite the level of generality as analogous classification problems in the case of DPO rewriting, even though there does exist a large body of work on classes of categories that admit SqPO constructions [16,39,36,14,37]. Within these classes, according to [13,14] guarantees for the existence of FPCs may be provided for categories that possess a so-called M -partial map classifier. However, it appears to be an open question of whether the statement of Lemma 3 on stability of monomorphisms under FPCs may be generalized to the setting of M -adhesive categories, where M is a class of monomorphisms. Relaying such questions to future work, we refer to Lemma 4 of Appendix A for a well-known instantiation of a suitable categorical setting from the SqPO literature in the form of the category FinGraph of finite directed multigraphs, which also serves to illustrate the FPC construction.
Assumption 1. C is an adhesive category in which all FPCs along monomorphisms exist, and in which monomorphisms are stable under FPCs.

Sesqui-Pushout rewriting
We will now develop a framework for Sesqui-Pushout (SqPO) rewriting in the setting of a category C satisfying Assumption 1, in close analogy to the framework of associative Double-Pushout (DPO) rewriting as introduced in [7,8]. Unlike in the general setting of SqPO rewriting, we will thus be able to not only prove a concurrency theorem (Section 3.1), but also an associativity property of the SqPO-type rule composition (Section 3.2).

Concurrent composition and concurrency theorem
For reasons that will become more transparent when introducing the SqPO-type rule algebra framework starting from Section 4, we opt for a non-standard convention of reading spans of monomorphisms "from right to left" (rather than the traditional "left to right"), which is why we will speak of "input" and "output" of rules rather than "left-" and "right hand sides" to avoid confusion.
Definition 4 (SqPO-type rewriting; compare [16], Def. 4). Let C be an adhesive category satisfying Assumption 1. Denote by Lin(C) the set of (isomorphism classes 2 of) so-called linear productions, defined as the set of spans of monomorphisms, (2) Given an object X ∈ obj(C) and a linear production p ∈ Lin(C), we denote the set of SqPO-admissible matches M sq p (X) as the set of monomorphisms m : I → X. Then the diagram below is constructed by taking the final pullback complement marked FPC followed by taking the pushout marked PO: We write p m (X) := X for the object "produced" by the above diagram. The process is called (SqPO-) derivation of X along production p and admissible match m, and denoted p m (X) Next, a notion of sequential composition of productions is introduced: Definition 5 (SqPO-type concurrent composition). Let p 1 , p 2 ∈ Lin(C) be two linear productions. Then an overlap of the output object O 1 of p 1 with the input object I 2 of p 2 , encoded as a span (4) is constructible as a pushout complement (with the cospan I 2 obtained by taking the pushout marked PO). In this case, the remaining parts of the diagram are formed by taking the final pullback complement marked FPC and the pushouts marked PO: If m ∈ M sq p 2 (p 1 ), we write p 2 m p 1 ∈ Lin(C) for the composite of p 2 with p 1 along the admissible match m, defined as Due to stability of monomorphisms under pushouts, pullbacks and FPCs in the setting of a category satisfying Assumption 1, all morphisms in Definitions 4 and 5 are guaranteed to be monomorphisms, whence in particular the span p 2 m p 1 is a span of monomorphisms and thus indeed an element of Lin(C).
At first sight, it might appear irritating that in the definition of the SqPO-type rule composition, the right hand part of (4) involves a pushout complement (marked POC), while the left hand part of the diagram in (4) features a final pullback complement (marked FPC). Intuitively, considering the case of graph rewriting for concreteness, in a given sequential application of two productions, while the application of the first production may lead to implicit edge deletions, the second production is incapable of having any causal interaction with edges deleted by the first production. In contrast, the second production may in a given sequential application very well implicitly delete edges present in the output object of the first production, which explains the presence of the FPC in the defining equation (4). We refer the interested readers to [5] for further intuitions attainable in terms of so-called rule diagrams for presenting rule compositions. The justification for Definition 5 in the general case is provided via the following concurrency theorem. Even though at least in certain specialized settings the "synthesis" part of this theorem has been foreseen already in [36] (where it is also commented that a full concurrency theorem for SqPO rewriting might be attainable), the following result appears to be new.
Theorem 2 (SqPO-type Concurrency Theorem). Let C be an adhesive category satisfying Assumption 1. Let p 1 , p 2 ∈ Lin(C) be two linear rules and X 0 ∈ ob(C) an object.
• Synthesis: Given a two-step sequence of SqPO derivations with X 1 := p 1 m 1 (X 0 ) and X 2 := p 2 m 2 (X 1 ), there exists a SqPO-composite rule q = p 2 n p 1 for a unique n ∈ M sq p 2 (p 1 ), and a unique SqPO-admissible match n ∈ M sq q (X), such that q n (X) • Analysis: Given an SqPO-admissible match n ∈ M sq p 2 (p 1 ) of p 2 into p 1 and an SqPO-admissible match n ∈ M sq q (X) of the SqPO-composite q = p 2 n p 1 into X, there exists a unique pair of SqPOadmissible matches m 1 ∈ M sq p 1 (X 0 ) and m 2 ∈ M sq p 2 (X 1 ) with X 1 := p 1 m 1 (X 0 ) such that Proof. See Appendix B.1.

Composition and associativity
The following theorem establishes that in analogy to the DPO rewriting setting of [7], also the sesquipushout variant of rule compositions possesses a form of associativity property.
Then the SqPO-composition operation .
. . on linear productions of C is associative in the following sense: given linear productions p 1 , p 2 , p 3 ∈ Lin(C), there exists a bijective correspondence between pairs of SqPO-admissible matches (m 21 , m 3 (21) ) and (m 32 , m (32)1 ) such that Proof. Intuitively, the associativity property in the SqPO case manifests itself in a form entirely analogous to the DPO case [7], whereby the data provided along the path highlighted in orange below permits to uniquely compute the data provided along the path highlighted in blue and vice versa (with both sets of overlaps computing the same "triple composite" production that is encoded as the composition of the three spans in the bottom front row): See Appendix B.2 for the precise technical details of the proof.
We invite the interested readers to compare the SqPO-type constructions presented here against those contained in the extended journal version [8] of [7] for the DPO framework, since this might lend some intuitions on the otherwise very abstract nature of the proofs to the experts.

From associativity to SqPO-type rule algebras
For the rule algebra constructions, we will require an additional structure: Definition 6 (Initial objects). An object ∅ ∈ obj(C) of some category C is said to be a strict initial object if for every object X ∈ obj(C), there exists a unique morphism ∅ → X, and if any morphism X → ∅ must be an isomorphism.
For example, the category Graph and its finitary restriction FinGraph possess a strict initial object (the empty graph). For the experts, it appears worthwhile noting the following result: Lemma 1 (Extensive categories; [34], Lem. 4.1). An adhesive category C is an extensive category 3 if and only if it possesses a strict initial object.
Assumption 2 (Prerequisites for SqPO-type rule algebras). We assume that C is an adhesive category satisfying Assumption 1, and which is in addition finitary and possesses a strict initial object ∅ ∈ obj(C).
Definition 7 (SqPO-type rule algebras). Let δ : Lin(C) → R C be defined as an isomorphism from Lin(C) to the basis of a free R-vector space R C ≡ (R C , +, ·), such that 4 In order to clearly distinguish between elements of Lin(C) and basis vectors of R C , we introduce the notation Define the SqPO rule algebra product R C on a category C that satisfies Assumption 2 as the binary operation where for two basis vectors R i = δ (p i ) encoding the linear rules p i ∈ Lin(C) (i = 1, 2), The definition is extended to arbitrary (finite) linear combinations of basis vectors by bilinearity, whence for p i , p j ∈ Lin(C) and α i , β j ∈ R, We call R sq C ≡ (R C , R C ) the SqPO-type rule algebra over the finitary adhesive and extensive category C.
The rule algebra product R 2 R C R 1 for R j = δ (r j ) ( j = 1, 2) thus encodes the non-determinism in the SqPO-type sequential composition of the linear rule r 2 with r 1 in terms of the "sum over all possible compositions". As the following example illustrates, since δ is defined to map from isomorphism classes of linear rules to basis vectors of R C , and since two distinct matches may lead to isomorphic composite rules, R 2 R C R 1 typically evaluates to a linear combination of basis vectors δ (r) with integer coefficients: Example 1. Let C = FinGraph be the category of finite directed multigraphs, with ∅ the empty graph. Then with ≡ R C , we find for example The result of the composition thus captures the combinatorial insight that there are two contributions that evaluate to an isomorphic rule algebra element. More generally, one finds the following structure of compositions of rule algebra elements based upon "discrete" graph rewriting rules: letting • n denote the n-vertex graph without edges (for n ≥ 0), one finds (for p, q, r, s ≥ 0) This result is further interpreted in Example 2.
Theorem 4 (Properties of R sq C ). For every category C satisfying Assumption 2, the associated SqPOtype rule algebra R sq C ≡ (R C , R C ) is an associative unital algebra, with unit element R ∅ := (∅ ⇐ ∅).
For the unital and associative SqPO-type rule algebras, one may provide a notion of representations in analogy to the DPO-type case (compare [3,7]): . Let C be a category satisfying Assumption 2, with a strict initial object ∅ ∈ ob(C), and let R sq C be its associated rule algebra of SqPO type. Denote byĈ the free R-vector space spanned by basis vectors |X indexed by isomorphism classes of objects, Then the canonical representation ρ sq C : R sq C → End R (Ĉ) of R sq C is defined as a morphism from the SqPO-type rule algebra R sq C to endomorphisms ofĈ, with and extended to arbitrary elements of R sq C and ofĈ by linearity. Example 2. Extending Example 1, letting ρ ≡ ρ sq FinGraph , note first that by definition for all (isomorphism classes of) finite multigraphs G ∈ obj(FinGraph)∼ = , |G = ρ(δ (G ← ∅ → ∅)) |∅ . Witĥ as a consequence of (14) of Example 1 one may verify that In other words, the data of (17) and (18) furnishes a representation of the famous Heisenberg-Weyl algebra that is of fundamental importance in combinatorics and physics (see e.g. [9,10,11]). An alternative such representation is given by the linear operatorsx (multiplication by x) and ∂ x (derivation by x) acting on the R-vector space spanned by monomials x n , which reproduces equations isomorphic to (17) and (18), with ∂ x x n = nx n−1 andxx n = x n+1 . However, the action ofD andX is of course defined on all states |G with G ∈ obj(FinGraph), so that we may e.g. compute the following "derivative of a graph": The following theorem states that ρ sq C as given in Definition 8 is indeed a homomorphism (and thus qualifies as a representation of R sq C ). Theorem 5 (SqPO-type canonical representation). For a category C satisfying Assumption 2, ρ sq C :

Applications of SqPO-type rule algebras to stochastic mechanics
In practical applications of stochastic rewriting systems, the type of rewriting semantics presents one of the key design choices. For example, if in a given situation a stochastic graph rewriting system should be implemented, choosing DPO-vs. SqPO-type rewriting entails two entirely different semantics in terms of the behavior of vertex deletion rules: in the former case, vertices may only be deleted if also all its incident edges are explicitly deleted as well, while in the latter case no such restriction applies (i.e. an application of a vertex deletion rule "automatically" leads to the deletion of all incident edges). Evidently, such fundamentally different behavior at the level of rewriting rules will also have strong influence on the dynamical behavior of the associated stochastic rewriting systems, whence it is of considerable practical interest to have a universal implementation of such systems available in both formalisms. We begin by specializing the general definition of continuous-time Markov chains (see e.g. [41,1]) to the setting of SqPO-type rewriting systems in close analogy to [3,6,7].
Definition 9 (Continuous-time Markov Chains (CTMCs); compare [7], Def. 7.1). Let C be a category satisfying Assumption 2, and which in addition possesses a countable set of isomorphism classes of objects obj(C)∼ = . LetĈ denote the free R-vector space introduced in Definition 8. We define the space Prob(C) as the space of sub-probability distributions in the following sense: Let Stoch(C) := End R (Prob(C)) be the space of endomorphisms of Prob(C), with elements referred to as sub-stochastic operators. Then a continuous-time Markov chain (CTMC) is specified in terms of a tuple of data (|Ψ(0) , H), where |Ψ(0) ∈ Prob(C) is the initial state, and where H ∈ End R (S C ) is the infinitesimal generator or Hamiltonian of the CTMC (with S C the space of real-valued sequences indexed by elements of obj(C)∼ = and with finite coefficients). H is required to be an infinitesimal (sub-) stochastic operator, which entails that for Then this data encodes the evolution semi-group E : R ≥0 → Stoch(C) as the (point-wise minimal nonnegative) solution of the Kolmogorov backwards or master equation: Consequently, the time-dependent state |Ψ(t) of the system is given by An important technical aspect of the above definition of CTMCs is the definition of the relevant space of (sub-)probability distributions in interaction with the definition of the infinitesimal generator H and of the space S C . Some remarks on this interaction and a short explanation of the relevant mathematical concepts are provided in Appendix B.5.
Our main approach in studying CTMCs based on rewriting systems will consist in analyzing the dynamical statistical behavior of so-called observables: We furthermore define the so-called projection operation | : S C → R via extending by linearity the definition of | acting on basis vectors ofĈ, These definitions induce a notion of correlators of observables (also referred to as (mixed) moments), defined for O 1 , . . . , O n ∈ O C and |Ψ ∈ Prob(C) as The precise relationship between the notions of CTMCs and SqPO-type rewriting rules as encoded in the corresponding SqPO-type rule algebra formalism is established in the form of the following theorem, where in particular the notion of observables is quite different in nature to the DPO-type analogon (compare Thm. 7.12 of [7]). This result is the first-of-its-kind universal definition of SqPO-type stochastic rewriting systems with "mass-action semantics" (where activities of productions are proportional to their number of admissible matches in a given system state).
Theorem 6 (SqPO-type stochastic mechanics framework). Let C be a category satisfying Assumption 2.
C } j∈J be a (finite) set of rule algebra elements, and {κ j ∈ R ≥0 } j∈J a collection of non-zero parameters (called base rates). Then one may construct the Hamiltonian H of the associated CTMC from this data according to Here, the notation O sq M for arbitrary objects M ∈ obj(C) denotes the observables (sometimes referred to as motif counting observables) for the resulting CTMC of SqPO-type, with We furthermore have the SqPO-type jump-closure property, whereby for all (O Proof. See Appendix B.5.

Application example: a dynamical random graph model
In order to illustrate our novel SqPO-type stochastic mechanics framework, let us consider a dynamical system evolving on the space of finite directed multigraphs.
Example 3. Let FinGraph be the finitary restriction of the category Graph (see also Lemma 4), and denote by ∅ ∈ FinGraph the strict initial object (the empty graph). We define a stochastic SqPO rewriting system based upon rules encoding vertex creation/deletion (v ± ) and edge creation/deletion (e ± ): Together with a choice of base rates ν ± , ε ± ∈ R ≥0 and an initial state |Ψ(0) ∈ Prob(FinGraph), this data defines a stochastic rewriting system with Hamiltonian H :=Ĥ +H, where ) and E ± := ρ sq FinGraph (δ (e ± )). Despite the apparent simplicity of this model (which might be seen as a paradigmatic example of a random graph model), the explicit analysis via the stochastic mechanics framework will uncover a highly non-trivial interaction of the dynamics of the vertex-and of the edge-counting observables. Intuitively, since in SqPO-rewriting no conditions are posed upon vertices that are to be deleted, the model is expected to possess a vertex dynamics that is the one of a so-called birth-death process. If it were not for the vertex deletions, one would find a similar dynamics for the edge-counting observables (compare e.g. the DPO-type rewriting model considered in [7]). However, since deletion of vertices deletes all incident edges, the dynamics of the edge-counting observable is rendered considerably more complicated, and in particular much less evident to foresee by heuristic arguments.
In order to compute the dynamics of the vertex counting observable O V := O , we follow the approach of exponential moment-generating functions put forward in [3,6,4] and define with λ a formal variable. M V (t; λ ) encodes the moments of the observable O V , in that taking the n-th derivative of M V (t; λ ) w.r.t. λ followed by setting λ → 0 yields the n-th moment of O V . Note that we must assume the finiteness of all statistical moments as standard in the probability theory literature in order for M V (t; λ ) to be well-posed, a property that we will in the case at hand indeed derive explicitly.
Referring the interested readers to [8] for further details, suffice it here to recall the following variant of the BCH formula (see e.g. [28], Prop. 3.35), for λ a formal variable and A, B two composable linear operators, with the convention that ad •0 ] is typically referred to as the commutator. We may then derive the formal evolution equation for M V (t; λ ): Since by definition | H = 0, it remains to compute the adjoint action Here, the result that [O V , E ± ] = 0 has a very simple intuitive meaning: in applications of the linear rules e ± , the number of vertices remains unchanged, whence the vanishing of the commutator. Combining these results with the SqPO-type jump-closure property (cf. Theorem 6), we finally arrive at the following formal evolution equation for M V (t; λ ): Supposing for simplicity an initial state The resulting initial value problem may be solved in closed-form via semi-linear normal-ordering techniques known from the combinatorics literature [22,9,11,6] (see also [8,4]), and we obtain (for t ≥ 0) In the limit t → ∞, the moment-generating function becomes that of a Poisson-distribution (of parameter ν + /ν − ), thus confirming the aforementioned intuition that the vertex-counting observable has the dynamical behavior of a so-called birth-death process (see e.g. [6]).
Let us consider next the dynamics of the edge-counting observable O E := O , where for brevity we will only consider the evolution of the mean edge count. The calculation of the evolution equation for the expectation value of O E simplifies to the analogue of the so-called Ehrenfest equation, Recalling that | H = 0, it remains to compute the commutator [O E , H]: Together with an initial condition such as e.g. |Ψ(0) = |G 0 for some (finite) directed graph G 0 with N V vertices and N E edges, and computing the closed-form expression for the first contribution in (40) from our previous solution (37) (as ∂ λ (∂ λ − 1)M V (t; λ ) followed by setting λ → 0), the initial value problem for the mean edge count evolution may be easily solved in closed form via the use of a computer algebra software such as MAPLE, MATHEMATICA or SAGE. It is also straightforward to verify that for an arbitrary initial state |Ψ(0) = |G 0 , the limit value of the mean edge count for t → ∞ reads Since the rates ν ± and ε ± are free parameters, the above result entails that in this model one may freely adjust the limit value of the average vertex count as encoded in (36) (whence ν + /ν − ) as well as the limit value of the average edge count via suitable choices of the parameters ε ± . For illustration, we present some plots of the mean edge count evolution for the case |Ψ(0) = |∅ and various choices of parameters in Figure 1.

Conclusion and Outlook
Extending our previous work on Double-Pushout (DPO) rewriting theories as presented in [3,7,4] to the important alternative setting of Sesqui-Pushout (SqPO) rewriting, we provide a number of original results in the form of concurrency and associativity theorems for SqPO rewriting theories on adhesive categories. These fundamental results in turn permit us to formulate so-called SqPO-type rule algebras, which play a central role in our novel universal stochastic mechanics framework. We strongly believe that these contributions will provide fruitful grounds for further developments both in theory and practice of rewriting beyond the specialists' communities, especially in view of static analysis techniques [2].
[41] J. R. Norris (1997) Notational convention: Here and as throughout this paper, while evidently category-theoretical constructions such as pushouts are only unique up to isomorphisms, we will typically nevertheless pick convenient representatives of the respective isomorphism classes to simplify our notations. As standard practice in the literature, we will thus e.g. fix the convention as in (42) to choose representatives appropriately to label the pushout along an isomorphism with "equality arrows" (rather than keeping object labels generic and decorating the relevant arrow with a " ∼ =" symbol).
Lemma 2. Let C be a category.
Proof. Referring to the references above for the proofs of the (well-known) statements (where necessary by specializing the more general case of M -adhesive categories to the case of adhesive categories via setting M to the class of all monomorphisms), it remains to prove our novel vertical FPC-pushout decomposition result. To this end, we first invoke pullback-pushout decomposition (Lemma 2(3d)) in order to demonstrate that since (3) + (4) is an FPC and thus also a pullback, and since (3) is a pushout and since x ∈ mono(C), (4) is a pullback. By applying vertical FPC-pullback decomposition, we may conclude that (4) is an FPC. In order to demonstrate that v ∈ mono(C), construct the commutative cube below left: Since the bottom square is the FPC (and thus pullback) (3) + (4), and since the right square is a pullback via Lemma 2(1c) (because v ∈ mono(C)), by pullback composition the square (Z , Z, X,Y ) (the right plus the bottom square) is a pullback. Thus assembling the commutative diagram as shown above right, since by assumption (3) is a pushout and all arrows except v are monomorphisms, invoking Theorem 7 below permits to prove that also v ∈ mono(C).
The last part of the preceding proof relied upon one of the quintessential properties of adhesive categories in view of associative rewriting theories: Theorem 7 (Effective unions; [34], Thm. 5.1). In an adhesive category C, given a commutative diagram such as in the middle of (1), if all morphisms except the morphism x are monomorphisms, if the square marked (A) is a pushout and if the exterior square is a pullback, then x is also a monomorphism.
The following result provides several important facts on FPCs.
Lemma 3 (cf. [36], Fact 2, and [16], Lemma 2 and Proposition 2). Let C be adhesive. For an arbitrary morphism f : A → B, (id B , f ) is an FPC of ( f , id A ) and vice versa. Moreover, every pushout square along monomorphisms is also an FPC square. FPCs are unique up to isomorphism and preserve monomorphisms. The latter property entails that if C ← − A and if a ∈ mono(C), then also d ∈ mono(C) and vice versa (while c ∈ mono(C) entails that b ∈ mono(C) by stability of monomorphisms under pullbacks in an adhesive category C).
For concreteness, we quote the following explicit construction of FPCs in the category Graph of directed multigraphs: Lemma 4 (FPCs for graphs; [16], Sec. 4.1 and Construction 5). Let Graph denote the adhesive category of directed multigraphs, with B Proofs

B.1 Proof of the SqPO concurrency theorem
Proof. Throughout this proof, in each individual constructive step it may be verified that due to the stability of monomorphisms under pullbacks and pushouts, due to the various decomposition lemmata provided in the form of Lemma 2, and on occasion due to Theorem 7 on effective unions in adhesive categories, all morphisms induced in the "Synthesis" and "Analysis" steps are in fact monomorphisms. For better readability, we will not explicitly mention the individual reasoning steps on this point except for a few intricate sub-steps, since they may be recovered in a straightforward manner.
-Analysis: Given the setting as depicted in (47a) of Figure 3, where the top row has the structure of an SqPO-composition (compare (4)), where the square (K 21 , K 1 , N 21 , K 2 ) is a pullback, the left "curvy" bottom square a pushout and the right "curvy" bottom square an FPC, we may obtain the configuration of (47c) as follows: construct 9 K 1 via taking the final pullback complement of K 1 → I 21 → X 0 (which implies the existence of an arrow K 21 → K 1 via the FPC property). Note in particular that according to Lemma 3, both arrows constructed via forming the aforementioned FPC are monomorphisms, and thus by stability of monomorphisms in an adhesive category (compare Definition 1 and Lemma 2(1c)), the arrow K 21 → K 1 is a monomorphism as well. Next, take the pushout X 1 = PO(K 1 ← K 1 → N 21 ), followed by constructing K 2 as the final pullback complement of K 2 → N 21 → X 1 (which implies due to the FPC property of the resulting square (K 2 , K 2 , X 1 , N 21 ) the existence of an arrow K 21 → K 2 ). Invoking pullback-pullback decomposition (Lemma 2(3a)) twice, followed by the van Kampen property (Def. 1), we may conclude that the square (K 21 , K 21 , K 2 , K 2 ) is a pushout. Thus invoking pushout-pushout decomposition (Lemma 2(3b)), we find that also (K 2 , K 2 , X 2 , O 21 ) is a pushout. We finally arrive at the configuration in (47d) via composition of pushout and FPC squares, respectively, thus concluding the proof.

B.2 Proof of the SqPO associativity theorem
Our proof strategy will be closely related to the one presented in [7] (with full technical details provided in [8]) for the analogous associativity theorem in the DPO-rewriting case. However, the SqPO-type case poses considerable additional challenges, since this rewriting semantics yields diagrams of a rather heterogeneous nature (including pullbacks, pushouts, pushout complements and FPCs) as compared to the DPO case, and in addition unlike DPO-type rule compositions, SqPO-type compositions are not reversible in general, which necessitates an independent proof of both directions of the bijective correspondence.
Proof. We first prove the claim in the "⇒" direction, i.e. starting from the set of data we have to demonstrate that one may uniquely (up to isomorphisms) construct from this information a pair of admissible matches and such that the property described in (6) holds. We begin by forming the SqPO-composite rule p 3(21) = p 3 m 3(21) p 21 , which results in the diagram by virtue of invoking SqPO-composition twice. For the remainder of the proof, it is very important to precisely determine the nature of each of the squares in this diagram: • To clarify the structure of the rightmost four squares at the bottom, consider the setting presented in (47a): since in the definition of the SqPO-composition as presented in (4) the nature of the squares to the right is that of pushout complement and pushout, respectively, it may be verified that applying the analysis procedure to the diagram in (47a) with thus the "curvy" front and right bottom faces both pushouts, one eventually arrives (by virtue of pushout-pushout and pushoutpullback decomposition) at the setting depicted in (47c) with all squares in the bottom row being pushouts. Thus the rightmost four squares at the bottom of (50) are all pushouts.
• By virtue of the definition of SqPO-composition, all vertical squares in the back of (47c) are pushouts, except for the square (K 2 , K 2 , N 21 , I 2 ), which is an FPC. Analogously, the bottom leftmost three squares are (in order from left to right) a pushout, an FPC and a pushout.
Here, the rightmost three squares on the top are formed in the evident fashion (and they are pushouts by virtue of Lemma 2(1a)), while the other arrows of the above diagram are constructed as follows: Invoking pushout-pullback, pushout-pushout and vertical FPC-pullback decompositions, it may be verified that (describing positions of front and top square pairs by the position of the respective front square, from left to right) • the leftmost front and top squares are pushouts, • the second from the left front and top squares are FPCs, • the third from the left front and top squares are pushouts, • in the next adjacent pair, the front square is an FPC and the top square a pushout, • the second from the right front and top squares are pushouts, and • the rightmost front and top squares are pushouts. Defining the pullback object M (32)1 = PB(I 32 → N 3(21) ←O 1 ), thus inducing an arrow M 21 → M 3 (21) , it remains to verify that the square (M 3 (21) , I 32 , N 3 (21) , O 1 ) is not only a pullback, but also a pushout square. This part of the proof requires a somewhat intricate diagram chase; since the required arguments are identical 10 to the "⇒" part of proof of DPO-type associativity as presented in [8], we omit this part of the proof here in the interest of brevity.
It thus remains to prove the claim in the "⇐" direction, i.e. starting from the set of data we need to demonstrate that one may uniquely (up to isomorphisms) construct from this information a pair of admissible matches and such that the property described in (6) holds. We begin by forming the SqPO-composite rule p (32)1 = p 32 m (32)1 p 1 , which results in the diagram 10 More precisely, the only difference in the structure of the relevant sub-diagram compared to the DPO case resides in the two FPC squares in the front and back in fourth position from the left (which happen to be pushout squares in the corresponding DPO-type proof), but the structure of this part of the diagram is not explicitly used in the proof in the DPO variant of the theorem, whence the claim follows. by virtue of invoking SqPO-composition twice. A careful inspection of the definition of the SqPOcomposition and of the analysis part of the SqPO concurrency theorem permit to verify that the nature of all squares thus constructed coincides precisely with the nature of the corresponding squares in the "⇒" part of the proof.
Constructing the pullback M 21 = PB(I 2 → I 32 ← M (32)1 ) (which by composition of pullbacks also leads to an arrow M 21 →O 1 ) and forming the three additional vertical squares on the far right in the evident fashion in the diagram below allows us to construct N 21 = PO(I 2 ← M 21 →O 1 ), which in turn via the universal property of pushouts induces an arrow N 21 → N (32)1 : The remaining new squares of the above diagram are constructed as follows: Moreover, by virtue of vertical FPC composition, the square (K 3 , K 3 , N 3 (21) , I 3 ) is an FPC, while via pushout composition the square (K 3 , Again, the nature of all squares constructed thus far coincides precisely with the structure as presented in the "⇒" part of the proof, with one notable exception: by virtue of vertical FPC-pullback decomposition, we may only conclude that the square (K 2 , K 2 , N (32)1 , N 21 ) is an FPC (but at this point we do not know whether it is also a pushout as in the analogous part of the diagram in the "⇒" part of the proof). However, an auxiliary calculation demonstrates that this square is in fact a pushout in disguise -consider the following "splitting" of the relevant sub-part of the diagram as shown below: The precise steps are as follows: the front left square in the diagram above left is an FPC; thus if one takes the pushout N (32)1 = PO(K 2 ← K 2 → N 21 ) as well as in the bottom back the pushout along the isomorphism of K 2 as displayed (yielding the arrows in the middle), followed by taking the pullback O 1 = PB(N (32)1 , N (32)1 , O 1 ) (which entails that the arrow M 3(21) → O 1 exists), it is straightforward to verify that O 1 ∼ = O 1 . Invoking the van Kampen property (recalling that by definition the right square on the bottom is a pushout), we find that (M 3 (21) , O 1 , N (32)1 , I 32 ) is a pushout. Thus by pushout-pushout decomposition, the square (O 1 , O 1 , N (32)1 , N (32)1 ) is a pushout, whence N (32)1 ∼ = N (32)1 . This in summary entails 11 that the square (K 2 , K 2 , N (32)1 , N 21 ) is not only an FPC, but in fact also a pushout.
Back to the main proof, defining the pullback object thus inducing an arrow M 32 → M 3 (21) , it remains to verify that the square (M 3 (21) , O 21 , N 3 (21) , I 3 ) is not only a pullback, but also a pushout square. Let us construct the auxiliary diagram as depicted in Figure 4, with objects obtained via taking suitable pullbacks as indicated. The four cubes that are drawn separately are the top, back, bottom and front cubes induced via the newly constructed arrows, and are oriented such that one may easily apply the van Kampen property in the next step of the proof (which in most cases requires a suitable 3d-rotation). Invoking pullback-pullback decomposition and the van Kampen property repeatedly, it may be verified that in the relevant sub-diagram as presented below we find the following structure of the squares: • All squares on the top are pushouts, except the second one from the right (which is a pullback).
• The second and third square from the left in the back of the diagram are pushouts, the other two back squares are pullbacks, with the same structure for the front squares.
(47d) Figure 3: Analysis part of the concurrency theorem. • Counting from left to right, the second and fourth square on the bottom are pushouts, the other two are pullbacks.
In particular, as indicated this entails that D ∼ = B. We proceed by performing the following "splitting" of the diagram: Start the "splitting" via taking the pushouts N 32 = PO(I 3 ← I 3 → N 32 ) (which entails that N 32 ∼ = N 32 ) and O 2 = PO(M 3(21) ← M 32 → O 2 ). By pullback-pullback decomposition followed by pushout-pullback decomposition, we may conclude that the resulting square (O 2 , N 32 , I 3 , M 3 (21) ) is a pushout. Note also that all vertical squares in the bottom left part of the diagram thus constructed are pullbacks (by virtue of suitable pullback decompositions).
Next, construct the pullbacks K 2 = PB(N 32 → N 3(21) ← K 2 ) and K 2 = PB(O 2 → O 21 ← K 2 ). By pushout-pullback decomposition, in the diagram on the right the top and bottom front squares and back squares in the second column are pushouts, while the square (K 2 , K 2 , K 2 , K 2 ) is a pullback. Performing the precise same steps in the next column, i.e. via taking the pullbacks D = PB(K 2 → K 2 ← D) and B = PB(K 2 → K 2 ← B), we obtain via pushout-pullback decomposition that the top and bottom front and top and bottom back squares in the third column are pushouts, while the square (B , B, D, D ) is a pullback. But since D ∼ = B and since isomorphisms are stable under pullback, we conclude that D ∼ = B , and thus that the square (B , B, D, D ) is in fact a pushout.

B.3 Proof of the theorem on SqPO rule algebra properties
Proof. Associativity of R C follows from the associativity of the operation . . . proved in Theorem 3. The claim that R ∅ = δ (∅ ← ∅ → ∅) is the unit element of the rule algebra R sq C follows directly from the definition of the rule algebra product for R ∅ R C R and R R C R ∅ for R ∈ R sq C . More concretely, we present below the category-theoretic composition calculation that underlies the equation R ∅ R C R = R: Here, it is important to note that the pushout complement used to construct the square marked POC always exists (see Lemma 2(1a)), whence the claim follows.

B.5 Proof of the SqPO stochastic mechanics framework theorem
Proof. By definition, the SqPO-type canonical representation of a generic rule algebra element (O p ⇐ I) ∈ R C is a row-finite linear operator, since by virtue of the finitarity of objects according to Assumption 2, for every object X ∈ obj(C) the set of SqPO-admissible matches M sq p (X) of the associated linear rule p = (O o ← − K i − → I) is finite. We may thus verify that the linear operator H possesses all the required properties of a so-called Q-matrix (or infinitesimal generator) of a CTMC [41, 1], i.e. its non-diagonal entries are non-negative, its diagonal entries are finite, and furthermore the row sums of H are zero (whence H constitutes a conservative and stable Q-matrix; compare (21) of Definition 9). It is crucial to note that while originally H as a linear combination of representations of rule algebra elements is only defined to act on finite linear combinations of basis vectors |X ofĈ, an important mathematical result from the theory of CTMCs entails that if a row-finite linear operator such as H is a stable and conservative Q-matrix, it extends to a linear operator on infinitely supported distributions (here over basis vectors of