4.1 Graph conditions and satisfaction relation

The basic graph conditions (BGCs) of BGL feature the two propositional connectives \(\wedge \) (called \(conjunction \)) and \(\lnot \) (called \(negation \)) as well as the additional operators \(\exists \) (called \(exists \)) and \(\nu \) (called \(restrict \)) for extending and restricting matches into a symbolic graph (called host graph), respectively.

The \(exists \) operator requires an extension of a given match into the host graph by matching further graph elements (such as nodes and edges) or by describing attribute values of already matched variables more precisely. Hence, the \(exists \) operator extends a context that is given by the match.

The novel \(restrict \) operator allows to select a submatch of a given match, which matches fewer elements but matches these elements in the same way as the given match. Hence, the \(restrict \) operator shrinks a context that is given by the match.

The operators of BGL can be combined freely in BGCs with the requirement that \(exists \) and \(restrict \) operators must build upon the symbolic graph that represents the given context as usual. Technically, the operator \(exists \) describes the extension of a finite context graph H to a finite context graph \(H'\) via a monomorphism and the \(restrict \) operator describes the restriction of a finite context graph H to a finite context graph \(H'\) via a monomorphism .

In BGCs in our examples, for improved readability, we only use inclusions and employ the notation introduced below for their visualization.

See Fig. 5 for an example of a BGC demonstrating the use of nesting and BGL operators not making use of attributes, Fig. 6 for an example of a BGC focusing on the attribute part in combination with the usage of the novel global variables, and Fig. 7 for an example of a BGC making use of the novel restrict operator.

The satisfaction relation for BGL is given below in the form of an inductive definition that relies on the inductive definition of BGCs. The definition follows [43, 82] for the operators \(conjunction \), \(negation \), and \(exists \). However, it also defines the satisfaction for the additional restrict operator and relies on partially injective morphisms that are allowed to map global variables to values. For the case when checking a graph against a BGC, the satisfaction relation is defined using the initial morphism and BGCs over the empty graph \(\varvec{\varnothing } \). This case depends on the satisfaction relation where a partially injective morphism , which represents a match of the current context graph H into the host graph G, is checked against a BGC over the graph H. For conjunction and negation, the satisfaction relation is defined as expected. For satisfaction of the BGC , the definition requires an extension of the match m (as in [43, 82]) in the form of a match that satisfies the subcondition \(\phi \) and that is consistent with f in the sense of the commutation condition \(m'\circ f=m\). This condition means (if f is an inclusion) that \(m'\) is defined as m for all elements in H and that \(m'\) has additional mappings for the elements that are in \(H'\) but not in H. This commutation condition also guarantees that the global variables in H/\(H'\) that are mapped by m/\(m'\) to values in \(\mathcal {V} \) are evaluated to these values throughout the satisfaction check for the entire subcondition \(\phi \). Finally, the satisfaction relation requires for the BGC that the restricted match satisfies the subcondition \(\phi \). Note that the satisfaction check for the exists operator may not succeed when there is no suitable extension match \(m'\) but that the restrict operator always succeeds in restricting the given match m to the match \(m\circ f\).

Definition 13

(Satisfaction of BGCs) If \(\bar{\phi }\in \mathcal {S}^{\mathsf {BGC}} _{H} \) is a BGC and is a partially injective morphism, then \(m\models _{\mathsf {BGC}} \bar{\phi } \), if one of the following items applies.

• \(\bar{\phi }=\wedge S \) and \(\forall \phi \in S.\;m\models _{\mathsf {BGC}} \phi \).

• \(\bar{\phi }=\lnot \phi \) and \(m\not \models _{\mathsf {BGC}} \phi \).

• and there is s.t. \(m=m'\circ f\) and \(m'\models _{\mathsf {BGC}} \phi \).

• and \(m\circ f\models _{\mathsf {BGC}} \phi \).

Also, if \(\bar{\phi }\in \mathcal {S}^{\mathsf {BGC}} _{\varvec{\varnothing }} \) and \({\textsf {i} } (G) \models _{\mathsf {BGC}} \bar{\phi } \), then \(G\models _{\mathsf {BGC}} \bar{\phi } \).

See Fig. 5, Fig. 6, and Fig. 7 for examples of satisfaction checks for BGCs. Moreover, a discussion on the inherent problems of BGL satisfaction checking and an operationalization of it is given in “Appendix B.”

4.2 Operation \({\textsf {shift} }\) and encoding of restrict

We adapt and extend the operation \({\textsf {shift} }\) from [32, pp. 15-16] and [82, Def. 17, p. 716] to our setting of symbolic graphs with global variables and the additional restrict operator.¹² Intuitively, the operation \({\textsf {shift} }\) describes the propagation of a BGC over a morphism (which we assume to be a monomorphism here) preserving the semantics w.r.t. the satisfaction relation. The operation is commonly used as in [32] for propagating BGCs that restrict rule applicability in the context of graph transformation.¹³

Definition 14

(Operation \({\textsf {shift} }\) ) If \(\bar{\phi }\in \mathcal {S}^{\mathsf {BGC}} _{H} \), \(\bar{\phi }'\in \mathcal {S}^{\mathsf {BGC}} _{G} \) are BGCs and is a monomorphism, then \({\textsf {shift} } (m,\bar{\phi }) =\bar{\phi }'\), if one of the following items applies.

• \(\bar{\phi }=\wedge S \) and \(\bar{\phi }'=\wedge \{{\textsf {shift} } (m,\phi ) \mid \phi \in S\} \).

• \(\bar{\phi }=\lnot \phi \) and \(\bar{\phi }'=\lnot {\textsf {shift} } (m,\phi ) \).

• and

  \(\bar{\phi }'{=}\vee \{\exists (f',{\textsf {shift} } (m',\phi )) \mid (m',f'){\in }{\textsf {overlap} } (f,m) \} \).

• and \(\bar{\phi }'=\nu (m\circ f,\phi ) \).

In the following, we also adapt the standard soundness result for the \({\textsf {shift} }\) operation from [32, pp. 15-17] to our setting (see Fig. 8 for a visualization).

We now provide the operation \({\textsf {enc} }_{\nu }\), which encodes the restrict operator using the other operators of BGL. This operation thereby shows that the novel restrict operator increases the descriptive expressiveness but not the expressiveness of the logic. Also, procedures for satisfaction checking must then not be developed for the entire logic but only for the fragment not using the restrict operator. The encoding relies on the operation \({\textsf {shift} }\) to replace instances of restrict operators. See Fig. 7 for an example of the application of the operation \({\textsf {enc} }_{\nu }\) .

As already motivated for the definition of the \({\textsf {shift} }\) operation above, the two perspectives of shifting a BGC forwards over a monomorphism and describing the condition BGC in the context restricted by f are symmetric.

We now state the correctness of this encoding.

The encoding operation \({\textsf {enc} }_{\nu }\) is also sound for graphs as a direct consequence of Theorem 3.

Note that the encoding operation \({\textsf {enc} }_{\nu }\) may increase the size of a BGC drastically because the replacement condition is based on the set of graph overlappings computed by \({\textsf {shift} }\) via \({\textsf {overlap} }\) that grows exponentially with its inputs. We conclude that the operator restrict increases the descriptive expressiveness as it allows to state certain properties more concisely. The operation \({\textsf {enc} }_{\nu }\) is supported by our prototypical implementation in AutoGraph.

5.1 Rules and steps for graph transformation

We adopt the DPO approach as in [29] where rules \(\rho \) consist of two monomorphisms and . These two monomorphisms describe the removal and addition of graph elements (for symbolic graphs, such elements are nodes, edges, node attributes, edge attributes, local variables, and global variables). On the one hand, all graph elements in L that \({\rho }{.}{{\textsf {del} }} \) does not map to are to be deleted. On the other hand, all graph elements in R that \({\rho }{.}{{\textsf {add} }} \) does not map to are to be added. To permit the DPO-based removal of variables (see explanations above and Fig. 9 for the comparison with [74]), we require that L, K, and R have an AC of \(\top \). To specify attribute modifications, a rule contains two maps and as well as an AC \({\rho }{.}{{\textsf {ac} }} \) on the set V. This set V contains unprimed and primed variables given by the variables originating from L and R. The correspondence between these two kinds of variables in V (i.e., between an unprimed x and its primed counterpart \(x'\)) is given via²²\({{\rho }{.}{{\textsf {del} }}}{.}{{\textsf {X} }}_{\textsf {P} } \) and \({{\rho }{.}{{\textsf {add} }}}{.}{{\textsf {X} }}_{\textsf {P} } \). Moreover, we require that V is the coproduct (i.e., the disjoint union) of the two sets of variables via \({\rho }{.}{{\textsf {lX} }} \) and \({\rho }{.}{{\textsf {rX} }} \), written , which means that each variable in V can be associated unambiguously with a variable either in L or in R. Finally, we use BGCs \({\rho }{.}{{\textsf {lC} }} \) and \({\rho }{.}{{\textsf {rC} }} \) as application conditions on L and R, which further restrict rule application in Definition 18. See Fig. 11a for a visualization of the components of a rule.

See Fig. 10a for an example of a rule with nontrivial graph modification, removal of variables, and variable modifications. In Fig. 10a, we use a notation for rules introduced below.

The following definition introduces the special case of the identity rule for later use. It is to be applicable to any graph (with a satisfiable AC) and does not change the graph when being applied.

In the following, we introduce transformation steps for symbolic graphs based on the notion of a rule from above (see Definition 18 for the formal definition and Fig. 11b, Fig. 11c for accompanying visualizations).

In our definition, we follow [74] and permit graph transformation steps only between graphs G and H that have both satisfiable ACs since graphs with unsatisfiable ACs do not represent any grounded graphs (cf. Definition 10). However, in comparison to the approaches in [29, 74], we decompose the graph transformation step into a transformation stage for the graph part and a transformation stage for the AC part. This decomposition of the graph transformation step into two stages is achieved by pruning the AC of the graph G leading to a restricted graph \(\bar{G}\).

In the first transformation stage, we apply the DPO step as usual on \(\bar{G}\), the given rule \(\rho \), and using the match that is obtained by restricting the match from G to \(\bar{G}\) via the AC inclusion morphism \({\textsf {acInc} } (G)\). The graph \(\bar{H}\) obtained by application of this DPO step is then extended to a graph H by adding an AC to \(\bar{H}\) as discussed subsequently. Note that the graphs \(\bar{G}\), D, and \(\bar{H}\) have the AC \(\top \) due to this construction and that the pushout complement D exists uniquely according to Lemma 10 from Appendix C since we require that only the morphism d but not \(b_1\) can map global variables to values. Also, as usual for DPO-based transformation, we check whether the match \(m_1\) and the comatch (obtained by extending the restricted comatch from \(\bar{H}\) to H via the AC inclusion morphism \({\textsf {acInc} } (H)\)) satisfy the left and the right application conditions \({\rho }{.}{{\textsf {lC} }} \) and \({\rho }{.}{{\textsf {rC} }} \), respectively.

Definition 18

(Steps) If

1. (1)

   • \({\textsf {sat} }_{\exists } ({G}{.}{{\textsf {ac} }}) \),

   • \(\rho \in \mathcal {S}^{\mathsf {rules}} \) is a rule,

   • ,

     \(m_1\models _{\mathsf {BGC}} {\rho }{.}{{\textsf {lC} }} \),

   • ,

     \({\textsf {acInc} } (G) \circ c_1=m_1\),

   • ,

     ,

     ,

   • ,

     ,

     \((c_2,b_2)~\text {is a pushout of}~({\rho }{.}{{\textsf {add} }},d) \),

   • ,

     \({\textsf {acInc} } (H) \circ c_2=m_2\),

   • \(m_2\models _{\mathsf {BGC}} {\rho }{.}{{\textsf {rC} }} \),

    
2. (2)

   • ,

     ,

     ,

   • is obtained by using the universal property of the coproduct \({\amalg } ({\rho }{.}{{\textsf {lX} }},{\rho }{.}{{\textsf {rX} }}) \),

   • \(\gamma _{ eq }=\wedge \{\sigma _1(x)= \sigma _2(x) \mid x\in {D}{.}{{\textsf {X} }}-{d}{.}{{\textsf {X} }} ({K}{.}{{\textsf {X} }})\} \)

     where \(\sigma _1=k_1\circ {{\textsf {acInc} } (G)}{.}{{\textsf {X} }}_{\mathcal {V}} \circ {b_1}{.}{{\textsf {X} }}_{\mathcal {V}} \)

     \(\quad \,\hbox {and}\,\, \sigma _2=k_2\circ {{\textsf {acInc} } (H)}{.}{{\textsf {X} }}_{\mathcal {V}} \circ {b_2}{.}{{\textsf {X} }}_{\mathcal {V}} \),

   • \(\gamma = \wedge \{ \sigma _{ VX }({\rho }{.}{{\textsf {ac} }}), k_1({G}{.}{{\textsf {ac} }}), \gamma _{ eq } \} \) is an AC,

   • \({\textsf {sat} }_{\forall } ( {H}{.}{{\textsf {ac} }} \leftrightarrow {\textsf {rev} } (k_2) (\exists k_1({G}{.}{{\textsf {X} }}) .\; \gamma ) ) \), and

   • \({\textsf {sat} }_{\exists } ({H}{.}{{\textsf {ac} }}) \),

    

then is the step transforming the graph G into the graph H using the step label \(\varsigma = ( {\varsigma }{.}{{\textsf {rule} }}, {\varsigma }{.}{{\textsf {match} }}, {\varsigma }{.}{{\textsf {comatch} }}, {\varsigma }{.}{{\textsf {del} }}, {\varsigma }{.}{{\textsf {add} }})\in \mathcal {S}^{\mathsf {steps}} \) satisfying \({\varsigma }{.}{{\textsf {rule} }} =\rho \), \({\varsigma }{.}{{\textsf {match} }} =m_1\), \({\varsigma }{.}{{\textsf {comatch} }} =m_2\), \({\varsigma }{.}{{\textsf {del} }} ={\textsf {acInc} } (G) \circ b_1\), and \({\varsigma }{.}{{\textsf {add} }} ={\textsf {acInc} } (G) \circ b_1\).

The definition of steps above covers the general case as visualized in Fig. 11b. Note that the resulting diagram is no DPO diagram since e.g. \({L}{.}{{\textsf {ac} }} ={D}{.}{{\textsf {ac} }} =\top \) would require that \({G}{.}{{\textsf {ac} }} =\top \) as well. In our tool-based implementation, we can simplify the construction of \({H}{.}{{\textsf {ac} }} \) because we (a) do not change the name of variables that are not matched by \(c_1\), (b) use fresh names for preserved variables, and (c) use fresh names for created variables. In this case, we can assume that \(\gamma _{ eq }=\top \) and that \(k_1\) and \({\textsf {rev} } (k_2) \) do not need to be applied. For an example of a simple transformation step, consider Fig. 10b and Fig. 10c for the graph part and the AC part.

5.2 (Timed) graph transformation sequences

We now define graph transformation sequences that can be obtained by performing a finite or an infinite number of steps using rules. However, we only provide the underlying data structure of graph sequences in the definition below and do not yet connect the notions of steps and graph sequences at this point. Such a graph sequence is defined as a mapping of indices from the set B to spans of morphisms where adjacent spans must have a common graph as end point and start point, i.e., the graph \(G_1\) is such a common start and end point of the two spans and in Fig. 25a on page 32).

Definition 19

(Graph Sequences) If \(G_0\in \mathbf {Graphs} \) is a graph, \(n\in \mathbf {N} \cup \{\infty \}\) is a length, and \(B=\{k\in \mathbf {N} \mid k<n\}\) is the set of indices from 0 to \(n-1\) (note that B is empty for \(n=0\)), then is a graph sequence of length n over \(G_0\), written \(\pi \in \Pi _{G_0} \), and \({\textsf {length} }(\pi ) =n\), if both items apply.²⁶

• \(0\in B\) and imply that \(G=G_0\).

• .

Moreover, we define the following abbreviations and operations.

• \(\Pi ^{\mathsf {fin}}_{G_0} =\{\pi \in \Pi _{G_0} \mid {\textsf {length} }(\pi ) \ne \infty \}\) is the class of all finite graph sequences over \(G_0\).

• If \(\pi \in \Pi ^{\mathsf {fin}}_{G_0} \) is a finite graph sequence over \(G_0\) and \({\textsf {length} }(\pi ) =0\), then \(\pi \) is empty, written \(\pi =\lambda \) (for the empty word \(\lambda \)).

• If \(\pi \in \Pi ^{\mathsf {fin}}_{G_0} \) is a finite graph sequence over \(G_0\), \({\textsf {length} }(\pi ) =n\), H is a graph, \(k\le n\), (\(k=0\) implies \(G_0=H\)), and (\(k>0\) implies ), then \(\pi \) starts with \(G_0\) and ends with H after k steps, written \(\pi ^{\mathsf {G}}(k) =H\).

• If \(\pi \in \Pi ^{\mathsf {fin}}_{G_0} \) is a finite graph sequence over \(G_0\), \({\textsf {length} }(\pi ) =n\), and \(\pi ^{\mathsf {G}}(n) =H\), then \(\pi \) starts with \(G_0\) and ends with H, written \(\pi \in \Pi ^{\mathsf {fin}}_{G_0,H} \).

• If \(\pi \in \Pi ^{\mathsf {fin}}_{G_0,H} \) is a finite graph sequence starting with \(G_0\) and ending with H, \({\textsf {length} }(\pi ) =n\), and \(\pi '=\{(n-(k+1),(r,\ell ))\mid (k,(\ell ,r))\in \pi \}\in \Pi ^{\mathsf {fin}}_{H,G_0} \) is the finite graph sequence starting with H and ending with \(G_0\) obtained from \(\pi \), then \(\pi '\) is the reversal of \(\pi \), written \({\textsf {rev} }(\pi ) =\pi '\).

In the following, we introduce timed graph sequences (TGSs) where each step consumes a positive amount of time. To operate on a TGS, we obtain the total time that has passed up to some point in the TGS by retrieving the total time from graphs in the TGS. For this purpose, we assume that the total time is stored in the graphs of the TGS e.g. in variables that are restricted by the ACs of the graphs. The total time stored in such a variable must then be increased in each graph transformation step by including such an increase in each rule of the timed graph transformation system. Note that graphs cannot occur more than once in a TGS because time must strictly increase but, apart from the stored total time, graphs may very well coincide as usual.²⁷ In the definition below, we abstract from a particular encoding for the total time and assume a partial function \( time \) that returns a strictly increasing sequence of total timepoints from (the set of all real numbers greater or equal to 0), which diverges for infinite TGSs when being applied to the graphs in a TGS.

Consider Fig. 15a where the partial function \( time \) can be defined to extract the value of the \(\text {time} \) attribute of the node S. Hence, the total time would be increased by 1, 100, 1, and 100 in the depicted spans.

5.3 (Timed) graph transformation systems

We now connect the notion of steps introduced in Definition 18 with the notion of (timed) graph sequences from above by means of (timed) graph transformation systems that generate (timed) graph sequences.

Graph transformation systems, which contain a finite set of finite rules R and a finite initial graph G, are introduced in the following definition.

The graph sequences that can be derived from the initial graph of a graph transformation system are those graph sequences in which each span of morphisms can be justified by a step using one of the rules in R of the graph transformation system.

Similarly to graph transformation systems, timed graph transformation systems contain a finite set of finite rules R and a finite initial graph G. As an additional component, timed graph transformation systems contain a partial function \( time \) for extracting the current global time from the derived graphs.

The timed graph sequences of timed graph transformation systems are constructed as for graph transformation systems above. Recall that the partial function \( time \) is only used for postprocessing of already derived TGSs.

With these definitions in place, we now present an example of a timed graph transformation system that is used in Sect. 7 and Sect. 8 later on.

7.1 Propagation of matches over timed graph sequences

To introduce the propagation of matches over TGSs, we first introduce the operation admissible-comatches. This operation takes a graph transformation span ,³¹ a match , and a (so-called) evolution pattern \(\theta \) with left- and right-hand side graphs L and R as inputs and then checks whether the changes given by the graph transformation span \((\ell ,r)\) are permitted by the evolution pattern \(\theta \) and returns a set of corresponding matches . In particular, the operation \({\textsf {admissible-comatches}}\) restricts the given match \(m_1\) according to the evolution pattern \(\theta \) (similarly to the BGC operator restrict), checks whether at least the deletions specified in the evolution pattern \(\theta \) are performed, checks whether at least the additions specified in the evolution pattern \(\theta \) are performed, and determines an extended match \(m_2\) according to the evolution pattern \(\theta \) (similarly to the BGC operator exists). That is, an evolution pattern describes that certain elements of the given match are not relevant, describes that certain elements must have been deleted and added, and that certain elements must be matchable.

This idea is similar to the concept of covariance and contravariance in programming languages. For example, an abstract function (e.g. contained in a Java interface) can be implemented by a concrete function (e.g. in a class implementing the interface) when \(f'\) permits at least the elements of A (i.e., \(A\subseteq A'\)) and when \(f'\) returns at most the elements of B (i.e., \(B'\subseteq B\)). In comparison, we require, informally speaking, that the actual deletions of the graph transformation span \((\ell ,r)\) are contained in the deletions specified in the evolution pattern \(\theta \) and that the additions specified in the evolution pattern \(\theta \) are contained in the actual additions of the graph transformation span \((\ell ,r)\).

Moreover, double pullback (DPB) graph transformation steps [46–49] permit deletions and additions beyond the deletions and additions carried out for a rule when applying a DPO graph transformation step. We compare our formalization and DPB-based graph transformation after Definition 30.

We now introduce evolution patterns before presenting the operation admissible-comatches afterwards in more detail. Evolution patterns contain, compared to rules from Definition 16, two additional monomorphisms \({\theta }{.}{{\textsf {res} }} \) and \({\theta }{.}{{\textsf {ext} }} \) that are used at the begin and the end of the diagram constructed by the operation admissible-comatches to restrict the given match (as for the operator restrict from BGL) and to extend the resulting comatch (as for the operator exists from BGL). For a visualization of the components of an evolution pattern, see Fig. 20.

For concrete examples of evolution patterns, we employ the following notation as used in the top row of Fig. 21.

We now introduce the operation admissible-comatches, which obtains the resulting set of comatches by constructing a diagram for each of them. Each of these diagrams is an adaptation of the diagram required for graph transformation steps from Definition 18. For this purpose, we assume a given graph transformation span , a given evolution pattern \(\theta \), and a given match . See Fig. 21 for an example where only the presented diagram is constructed resulting in a single comatch \(m_2\).

In the first stage (focusing on the graph part; see Fig. 22 for a visualization), we construct a diagram with four squares that are related to the four components \({\theta }{.}{{\textsf {res} }} \), \({\theta }{.}{{\textsf {del} }} \), \({\theta }{.}{{\textsf {add} }} \), and \({\theta }{.}{{\textsf {ext} }} \) of the evolution pattern \(\theta \). The first square describes the match restriction based on \({\theta }{.}{{\textsf {res} }} \). The second and third squares describe the checks whether at least the deletions and additions specified by \({\theta }{.}{{\textsf {del} }} \) and \({\theta }{.}{{\textsf {add} }} \) have been performed in the given graph transformation span. The fourth square describes the extension to a match according to \({\theta }{.}{{\textsf {ext} }} \). The permission to delete and add elements beyond what is specified in \({\theta }{.}{{\textsf {del} }} \) and \({\theta }{.}{{\textsf {add} }} \) is implemented in the second and third square by checking whether the minimal changes (computed using pushout complement and pushout) can be embedded into the given graph transformation span (cf. the triangles \(a_1\circ d_2=b_1\) and \(e_2\circ a_2=b_2\) in Fig. 22).

In the second stage (focusing on attributes; see Fig. 23 for a visualization), we check whether the attribute values have changed from G to H in a way compatible with the AC \({\theta }{.}{{\textsf {ac} }} \) of the given evolution pattern \(\theta \). To this end, we construct for the diagram that was constructed in the first stage a common variable namespace for G and H as for the notion of steps and then check whether \({\theta }{.}{{\textsf {ac} }} \) is implied by the ACs of G and H.

We now formalize these explanations to construct admissible comatches \(m_2\) in the following definition. See Fig. 22 and Fig. 23 for accompanying visualizations.

Definition 30

(Admissible Comatches) If

1. (1)

   • \(\theta \in \mathcal {S}^{\mathsf {EP}} \) is an evolution pattern,

   • ,

     \(m_1\models _{\mathsf {BGC}} {\theta }{.}{{\textsf {lC} }} \),

   • ,

     \({\textsf {acInc} } (G) \circ c_1=m_1\circ {\theta }{.}{{\textsf {res} }} \),(items (1)+(2))

   • ,

     ,

     \((c_1,a_1)\) is a pushout of \(({\theta }{.}{{\textsf {del} }},d_1)\),(item (3))

   • ,

     \(a_1\circ d_2=b_1\),(item (4))

   • ,

     \(d_2\circ d=d_1\),(item (5))

   • ,

     ,

     \((e_1,a_2)\) is a pushout of \(({\theta }{.}{{\textsf {add} }},d)\),(item (6))

   • ,

     \(e_2\circ a_2=b_2\),(item (7))

   • ,

     \(e_2\circ e_1=c_2\),(item (8))

   • ,

     \({\textsf {acInc} } (H) \circ c_2=m_2\circ {\theta }{.}{{\textsf {ext} }} \),(items (9)+(10))

   • \(m_2\models _{\mathsf {BGC}} {\theta }{.}{{\textsf {rC} }} \),

    
2. (2)

   • ,

     ,

     ,

   • is obtained by using the universal property of the coproduct \({\amalg } ({\theta }{.}{{\textsf {lX} }},{\theta }{.}{{\textsf {rX} }}) \),

   • \(\gamma = k_1({G}{.}{{\textsf {ac} }})\wedge k_2({H}{.}{{\textsf {ac} }}) \rightarrow \sigma _{ VX }({\theta }{.}{{\textsf {ac} }}) \) is an AC, and

   • \({\textsf {sat} }_{\forall } (\gamma ) \),

    

then is an admissible comatch for the graph transformation span \(({\textsf {acInc} } (G) \circ b_1,{\textsf {acInc} } (H) \circ b_2)\), the match morphism \(m_1\), and the evolution pattern \(\theta \), written \(m_2\,\,{\in }\,\,{\textsf {admissible-comatches}}\,\, {(({\textsf {acInc} } (G) \,\,{\circ }\,\,b_1,\, {\textsf {acInc} } (H)}\,{\circ } b_2), {m_1},{\theta })\).

Note that, using the DPB approach mentioned above, we could alternatively construct such that \(({\theta }{.}{{\textsf {del} }},d)\) is a pullback of \((c_1,b_1)\) and by constructing such that \(({\theta }{.}{{\textsf {add} }},d)\) is a pullback of \((c_2,b_2)\). A similar correspondence between DPO and DPB graph transformation has been presented e.g. in [48] where additional deletions are applied before the pushout complement is constructed. However, we believe that the definition above (albeit being more verbose) explains the construction of d and \(c_2\) more clearly by relying on the standard constructions for pushout complements and pushouts (the alternative DPB-based formalization requires the construction of pullback complements and pullbacks for the special case when three of the four morphisms are given already) and by presenting the additional deletions and additions using the two triangles explicitly.

We use this definition of admissible cospans below to propagate a match over the spans of a finite graph sequence for a given evolution pattern and a match of the left-hand side graph of the evolution pattern into the first graph of the given sequence. For this purpose, we now define the derived span of a graph sequence using the iterated pullback construction (cf. [31, Definition 4.1, p. 44]). This construction allows to contract a given finite graph sequence into a graph sequence of length one by forgetting about all interior steps of the sequence but preserving the relationship between elements of the first and the last graph of that sequence.³³ See Fig. 24 and Fig. 25a for a general visualization and an exemplary computation of a derived span.

Definition 31

(Derived Spans) If \(\pi \in \Pi ^{\mathsf {fin}}_{G_0,H} \) is a finite graph sequence that starts in \(G_0\) and that ends in H, then , if one of the following items applies.

• \({\textsf {length} }(\pi ) =0\) and \((\ell ,r)=({\textsf {id} } (G_0),{\textsf {id} } (G_0))\).

• \({\textsf {length} }(\pi ) =1\) and \((\ell ,r)=\pi (0)\).

• \({\textsf {length} }(\pi ) =2\), \(\pi (0)=(\ell _0,r_0)\), \(\pi (1)=(\ell _1,r_1)\), \((r_0',\ell _1')~\text {is a pullback of}~(r_0,\ell _1) \), and \((\ell ,r)=(\ell _0\circ r_0',r_1\circ \ell _1')\).

• \({\textsf {length} }(\pi ) >2\) and \((\ell ,r)= {\textsf {derivedSpan} }(\{(0,{\textsf {derivedSpan} }(\{(0,\pi (0)),(1,\pi (1))\})), (1,{\textsf {derivedSpan} }(\{(n,x)\mid (n+2,x)\in \pi \}))\})\).

We now define the propagation of a match over a finite graph sequence for a given evolution pattern by obtaining the admissible comatches for the derived span computed for the given graph sequence. See Fig. 25b for an example of a match propagation over the derived span from Fig. 25a.

Note that the definition of a propagated match can be used also in the reverse direction by reversing the rule and the graph sequence beforehand.

We now extend the propagation of matches to the case where a match is to be propagated over a subsequence of a TGS identified by two total timepoints. That is, given a TGS \(\pi \) that contains the TGS \(\pi '\) between two provided timepoints \(t_1\) and \(t_2\) where \(\pi '\) starts with graph G and ends with graph H, we want to propagate a match of L into G over the timed spans of \(\pi '\) into a match of a graph R into H. Reusing the match propagation defined above based on evolution patterns, this propagation may result in an empty set of matches when matched elements are deleted by the timed spans between \(t_1\) and \(t_2\). This time-based propagation operation is crucial for MTGL where we want to check e.g. whether a matched element also existed earlier (for the case when \(t_2<t_1\)) or exists later (for the case of \(t_2>t_1\)) in the given TGS \(\pi \). For the semantics of MTGL later on, we not only check for the existence of a suitable propagated match but also obtain the resulting matches of R into the graph in \(\pi \) at timepoint \(t_2\) to evaluate further conditions based on these resulting matches.

Consider again Fig. 25a where the partial function \( time \) extracts the current time from the \(\text {id} \) attribute of node a. Then, Fig. 25b provides an example of a time-based propagation of the match \(m_1\) to the match \(m_2\) from the timepoint \(t_1=0\) (for the graph \(G_0\)) to the timepoint \(t_2=4\) (for the graph \(G_2\)).

7.2 Syntax and semantics of MTGL

We introduce the metric temporal graph logic (MTGL) with its syntax and semantics after a brief introduction of design choices.

Propositional temporal logics such as the linear temporal logic (LTL) can be defined on the foundation of labeled transition systems (S, R, L) containing a set of states S, a binary step relation \(R\subseteq S\times S\), and a labeling function assigning a set of atomic propositions to each state. The conditions of such temporal logics then express properties that are to be satisfied by a given path of that labeled transition system. In particular, LTL allows to express (a) state properties based on elements of \( AP \) and propositional operators such as negation and conjunction as well as temporal operators to express (b) sequence properties based on the next operator stating that an LTL condition is satisfied in the next state and the until operator stating that an LTL property \(\phi _2\) is satisfied at some later state in the given path and that all states visited in between satisfy another LTL property \(\phi _1\). Further operators such as eventually and globally can be derived from the given operators.

Other temporal logics feature (a) operators that refer to earlier states using the operators previous and since (corresponding to the next and until operators), (b) metric temporal operators such as the metric-until operator that are then equipped with an interval describing the relative time at which the condition \(\phi _2\) has to be satisfied in the future,³⁴ and (c) combinations of (a) and (b) such as in the metric temporal logic (MTL) [60].

The use of atomic propositions in propositional temporal logics limits their expressiveness on the one hand but allows in some cases for the development of model checking approaches on the other hand [8]. In contrast, nonpropositional temporal logics do not make use of atomic propositions and may be defined on the more general Kripke frames where the labeling function of labeled transition systems is omitted. The goal of these logics is to express properties that cannot be expressed in propositional (metric) (temporal) logics. Such additional properties then refer to the content of states, which are given in our context by graphs in a TGS. For example, a particular element of such a graph may be tracked across multiple states. Other examples of nonpropositional (metric) temporal logics have been discussed e.g. in [9] (\(\mu \mathcal {G}2\): a combination of the \(\mu \)-calculus and second-order graph logic for labeled graphs) and [13] (metric temporal first-order logic (MFOTL): a combination of first-order logic using relations to store information and MTL).

We now introduce MTGL as a nonpropositional metric temporal logic where graphs are handled as first-class citizens meaning that conditions of MTGL directly contain graphs and graph morphisms as in BGL and GL instead of using encodings as in \(\mu \mathcal {G}2\) and MFOTL.

MTGL supports the two metric temporal operators \({\textsf {U} } \) (called until) and \({\textsf {S} } \) (called since) mentioned above. These two operators are, however, derived operators in our logic because we cover both of them using the operator (called delta-lock). That is, delta-lock can be parameterized to behave like until or since. The nonpropositional character of MTGL is given by the use of matches of graphs from conditions of MTGL into the graphs of the TGS at hand. These matches are then propagated (as introduced in the previous subsection) over spans of the TGS allowing to express (using evolution patterns) conditions on how matched parts change over time. In particular, matches into graphs of the TGS are propagated forwards/backwards in the TGS for the until /since operator.

Moreover, MTGL supports the operator \(\boxdot \) (called delta-release), which is used in combination with delta-lock. For example, the special case of the until operator requires a propagation of a match m into a graph G of the TGS forwards resulting in a match \(m'\) but this forwards propagation alone only transfers information forwards. With delta-release, we allow to express statements that result in an additional backward propagation of \(m'\) into a match \(m''\) into the original graph G. The additional propagation of match \(m'\) allows to express statements at graph G based on graph elements and attributes matched by \(m'\).

Compared to [38, 81], we now additionally support conditions referring to the past but also handle the central capabilities of MTGL (binding of graph elements and comparison of attribute values) at a more fundamental level using evolution patterns and the delta-release operator, which leads to an increased expressiveness.

In MTGL, we specify sets of timepoints using ACs in the form of duration specifications, which have a single free variable \(\tau \in \mathcal {X} \) of sort \(\mathsf {real} \). The semantics of a duration specification \(\gamma \) is given by the set of all reals that satisfy \(\gamma \). For example, the interval \(I=[2,4)\) can be represented using \(\gamma =(2\le \tau )\wedge (\tau < 4) \) for which \({\textsf {sem} }(\gamma ) =I\). Moreover, for shifting of a duration specification, we formalize the statement \(\bar{x}\in {\textsf {sem} }(\gamma ) +\bar{y}\) where \(\bar{x}\) and \(\bar{y}\) are reals from \(\mathbf {R} \) using ACs. For this purpose, we represent \(\bar{x}\) and \(\bar{y}\) by variables x and y of sort \(\mathsf {real} \) and define an AC on these two variables. The resulting AC \(\gamma '\) then restricts x and y analogously to the statement \(\bar{x}\in {\textsf {sem} }(\gamma ) +\bar{y}\) above. For example, \(\bar{x}\in [2,4)+\bar{y}\) is represented using the AC \(\gamma =\exists \tau .\;x=\tau + y \wedge (2\le \tau )\wedge (\tau < 4) \).

Note that many other metric temporal logics already impose the restriction that sets of timepoints must be specified by means of certain kinds of intervals. These logics thereby describe already on the syntax-level restrictions under which model checking of their conditions is decidable (see [19] for a survey on the expressiveness and algorithmic results for several metric temporal logics).

In the following, we introduce the metric temporal graph conditions (MTGCs) on a more detailed level. Firstly, MTGL supports the two propositional operators \(conjunction \) and \(negation \) as for GL and BGL and, secondly, the two metric temporal operators (called \(delta{\text {-}}{}lock \)) and \(\boxdot \) (called \(delta{\text {-}}{}release \)). The \(delta{\text {-}}{}lock \) operator is an extension of the \(delta \) operator of GL. In addition to its right-hand side argument \((\theta _2,\psi _2)\) it has a left-hand side argument \((\theta _1,\psi _1)\) and a duration specification \(\gamma \) describing a delay \(\delta \in {\textsf {sem} }(\gamma ) \) as usual. For the special cases of the until and since operators, \((\theta _2,\psi _2)\) is checked at timepoint \(t+\delta \) and \((\theta _1,\psi _1)\) is checked for the timepoints between t and \(t+\delta \) (where \(\delta \ge 0\) corresponds to the case of until and \(\delta \le 0\) corresponds to the case of since). Moreover, the search restriction specifier \(\kappa \) is employed to further restrict the timepoints and matches used for satisfying \((\theta _2,\psi _2)\). In particular (see Fig. 26 for an example illustrating the differences between the search restriction specifiers), (a) \(\kappa =\mathsf {E} \) (called exists-match) imposes no further restriction and permits that any match compatible with the duration specification is used (for the duration specification \(\tau =0\) local state properties are stated and the duration specification \(\top \) allows to match elements at any timepoint in the TGS), (b) \(\kappa =\mathsf {N} \) (called new-match) imposes the restriction that \((\theta _2,\psi _2)\) could not be satisfied at some earlier (later) timepoint compared to \(t+\delta \) for \(\delta \ge 0\) (\(\delta <0\)) using the same binding (this search restriction specifier is used in our running example to determine the earliest time at which a result is added to be able to compare this earliest time with the imposed deadline), and (c) \(\kappa =\mathsf {C} \) (called closest-match) imposes the restriction that \((\theta _2,\psi _2)\) could not be satisfied at some timepoint \(t+\delta '\) that is closer to t than \(t+\delta \) by any binding (this search restriction specifier is motivated by the use of the state prophecy and state history operators from [77] that are able to focus on the next/previous match).

A limitation of the \(delta{\text {-}}{}lock \) operator is that the satisfaction checks required for this operator (i.e., the check of \((\theta _1,\psi _1)\) for all timepoints between t and \(t+\delta \) and the check of \((\theta _2,\psi _2)\) at timepoint \(t+\delta \)) are executed in isolation from each other. This means that desired commonalities between these satisfaction checks in terms of matched graph elements and values of matched attributes require additional techniques.

Firstly, as demonstrated by the following example, the current context graph H at timepoint t determines a common part to be used in all these satisfaction checks.

Secondly, we demonstrate in the following example a problem for sharing certain bindings among satisfaction checks at different timepoints. This problem is resolved subsequently using the additional MTGL operator delta-release. In the example, graph elements and values of attributes that are additionally matched at timepoint \(t+\delta \) by \((\theta _2,\psi _2)\) are not available when checking \((\theta _1,\psi _1)\) at the timepoints between t and \(t+\delta \).

To specify properties as in the latter example, we employ the \(delta{\text {-}}{}release \) operator \(\boxdot (\theta ,\psi ) \), which has no counterpart in logics such as MTL without binding capabilities. The operator \(delta{\text {-}}{}release \) is used to specify, similarly to the left-hand side argument \((\theta _1,\psi _1)\) of the \(delta{\text {-}}{}lock \) operator, a property \((\theta ,\psi )\) that has to be satisfied in the obtained interval between t and \(t+\delta \). While the left-hand side argument \((\theta _1,\psi _1)\) of the \(delta{\text {-}}{}lock \) operator is checked for the TGS in the interval from the current time point t to the timepoint \(t+\delta \), the argument of the \(delta{\text {-}}{}release \) operator is checked in the reverse direction starting with a context graph established at the timepoint \(t+\delta \).

We now introduce the syntax of MTGL by formally defining its MTGCs.

Note that in the definition above, we only permit occurrences of the \(delta{\text {-}}{}release \) operator in the right-hand side argument of the \(delta{\text {-}}{}lock \) operator. Moreover, we use a depth parameter \(n\in \mathbf {N} \) for the number of open \(delta{\text {-}}{}lock \) calls to ensure that the number of \(delta{\text {-}}{}release \) calls does not exceed the number of \(delta{\text {-}}{}lock \) calls (i.e., to ensure that each instance of the \(delta{\text {-}}{}release \) operator has an enclosing instance of the \(delta{\text {-}}{}lock \) operator). The use of this depth parameter guarantees in the semantics of MTGL (as explained in more detail below) that whenever an instance of the \(delta{\text {-}}{}release \) operator is checked, a timepoint specifying the origin of a previous instance of the \(delta{\text {-}}{}lock \) operator is available.

The formalization of the properties from Example 3 and Example 4 is given in Fig. 27b and Fig. 27d, respectively, where we use the notation introduced subsequently.

The satisfaction relation of MTGL is defined as the satisfaction relation of GL for the operators conjunction and negation and also covers the two additional operators delta-lock and delta-release.

Definition 36

(Satisfaction of MTGCs) If \(\pi \in \Pi ^{ time }_{G} \) is a TGS, is a word of n timepoints, is a timepoint, is a partially injective monomorphism, and \(\bar{\psi }\in {\mathcal {S}}_{n ,H}^{\mathsf {MTGC}}\) is an MTGC over H of depth n, then \((\pi , ts ,t,m)\models _{\text {MTGC}} \bar{\psi } \), if one of the following items applies.

\(\bullet \): 

\(\bar{\psi }=\wedge S \) and \(\forall \psi \in S.\;(\pi , ts ,t,m)\models _{\text {MTGC}} \psi \).

\(\bullet \): 

\(\bar{\psi }=\lnot \psi \) and \((\pi , ts ,t,m)\not \models _{\text {MTGC}} \psi \).

\(\bullet \): 

and there are \(\delta \in {\textsf {sem} }(\gamma ) \) and³⁵\(\tilde{m}\in {\textsf {PM} } (\pi ,t,t+\delta ,m,\theta _2) \) s.t.

\(\bullet \): 

\((\pi , ts \cdot t,t+\delta ,\tilde{m})\models _{\text {MTGC}} \psi _2 \),³⁶

\(\bullet \): 

if \(\kappa =\mathsf {N} \),

I is an interval³⁷ over ,

\(I=[0,t+\delta )\) if \(\delta \ge 0\),

and \(I=(t+\delta ,\infty )\) if \(\delta <0\),

then each

satisfies \({\textsf {PM} } (\pi ,t+\delta ,t',\tilde{m},{\textsf {id} }) =\varnothing \),³⁸

\(\bullet \): 

if \(\kappa =\mathsf {C} \),

then each \(\delta '\in ((\delta ,0]\cup [0,\delta ))\cap {\textsf {sem} }(\gamma ) \)

satisfies \({\textsf {PM} } (\pi ,t,t+\delta ',m,\theta _2) =\varnothing \),³⁹ and

\(\bullet \): 

for each \(\delta '\in (\delta ,0]\cup [0,\delta )\)

there is \(\tilde{m}\in {\textsf {PM} } (\pi ,t,t+\delta ',m,\theta _1) \)

s.t. \((\pi , ts ,t+\delta ',\tilde{m})\models _{\text {MTGC}} \psi _1 \).⁴⁰

\(\bullet \): 

\(\bar{\psi }=\boxdot (\theta ,\psi ) \), \( ts = ts' \cdot t'\), and

for each \(t''\in [t',t)\cup (t,t']\)

there is \(\tilde{m}\in {\textsf {PM} } (\pi ,t,t'',m,\theta ) \)

s.t. \((\pi , ts ',t'',\tilde{m})\models _{\text {MTGC}} \psi \).⁴¹

Also, if \(\bar{\psi }\in {\mathcal {S}}_{\varvec{\varnothing }}^{\mathsf {MTGC}}\) and \((\pi ,\lambda ,0,{\textsf {i} } (G))\models _{\text {MTGC}} \bar{\psi } \), then \(\pi \models _{\text {MTGC}} \bar{\psi } \).

For our running example, see Fig. 15 for a TGS \(\pi \), which does not satisfy the MTGC \(\psi _1\) from Fig. 28a. The TGS \(\pi \) does not satisfy \(\psi _1\) because, for the node \(T_2\) of type :Task created at the timepoint 102 with \(\text {id}\) attribute 1, there is not eventually a unique node R of type \({\text {:Result}}\) with \(\text {id}\) attribute 1 and \(\text {value} \) attribute \( ok \). Indeed, the node \(R_2\) is the only node of type \({\text {:Result}}\) that is created in the described timepoint interval with the \(\text {id}\) attribute 1 of the node \(T_2\) and \(\text {value} \) attribute \( ok \) but there is the additional node \(R_1\) of type \({\text {:Result}}\) with the \(\text {id}\) attribute 1, which invalidates uniqueness. Basically, the absence of such nodes of type \({\text {:Result}}\) generated from previous tasks is not ensured using an application condition in the rule \(\rho _{ SpawnTask }\) in Fig. 13a. The error occurs when an old result is not yet removed using the rule \(\rho _{ ConsumeResult }\) and is more likely in real systems when the set of admissible \(\text {id}\) attributes is small⁴² or when they are chosen in a deterministic order.

Metric temporal logics vary not only in their selection of operators (such as until and since) and the underlying data structures for states (such as graphs, relations, and sets of atomic proposition) but also in their interpretation of how continuous time is related to discrete steps. In [75] two basic alternative kinds of semantics are discussed. On the one hand, point-based semantics such as in MFOTL [13] (also see [4, 5, 51, 53, 54, 84]) quantify for the metric temporal operators over the countable set of timepoints in a dense-time interval that are associated to the events that alter the state, which means that, effectively, only discrete steps are considered that are associated with a continuous variable representing the current global time. On the other hand, interval-based semantics such as in MTGL (also see [3, 6, 52, 77]) quantify for the metric temporal operators over all timepoints in the entire dense-time interval. As argued in [75], a common reason for using the point-based semantics is that MTL satisfiability is decidable for the point-based semantics but not for the interval-based semantics. However, while deciding MTGL satisfiability is generally also of interest to exclude unsatisfiable MTGC -based specifications, it is not our focus as of now.

By means of the example in Fig. 29, we now discuss the general difference between point-based and interval-based semantics. The TGS \(\pi \) from Fig. 29a satisfies the MTGC \(\psi \) from Fig. 29b when \(\delta \le 6\) because the node of type :A can be matched at global time 4, which permits to wait for the required node of type \({\text {:B}}\) for 4 further time units until global time 8. In comparison, when the corresponding TGS and the corresponding condition in MFOTL are considered, it turns out that \(\delta \le 4\) is required for satisfaction because the point-based semantics of MFOTL can only jump to the global time 2 for matching the node of type :A. Hence, as also mentioned in [75], point-based semantics takes the perspective of specifying events whereas interval-based semantics takes the perspective of specifying states.

7.3 Folding of timed graph sequences

We now introduce the operation \({\textsf {Fold} }^{\textsf {tgs} } \) for translating TGSs that contain only grounded graphs (where each variable has a unique value) into a single graph, which is called graph with history (GH). This GH contains for each node and edge occurring in the TGS the total timepoint when it was created and, if it was deleted, the total timepoint when it was deleted. To capture these total timepoints, we use additional \(\text {cts} \) (creation timestamp) and \(\text {dts} \) (deletion timestamp) attributes of sort \(\mathsf {real} \).⁴³ See Fig. 12a where we have added such attributes in the type graph already for our running example. Furthermore, for our running example, we obtain the GH in Fig. 15b from the TGS given in Fig. 15a. Note that, in comparison to the notion of a derived span (see Definition 31), which drops all interior information contained in a graph sequence or a TGS, we now want to collect all this interior information into the resulting GH.

To fold a finite TGS, we first obtain a GH from the first graph of a TGS.

Definition 38

(Operation \({\textsf {Fold} }^{\textsf {1st} }\)) If \(G\in \mathbf {Graphs} \) is a graph and is an inclusion morphism obtained by

• adding the attribute \(\text {cts} =0\) to all nodes in G,

• adding the attribute \(\text {dts} =-1\) to all nodes in G,

• adding the attribute \(\text {cts} =0\) to all edges in G, and

• adding the attribute \(\text {dts} =-1\) to all edges in G,

then is the graph-folding of the graph G into the GH \(G'\), written \({\textsf {Fold} }^{\textsf {1st} } (G) =m\).

Note that the inclusion morphism identifies the elements of the graph G in its GH \(G'\).

We now define the operation that folds a single span for a given monomorphism into a monomorphism where \(G'\) and \(H'\) are GHs of G and H, respectively. The resulting monomorphism \(m'\) is obtained as follows. For nodes and edges freshly added by r, we add \(\text {cts}\) attributes set to the current global time (extracted from H) and add \(\text {dts}\) attributes initially set to \(-1\) (denoting that these elements have not yet been deleted). Moreover, for nodes and edges freshly deleted by \(\ell \), we add \(\text {dts}\) attributes set to the current global time (extracted from H) and remove the \(\text {dts} =-1\) attributes previously included. Note that the following definition does not depend on the syntactic representation of the ACs of graphs (which we want to handle up to equivalence). Instead, we wrap ACs of graphs in additional quantification and conjunction and silently assume that such ACs of graphs are simplified as in our exemplary application in Fig. 15. See Fig. 30 for an accompanying visualization.

Definition 39

(Operation \({\textsf {Fold} }^{\textsf {span} }\)) If

• is a monomorphism,

• is a span,

• \(N_2={m}{.}{{\textsf {N} }} ({G}{.}{{\textsf {N} }}-{\ell }{.}{{\textsf {N} }} ({D}{.}{{\textsf {N} }}))\) contains the nodes that are removed by \(\ell \),

• \(E_2={m}{.}{{\textsf {E} }} ({G}{.}{{\textsf {E} }}-{\ell }{.}{{\textsf {E} }} ({D}{.}{{\textsf {E} }}))\) contains the edges that are removed by \(\ell \),

• \(D'\) is obtained from \(G'\) resulting in some monomorphism and an inclusion satisfying \(m\circ \ell =b_1\circ d\) by

  1. (1)

     setting the set of variables V to be empty,

      
  2. (2)

     removing the \(\text {dts} =-1\) attributes from nodes and edges in \(N_2\) and \(E_2\) while adding the local variables that are connected to these attributes to V, and

      
  3. (3)

     setting \({D'}{.}{{\textsf {ac} }} \) to \(\exists V.\;{G'}{.}{{\textsf {ac} }} \) to adapt the AC according to the removal of the variables in V,

      

• that adds the elements freshly added by r to \(D'\) resulting in the graph X,

• \( time (H) =t\) is the current global time of H,

• \(N_1={\bar{m}}{.}{{\textsf {N} }} ({H}{.}{{\textsf {N} }}-{r}{.}{{\textsf {N} }} ({D}{.}{{\textsf {N} }}))\) contains the nodes that are added by r,

• \(E_1={\bar{m}}{.}{{\textsf {E} }} ({H}{.}{{\textsf {E} }}-{r}{.}{{\textsf {E} }} ({D}{.}{{\textsf {E} }}))\) contains the edges that are added by r,

• \(H'\) is obtained from X resulting in some monomorphisms and satisfying \(m'=b_3\circ \bar{m}\) by

  1. (1)

     setting the set of ACs S to be empty,

      
  2. (2)

     adding the attributes \(\text {cts} =t\) and \(\text {dts} =-1\) with fresh local variables to all nodes and edges in \(N_1\) and \(E_1\) while inserting the used ACs into S,

      
  3. (3)

     adding the attribute \(\text {dts} =t\) with a fresh local variable to all nodes and edges in \(b_2(N_2)\) and \(b_2(E_2)\) while inserting the used ACs into S, and

      
  4. (4)

     setting \({H'}{.}{{\textsf {ac} }} \) to some AC that is equivalent to \({X}{.}{{\textsf {ac} }} \wedge (\wedge S) \),

      

then is the span-folding of the span \((\ell ,r)\) w.r.t. the monomorphism into the GH \(H'\), written \({\textsf {Fold} }^{\textsf {span} } (m,(\ell ,r)) =m'\).

Finally, we define the iterated folding of an entire finite TGS using the operations \({\textsf {Fold} }^{\textsf {1st} }\) and \({\textsf {Fold} }^{\textsf {span} }\).

Definition 40

(Operation \({\textsf {Fold} }^{\textsf {tgs} }\)) If \(\pi \in \Pi ^{\mathsf {fin}, time }_{G,H} \) is a finite TGS starting in G and ending in H, and , are monomorphisms, then \(m'\) is the tgs-folding of \(\pi \) w.r.t. the monomorphism m, written \({\textsf {Fold} }^{\textsf {tgs} } (m,\pi ) =m'\), if one of the following items applies.

• \({\textsf {length} }(\pi ) =0\) and \(m'=m\).

• \({\textsf {length} }(\pi ) >0\) and \(m'={\textsf {Fold} }^{\textsf {tgs} } ({\textsf {Fold} }^{\textsf {span} } (m,\pi (0)), \{(k,x)\mid (k+1,x)\in \pi \})\).

Also, if \({\textsf {Fold} }^{\textsf {tgs} } ({\textsf {Fold} }^{\textsf {1st} } (G),\pi ) =m'\), then \(m'\) is the tgs-folding of \(\pi \), written \({\textsf {Fold} }^{\textsf {tgs} } (\pi ) =m'\).

Since the operation \({\textsf {Fold} }^{\textsf {span} }\) above also constructs a span from the GH \(G'\) to the GH \(H'\), we can observe that the incremental folding executed by \({\textsf {Fold} }^{\textsf {tgs} } \) straightforwardly results in the construction of a TGS \(\pi '\) of GHs where the ith GH in \(\pi '\) corresponds to the folding of the prefix of \(\pi \) of length i.

See Fig. 15b for an example of a GH that is obtained from the TGS given in Fig. 15a using \({\textsf {Fold} }^{\textsf {tgs} }\).

It is important to point out that timepoints of attribute modifications are not directly recorded in the GH by the folding operations introduced here. As a consequence, attributes that are referred to by MTGCs and that may be changed in a given TGS often need to be contained in separate nodes to be able to track their values over time when using our encoding-based approach presented in the next subsection. The reason for this is that deleted node and edge attributes remain in the GH and that only the last value of an attribute is stored in the GH. This is particularly helpful for the current global time that may be recorded in an attribute that is matched and preserved in each step (cf. our running example where the \(\text {time} \) attribute of the system node is changed when applying a rule from Fig. 13 or Fig. 14). In our running example, we change the attribute \(\text {limit} \) of systems when spawning new tasks but we do not refer to this attribute in the MTGCs in Fig. 26. However, we change the attribute \(\text {dur} \) of tasks and refer to this attribute in the MTGC \(\psi _3\) in Fig. 26d. Hence, in our tool-based evaluation, we use the adapted type graph from Fig. 31 where the attribute \(\text {dur} \) of a task is stored in an additional node for which \(\text {cts} \) and \(\text {dts} \) attributes are then added by the folding operations presented above. The adaption of a given type graph to store node and edge attribute is always possible but we omit its formal handling here since also the rules of the (timed) graph transformation system as well as the MTGCs would need to be adapted to such a changed type graph as well on a technical level.

7.4 Encoding of MTGL in GL

The problem of satisfaction checking for metric temporal logics is far more difficult than for temporal logics because the intervals during which elements are alive (i.e., during which atomic proposition are satisfied) must be checked w.r.t. the intervals provided in the condition. Moreover, this problem is especially difficult when operators such as until or since are nested. This observation is also true for the case for MTGL where a procedure for checking the satisfaction of a given MTGC by a TGS is difficult for nested delta-lock operators. To obtain an effective and suitably efficient procedure for MTGL satisfaction checking, we now continue by presenting an encoding in the form of the operation , which translates MTGCs into GCs.⁴⁴ In the context of our general approach (cf. Fig. 1), we define such that it is compatible with the operation \({\textsf {Fold} }^{\textsf {tgs} }\) from Definition 40. To this end, we provide support for MTGL satisfaction checking via the two operations \({\textsf {Fold} }^{\textsf {tgs} }\) and that simplify the satisfaction checking problem to the setting of GL for which we can then employ tool support or apply the further encodings \({\textsf {enc} }_{\Delta }\) and \({\textsf {enc} }_{\nu }\) if desired. That is, instead of checking satisfaction for a given MTGC \(\psi \) and a given TGS \(\pi \), we check whether the GH obtained from \(\pi \) using \({\textsf {Fold} }^{\textsf {tgs} }\) satisfies the GC \(\phi \) obtained by applying to \(\psi \). For our running example, we have applied the operation \({\textsf {Fold} }^{\textsf {tgs} }\) to the TGS given in Fig. 15a to obtain the GH from Fig. 15b.

The operation relies on the fact that the GH obtained from folding a TGS contains for each node/edge occurring in the TGS so far the timepoints of creation and (if it was deleted) deletion using additional \(\text {cts}\) and \(\text {dts}\) attributes. We subsequently refer to the variables that are connected to the \(\text {cts}\) and \(\text {dts}\) attributes of a node/edge \(\alpha \) using \(x_{c,\alpha }\) and \(x_{d,\alpha }\), respectively. For our running example, the type graph \( TG \) containing such \(\text {cts}\) and \(\text {dts}\) attributes is given in Fig. 12a.

The GC that is obtained using the operation from an MTGC encodes the checks for MTGL operators according to the semantics of MTGL from Definition 36 using additional global variables for quantifying over observation timepoints. Moreover, additional ACs that refer to the \(\text {cts}\) and \(\text {dts}\) attributes are used to ensure that all additionally matched elements have been created and not yet deleted w.r.t. a timepoint or, alternatively, that elements that are no longer matched have been deleted before a timepoint when this is required.

We now introduce four minor operations used in the operation later on.

The operation \({\textsf {alive} }\) returns for a graph H an AC. The graph H is part of the GC obtained below using for a given MTGC and the AC obtained using \({\textsf {alive} }\) is then part of the AC of H. The purpose of the generated AC is that when the operation \({\textsf {Fold} }^{\textsf {tgs} }\) generates a GH for a given TGS \(\pi \), then H can only be matched to graph elements of that GH for a given global time represented by a variable x when each matched graph element exists in the graph of \(\pi \) at the global time stored in x. That is, the AC ensures that all of the matched nodes/edges have been created before the timepoint given by x and that none of them has been deleted before the timepoint given by x.

The operation \({\textsf {earliest} }\) is used in a similar way for a graph H and returns also an AC to be used in H. The difference is that the AC generated by \({\textsf {earliest} }\) ensures that none of the matched graph elements existed before the global time given by the variable x. That is, one of the matched graph elements called \(\alpha \) must have been created at the timepoint given by x and none of the other graph elements \(\beta \) must have been created after that timepoint. This AC thereby ensures that the graph H could not have been matched to the same elements at an earlier timepoint because the graph element \(\alpha \) could not have been matched earlier. The AC generated by \({\textsf {earliest} }\) in this way is used in when encoding an MTGC using the search restriction specifier new-match.

For our running example, see Fig. 32 for the GC that results from applying the operation , which is introduced in the following, to the MTGC from Fig. 28a where we make use of ACs including the operations \({\textsf {alive} }\) and \({\textsf {earliest} }\). Note that, to simplify notation, we also apply \({\textsf {alive} }\) and \({\textsf {earliest} }\) by just providing a set of graph elements instead of an entire graph.

The operation \({\textsf {ruleAdd} }\) creates a restriction-extension pattern by adding a set of global variables V, by adding a further global variable x, and by requiring the satisfaction of an AC \(\gamma \). Also, the restriction-extension pattern additionally subsumes a given context graph H and its AC states that the variables in V remain unchanged. Restriction-extension patterns constructed using \({\textsf {ruleAdd} }\) are used to quantify over the additional global variable x that represents an observation timepoint in the satisfaction relation of MTGL (see Definition 36).

For our running example, the application of the operation \({\textsf {ruleAdd} }\) results in the restriction-extension patterns used in lines 2 and 4 of the GC from Fig. 32. The restriction-extension pattern used in line 2 in this resulting GC states that (due to the negation in the beginning of the line) the subcondition should be satisfied for every value of the additional global variable \(x_1\) that satisfies the AC \(x_0\le x_1 \). Herein, the global variable \(x_0\) represents the current observation timepoint given by the variable t in Definition 36. Moreover, the AC \(x_0\le x_1 \) represents the statement that the new observation timepoint (called \(t'\) in Definition 36) must be one of the values described by the duration specification used in the MTGC, which is \([0,\infty )\) in this case. The restriction-extension pattern in line 4 of Fig. 32 states that there is a timepoint represented by \(x_2\) at most 10000 time units in the future measured from the previous observation timepoint represented by \(x_1\).

The operation \({\textsf {ruleExt} }\) takes an evolution pattern \(\theta \) and generates a restriction-extension pattern \(\rho \) from it by adding the variables contained in a set V as global variables.⁴⁵ Moreover, the AC of the resulting restriction-extension pattern additionally requires the satisfaction of a given AC \(\gamma \) and that the variables in V remain unchanged. Finally, the components \({\rho }{.}{{\textsf {res} }} \) and \({\rho }{.}{{\textsf {ext} }} \) are obtained by composing \({\theta }{.}{{\textsf {del} }} \) and \({\theta }{.}{{\textsf {res} }} \) for \({\rho }{.}{{\textsf {res} }} \) and by composing \({\theta }{.}{{\textsf {add} }} \) and \({\theta }{.}{{\textsf {ext} }} \) for \({\rho }{.}{{\textsf {ext} }} \) where we note that the checks regarding the addition and deletion of graph elements is covered by the ACs generated in .

For our running example, the application of the operation \({\textsf {ruleExt} }\) results in the restriction-extension patterns used in lines 3, 5, and 7 of the GC from Fig. 32 by adapting the three evolution patterns used in the MTGC from Fig. 28a.

We now introduce the operation , which proceeds by first creating a restriction-extension pattern to existentially quantify a global variable \(x_0\) denoting the initial current observation timepoint with an initial value of 0. We then apply the inductive operation , which is parameterized by (a) a word of global variables representing the return addresses for the delta-release operator (which is initially empty), (b) a global variable \( x_{outer} \) representing the timepoint t in the satisfaction relation (which is initially \(x_0\)), and (c) a set of global variables V that occur in a particular part of the resulting GC (which is initially \(\{x_0\}\)).

Definition 45

(Operation ) If \(\psi \in {\mathcal {S}}_{0, \varvec{\varnothing }}^{\mathsf {MTGC}}\) is an MTGC to be encoded using , \(\rho ={\textsf {ruleAdd} } (\varvec{\varnothing },\varnothing ,x_0,x_0=0) \) is a restriction-extension pattern adding the variable \(x_0\) representing the initial observation timepoint 0 to the empty graph, and is the encoding of \(\psi \) relative to \(x_0\), then is the encoding of \(\psi \) where , if one of the following items applies.

\(\bullet \): 

conjunction:

• \(\psi =\wedge S \) and

• .

\(\bullet \): 

negation:

\(\bullet \): 

\(\psi =\lnot \bar{\psi } \) and

\(\bullet \): 

.

\(\bullet \): 

delta-lock:

\(\bullet \): 

input metric temporal graph condition \(\psi \):

\(\bullet \): 

,

\(\bullet \): 

\({\theta _1}{.}{{\textsf {lG} }} ={\theta _2}{.}{{\textsf {lG} }} =H\),

\(\bullet \): 

\({\theta _1}{.}{{\textsf {rG} }} =H_1'\),

\(\bullet \): 

\({\theta _2}{.}{{\textsf {rG} }} =H_2'\),

\(\bullet \): 

restriction-extension pattern \(\rho _2'\):

\(\bullet \): 

\(x_2\notin V\),

\(\bullet \): 

\(\rho _2'={\textsf {ruleAdd} } (H,V,x_2,{\textsf {shift} }_{\textsf {DS} } (\gamma ,x_2, x_{outer} )) \),

\(\bullet \): 

restriction-extension pattern \(\rho _2''\):

\(\bullet \): 

\(\gamma _2''={{\textsf {alive} }(x_2,H_2')} \wedge (\mathsf {if~} \kappa =\mathsf {N} \mathsf {~then~} {{\textsf {earliest} }(x_2,H_2')} \mathsf {~else~} \top ), \)

\(\bullet \): 

\(\rho _2''={\textsf {ruleExt} } (\theta _2,V\cup \{x_2\},\gamma _2'') \),

\(\bullet \): 

graph condition \(\phi _2\):

\(\bullet \): 

,

\(\bullet \): 

restriction-extension pattern \(\rho _1'\):

\(\bullet \): 

\(x_1\notin V\),

\(\bullet \): 

\(\gamma _1= x_2< x_1 \wedge x_1\le x_{outer} \),

\(\bullet \): 

\(\gamma _2= x_{outer} \le x_1 \wedge x_1< x_2 \),

\(\bullet \): 

\(\rho _1'={\textsf {ruleAdd} } (H,V\cup \{x_2\},x_1,\gamma _1\vee \gamma _2) \),

\(\bullet \): 

restriction-extension pattern \(\rho _1''\):

\(\bullet \): 

\(\rho _1''={\textsf {ruleExt} } (\theta _1,V\cup \{x_2,x_1\},{{\textsf {alive} }(x_1,H_1')}) \),

\(\bullet \): 

graph condition \(\phi _1\):

\(\bullet \): 

,

\(\bullet \): 

restriction-extension pattern \(\bar{\rho }_2'\):

\(\bullet \): 

\(\bar{x}_2\notin V\),

\(\bullet \): 

\(\bar{\gamma }_1= x_2< \bar{x}_2 \wedge \bar{x}_2\le x_{outer} \),

\(\bullet \): 

\(\bar{\gamma }_2= x_{outer} \le \bar{x}_2 \wedge \bar{x}_2< x_2 \),

\(\bullet \): 

\(\bar{\gamma }_3= (\bar{\gamma }_1\vee \bar{\gamma }_2) \wedge {\textsf {shift} }_{\textsf {DS} } (\gamma ,\bar{x}_2, x_{outer} ) \),

\(\bullet \): 

\(\bar{\rho }_2'={\textsf {ruleAdd} } (H,V\cup \{x_2\},\bar{x}_2,\bar{\gamma }_3) \),

\(\bullet \): 

restriction-extension pattern \(\bar{\rho }_2''\):

\(\bullet \): 

\(\bar{\rho }_2''={\textsf {ruleExt} } (\theta _2,V\cup \{x_2,\bar{x}_2\},{{\textsf {alive} }(\bar{x}_2,H_2')}) \),

\(\bullet \): 

graph condition \(\bar{\phi }_2\):

\(\bullet \): 

, and

\(\bullet \): 

output graph condition \(\phi \):

\(\bullet \): 

\(\phi = \Delta ^{\mathsf {E}}(\rho _2', \Delta ^{\mathsf {E}}(\rho _2'',\phi _2) \wedge \Delta ^{\mathsf {A}}(\rho _1',\Delta ^{\mathsf {E}}(\rho _1'',\phi _1)) \wedge \bar{\phi }_2 ) \).

\(\bullet \): 

delta-release:

\(\bullet \): 

input metric temporal graph condition \(\psi \):

\(\bullet \): 

\(\psi =\boxdot (\bar{\theta },\bar{\psi }) \),

\(\bullet \): 

\({\bar{\theta }}{.}{{\textsf {lG} }} =H\),

\(\bullet \): 

\({\bar{\theta }}{.}{{\textsf {rG} }} =H'\),

\(\bullet \): 

\( xs = xs' \cdot x_{last} \),

\(\bullet \): 

restriction-extension pattern \(\bar{\rho }'\):

\(\bullet \): 

\(x\notin V\),

\(\bullet \): 

\(\gamma _1= x_{last} \le x \wedge x< x_{outer} \),

\(\bullet \): 

\(\gamma _2= x_{outer} < x \wedge x\le x_{last} \),

\(\bullet \): 

\(\bar{\rho }'={\textsf {ruleAdd} } (H,V,x,\gamma _1\vee \gamma _2) \),

\(\bullet \): 

restriction-extension pattern \(\bar{\rho }''\):

\(\bullet \): 

\(\bar{\rho }''={\textsf {ruleExt} } (\bar{\theta },V\cup \{x\},{{\textsf {alive} }(x,H')}) \),

\(\bullet \): 

graph condition \(\bar{\phi }\):

\(\bullet \): 

, and

\(\bullet \): 

output graph condition \(\phi \):

\(\bullet \): 

\(\phi = \Delta ^{\mathsf {A}}(\bar{\rho }', \Delta ^{\mathsf {E}}(\bar{\rho }'',\bar{\phi }) ) \).

For our running example, see again Fig. 32 for the encoding of the MTGC from Fig. 28a using . Note that all usages of the delta-lock operator in the given MTGC have a trivial left-hand side argument. Hence, when applying the operation , we observe that the GC \(\Delta ^{\mathsf {A}}(\theta _1',\Delta ^{\mathsf {E}}(\theta _1'',\phi _1)) \) is trivially satisfied because \(\phi _1\) is equivalent to \(\top \). To simplify the presentation, we have omitted these additional trivial subconditions in Fig. 32. Also note that the two negation operators in lines 2 and 4 originate from the universal quantification in the given MTGC.

We now state the soundness of the encoding operation defined above.

We conclude from this theorem that the two operations \({\textsf {Fold} }^{\textsf {tgs} }\) and can be used together to translate the MTGC satisfaction problem into a GC satisfaction problem. Moreover, we can apply \({\textsf {enc} }_{\Delta }\) (see Corollary 2) and \({\textsf {enc} }_{\nu }\) (see Corollary 1) to translate the GC satisfaction checking problem into a BGC satisfaction checking problem. The operations , \({\textsf {enc} }_{\Delta }\), and \({\textsf {enc} }_{\nu }\) as well as BGC satisfaction checking (see Corollary 3) are supported by our prototypical implementation in AutoGraph.