11institutetext: Hasso Plattner Institute at the University of Potsdam
Prof.-Dr.-Helmert-Str. 2-3, D-14482 Potsdam, Germany
11email<EMAIL_ADDRESS>
# Localized RETE for Incremental Graph Queries

Matthias Barkowsky  Holger Giese

###### Abstract

Context: The growing size of graph-based modeling artifacts in model-driven
engineering calls for techniques that enable efficient execution of graph
queries. Incremental approaches based on the RETE algorithm provide an
adequate solution in many scenarios, but are generally designed to search for
query results over the entire graph. However, in certain situations, a user
may only be interested in query results for a subgraph, for instance when a
developer is working on a large model of which only a part is loaded into
their workspace. In this case, the global execution semantics can result in
significant computational overhead.

Contribution: To mitigate the outlined shortcoming, in this paper we propose
an extension of the RETE approach that enables local, yet fully incremental
execution of graph queries, while still guaranteeing completeness of results
with respect to the relevant subgraph.

Results: We empirically evaluate the presented approach via experiments
inspired by a scenario from software development and an independent social
network benchmark. The experimental results indicate that the proposed
technique can significantly improve performance regarding memory consumption
and execution time in favorable cases, but may incur a noticeable linear
overhead in unfavorable cases.

##  1 Introduction

In model-driven engineering, models constitute important development artifacts
[29]. With complex development projects involving large, interconnected
models, performance of automated model operations becomes a primary concern.

Incremental graph query execution based on the RETE algorithm [19] has been
demonstrated to be an adequate solution in scenarios where an evolving model
is repeatedly queried for the same information [33]. In this context, the RETE
algorithm essentially tackles the problem of querying a usually graph-based
model representation via operators from relational algebra [12]. With these
operators not designed to exploit the locality found in graph-based encodings,
current incremental querying techniques require processing of the entire model
to guarantee complete results. However, in certain situations, global query
execution is not required and may be undesirable due to performance
considerations.

For instance, a developer may be working on only a part of a model loaded into
their workspace, with a large portion of the full model still stored on disk.
A concrete example of this would be a developer using a graphical editor to
modify an individual block diagram from a collection of interconnected block
diagrams, which together effectively form one large model. As the developer
modifies the model part in their workspace, they may want to continuously
monitor how their changes impact the satisfaction of some consistency
constraints via incremental model queries. In this scenario, existing
techniques for incremental query execution require loading and querying the
entire collection of models, even though the user is ultimately only
interested in the often local effect of their own changes.

The global RETE execution semantics then results in at least three problems:
First, the computation of query results for the full model, of which only a
portion is relevant to the user, may incur a substantial overhead on initial
query execution time. Second, incremental querying techniques are known to
create and store a large number of intermediate results [33], many of which
can in this scenario be superfluous, causing an overhead in memory
consumption. Third, query execution requires loading the entire model into
memory, potentially causing an overhead in loading time and increasing the
overhead in memory consumption.

These problems can be mitigated to some extent by employing local search [13,
22, 6], which better exploits the locality of the problem and lazy loading
capabilities of model persistence layers [1, 14], instead of a RETE-based
technique. However, resorting to local search can result in expensive
redundant search operations that are only avoided by fully incremental
solutions [33].

In this paper, we instead propose to tackle the outlined shortcoming of
incremental querying techniques via an extension of the RETE approach. This is
supported by a relaxed notion of completeness for query results that accounts
for situations where the computation for the full model is unnecessary.
Essentially, this enables a distinction between the full model, for which
query results do not necessarily have to be complete, and a relevant model
part, for which complete results are required. The extended RETE approach then
anchors query execution to the relevant model part and lazily fetches
additional model elements required to compute query results that meet the
relaxed completeness requirement. Our approach thereby avoids potentially
expensive global query execution and allows an effective integration of
incremental queries with model persistence layers.

The remainder of this paper is structured as follows: Section 2 provides a
summary of our notion of graphs, graph queries, and the RETE mechanism for
query execution. Section 3 discusses our contribution in the form of a relaxed
notion of completeness for query results and an extension to the RETE querying
mechanism that enables local, yet fully incremental execution of model
queries. A prototypical implementation of our approach is evaluated regarding
execution time and memory consumption in Section 4. Section 5 discusses
related work, before Section 6 concludes the paper and provides an outlook on
future work.

##  2 Preliminaries

In the following, we briefly reiterate the definitions of graphs and graph
queries and summarize the RETE approach to incremental graph querying.

###  2.1 Graphs and Graph Queries

As defined in [17], a _graph_ is a tuple $G=(V^{G},E^{G},s^{G},t^{G})$, with
$V^{G}$ the set of vertices, $E^{G}$ the set of edges, and
$s^{G}:E^{G}\rightarrow V^{G}$ and $t^{G}:E^{G}\rightarrow V^{G}$ functions
mapping edges to their source respectively target vertices.

A mapping from a graph $Q$ into another graph $H$ is defined via a _graph
morphism_ $m:Q\rightarrow H$, which is characterized by two functions
$m^{V}:V^{Q}\rightarrow V^{H}$ and $m^{E}:E^{Q}\rightarrow E^{H}$ such that
$s^{H}\circ m^{E}=m^{V}\circ s^{Q}$ and $t^{H}\circ m^{E}=m^{V}\circ t^{Q}$.

A graph $G$ can be typed over a type graph $TG$ via a graph morphism
$type^{G}:G\rightarrow TG$, forming the _typed graph_ $G^{T}=(G,type^{G})$. A
_typed graph morphism_ from $G^{T}=(G,type^{G})$ into another typed graph
$H^{T}=(H,type^{H})$ with type graph $TG$ is a graph morphism
$m^{T}:G\rightarrow H$ such that $type^{H}\circ m^{T}=type^{G}$.

We say that $G$ is _edge-dominated_ if $\forall e_{TG}\in E^{TG}:|\\{e\in
E^{G}|type(e)=e_{TG}\\}|\geq max(|\\{v\in
V^{G}|type(v)=s^{TG}(e_{TG})\\}|,|\\{v\in V^{G}|type(v)=t^{TG}(e_{TG})\\}|)$.

A _model_ is then simply given by a (typed) graph. In the remainder of the
paper, we therefore use the terms graph and model interchangably.

A _graph query_ as considered in this paper is characterized by a (typed)
query graph $Q$ and can be executed over a (typed) host graph $H$ by finding
(typed) graph morphisms $m:Q\rightarrow H$. We also call these morphisms
_matches_ and denote the set of all matches from $Q$ into $H$ by
$\mathcal{M}^{Q}_{H}$. Typically, a set of matches is considered a complete
query result if it contains all matches in $\mathcal{M}^{Q}_{H}$.

###  2.2 Incremental Graph Queries with RETE

The RETE algorithm [19] forms the basis of mature incremental graph querying
techniques [34]. Therefore, the query graph is recursively decomposed into
simpler subqueries, which are arranged in a second graph called RETE net. In
the following, we will refer to the vertices of RETE nets as _(RETE) nodes_.

Each RETE node is associated with a subgraph of the query graph for which it
computes matches. This computation may depend on matches computed by other
RETE nodes. Such dependencies are represented by edges from the dependent node
to the dependency node. For each RETE net, one of its nodes is designated as
the _production node_ , which computes the net’s overall result. A RETE net is
thus given by a tuple $(N,p)$, where the _RETE graph_ $N$ is a graph of RETE
nodes and dependency edges and $p\in V^{N}$ is the production node.

We describe the _configuration_ of a RETE net $(N,p)$ during execution by a
function $\mathcal{C}:V^{N}\rightarrow\mathcal{P}(\mathcal{M}_{\Omega})$, with
$\mathcal{P}$ denoting the power set and $\mathcal{M}_{\Omega}$ the set of all
graph morphisms. $\mathcal{C}$ then assigns each node in $V^{N}$ a _current
result set_.

For a starting configuration $\mathcal{C}$ and host graph $H$, executing a
RETE node $n\in V^{N}$ with associated query subgraph $Q$ yields the updated
configuration $\mathcal{C}^{\prime}=execute(n,N,H,\mathcal{C})$, with

$\mathcal{C}^{\prime}(n^{\prime})=\begin{cases}\mathcal{R}(n,N,H,\mathcal{C})&\quad\text{if
}$n' = n$\\\ \mathcal{C}(n^{\prime})&\quad\text{otherwise},\end{cases}$

where $\mathcal{R}$ is a function defining the _target result set_ of a RETE
node $n$ in the RETE graph $N$ for $H$ and $\mathcal{C}$ such that
$\mathcal{R}(n,N,H,\mathcal{C})\subseteq\mathcal{M}^{Q}_{H}$.

We say that $\mathcal{C}$ is _consistent_ for a RETE node $n\in V^{N}$ and
host graph $H$ iff $\mathcal{C}(n)=\mathcal{R}(n,N,H,\mathcal{C})$. If
$\mathcal{C}$ is consistent for all $n\in V^{N}$, we say that $\mathcal{C}$ is
consistent for $H$. If $H$ is clear from the context, we simply say that
$\mathcal{C}$ is consistent.

Given a host graph $H$ and a starting configuration $\mathcal{C}_{0}$, a RETE
net $(N,p)$ is executed via the execution of a sequence of nodes
$O=n_{1},n_{2},...,n_{x}$ with $n_{i}\in V^{N}$. This yields the trace
$\mathcal{C}_{0},\mathcal{C}_{1},\mathcal{C}_{2},...,\mathcal{C}_{x}$, with
$\mathcal{C}_{y}=execute(n_{y},N,H,\mathcal{C}_{y-1})$, and the result
configuration $execute(O,N,H,\mathcal{C}_{0})=\mathcal{C}_{x}$.

$(N,p)$ can initially be executed over $H$ via a sequence $O$ that yields a
consistent configuration $\mathcal{C}_{x}=execute(O,N,H,\mathcal{C}_{0})$,
where $\mathcal{C}_{0}$ is an empty starting configuration with $\forall n\in
V^{N}:\mathcal{C}_{0}(n)=\emptyset$. Incremental execution of $(N,p)$ can be
achieved by retaining a previous result configuration and using it as the
starting configuration for execution over an updated host graph. This requires
incremental implementations of RETE node execution procedures that update
previously computed result sets for changed inputs instead of computing them
from scratch.

In the most basic form, a RETE net for the query graph $Q$ consists of two
kinds of nodes, _edge input nodes_ and _join nodes_. Edge input nodes have no
dependencies, are associated with a query subgraph consisting of a single edge
and its adjacent vertices, and directly extract the (trivial) matches for $Q$
from a host graph. Join nodes have two dependencies with some associated query
subgraphs $Q_{l}$ and $Q_{r}$ such that $V^{Q_{l}\cap Q_{r}}\neq\emptyset$ and
are associated with the subgraph $Q=Q_{l}\cup Q_{r}$. A join node computes
matches for this union subgraph by combining the matches from its dependencies
along the overlap graph $Q_{\cap}=Q_{l}\cap Q_{r}$.

In the following, we assume query graphs to be weakly connected and contain at
least one edge. A RETE net that computes matches for a query graph $Q$ can
then be constructed as a tree of join nodes over edge input nodes. The join
nodes thus gradually compose the trivial matches at the bottom into matches
for more complex query subgraphs. We call such tree-like RETE nets _well-
formed_. An execution sequence that always produces a consistent configuration
is given by a reverse topological sorting of the net. The root node of the
tree then computes the set of all matches for $Q$ and is designated as the
net’s production node.

Connected graphs without edges consist of only a single vertex, making query
execution via _vertex input nodes_ , which function analogously to edge input
nodes, trivial. Disconnected query graphs can be handled via separate RETE
nets for all query graph components and the computation of a cartesian
product.

Figure 1 shows an example graph query from the software domain and an
associated RETE net. The query searches for paths of a package, class, and
field. The RETE net constructs matches for the query by combining edges from a
package to a class with edges from a class to a field via a natural join.

p:Pkgc:Classf:Fieldcefe

$\bowtie$$p\rightarrow c$$c\rightarrow f$

Figure 1: Example graph query (left) and corresponding RETE net (right)

##  3 Incremental Queries over Subgraphs

As outlined in Section 1, users of model querying mechanisms may only be
interested in query results, that is, matches, related to some part of a model
that is relevant to them rather than the complete model. However, simply
executing a query only over the relevant subgraph and ignoring context
elements is not sufficient in many situations, for instance if the full effect
of modifications to the relevant subgraph should be observed, since such
modifications may affect matches that involve elements outside the relevant
subgraph. Instead, completeness in such scenarios essentially requires the
computation of all matches that somehow _touch_ the relevant subgraph.

In order to capture this need for local completeness, but avoid the
requirement for global execution inherent to the characterization in Section
2.1, we define completeness under a relevant subgraph of some host graph as
follows:

###### Definition 1

_(Completeness of Query Results under Subgraphs)_ We say that a set of matches
$M$ from query graph $Q$ into host graph $H$ is complete under a subgraph
$H_{p}\subseteq H$ iff $\forall m\in\mathcal{M}^{Q}_{H}:(\exists v\in
V^{Q}:m(v)\in V^{H_{p}})\Rightarrow m\in M$.

###  3.1 Marking-sensitive RETE

Due to its reliance on edge and vertex input nodes and their global execution
semantics, incremental query execution via the standard RETE approach is
unable to exploit the relaxed notion of completeness from Definition 1 for
query optimization and does not integrate well with mechanisms relying on
operation locality, such as model persistence layers based on lazy loading [1,
14].

While query execution could be localized to a relevant subgraph by executing
edge and vertex inputs nodes only over the subgraph, execution would then only
yield matches where _all_ involved elements are in the relevant subgraph. This
approach would hence fail to meet the completeness criterion of Definition 1.

To enable incremental queries with complete results under the relevant
subgraph, we instead propose to anchor RETE net execution to subgraph elements
while allowing the search to retrieve elements outside the subgraph that are
required to produce complete results from the full model.

Therefore, we extend the standard RETE mechanism by a marking for intermediate
results, which allows such intermediate results to carry information that can
later be used to control their propagation in the RETE net. In our extension,
an intermediate result is therefore characterized by a tuple $(m,\phi)$ of a
match $m$ and a marking $\phi\in\overline{\mathbb{N}}$, where we define
$\overline{\mathbb{N}}:=\mathbb{N}\cup\\{\infty\\}$. A marking-sensitive
configuration is hence given by a function
$\mathcal{C}^{\Phi}:V^{N}\rightarrow\mathcal{P}(\mathcal{M}_{\Omega}\times\overline{\mathbb{N}})$.

Furthermore, in our extension, result computation distinguishes between the
full host graph $H$ and the relevant subgraph $H_{p}\subseteq H$. For marking-
sensitive RETE nodes, we hence extend the function for target result sets by a
parameter for $H_{p}$. The target result set of a marking-sensitive RETE node
$n^{\Phi}\in V^{N^{\Phi}}$ with associated subgraph $Q$ for $H$, $H_{p}$, and
a marking-sensitive configuration $\mathcal{C}^{\Phi}$ is then given by
$\mathcal{R}^{\Phi}(n^{\Phi},N^{\Phi},H,H_{p},\mathcal{C}^{\Phi})$, with
$\mathcal{R}^{\Phi}(n^{\Phi},N^{\Phi},H,H_{p},\mathcal{C}^{\Phi})\subseteq\mathcal{M}^{Q}_{H}\times\overline{\mathbb{N}}$.

We adapt the _join node_ , _union node_ , and _projection node_ to marking-
sensitive variants that assign result matches the maximum marking of related
dependency matches and otherwise work as expected from relational algebra
[12]. We also adapt the _vertex input node_ to only consider vertices in the
relevant subgraph $H_{p}$ and assign matches the marking $\infty$. Finally, we
introduce _marking assignment nodes_ , which assign matches a fixed marking
value, _marking filter nodes_ , which filter marked matches by a minimum
marking value, and _forward and backward navigation nodes_ , which work
similarly to edge input nodes but only extract edges that are adjacent to host
graph vertices included in the current result set of a designated dependency.
Note that an efficient implementation of the backward navigation node requires
reverse navigability of host graph edges.111Formal definitions for the adapted
node semantics can be found in Appendix 0.D.

To obtain query results in the format of the standard RETE approach, we define
the _stripped result set_ of a marking-sensitive RETE node $n^{\Phi}$ for a
marking-sensitive configuration $\mathcal{C}^{\Phi}$ as
$\mathcal{R}^{\Phi}_{X}(n^{\Phi},\mathcal{C}^{\Phi})=\\{m|(m,\phi)\in\mathcal{C}^{\Phi}(n^{\Phi})\\}$,
that is, the set of matches that appear in tuples in the node’s current result
set in $\mathcal{C}^{\Phi}$.

###  3.2 Localized Search with Marking-sensitive RETE

Based on these adaptations, we introduce a recursive $localize$ procedure,
which takes a regular, well-formed RETE net $(N,p)$ as input and outputs a
marking-sensitive RETE net that performs a localized search that does not
require searching the full model to produce complete results according to
Definition 1.

If $p=[v\rightarrow w]$ is an edge input node, the result of localization for
$(N,p)$ is given by $localize((N,p))=(LNS(p),[\cup]^{\Phi})$. The _local
navigation structure_ $LNS(p)$ consists of seven RETE nodes as shown in Figure
2 (left): (1, 2) Two marking-sensitive vertex input nodes $[v]^{\Phi}$ and
$[w]^{\Phi}$, (3, 4) two marking-sensitive union nodes $[\cup]^{\Phi}_{v}$ and
$[\cup]^{\Phi}_{w}$ with $[v]^{\Phi}$ respectively $[w]^{\Phi}$ as a
dependency, (5) a forward navigation node $[v\rightarrow_{n}w]^{\Phi}$ with
$[\cup]^{\Phi}_{v}$ as a dependency, (6) a backward navigation node
$[w\leftarrow_{n}v]^{\Phi}$ with $[\cup]^{\Phi}_{w}$ as a dependency, and (7)
a marking-sensitive union node $[\cup]^{\Phi}$ with dependencies
$[v\rightarrow_{n}w]^{\Phi}$ and $[w\leftarrow_{n}v]^{\Phi}$.

Importantly, the marking-sensitive vertex input nodes of the local navigation
structure are executed over the relevant subgraph, whereas the forward and
backward navigation nodes are executed over the full model. Intuitively, the
local navigation structure thus takes the role of the edge input node, but
initially only extracts edges that are adjacent to a vertex in the relevant
subgraph.

If $p$ is a join node, it has two dependencies $p_{l}$ and $p_{r}$ with
associated query subgraphs $Q_{l}$ and $Q_{r}$, which are the roots of two
RETE subtrees $N_{l}$ and $N_{r}$. In this case, $(N,p)$ is localized as
$localize((N,p))=(N^{\Phi},p^{\Phi})=(N^{\Phi}_{\bowtie}\cup N^{\Phi}_{l}\cup
N^{\Phi}_{r}\cup RPS_{l}\cup RPS_{r},[\bowtie]^{\Phi})$, where
$(N^{\Phi}_{l},p^{\Phi}_{l})=localize((N_{l},p_{l}))$,
$(N^{\Phi}_{r},p^{\Phi}_{r})=localize((N_{r},p_{r}))$, $N^{\Phi}_{\bowtie}$
consists of the marking-sensitive join $[\bowtie]^{\Phi}$ with dependencies
$p^{\Phi}_{l}$ and $p^{\Phi}_{r}$, $RPS_{l}=RPS(p^{\Phi}_{l},N^{\Phi}_{r})$,
and $RPS_{r}=RPS(p^{\Phi}_{r},N^{\Phi}_{l})$.

The _request projection structure_ $RPS_{l}=RPS(p^{\Phi}_{l},N^{\Phi}_{r})$
contains three RETE nodes as displayed in Figure 2 (center): (1) A marking
filter node $[\phi>h]^{\Phi}$ with $p^{\Phi}_{l}$ as a dependency, (2) a
marking-sensitive projection node $[\pi_{Q_{v}}]^{\Phi}$ with
$[\phi>h]^{\Phi}$ as a dependency, and (3) a marking assignment node
$[\phi:=h]^{\Phi}$ with $[\pi_{Q_{v}}]^{\Phi}$ as a dependency. The value of
$h$ is given by the height of the join tree of which $p$ is the root and
$Q_{v}$ is a graph consisting of a single vertex $v\in V^{Q_{l}\cap Q_{r}}$.
The request projection structure is then connected to an arbitrary local
navigation structure in $N^{\Phi}_{r}$ that has a marking-sensitive node input
$[v]^{\Phi}$ associated with $Q_{v}$. Therefore, it also adds a dependency
from the marking-sensitive union node $[\cup]^{\Phi}_{v}$ that already depends
on $[v]^{\Phi}$ to the marking assignment node $[\phi:=h]^{\Phi}$. The
mirrored structure $RPS_{r}=RPS(p^{\Phi}_{r},N^{\Phi}_{l})$ is constructed
analogously.

Via the request projection structures, partial matches from one join
dependency can be propagated to the subnet under the other dependency.
Intuitively, the inserted request projection structures thereby allow the
join’s dependencies to request the RETE subnet under the other dependency to
fetch and process the model parts required to complement the first
dependency’s results. The marking of a match then signals up to which height
in the join tree complementarity for that match is required. Notably, matches
involving elements in the relevant subgraph are marked $\infty$, as
complementarity for them is required at the very top to guarantee completeness
of the overall result.

The result of applying $localize$ to the example RETE net in Figure 1 is
displayed in Figure 2 (right). It consists of a marking sensitive join and two
local navigation structures connected via request projection structures.

$\cup$$\Phi$$v\rightarrow_{n}w$$\Phi$$w\leftarrow_{n}v$$\Phi$$\cup$$\Phi$$\cup$$\Phi$$v$$\Phi$$w$$\Phi$

$\phi:=h$$\Phi$$\pi_{Q_{v}}$$\Phi$$\phi>h$$\Phi$

$\bowtie$$\Phi$$LNS^{p\rightarrow c}$$LNS^{c\rightarrow
f}$$RPS^{c}_{r}$$RPS^{c}_{l}$

Figure 2: LNS (left), RPS (center), and localized RETE net (right)

A consistent configuration for a localized RETE net then indeed guarantees
query results that are complete according to Definition 1:

###### Theorem 3.1

Let $H$ be a graph, $H_{p}\subseteq H$, $(N,p)$ a well-formed RETE net, and
$Q$ the query graph associated with $p$. Furthermore, let $\mathcal{C}^{\Phi}$
be a consistent configuration for the localized RETE net
$(N^{\Phi},p^{\Phi})=localize((N,p))$. The set of matches given by the
stripped result set $\mathcal{R}^{\Phi}_{X}(p^{\Phi},\mathcal{C}^{\Phi})$ is
then complete under $H_{p}$.

###### Proof

(Idea)222See Appendix 0.D for detailed proofs. It can be shown via induction
over the height of $N$ that request projection structures ensure the
construction of all intermediate results required to guarantee completeness of
the overall result under $H_{p}$.

Notably, the insertion of request projection structures creates cycles in the
localized RETE net, which prevents execution via a reverse topological
sorting. However, the marking filter and marking assignment nodes in the
request projection structures effectively prevent cyclic execution at the
level of intermediate results: Because matches in the result set of a
dependency of some join at height $h$ that are only computed on request from
the other dependency are marked $h$, these matches are filtered out in the
dependent request projection structure. An execution order for the localized
RETE net $(N^{\Phi},p^{\Phi})=localize((N,p))$ can thus be constructed
recursively via an $order$ procedure as follows:

If $p$ is an edge input node, the RETE graph given by $N^{\Phi}=LNS(p)$ is a
tree that can be executed via a reverse topological sorting of the nodes in
$LNS(p)$, that is, $order((N^{\Phi},p^{\Phi}))=toposort(LNS(p))^{-1}$.

If $p$ is a join, according to the construction, the localized RETE graph is
given by $N^{\Phi}=N^{\Phi}_{\bowtie}\cup N^{\Phi}_{l}\cup N^{\Phi}_{r}\cup
RPS_{l}\cup RPS_{r}$. In this case, an execution order for
$(N^{\Phi},p^{\Phi})$ can be derived via the concatenation
$order((N^{\Phi},p^{\Phi}))=order(RPS_{r})\circ order(N^{\Phi}_{l})\circ
order(RPS_{l})\circ order(N^{\Phi}_{r})\circ order(RPS_{r})\circ
order(N^{\Phi}_{l})\circ order(N^{\Phi}_{\bowtie})$, where
$order(RPS_{l})=toposort(RPS_{l})^{-1}$,
$order(RPS_{r})=toposort(RPS_{r})^{-1}$, and
$order(N^{\Phi}_{\bowtie})=[p^{\Phi}]$, that is, the sequence containing only
$p^{\Phi}$.

Executing a localized RETE net $(N^{\Phi},p^{\Phi})$ via
$order((N^{\Phi},p^{\Phi}))$ then guarantees a consistent result configuration
for any starting configuration:

###### Theorem 3.2

Let $H$ be a graph, $H_{p}\subseteq H$, $(N,p)$ a well-formed RETE net, and
$\mathcal{C}^{\Phi}_{0}$ an arbitrary starting configuration. Executing the
marking-sensitive RETE net $(N^{\Phi},p^{\Phi})=localize((N,p))$ via
$O=order((N^{\Phi},p^{\Phi}))$ then yields a consistent configuration
$\mathcal{C}^{\Phi}=execute(O,N^{\Phi},H,H_{p},\mathcal{C}^{\Phi}_{0})$.

###### Proof

(Idea) Follows because the inserted marking filter nodes prevent cyclic
execution behavior at the level of intermediate results.

Combined with the result from Theorem 3.1, this means that a localized RETE
net can be used to compute complete query results for a relevant subgraph in
the sense of Definition 1, as outlined in the following corollary:

###### Corollary 1

Let $H$ be a graph, $H_{p}\subseteq H$, $(N,p)$ a well-formed RETE net, and
$Q$ the query graph associated with $p$. Furthermore, let
$\mathcal{C}^{\Phi}_{0}$ be an arbitrary starting configuration for the
localized RETE net $(N^{\Phi},p^{\Phi})=localize((N,p))$ and
$\mathcal{C}^{\Phi}=execute(order((N^{\Phi},p^{\Phi})),N^{\Phi},H,H_{p},\mathcal{C}^{\Phi}_{0})$.
The set of matches from $Q$ into $H$ given by
$\mathcal{R}^{\Phi}_{X}(p^{\Phi},\mathcal{C}^{\Phi})$ is then complete under
$H_{p}$.

###### Proof

Follows directly from Theorem 3.1 and Theorem 3.2.

###  3.3 Performance of Localized RETE Nets

Performance of a RETE net $(N,p)$ with respect to both execution time and
memory consumption is largely determined by the _effective size_ of a
consistent configuration $\mathcal{C}$ for $(N,p)$, which we define as
$|\mathcal{C}|_{e}:=\sum_{n\in V^{N}}\sum_{m\in\mathcal{C}(n)}|m|$. In this
context, we define the size of a match $m:Q\rightarrow H$ as
$|m|:=|m^{V}|+|m^{E}|=|V^{Q}|+|E^{Q}|$. It can then be shown that localization
incurs only a constant factor overhead on the effective size of $\mathcal{C}$
for any edge-dominated host graph:

###### Theorem 3.3

Let $H$ be an edge-dominated graph, $H_{p}\subseteq H$, $(N,p)$ a well-formed
RETE net with $Q$ the associated query graph of $p$, $\mathcal{C}$ a
consistent configuration for $(N,p)$ for host graph $H$, and
$\mathcal{C}^{\Phi}$ a consistent configuration for the localized RETE net
$(N^{\Phi},p^{\Phi})=localize((N,p))$ for host graph $H$ and relevant subgraph
$H_{p}$. It then holds that $\sum_{n^{\Phi}\in
V^{N^{\Phi}}}\sum_{(m,\phi)\in\mathcal{C}(n^{\Phi})}|m|\leq
7\cdot|\mathcal{C}|_{e}$.

###### Proof

(Idea) Follows because localization only increases the number of RETE nodes by
factor 7 and marking-sensitive result sets contain no duplicate matches.

By Theorem 3.3, it then follows that localization of a RETE net incurs only a
constant factor overhead on memory consumption even in the worst case where
the relevant subgraph is equal to the full model:

###### Corollary 2

Let $H$ be an edge-dominated graph, $H_{p}\subseteq H$, $(N,p)$ a well-formed
RETE net, $\mathcal{C}$ a consistent configuration for $(N,p)$ for host graph
$H$, and $\mathcal{C}^{\Phi}$ a consistent configuration for the localized
RETE net $(N^{\Phi},p^{\Phi})=localize((N,p))$ for host graph $H$ and relevant
subgraph $H_{p}$. Assuming that storing a match $m$ requires an amount of
memory in $O(|m|)$ and storing an element from $\overline{\mathbb{N}}$
requires an amount of memory in $O(1)$, storing $\mathcal{C}^{\Phi}$ requires
memory in $O(|\mathcal{C}|_{e})$.

###### Proof

(Idea) Follows from Theorem 3.3.

In the worst case, a localized RETE net would still be required to compute a
complete result. In this scenario, the execution of the localized RETE net may
essentially require superfluous recomputation of match markings, causing
computational overhead. When starting with an empty configuration, the number
of such recomputations per match is however limited by the size of the query
graph, only resulting in a small increase in computational complexity:

###### Theorem 3.4

Let $H$ be an edge-dominated graph, $H_{p}\subseteq H$, $(N,p)$ a well-formed
RETE net for query graph $Q$, $\mathcal{C}$ a consistent configuration for
$(N,p)$, and $\mathcal{C}^{\Phi}_{0}$ the empty configuration for
$(N^{\Phi},p^{\Phi})=localize((N,p))$. Executing $(N^{\Phi},p^{\Phi})$ via
$execute(order((N^{\Phi},p^{\Phi})),N^{\Phi},H,H_{p},\mathcal{C}^{\Phi}_{0})$
then takes $O(T\cdot(|Q_{a}|+|Q|))$ steps, with $|Q_{a}|$ the average size of
matches in $\mathcal{C}$ and $T=\sum_{n\in V^{N}}|\mathcal{C}(n)|$.

###### Proof

(Idea) Follows since the effort for initial construction of matches by the
marking-sensitive RETE net is linear in the total size of the constructed
matches and the marking of a match changes at most $|Q|$ times.

Assuming an empty starting configuration, a regular well-formed RETE net
$(N,p)$ can be executed in $O(|\mathcal{C}|_{e})$ steps, which can also be
expressed as $O(T\cdot|Q_{a}|)$. The overhead of a localized RETE net compared
to the original net can thus be characterized by the factor
$\frac{|Q|}{|Q_{a}|}$. Assuming that matches for the larger query subgraphs
constitute the bulk of intermediate results, which seems reasonable in many
scenarios, $\frac{|Q|}{|Q_{a}|}$ may be approximated by a constant factor.

For non-empty starting configurations and incremental changes, no sensible
guarantees can be made. On the one hand, in a localized RETE net, a host graph
modification may trigger the computation of a large number of intermediate
results that were previously omitted due to localization. On the other hand,
in a standard RETE net, a modification may result in substantial effort for
constructing superfluous intermediate results that can be avoided by
localization. Depending on the exact host graph structure and starting
configuration, execution may thus essentially require a full recomputation for
either the localized or standard RETE net but cause almost no effort for the
other variant.

##  4 Evaluation

We aim to investigate whether RETE net localization can improve performance of
query execution in scenarios where the relevant subgraph constitutes only a
fraction of the full model, considering initial query execution time,
execution time for incrementally processing model updates, and memory
consumption as performance indicators.333Experiments were executed on a Linux
SMP Debian 4.19.67-2 computer with Intel Xeon E5-2630 CPU (2.3 GHz clock rate)
and 386 GB system memory running OpenJDK 11.0.6. Reported measurements
correspond to the arithmetic mean of measurements for 10 runs. Memory
measurements were obtained using the Java Runtime class. To represent graph
data, all experiments use EMF [2] object graphs that enable reverse navigation
of edges. Our implementation is available under [3]. More details and query
visualizations can be found in Appendix 0.C and 0.B. We experiment with the
following querying techniques:

  * •

STANDARD: Our own implementation of a regular RETE net with global execution
semantics [8].

  * •

LOCALIZED: Our own implementation of the RETE net used for STANDARD, localized
according to the description in Section 3.2.

  * •

VIATRA: The external RETE-based VIATRA tool [34].

  * •

SDM*: Our own local-search-based Story Diagram Interpreter tool [22]. Note
that we only consider searching for new query results. We thus
underapproximate the time and memory required for a full solution with this
strategy, which would also require maintaining previously found results.

###  4.1 Synthetic Abstract Syntax Graphs

We first attempt a systematic evaluation via a synthetic experiment, which
emulates a developer loading part of a large model into their workspace and
monitoring some well-formedness constraints as they modify the loaded part,
that is, relevant subgraph, without simultaneous changes to other model parts.

We therefore generate Java abstract syntax graphs with 1, 10, 100, 1000, and
10000 packages, with each package containing 10 classes with 10 fields
referencing other classes. As relevant subgraph, we consider a single package
and its contents. We then execute a query searching for paths consisting of a
package and four classes connected via fields. After initial query execution,
we modify the relevant subgraph by creating a class with 10 fields in the
considered package and perform an incremental update of query results. This
step is repeated 10 times.

Figure 3 (right) displays the execution times for the initial execution of the
query. The execution time of LOCALIZED remains around 120 ms for all model
sizes. The execution time for SDM* slowly grows from around 350 ms to 1025 ms
due to indexing effort that is necessary for observing model changes. In
contrast, the execution time for the other RETE-based strategies clearly
scales with model size, with the execution time for STANDARD growing from
around 13 ms for the smallest model to more than 184 000 ms for the largest
model. On the one hand, localization thus incurs a noticeable overhead in
initial execution time for the smallest model, where even localized query
execution is essentially global. On the other hand, it significantly improves
execution time for the larger models and even achieves better scalability than
the local-search-based tool in this scenario.

The average times for processing a model update are displayed in Figure 3
(center). Here, all strategies achieve execution times mostly independent of
model size. While the measurements for STANDARD fluctuate, likely due to the
slightly unpredictable behavior of hash-based indexing structures, average
execution times remain low overall and below 10 ms for LOCALIZED. Still,
localization incurs a noticeable overhead up to factor 6 compared to STANDARD
and VIATRA. This overhead is expected, since in this scenario, all considered
updates affect the relevant subgraph and thus impact the results of the
localized RETE net similarly to the results of the standard RETE nets.
Consequently, localization does not reduce computational effort, but causes
overhead instead.

Finally, Figure 3 (left) shows the memory measurements for all strategies and
models after the final update. Here, LOCALIZED again achieves a substantial
improvement in scalability compared to the other RETE-based strategies, with a
slightly higher memory consumption for the smallest model and an improvement
by factor 120 over STANDARD for the largest model. This is a result of the
localized RETE net producing the same number of intermediate results for all
model sizes, with the slight growth in memory consumption likely a product of
the growing size of the model itself. SDM*, not storing any matches, performs
better for all but the largest model, where memory consumption surpasses the
measurement for LOCALIZED. This surprising result can probably be explained by
the fact that SDM* has to index the full model to observe modifications,
causing an overhead in memory consumption.

Figure 3: Measurements for the synthetic abstract syntax graph scenario (log
scale)

In addition to these experiments, where the full model is always stored in
main memory, we also experimented with a model initially stored on disk via
the persistence layer CDO [1]. Measurements mostly mirror those for the main-
memory-based experiment. Notably though, in conjunction with CDO the LOCALIZED
strategy achieves almost ideal scalability regarding memory consumption for
this scenario, with measurements around 70 MB for all model sizes.444See
Appendix 0.B for measurement results.

###  4.2 Real Abstract Syntax Graphs

To evaluate our approach in the context of a more realistic application
scenario, we perform a similar experiment using real data and queries inspired
by object-oriented design patterns [20]. In contrast to the synthetic
scenario, this experiment emulates a situation where modifications may concern
not only the relevant subgraph but the entire model, for instance when
multiple developers are simulatenously working on different model parts.

We therefore extract a history of real Java abstract syntax graphs with about
16 000 vertices and 45 000 edges from a software repository using the MoDisco
tool [11]. After executing the queries over the initial commit, we replay the
history and perform incremental updates of query results after each commit. As
relevant subgraph, we again consider a single package and its contents.

Figure 4 displays the aggregate execution time for processing the commits one
after another for the queries where LOCALIZED performed best and worst
compared to STANDARD, with the measurement at $x=0$ indicating the initial
execution time for the starting model. Initial execution times are similarly
low due to a small starting model and in fact slightly higher for LOCALIZE.
However, on aggregate LOCALIZED outperforms STANDARD with an improvement
between factor 5 and 18 due to significantly lower update times, which are
summarized in Figure 5 (left). In this case, the improvement mostly stems from
the more precise monitoring of the model for modifications: The RETE nets of
both STANDARD and LOCALIZED remain small due to strong filtering effects in
the query graphs. However, while STANDARD spends significant effort on
processing model change notifications due to observing all appropriately typed
model elements, this effort is substantially reduced for LOCALIZED, which only
monitors elements relevant to query results required for completeness under
the relevant subgraph. The execution times of SDM* can be explained by the
same effect. Interestingly, VIATRA seems to implement an improved handling of
such notifications, achieving improved execution times for particularly small
updates even compared to localize, but requiring more time if an update
triggers changes to the RETE net. Combined with a higher RETE net
initialization time, this results in LOCALIZED also outperforming VIATRA for
all considered queries.

Regarding memory consumption, all strategies perform very similarly, which is
mostly a result of the size of the model itself dominating the measurement and
hiding the memory impact of the rather small RETE nets.

Figure 4: Execution times for the real abstract syntax graph scenario Figure
5: Summary of update processing times for different scenarios (log scale)

###  4.3 LDBC Social Network Benchmark

Finally, we also experiment with the independent LDBC Social Network Benchmark
[18, 5], simulating a case where a user of a social network wants to
incrementally track query results relating to them personally.

We therefore generate a synthetic social network consisting of around 850 000
vertices, including about 1700 persons, and 5 500 000 edges using the
benchmark’s data generator and the predefined scale factor 0.1. We
subsequently transform this dataset into a sequence of element creations and
deletions based on the timestamps included in the data. We then create a
starting graph by replaying the first half of the sequence and perform an
initial execution of adapted versions of the benchmark queries consisting of
plain graph patterns, with a person with a close-to-average number of contacts
in the final social network designated as relevant subgraph. After the initial
query execution, we replay the remaining changes, incrementally updating the
query results after each change.

The resulting execution times for the benchmark queries where LOCALIZED
performed best and worst compared to STANDARD are displayed in Figure 6. A
summary of all update time measurements for LOCALIZED in comparison with
STANDARD is also displayed in Figure 5 (right). For all queries, LOCALIZED
ultimately outperforms the other approaches by a substantial margin, as the
localized RETE version forgoes the computation of a large number of irrelevant
intermediate results due to the small relevant subgraph on the one hand and
avoids redundant computations on the other hand.

Figure 6: Execution times for the LDBC scenario Figure 7: Memory measurements
for the LDBC scenario

The memory measurements in Figure 7 mostly mirror execution times for RETE-
based approaches, with the memory consumption for LOCALIZED always lower than
for STANDARD and VIATRA except for a period at the beginning of the execution
of the query INTERACTIVE_5, where STANDARD outperforms LOCALIZED. The weaker
performance for INTERACTIVE_5 and INTERACTIVE_10 likely stems from the fact
that these queries contain cycles, which act as strong filters for subsequent
(intermediate) results and achieve a somewhat similar effect as localization.
The weaker performance of VIATRA for INTERACTIVE_5 is a product of the usage
of a suboptimal RETE net. As expected, memory consumption is lowest for SDM*
for all queries.

###  4.4 Discussion

On the one hand, our experimental results demonstrate that in situations where
the relevant subgraph constitutes only a fraction of the full model, RETE net
localization can improve the performance of incremental query execution
compared to both the standard RETE approach and a solution based on local
search. In such scenarios, localization can improve scalability with respect
to initial query execution time and memory consumption, as demonstrated in
Sections 4.1 and 4.3 and, if changes are not restricted to the relevant
subgraph, also update processing time, as shown in Sections 4.2 and 4.3.

On the other hand, as demonstrated in Section 4.1, localization incurs an
overhead on update processing time if changes are only made to the relevant
subgraph and on initial execution time and memory consumption if the relevant
subgraph contains most of the elements in the full model. While this overhead
will essentially be limited to a constant factor in many scenarios, as
analyzed in Section 3.3, the standard RETE approach remains preferable for
query execution with global semantics or if modifications are restricted to
the relevant subgraph and initial query execution time and memory consumption
are irrelevant.

To mitigate internal threats to the validity of our results resulting from
unexpected JVM behavior, we have performed 10 runs of all experiments.
However, with reliable memory measurements a known pain point of Java-based
experiments, the reported memory consumption values are still not necessarily
accurate and can only serve as an indicator. To minimize the impact of the
implementation on conceptual observations, we compare the prototypical
implementation of our approach to a regular RETE implementation [8], which
shares a large portion of the involved code, and to two existing tools [34,
22].

We have attempted to address external threats to validity via experiments
accounting for different application domains and a combination of synthetic
and real-world queries and data, including a setting from an established,
independent benchmark. Still, our results cannot be generalized and do not
support quantitative claims, but serve to demonstrate conceptual advantages
and disadvantages of the presented approach.

##  5 Related Work

With graph query execution forming the foundation of many applications, there
already exists an extensive body of research regarding its optimization.

Techniques based on local search [13, 21, 22, 6, 24, 10, 28] constitute one
family of graph querying approaches. While they are designed to exploit
locality in the host graph to improve execution time, repeated query execution
leads to redundant computations that are only avoided by fully incremental
techniques.

In [16], Egyed proposes a scoping mechanism for local search to support
incremental query execution, only recomputing query results when a graph
element touched during query execution changes. While this approach offers
some degree of incrementality, it is limited to queries with designated root
elements that serve as an anchor in the host graph and may still result in
redundant computations, since query reevaluation is only controlled at the
granularity of root elements.

A second family of solutions is based on discrimination networks [25, 35, 34,
9], the most prominent example of which are RETE nets.

VIATRA [34] is a mature tool for incremental graph query execution based on
the RETE algorithm [19], which supports advanced concepts for query
specification and optimization not considered in this paper. Notably, VIATRA
allows reuse of matches for isomorphic query subgraphs within a single RETE
net. This is achieved via RETE structures not covered by the rather
restrictive definition of well-formedness used in this paper, which points to
an interesting direction for future work. However, while VIATRA also has a
local search option for query execution, it does not integrate local search
with the incremental query engine but rather offers it as an alternative.

Beyhl [9] presents an incremental querying technique based on a generalized
version of RETE nets, called Generalized Discrimination Networks (GDNs) [25].
The main difference compared to the RETE algorithm is the lack of join nodes.
Instead, more complex nodes that directly compute complex matches using local
search are employed. The approach however represents more of a means of
controlling the trade-off between local search and RETE rather than an
integration and still requires a global computation of matches for the entire
host graph.

In previous work [7], we have made a first step in the direction of localizing
RETE-based query execution. While this earlier technique already allowed
anchoring the execution of a RETE net to certain host graph vertices, this
anchoring was based on typing information and its results did not meet the
definition of completeness introduced in this paper.

Model repositories such as CDO [1] and NeoEMF [14] provide support for query
execution over partial models via lazy loading. As persistence layers, these
solutions however focus on implementing an interface of atomic model access
operations in order to be agnostic regarding the employed query mechanism.

The Mogwaï tool [15] aims to improve query execution over persistence layers
like CDO and NeoEMF by mapping model queries to native queries for the
underlying database system instead of using the atomic model access operations
provided by the layer’s API, avoiding loading the entire model into main
memory. The tool however does not consider incremental query execution.

Jahanbin et al. propose an approach for querying partially loaded models
stored via persistence layers [27] or as XMI files [26]. In contrast to the
solution presented in this paper, their approach still aims to always provide
complete query results for the full model and is thus based on static analysis
and typing information rather than dynamic exploitation of locality.

Query optimization for relational databases is a research topic that has been
under intense study for decades [30, 31, 32]. Generally, many of the
techniques from this field are applicable to RETE nets, which are ultimately
based on relational algebra and related to materialized views in relational
databases [23]. However, relational databases lack the notion of locality
inherent to graph-based encodings and are hence not tailored to exploit local
navigation.

This shortcoming has given rise to a number of graph databases [4], which
employ a graph-based data representation instead of a relational encoding and
form the basis of some model persistance layers like NeoEMF [14]. While these
database systems are designed to accommodate local navigation, to the best of
our knowledge, support for incremental query execution is still lacking.

##  6 Conclusion

In this paper, we have presented a relaxed notion of completeness for query
results that lifts the requirement of strict completeness of results for graph
queries and thereby the need for necessarily global query execution. Based on
this relaxed notion of completeness, we have developed an extension of the
RETE approach that allows local, yet fully incremental execution of graph
queries. An initial evaluation demonstrates that the approach can improve
scalability in scenarios with small relevant subgraphs, but causes an overhead
in unfavorable cases.

In future work, we plan to extend our technique to accommodate advanced
concepts for query specification, most importantly nested graph conditions.
Furthermore, we want to investigate whether the proposed solution can be
adapted to support bulk loading of partial models in order to reduce overhead
caused by lazy loading strategies employed by model persistence layers.

## References

  * [1] Eclipse CDO Model Repository. https://projects.eclipse.org/projects/modeling.emf.cdo, last accessed 5 January 2024
  * [2] EMF: Eclipse Modeling Framework. https://www.eclipse.org/modeling/emf/, last accessed 27 January 2024
  * [3] Localized RETE for Incremental Graph Queries Evaluation Artifacts. https://github.com/hpi-sam/Localized-RETE-for-Incremental-Graph-Queries, last accessed 5 February 2024
  * [4] Angles, R.: A comparison of current graph database models. In: 2012 IEEE 28th International Conference on Data Engineering Workshops. pp. 171–177. IEEE (2012)
  * [5] Angles, R., Antal, J.B., Averbuch, A., Birler, A., Boncz, P., Búr, M., Erling, O., Gubichev, A., Haprian, V., Kaufmann, M., Pey, J.L.L., Martínez, N., Marton, J., Paradies, M., Pham, M.D., Prat-Pérez, A., Püroja, D., Spasić, M., Steer, B.A., Szakállas, D., Szárnyas, G., Waudby, J., Wu, M., Zhang, Y.: The LDBC Social Network Benchmark (2024)
  * [6] Arendt, T., Biermann, E., Jurack, S., Krause, C., Taentzer, G.: Henshin: advanced concepts and tools for in-place EMF model transformations. In: International Conference on Model Driven Engineering Languages and Systems. Springer (2010)
  * [7] Barkowsky, M., Brand, T., Giese, H.: Improving adaptive monitoring with incremental runtime model queries. In: SEAMS 2021. pp. 71–77. IEEE (2021)
  * [8] Barkowsky, M., Giese, H.: Host-graph-sensitive RETE nets for incremental graph pattern matching with nested graph conditions. Journal of Logical and Algebraic Methods in Programming 131, 100841 (2023)
  * [9] Beyhl, T.: A framework for incremental view graph maintenance. Ph.D. thesis, Hasso Plattner Institute at the University of Potsdam (2018)
  * [10] Bi, F., Chang, L., Lin, X., Qin, L., Zhang, W.: Efficient subgraph matching by postponing cartesian products. In: Proceedings of the 2016 International Conference on Management of Data. pp. 1199–1214. ACM (2016)
  * [11] Bruneliere, H., Cabot, J., Jouault, F., Madiot, F.: MoDisco: a generic and extensible framework for model driven reverse engineering. In: Proceedings of the IEEE/ACM international conference on Automated software engineering (2010)
  * [12] Codd, E.F.: A relational model of data for large shared data banks. Communications of the ACM 13(6), 377–387 (1970)
  * [13] Cordella, L.P., Foggia, P., Sansone, C., Vento, M.: A (sub) graph isomorphism algorithm for matching large graphs. IEEE transactions on pattern analysis and machine intelligence 26(10), 1367–1372 (2004)
  * [14] Daniel, G., Sunyé, G., Benelallam, A., Tisi, M., Vernageau, Y., Gómez, A., Cabot, J.: NeoEMF: A Multi-database Model Persistence Framework for Very Large Models. Science of Computer Programming 149, 9–14 (2017)
  * [15] Daniel, G., Sunyé, G., Cabot, J.: Scalable queries and model transformations with the mogwai tool. In: Theory and Practice of Model Transformation: 11th International Conference, ICMT 2018, Held as Part of STAF 2018, Toulouse, France, June 25–26, 2018, Proceedings 11. pp. 175–183. Springer (2018)
  * [16] Egyed, A.: Instant Consistency Checking for the UML. In: Proceedings of the 28th international conference on Software engineering. pp. 381–390 (2006)
  * [17] Ehrig, H., Ehrig, K., Prange, U., Taentzer, G.: Fundamentals of algebraic graph transformation. Springer (2006)
  * [18] Erling, O., Averbuch, A., Larriba-Pey, J., Chafi, H., Gubichev, A., Prat, A., Pham, M.D., Boncz, P.: The LDBC social network benchmark: Interactive workload. In: Proceedings of the 2015 ACM SIGMOD International Conference on Management of Data. pp. 619–630. ACM (2015)
  * [19] Forgy, C.L.: Rete: A fast algorithm for the many pattern/many object pattern match problem. In: Readings in Artificial Intelligence and Databases, pp. 547–559. Elsevier (1989)
  * [20] Gamma, E., Helm, R., Johnson, R., Vlissides, J.: Design patterns: Abstraction and reuse of object-oriented design. In: ECOOP’93—Object-Oriented Programming: 7th European Conference Kaiserslautern, Germany, July 26–30, 1993 Proceedings 7. pp. 406–431. Springer (1993)
  * [21] Geiß, R., Batz, G.V., Grund, D., Hack, S., Szalkowski, A.: GrGen: A fast SPO-based graph rewriting tool. In: International Conference on Graph Transformation. pp. 383–397. Springer (2006)
  * [22] Giese, H., Hildebrandt, S., Seibel, A.: Improved Flexibility and Scalability by Interpreting Story Diagrams. Electronic Communications of the EASST 18 (2009)
  * [23] Gupta, A., Mumick, I.S., et al.: Maintenance of materialized views: Problems, techniques, and applications. IEEE Data Eng. Bull. 18(2), 3–18 (1995)
  * [24] Han, W.S., Lee, J., Lee, J.H.: Turboiso: towards ultrafast and robust subgraph isomorphism search in large graph databases. In: Proceedings of the 2013 ACM SIGMOD International Conference on Management of Data. pp. 337–348 (2013)
  * [25] Hanson, E.N., Bodagala, S., Chadaga, U.: Trigger condition testing and view maintenance using optimized discrimination networks. IEEE Transactions on Knowledge and Data Engineering 14(2), 261–280 (2002)
  * [26] Jahanbin, S., Kolovos, D., Gerasimou, S.: Towards memory-efficient validation of large xmi models. In: 2023 ACM/IEEE International Conference on Model Driven Engineering Languages and Systems Companion (MODELS-C). pp. 241–250. IEEE (2023)
  * [27] Jahanbin, S., Kolovos, D., Gerasimou, S., Sunyé, G.: Partial loading of repository-based models through static analysis. In: Proceedings of the 15th ACM SIGPLAN International Conference on Software Language Engineering. pp. 266–278 (2022)
  * [28] Jüttner, A., Madarasi, P.: VF2++—An improved subgraph isomorphism algorithm. Discrete Applied Mathematics 242, 69–81 (2018)
  * [29] Kent, S.: Model driven engineering. In: International conference on integrated formal methods. pp. 286–298. Springer (2002)
  * [30] Krishnamurthy, R., Boral, H., Zaniolo, C.: Optimization of nonrecursive queries. In: VLDB. vol. 86, pp. 128–137 (1986)
  * [31] Lee, C., Shih, C.S., Chen, Y.H.: Optimizing large join queries using a graph-based approach. IEEE Transactions on Knowledge and Data Engineering 13(2), 298–315 (2001)
  * [32] Leis, V., Gubichev, A., Mirchev, A., Boncz, P., Kemper, A., Neumann, T.: How good are query optimizers, really? Proceedings of the VLDB Endowment 9(3), 204–215 (2015)
  * [33] Szárnyas, G., Izsó, B., Ráth, I., Varró, D.: The Train Benchmark: cross-technology performance evaluation of continuous model queries. Software & Systems Modeling 17, 1365–1393 (2018)
  * [34] Varró, D., Bergmann, G., Hegedüs, Á., Horváth, Á., Ráth, I., Ujhelyi, Z.: Road to a reactive and incremental model transformation platform: three generations of the VIATRA framework. Software & Systems Modeling 15(3), 609–629 (2016)
  * [35] Varró, G., Deckwerth, F.: A Rete Network Construction Algorithm for Incremental Pattern Matching. In: International Conference on Theory and Practice of Model Transformations. pp. 125–140. Springer (2013)

##  Appendix 0.A Localized RETE Example Execution

Abstracting from the internal structure of local navigation structures and
request projection structures, the $order$ procedure would produce the
execution order $RPS^{c}_{r}$, $LNS^{p\rightarrow c}$, $RPS^{c}_{l}$,
$LNS^{c\rightarrow f}$, $RPS^{c}_{r}$, $LNS^{p\rightarrow c}$,
$[\bowtie]^{\Phi}$ for the example localized RETE net in Figure 2 (right). An
execution of this sequence, which is visualized in Figure 8, would then
proceed as follows:

  1. a.

The starting configuration for the RETE net may be inconsistent for all of the
net’s nodes, for instance due to being empty (if this is the net’s initial
execution), because of unprocessed host graph changes (if this is a repeated
execution after incremental host graph changes), or because the provided
starting configuration is simply erroneous.

  2. b.

The execution of $RPS^{c}_{r}$ in the first step (indicated by a bold border
and label in Figure 8(a)), which is only necessary to handle an erroneous
starting configuration, then guarantees a consistent configuration for all
nodes in $RPS^{c}_{r}$ by effectively correcting any errors. This is indicated
by the label being underlined in Figure 8(b).

  3. c.

After the execution of $LNS^{p\rightarrow c}$ in the second step, the
resulting configuration is also consistent for all nodes in $LNS^{p\rightarrow
c}$, since $LNS^{p\rightarrow c}$ is a tree and can thus simply be executed
via a reverse topological sorting. Essentially, this step either initially
populates the empty current result sets of the nodes in $LNS^{p\rightarrow c}$
in case of an empty starting configuration or handles any relevant changes to
host graph or relevant subgraph. In this context, a relevant change can either
be the creation or deletion of an edge of type $ce$ or the inclusion or
exclusion of a vertex to or from the relevant subgraph. Ultimately, the
current result set of the union node at the top of $LNS^{p\rightarrow c}$ then
contains at least all edges of type $ce$ that are adjacent to a vertex in the
relevant subgraph, with these matches marked $\infty$.

  4. d.

The execution of $RPS^{c}_{l}$ in the third step ensures consistency for all
nodes in $RPS^{c}_{l}$. Essentially, each host graph vertex to which the query
graph vertex $c$ is mapped in at least one match with marking $\phi>1$ in the
root of $LNS^{p\rightarrow c}$ is added to the result set of the root of
$RPS^{c}_{l}$ and assigned a marking of $1$ (the height of the original, well-
formed RETE net in Figure 1 (right)).

  5. e.

Executing $LNS^{c\rightarrow f}$ in the fourth step now not only guarantees
that all edges of type $fe$ that touch the relevant subgraph are included in
the result set of the root of $LNS^{c\rightarrow f}$ with a marking of
$\infty$. In addition, because of the dependency of $LNS^{c\rightarrow f}$ on
$RPS^{c}_{l}$, the execution also ensures the same for $fe$ edges adjacent to
a host graph vertex in the image of a match for the root of $RPS^{c}_{l}$ and
thus $LNS^{p\rightarrow c}$, if the marking of that match is greater than $1$.
These matches are however only marked $1$, signalling that they were only
computed on request from $LNS^{p\rightarrow c}$. Intuitively, this guarantees
that the current result set for the root of $LNS^{c\rightarrow f}$ also
contains all matches that are required to complement matches in
$LNS^{p\rightarrow c}$ that involve a host graph vertex in the relevant
subgraph. Because $RPS^{c}_{r}$ depends on $LNS^{c\rightarrow f}$,
$RPS^{c}_{r}$ may now be inconsistent again.

  6. f.

The execution of $RPS^{c}_{r}$ restores consistency for $RPS^{c}_{r}$ by
adding all matches for $LNS^{c\rightarrow f}$ that are marked $\infty$, that
is, involve a vertex from the relevant subgraph, to the root node of
$RPS^{c}_{r}$. These matches are marked $1$. Notably, due to the marking
filter node in $RPS^{c}_{r}$, matches that are only marked $1$ in the current
result set of $LNS^{c\rightarrow f}$ are not considered.

  7. g.

Executing $LNS^{p\rightarrow c}$ now also adds all edges of type $ce$ required
to complement matches for $LNS^{c\rightarrow f}$ that touch the relevant
subgraph to the result set of $LNS^{p\rightarrow c}$. Again, these matches are
only marked $1$. The dependency of $RPS^{c}_{l}$ on $LNS^{p\rightarrow c}$
could now mean that $RPS^{c}_{l}$ may be inconsistent again. However, the last
execution of $LNS^{p\rightarrow c}$ can only have created (or potentially
deleted) matches with marking $1$. The reason for this is that the only
changes that were processed during the last execution of $LNS^{p\rightarrow
c}$ were changes to the result set of $RPS^{c}_{r}$, which only contains
matches marked $1$ due to the marking assignment node in the request
projection structure. Due to the marking filter node at the bottom of
$RPS^{c}_{l}$, these changes do not affect the consistency of any node in
$RPS^{c}_{l}$, meaning that $RPS^{c}_{l}$ is still consistent despite the
dependency.

  8. h.

Finally, the execution of $[\bowtie]^{\Phi}$ ensures the consistency of the
last remaining RETE node. According to Corollary 1, the result set of
$[\bowtie]^{\Phi}$ is now complete under the relevant subgraph. Intuitively,
this can be explained by the fact that the result set of $LNS^{p\rightarrow
c}$ contains all edges of type $ce$ that touch the relevant subgraph,
$LNS^{c\rightarrow f}$ contains all matches required to complement these
edges, and vice-versa.

$\bowtie$$\Phi$$LNS^{p\rightarrow c}$$LNS^{c\rightarrow
f}$$\mathbf{RPS^{c}_{r}}$$RPS^{c}_{l}$ (a)

$\bowtie$$\Phi$$\mathbf{LNS^{p\rightarrow c}}$$LNS^{c\rightarrow
f}$$RPS^{c}_{r}$$RPS^{c}_{l}$ (b)

$\bowtie$$\Phi$$LNS^{p\rightarrow c}$$LNS^{c\rightarrow
f}$$RPS^{c}_{r}$$\mathbf{RPS^{c}_{l}}$ (c)

$\bowtie$$\Phi$$LNS^{p\rightarrow c}$$\mathbf{LNS^{c\rightarrow
f}}$$RPS^{c}_{r}$$RPS^{c}_{l}$ (d)

$\bowtie$$\Phi$$LNS^{p\rightarrow c}$$LNS^{c\rightarrow
f}$$\mathbf{RPS^{c}_{r}}$$RPS^{c}_{l}$ (e)

$\bowtie$$\Phi$$\mathbf{LNS^{p\rightarrow c}}$$LNS^{c\rightarrow
f}$$RPS^{c}_{r}$$RPS^{c}_{l}$ (f)

$\mathbf{\bowtie}$$\Phi$$LNS^{p\rightarrow c}$$LNS^{c\rightarrow
f}$$RPS^{c}_{r}$$RPS^{c}_{l}$ (g)

${\bowtie}$$\Phi$$LNS^{p\rightarrow c}$$LNS^{c\rightarrow
f}$$RPS^{c}_{r}$$RPS^{c}_{l}$ (h)

Figure 8: Example execution of the RETE net from Figure 2 (right)

##  Appendix 0.B Additional Measurements

###  0.B.1 Synthetic Abstract Syntax Graphs (CDO)

Figure 9: Measurements for the synthetic abstract syntax graph scenario, with
models stored via CDO (log scale)

###  0.B.2 Real Abstract Syntax Graphs

Figure 10: Execution times for the real abstract syntax graph scenario Figure
11: Execution times for the real abstract syntax graph scenario Figure 12:
Memory measurements for the real abstract syntax graph scenario Figure 13:
Memory measurements for the real abstract syntax graph scenario

###  0.B.3 LDBC Social Network Benchmark

Figure 14: Execution times for the LDBC scenario. For INTERACTIVE_6 and
INTERACTIVE_9, VIATRA aborted with an exception presumably indicating too high
memory consumption. For INTERACTIVE_3, all strategies ran out of memory.
Figure 15: Execution times for the LDBC scenario. For INTERACTIVE_3, all
strategies ran out of memory. Figure 16: Memory measurements for the LDBC
scenario. For INTERACTIVE_6 and INTERACTIVE_9, VIATRA aborted with an
exception presumably indicating too high memory consumption. For
INTERACTIVE_3, all strategies ran out of memory. Figure 17: Memory
measurements for the LDBC scenario. For INTERACTIVE_3, all strategies ran out
of memory.

##  Appendix 0.C Queries

###  0.C.1 Synthetic Abstract Syntax Graphs Queries

Figure 18: Simple path query for the synthetic abstract syntax graph scenario

###  0.C.2 Real Abstract Syntax Graphs Queries

Figure 19: Composite query for the real abstract syntax graph scenario Figure
20: Observer query for the real abstract syntax graph scenario Figure 21:
Singleton query for the real abstract syntax graph scenario Figure 22:
Strategy query for the real abstract syntax graph scenario

###  0.C.3 LDBC Social Network Benchmark Queries

Figure 23: Query “Interactive 1” for the LDBC scenario Figure 24: Query
“Interactive 2” for the LDBC scenario Figure 25: Query “Interactive 3” for the
LDBC scenario Figure 26: Query “Interactive 4” for the LDBC scenario Figure
27: Query “Interactive 5” for the LDBC scenario Figure 28: Query “Interactive
6” for the LDBC scenario Figure 29: Query “Interactive 7” for the LDBC
scenario Figure 30: Query “Interactive 8” for the LDBC scenario Figure 31:
Query “Interactive 9” for the LDBC scenario Figure 32: Query “Interactive 10”
for the LDBC scenario Figure 33: Query “Interactive 11” for the LDBC scenario
Figure 34: Query “Interactive 12” for the LDBC scenario

##  Appendix 0.D Technical Details

###  0.D.1 Additional Definitions

####  0.D.1.1 Fully Complete Query Results

###### Definition 2

_Completeness of Query Results_ We say that a set of matches $M$ from query
graph $Q$ into host graph $H$ is complete iff $M=\mathcal{M}^{Q}_{H}$.

####  0.D.1.2 Target Result Sets of Marking-Sensitive RETE Nodes

Let $H$ be a host graph, $H_{p}\subseteq H$ the relevant subgraph,
$(N^{\Phi},p^{\Phi})$ the containing marking-sensitive RETE net, and
$\mathcal{C}^{\Phi}$ a configuration for $(N^{\Phi},p^{\Phi})$. In order to
allow targeted processing of markings and local navigation in the model, we
introduce several types of marking-sensitive RETE nodes with the following
target result set functions:

  * •

The target result set of a _marking-sensitive join node_ $[\bowtie]^{\Phi}$
with marking-sensitive dependencies $n^{\Phi}_{l}$ and $n^{\Phi}_{r}$ with
associated subgraphs $Q_{l}$ and $Q_{r}$ such that
$V^{Q_{\cap}}\neq\emptyset$, where $Q_{\cap}=Q_{l}\cap Q_{r}$, is given by
$\mathcal{R}^{\Phi}([\bowtie]^{\Phi},N^{\Phi},H,H_{p},\mathcal{C}^{\Phi})=\\{(m_{l}\cup
m_{r},max(\phi_{l},\phi_{r}))|(m_{l},\phi_{l})\in\mathcal{C}^{\Phi}(n^{\Phi}_{l})\wedge(m_{r},\phi_{r})\in\mathcal{C}^{\Phi}(n^{\Phi}_{r})\wedge
m_{l}|_{Q_{\cap}}=m_{r}|_{Q_{\cap}}\\}$.

  * •

The target result set of a _marking-sensitive union node_ $[\cup]^{\Phi}$ with
a set of marking-sensitive dependencies $N^{\Phi}_{\alpha}$ with common
associated query subgraph $Q_{\alpha}$ is given by
$\mathcal{R}^{\Phi}([\cup]^{\Phi},N^{\Phi},H,H_{p},\mathcal{C}^{\Phi})=\\{(m,\phi_{max}))|(m,\phi_{max})\in\bigcup_{n_{\alpha}\in
N^{\Phi}_{\alpha}}\mathcal{C}^{\Phi}(n^{\Phi}_{\alpha})\wedge\phi_{max}=max(\\{\phi^{\prime}|(m,\phi^{\prime})\in\bigcup_{n_{\alpha}\in
N^{\Phi}_{\alpha}}\mathcal{C}^{\Phi}(n^{\Phi}_{\alpha})\\})\\}$.

  * •

The target result set of a _marking-sensitive projection node_
$[\pi_{Q}]^{\Phi}$ with marking-sensitive dependency $n^{\Phi}_{\alpha}$ and
associated query subgraph $Q$ is given by
$\mathcal{R}^{\Phi}([\pi_{Q}]^{\Phi},N^{\Phi},H,H_{p},\mathcal{C}^{\Phi})=\\{(m|_{Q},\phi_{max}))|(m,\phi_{max})\in\mathcal{C}^{\Phi}(n^{\Phi}_{\alpha})\wedge\phi_{max}=max(\\{\phi^{\prime}|(m^{\prime},\phi^{\prime})\in\mathcal{C}^{\Phi}(n^{\Phi}_{\alpha})\wedge
m^{\prime}|_{Q}=m|_{Q}\\})\\}$.

  * •

The target result set of a _marking assignment node_ $[\phi:=x]^{\Phi}$ with
marking-sensitive dependency node $n^{\Phi}_{\alpha}$ is given by
$\mathcal{R}^{\Phi}([\phi:=x]^{\Phi},N^{\Phi},H,H_{p},\mathcal{C}^{\Phi})=\\{(m,x)|(m,\phi)\in\mathcal{C}^{\Phi}(n^{\Phi}_{\alpha})\\}$.

  * •

The target result set of a _marking filter node_ $[\phi>x]^{\Phi}$ with
marking-sensitive dependency $n^{\Phi}_{\alpha}$ is given by
$\mathcal{R}^{\Phi}([\phi>x]^{\Phi},N^{\Phi},H,H_{p},\mathcal{C}^{\Phi})=\\{(m,\phi)|(m,\phi)\in\mathcal{C}^{\Phi}(n^{\Phi}_{\alpha})\wedge\phi>x\\}$.

  * •

The target result set of a _forward navigation node_
$[v\rightarrow_{n}w]^{\Phi}$ with associated subgraph
$Q=(\\{v,w\\},\\{e\\},\\{(e,v)\\},\\{(e,w)\\})$ and marking-sensitive
dependency $n^{\Phi}_{v}$ with associated subgraph
$Q_{v}=(\\{v\\},\emptyset,\emptyset,\emptyset)$ is given by
$\mathcal{R}^{\Phi}([v\rightarrow_{n}w]^{\Phi},N^{\Phi},H,H_{p},\mathcal{C}^{\Phi})=\\{(m,\phi_{max})|m\in\mathcal{M}^{Q}_{H}\wedge\exists(m_{v},\phi_{max})\in\mathcal{C}^{\Phi}(n^{\Phi}_{v}):m_{v}=m|_{Q_{v}}\wedge\phi_{max}=max(\\{\phi^{\prime}|(m_{v}^{\prime},\phi^{\prime})\in\mathcal{C}^{\Phi}(n^{\Phi}_{v})\wedge
m_{v}^{\prime}=m|_{Q_{v}}\\})\\}\\}$.

  * •

The target result set of a _backward navigation node_
$[w\leftarrow_{n}v]^{\Phi}$ with associated subgraph
$Q=(\\{v,w\\},\\{e\\},\\{(e,v)\\},\\{(e,w)\\})$ and marking-sensitive
dependency $n^{\Phi}_{w}$ with associated subgraph
$Q_{w}=(\\{w\\},\emptyset,\emptyset,\emptyset)$ is given by
$\mathcal{R}^{\Phi}([w\leftarrow_{n}v]^{\Phi},N^{\Phi},H,H_{p},\mathcal{C}^{\Phi})=\\{(m,\phi_{max})|m\in\mathcal{M}^{Q}_{H}\wedge\exists(m_{w},\phi_{max})\in\mathcal{C}^{\Phi}(n^{\Phi}_{w}):m_{w}=m|_{Q_{w}}\wedge\phi_{max}=max(\\{\phi^{\prime}|(m_{w}^{\prime},\phi^{\prime})\in\mathcal{C}^{\Phi}(n^{\Phi}_{w})\wedge
m_{w}^{\prime}=m|_{Q_{w}}\\})\\}\\}$.

  * •

The target result set of a _marking-sensitive vertex input node_ $[v]^{\Phi}$
with associated subgraph $Q=(\\{v\\},\emptyset,\emptyset,\emptyset)$ is given
by
$\mathcal{R}^{\Phi}([v]^{\Phi},N^{\Phi},H,H_{p},\mathcal{C}^{\Phi})=\\{(m,\infty)|m\in\mathcal{M}^{Q}_{H_{p}}\\}$.

####  0.D.1.3 Extension Points of Localized RETE Nets

Given a local navigation structure $LNS(p)$ containing the marking-sensitive
vertex input nodes $[v]^{\Phi}$ and $[w]^{\Phi}$, we call
$\chi(LNS(p))=\\{[\cup]^{\Phi}_{v},[\cup]^{\Phi}_{w}\\}$ the _extension
points_ of $LNS(p)$.

Let $(N,p)$ be a well-formed RETE net with $p$ a join node. For the localized
RETE net $(N^{\Phi},p^{\Phi})=localize((N,p))$ with
$N^{\Phi}=N^{\Phi}_{\bowtie}\cup N^{\Phi}_{l}\cup N^{\Phi}_{r}\cup RPS_{l}\cup
RPS_{r}$, the extension points of $N^{\Phi}$ are given by
$\chi(N^{\Phi})=\chi(N^{\Phi}_{l})\cup\chi(N^{\Phi}_{r})$.

###  0.D.2 Theorems, Lemmata, and Proofs

####  0.D.2.1 Localized RETE Result Completeness

###### Theorem 0.D.1

Let $H$ be a graph, $H_{p}\subseteq H$, $(N,p)$ a well-formed RETE net, and
$Q$ the query graph associated with $p$. Furthermore, let $\mathcal{C}^{\Phi}$
be a consistent configuration for the localized RETE net
$(N^{\Phi},p^{\Phi})=localize((N,p))$. The set of matches from $Q$ into $H$
given by the stripped result set
$\mathcal{R}^{\Phi}_{X}(p^{\Phi},\mathcal{C}^{\Phi})$ is then complete under
$H_{p}$.

###### Proof

As a consequence of the definition of well-formed RETE nets, for each edge
$e\in E^{Q}$, there must be an edge input node in the RETE net $(N,p)$. By
construction of $(N^{\Phi},p^{\Phi})$, there must then be a local navigation
structure in $N^{\Phi}$ for each such edge input node. By the definition of
well-formed RETE nets, we furthermore know that each query graph vertex $v\in
V^{Q}$ must have at least one adjacent edge.

Consequently, for each query graph vertex $v\in V^{Q}$, there must be a local
navigation structure in $N^{\Phi}$ that contains a marking-sensitive vertex
input node $[v]^{\Phi}$ that is associated with the query subgraph
$Q_{v}=(\\{v\\},\emptyset,\emptyset,\emptyset)$. By construction, $[v]^{\Phi}$
then is a dependendency of a marking-sensitive union node $[\cup]^{\Phi}_{v}$
that is also associated with the query subgraph $Q_{v}$ and is an extension
point of the local navigation structure and thus of $N^{\Phi}$.

Since $\mathcal{C}^{\Phi}$ is consistent, by the semantics of the marking-
sensitive vertex input node, it follows that $\forall
m_{v}\in\mathcal{M}^{Q_{v}}_{H}:m_{v}(v)\in
V^{H_{p}}\Rightarrow(m_{v},\infty)\in C([v]^{\Phi})$. By the semantics of the
marking-sensitive union node, it must then also hold that $\forall
m_{v}\in\mathcal{M}^{Q_{v}}_{H}:m_{v}(v)\in
V^{H_{p}}\Rightarrow(m_{v},\infty)\in C([\cup]^{\Phi}_{v})$.

For any such match $m_{v}\in\mathcal{M}^{Q_{v}}_{H}$ with $m_{v}(v)\in H_{p}$,
from Lemma 1, it then follows that $\forall
m\in\mathcal{M}^{Q}_{H}:m(v)=m_{v}(v)\Rightarrow(m,\infty)\in\mathcal{C}^{\Phi}(p^{\Phi})$.
Because $Q_{v}\subseteq Q$ and thus $\forall m\in\mathcal{M}^{Q}_{H}:m(v)\in
V^{H_{p}}\Rightarrow\exists m_{v}\in\mathcal{M}^{Q_{v}}_{H}:m_{v}(v)\in
V^{H_{p}}$, it must thereby hold that $\forall m\in\mathcal{M}^{Q}_{H}:m(v)\in
V^{H_{p}}\Rightarrow(m,\infty)\in\mathcal{C}^{\Phi}(p^{\Phi})$.

Since this is the case for all $v\in V^{Q}$, it follows that $\forall
m\in\mathcal{M}^{Q}_{H}:(\exists v\in V^{Q}:m(v)\in
V^{H_{p}})\Rightarrow(m,\infty)\in\mathcal{C}^{\Phi}(p^{\Phi})$.

Thus, it finally follows that $\forall m\in\mathcal{M}^{Q}_{H}:(\exists v\in
V^{Q}:m(v)\in V^{H_{p}})\Rightarrow
m\in\mathcal{R}^{\Phi}_{X}(p^{\Phi},\mathcal{C}^{\Phi})$. Hence,
$\mathcal{R}^{\Phi}_{X}(p^{\Phi},\mathcal{C}^{\Phi})$ is complete under
$H_{p}$.

####  0.D.2.2 Localized RETE Execution Order Consistency

###### Theorem 0.D.2

Let $H$ be a graph, $H_{p}\subseteq H$, $(N,p)$ a well-formed RETE net, and
$\mathcal{C}^{\Phi}_{0}$ an arbitrary starting configuration. Executing the
marking-sensitive RETE net $(N^{\Phi},p^{\Phi})=localize((N,p))$ via
$O=order((N^{\Phi},p^{\Phi}))$ then yields a consistent configuration
$\mathcal{C}^{\Phi}=execute(O,N^{\Phi},H,H_{p},\mathcal{C}^{\Phi}_{0})$.

###### Proof

Follows directly from Lemma 13.

####  0.D.2.3 Localized RETE Execution Correctness

###### Corollary 3

Let $H$ be a graph, $H_{p}\subseteq H$, $(N,p)$ a well-formed RETE net, and
$Q$ the query graph associated with $p$. Furthermore, let
$\mathcal{C}^{\Phi}_{0}$ be an arbitrary starting configuration for the
localized RETE net $(N^{\Phi},p^{\Phi})=localize((N,p))$ and
$\mathcal{C}^{\Phi}=execute(order((N^{\Phi},p^{\Phi})),N^{\Phi},H,H_{p},\mathcal{C}^{\Phi}_{0})$.
The set of matches from $Q$ into $H$ given by
$\mathcal{R}^{\Phi}_{X}(p^{\Phi},\mathcal{C}^{\Phi})$ is then complete under
$H_{p}$.

###### Proof

Follows directly from Theorem 3.1 and Theorem 3.2.

####  0.D.2.4 Localized RETE Configuration Size

###### Theorem 0.D.3

Let $H$ be an edge-dominated graph, $H_{p}\subseteq H$, $(N,p)$ a well-formed
RETE net with $Q$ the associated query graph of $p$, $\mathcal{C}$ a
consistent configuration for $(N,p)$ for host graph $H$, and
$\mathcal{C}^{\Phi}$ a consistent configuration for the localized RETE net
$(N^{\Phi},p^{\Phi})=localize((N,p))$ for host graph $H$ and relevant subgraph
$H_{p}$. It then holds that $\sum_{n^{\Phi}\in
V^{N^{\Phi}}}\sum_{(m,\phi)\in\mathcal{C}(n^{\Phi})}|m|\leq
7\cdot|\mathcal{C}|_{e}$.

###### Proof

For each edge input node $[v\rightarrow w]$ in $N$ with associated query
subgraph $Q_{e}$, $N^{\Phi}$ contains the seven nodes of the corresponding
local navigation structure $LNS([v\rightarrow w])$: $[v]^{\Phi}$,
$[w]^{\Phi}$, $[\cup]^{\Phi}_{v}$, $[\cup]^{\Phi}_{w}$,
$[v\rightarrow_{n}w]^{\Phi}$, $[w\leftarrow_{n}v]^{\Phi}$, and
$[\cup]^{\Phi}$. By the semantics of $[v\rightarrow w]$, it must hold that
$\mathcal{C}([v\rightarrow w])=\mathcal{M}^{Q_{e}}_{H}$.

By the semantics of the forward and backward local navigation nodes, we know
that
$\mathcal{R}^{\Phi}_{X}([v\rightarrow_{n}w]^{\Phi},\mathcal{C}^{\Phi})\subseteq\mathcal{M}^{Q_{e}}_{H}$
and
$\mathcal{R}^{\Phi}_{X}([w\leftarrow_{n}v]^{\Phi},\mathcal{C}^{\Phi})\subseteq\mathcal{M}^{Q_{e}}_{H}$
and thus, by the semantics of the marking sensitive union node,
$\mathcal{R}^{\Phi}_{X}([\cup]^{\Phi},\mathcal{C}^{\Phi})\subseteq\mathcal{M}^{Q_{e}}_{H}$.

Furthermore, by the semantics of the marking sensitive input nodes, it must
hold that
$\mathcal{R}^{\Phi}_{X}([v]^{\Phi},\mathcal{C}^{\Phi})\subseteq\mathcal{M}^{Q_{v}}_{H}$
and
$\mathcal{R}^{\Phi}_{X}([w]^{\Phi},\mathcal{C}^{\Phi})\subseteq\mathcal{M}^{Q_{w}}_{H}$,
where $Q_{v}$ and $Q_{w}$ are the query subgraphs associated with $v$
respectively $w$. By the semantics of the marking sensitive union nodes and
the assumption regarding the common query subgraph associated with their
dependencies, it must also hold that
$\mathcal{R}^{\Phi}_{X}([\cup]_{v}^{\Phi},\mathcal{C}^{\Phi})\subseteq\mathcal{M}^{Q_{v}}_{H}$
and
$\mathcal{R}^{\Phi}_{X}([\cup]_{w}^{\Phi},\mathcal{C}^{\Phi})\subseteq\mathcal{M}^{Q_{w}}_{H}$.

By the semantics of the involved marking-sensitive RETE nodes, for each node
in $LNS([n_{1}\rightarrow n_{2}])$, each match can only be associated with at
most one marking in the node’s current result set in $\mathcal{C}^{\Phi}$.
Furthermore, by assumption, it holds that
$\mathcal{M}^{Q_{v}}_{H}\leq\mathcal{M}^{Q_{e}}_{H}$ and
$\mathcal{M}^{Q_{w}}_{H}\leq\mathcal{M}^{Q_{e}}_{H}$. Lastly, we know that
$|Q_{v}|=|Q_{w}|\leq|Q_{e}|$.

It thus holds that $\sum_{n^{\Phi}\in V^{LNS([v\rightarrow
w])}}\sum_{(m,\phi)\in\mathcal{C}(n^{\Phi})}|m|\leq
7\cdot\sum_{m\in\mathcal{C}([v\rightarrow w])}|m|$.

For each join node $[\bowtie]$ in $N$ with associated query subgraph
$Q_{\bowtie}$ and dependencies $n_{l}$ and $n_{r}$, $N^{\Phi}$ contains the
corresponding marking-sensitive join node $[\bowtie]^{\Phi}$ with dependencies
$n^{\Phi}_{l}$ and $n^{\Phi}_{r}$ corresponding to $n_{l}$ respectively
$n_{r}$, as well as the six nodes from the related request projection
structures: $[\phi>h]^{\Phi}_{l}$, $[\pi_{Q_{v}}]^{\Phi}_{l}$,
$[\phi>h]^{\Phi}_{l}$, $[\phi>h]^{\Phi}_{r}$, $[\pi_{Q_{v}}]^{\Phi}_{r}$, and
$[\phi>h]^{\Phi}_{r}$.

By the semantics of join and marking sensitive join, we know that
$\mathcal{C}(n_{l})\subseteq\mathcal{R}^{\Phi}_{X}(n^{\Phi}_{l},\mathcal{C}^{\Phi})\wedge\mathcal{C}(n_{r})\subseteq\mathcal{R}^{\Phi}_{X}(n^{\Phi}_{r},\mathcal{C}^{\Phi})\Rightarrow\mathcal{C}([\bowtie])\subseteq\mathcal{R}^{\Phi}_{X}([\bowtie]^{\Phi},\mathcal{C}^{\Phi})$.
For every edge input node $[v\rightarrow w]$ in $N$, we know that
$\mathcal{C}([v\rightarrow
w])\subseteq\mathcal{R}^{\Phi}_{X}([\cup]^{\Phi},\mathcal{C}^{\Phi})$, where
$[\cup]^{\Phi}$ is the root node of $LNS([v\rightarrow w])$. It is easy to see
that thereby, it must hold that
$\mathcal{C}([\bowtie])\subseteq\mathcal{R}^{\Phi}_{X}([\bowtie]^{\Phi},\mathcal{C}^{\Phi})$.
By Lemma 12, it follows that
$\sum_{(m,\phi)\in\mathcal{C}([\bowtie]^{\Phi})}|m|\leq\sum_{m\in\mathcal{C}([\bowtie])}|m|$.

All nodes in
$RPS_{\bowtie}=\\{[\phi>h]^{\Phi}_{l},[\pi_{Q_{v}}]^{\Phi}_{l},[\phi>h]^{\Phi}_{l},[\phi>h]^{\Phi}_{r},[\pi_{Q_{v}}]^{\Phi}_{r},[\phi>h]^{\Phi}_{r}\\}$
have the same associated query subgraph $Q_{v}\subseteq Q_{\bowtie}$. Thus, we
know that for any pair of matches
$m_{v}\in\mathcal{R}^{\Phi}_{X}(n^{\Phi}_{v},\mathcal{C}^{\Phi})$ and
$m_{\bowtie}\in\mathcal{C}([\bowtie])$, with $n^{\Phi}_{v}\in RPS_{\bowtie}$,
it must hold that $|m_{v}|\leq|m_{\bowtie}|$. Furthermore, by the semantics of
the marking filter, marking-sensitive projection and marking assignment nodes,
we know that for all $n^{\Phi}_{v}\in RPS_{\bowtie}$, it holds that
$|\mathcal{C}^{\Phi}((n^{\Phi}_{v})|\leq|\mathcal{C}^{\Phi}([\bowtie]^{\Phi})|\leq|\mathcal{C}([\bowtie])|$.
It thus follows for all six $n^{\Phi}_{v}\in RPS_{\bowtie}$ that
$\sum_{(m,\phi)\in\mathcal{C}(n^{\Phi}_{v})}|m|\leq\sum_{m\in\mathcal{C}([\bowtie])}|m|$.
Hence, it must hold that $\sum_{n^{\Phi}_{\bowtie}\in
RPS_{\bowtie}\cup\\{[\bowtie]^{\Phi}\\}}\sum_{(m,\phi)\in\mathcal{C}(n^{\Phi}_{\bowtie})}|m|\leq
7\cdot\sum_{m\in\mathcal{C}([\bowtie])}|m|$.

Since $N^{\Phi}$ only consists of the local navigation structures
corresponding to edge input nodes in $N$ and marking-sensitive joins
corresponding to joins in $N$ along with the accordingly constructed request
projection structures, it follows that $\sum_{n^{\Phi}\in
V^{N^{\Phi}}}\sum_{(m,\phi)\in\mathcal{C}(n^{\Phi})}|m|\leq
7\cdot|\mathcal{C}|$.

####  0.D.2.5 Localized RETE Memory Consumption

###### Corollary 4

Let $H$ be an edge-dominated graph, $H_{p}\subseteq H$, $(N,p)$ a well-formed
RETE net, $\mathcal{C}$ a consistent configuration for $(N,p)$ for host graph
$H$, and $\mathcal{C}^{\Phi}$ a consistent configuration for the localized
RETE net $(N^{\Phi},p^{\Phi})=localize((N,p))$ for host graph $H$ and relevant
subgraph $H_{p}$. Assuming that storing a match $m$ requires an amount of
memory in $O(|m|)$ and storing an element from $\overline{\mathbb{N}}$
requires an amount of memory in $O(1)$, storing $\mathcal{C}^{\Phi}$ requires
memory in $O(|\mathcal{C}|_{e})$.

###### Proof

Follows directly from Theorem 3.3 and the fact that no node in a well-formed
or localized RETE net is associated with an empty query subgraph, and a
consistent configuration for either kind of RETE net thus contains no empty
matches.

####  0.D.2.6 Standard RETE Time Complexity

###### Theorem 0.D.4

Let $H$ be a graph, $(N,p)$ a well-formed RETE net for query graph $Q$, and
$\mathcal{C}_{0}$ the empty configuration for $(N,p)$. Executing $(N,p)$ via a
reverse topological sorting
$\mathcal{C}_{1}=execute(toposort^{-1}(N),N,H,\mathcal{C}_{0})$ then takes
$O(|\mathcal{C}_{1}|)$ steps.

###### Proof

Given a suitable representation of $H$ that allows efficient retrieval of
matching edges, an edge input node $n_{e}\in V^{N}$ can be executed by
enumerating the matching edges, creating the corresponding trivial matches,
and adding them to $\mathcal{C}_{0}(n_{e})$. Assuming indexing structures that
allow insertion times linear in the size of the inserted match, this takes
effort in $O(S)$, where $S=\sum_{m\in\mathcal{C}_{1}(n_{e})}|m|$.

A join node $n_{\bowtie}\in V^{N}$ with dependencies $n_{l}$ and $n_{r}$ can
be executed for configuration $\mathcal{C}_{0.x}$ by enumerating the matches
from $\mathcal{C}_{0.x}(n_{l})$, retrieving the complementary matches from
$\mathcal{C}_{0.x}(n_{r})$, constructing the corresponding matches for
$n_{\bowtie}$ and adding them to $\mathcal{C}_{0}(n_{\bowtie})$. Notably, each
enumerated combination of a match from $\mathcal{C}_{0.x}(n_{l})$ and a
complementary match from $\mathcal{C}_{0.x}(n_{r})$ results in a distinct
match for $n_{\bowtie}$. Thus, assuming ideal indexing structures that allow
match enumeration in time linear in the number of matches, retrieval of
complementary matches in time linear in the size of the opposite match, and
insertion times linear in the size of the inserted match, execution of
$n_{\bowtie}$ takes effort in $O(S_{l}+S_{\bowtie})$, where
$S_{l}=\sum_{m_{l}\in\mathcal{C}_{0.x}(n_{l})}|m_{l}|$ and
$S_{\bowtie}=\sum_{m\in\mathcal{C}_{1}(n_{\bowtie})}|m|$.

Because each node in $V^{N}$ is only contained once in $toposort^{-1}(N)$ and
has at most one dependent node due to the well-formedness criterion, execution
of $(N,p)$ thus takes $O(|\mathcal{C}_{1}|)$ steps.

####  0.D.2.7 Localized RETE Time Complexity

###### Theorem 0.D.5

Let $H$ be an edge-dominated graph, $H_{p}\subseteq H$, $(N,p)$ a well-formed
RETE net for query graph $Q$, $\mathcal{C}$ a consistent configuration for
$(N,p)$, and $\mathcal{C}^{\Phi}_{0}$ the empty configuration for the
localized RETE net $(N^{\Phi},p^{\Phi})=localize((N,p))$. Executing
$(N^{\Phi},p^{\Phi})$ via
$execute(order((N^{\Phi},p^{\Phi})),N^{\Phi},H,H_{p},\mathcal{C}^{\Phi}_{0})$
then takes $O(T\cdot(|Q_{a}|+|Q|))$ steps.

###### Proof

From Lemmata 22-29 and $\mathcal{C}^{\Phi}_{0}$ being empty it follows that
matches are never removed from a current result set during the execution of
$(N^{\Phi},p^{\Phi})$ and their marking in such a current result set is never
decreased. $\mathcal{C}^{\Phi}_{0}$ being empty also entails that
$\mathcal{C}^{\Phi}_{0}$ is consistent for all nodes in $N^{\Phi}$ except for
marking-sensitive vertex input nodes.

By Lemmata 14-21, we then know that whenever a marking-sensitive node
$n^{\Phi}$ that is not a marking-sensitive join node is executed, execution
takes $O(S^{+}_{D}+S^{+}_{R}+N^{\uparrow}_{D}+N^{\uparrow}_{R})$ steps, where,
compared to the last execution of $n^{\Phi}$, $S^{+}_{D}$ is the total size of
matches added to the current result sets of dependencies of $n^{\Phi}$,
$S^{+}_{R}$ is the total size of matches added to the current result set of
$n^{\Phi}$, $N^{\uparrow}_{D}$ is the number of matches whose marking has been
increased in the result sets of depedencies of $n^{\Phi}$, and
$N^{\uparrow}_{R}$ is the number of matches whose marking has been increased
in the result set of $n^{\Phi}$.

Each match is only added to a result set once and by the construction of
$(N^{\Phi},p^{\Phi})$, at most $|Q|$ different marking values are possible for
matches in a configuration for $(N^{\Phi},p^{\Phi})$. Furthermore, by the
construction of $(N^{\Phi},p^{\Phi})$, each node in $N^{\Phi}$ can be a
dependency of at most two other RETE nodes. It thus follows that the total
effort for executing all non-join nodes in $N^{\Phi}$ must be in
$O(|\mathcal{C}|+|Q|\cdot T)$.

For marking-sensitive join nodes, a slightly different argument has to be
made, since the number of steps required for an individual execution is not
necessarily in $O(S^{+}_{D}+S^{+}_{R}+N^{\uparrow}_{D}+N^{\uparrow}_{R})$.
This is due to the fact that the increase of a marking of a match in the
result set of one of the join node’s dependencies may make recomputation of
the marking of a number of matches in the join’s current result set necessary
without actually resulting in any change.

However, we can observe that the effort for processing matches newly added to
the result sets of the dependencies of a marking-sensitive join node
$[\bowtie]^{\Phi}$ is in $O(S^{+}_{D}+S^{+}_{R})$. This is due to the fact
that, assuming consistency of the previous configuration for
$[\bowtie]^{\Phi}$, these changes can be handled by constructing the new
intermediate results spawned by the newly added dependency matches. For each
such newly added dependency match, all complementary matches from the opposite
dependency have to be retrieved and combined into result matches.

This takes effort in the size of the newly added dependency match and, since
the query subgraphs associated with dependencies of $[\bowtie]^{\Phi}$ are
subgraphs of the query subgraph associated with $[\bowtie]^{\Phi}$ and each
complementary match for the opposite dependency results in a distinct
intermediate result for the join, the combined size of newly created result
matches.

Assuming changes to dependency result sets are cached and ideal indexing
structures, this entails an overall effort in $O(S^{+}_{D}+S^{+}_{R})$ for
handling matches newly added to the result sets of dependencies of
$[\bowtie]^{\Phi}$. An increase of the marking of a match in the result set of
a dependency of $[\bowtie]^{\Phi}$ can be handled by recomputing the marking
of all associated matches in the result set of $[\bowtie]^{\Phi}$. By
explicitly storing the associated result matches of each dependency match,
this only requires effort in the number of such associated result matches.

The number of associated result matches may not correspond to the number of
result matches whose marking actually increases, since the result match
marking also depends on the marking of the complementary match in the opposite
dependency. However, since each result match is associated with exactly two
dependency matches, we know that overall, the effort for recomputing the
marking of result matches must still be linear in the number of result tuples
and the number of different possible markings. Combined with the baseline
effort for processing marking increases for dependency matches and the effort
for handling newly added dependency matches, this means that the total effort
for executing all marking-sensitive join nodes in $N^{\Phi}$ must also be in
$O(|\mathcal{C}|+|Q|\cdot T)$.

Assuming that redundant execution of nodes whose dependency result sets have
not changed since the last execution is avoided via a notification mechanism,
this yields an overall effort in $O(|\mathcal{C}|+|Q|\cdot T)$ for executing
$(N^{\Phi},p^{\Phi})$ via
$execute(order((N^{\Phi},p^{\Phi})),N^{\Phi},H,H_{p},\mathcal{C}^{\Phi}_{0})$.

####  0.D.2.8 Supplementary Lemmata

###### Lemma 1

Let $H$ be a graph, $(N,p)$ a well-formed RETE net with join tree height $h$
and $Q$ the query graph associated with $p$, $(X^{\Phi},p_{X}^{\Phi})$ a
modular extension of the localized RETE net
$(N^{\Phi},p^{\Phi})=localize((N,p))$, and $\mathcal{C}$ a configuration for
$(X^{\Phi},p_{X}^{\Phi})$ that is consistent for all nodes in $V^{N^{\Phi}}$.
Furthermore, let $x\in\chi(N^{\Phi})$,
$Q_{v}=(\\{v\\},\emptyset,\emptyset,\emptyset)$ the query subgraph associated
with $x$, and $(m^{\prime},\psi)\in\mathcal{C}(x)$ such that $\psi>h$ for some
match $m^{\prime}:Q_{v}\rightarrow H$. It then holds that $\forall
m\in\mathcal{M}^{Q}_{H}:m(v)=m^{\prime}(v)\Rightarrow\exists(m,\phi)\in\mathcal{C}(p^{\Phi}):\phi\geq\psi$.

###### Proof

We prove the lemma by induction over the height $h$ of the join tree $N$.

Let $m\in\mathcal{M}^{Q}_{H}$ such that $m(v)=m^{\prime}(v)$.

In the base case of $h=0$, $N$ consists of a single edge input node $p$ and
$(N^{\Phi},p^{\Phi})$ is hence given by
$(N^{\Phi},p^{\Phi})=(LNS(p),[\cup]^{\Phi})$. We thus also know that
$\chi(N^{\Phi})=\\{[\cup]^{\Phi}_{v},[\cup]^{\Phi}_{w}\\}$. We can then
distinguish two cases:

Case 1: $x=[\cup]^{\Phi}_{v}$. By the semantics of the forward navigation node
$[v\rightarrow_{n}w]^{\Phi}$, which must have $Q$ as its associated query
subgraph, and by $\mathcal{C}$ being consistent for all nodes in
$V^{N^{\Phi}}$, it follows that
$(m,\psi)\in\mathcal{C}([v\rightarrow_{n}w]^{\Phi})$. By the semantics of the
marking sensitive union node $p^{\Phi}=[\cup]^{\Phi}$, it then follows that
$(m,\phi)\in\mathcal{C}(p^{\Phi})$ for some $\phi\geq\psi$.

Case 2: $x=[\cup]^{\Phi}_{w}$. By the semantics of the backward navigation
node $[w\leftarrow_{n}v]^{\Phi}$, which must have $Q$ as its associated query
subgraph, and by $\mathcal{C}$ being consistent for all nodes in
$V^{N^{\Phi}}$, it follows that
$(m,\psi)\in\mathcal{C}([w\leftarrow_{n}v]^{\Phi})$. By the semantics of the
marking sensitive union node $p^{\Phi}=[\cup]^{\Phi}$, it then follows that
$(m,\phi)\in\mathcal{C}(p^{\Phi})$ for some $\phi\geq\psi$.

Thus, the lemma holds in the base case.

For the induction step, we show that if the lemma holds for all well-formed
RETE nets with join tree height $h$, it must also hold for any well-formed
RETE net $(N,p)$ with join tree height $h+1$.

Since $h+1\geq 1$, we know that $p$ must be a join node. $(N^{\Phi},p^{\Phi})$
is hence given by $(N^{\Phi},p^{\Phi})=(N^{\Phi}_{\bowtie}\cup
N^{\Phi}_{l}\cup N^{\Phi}_{r}\cup RPS_{l}\cup RPS_{r},p^{\Phi})$, with
$(N^{\Phi}_{l},p^{\Phi}_{l})=localize((N_{l},p_{l}))$, where $(N_{l},p_{l})$
is the RETE subnet under the left dependency of $p^{\Phi}$, and
$(N^{\Phi}_{r},p^{\Phi}_{r})=localize((N_{r},p_{r}))$, where $(N_{r},p_{r})$
is the RETE subnet under the right dependency of $p^{\Phi}$. We thus also know
that $\chi(N^{\Phi})=\chi(N^{\Phi}_{l})\cup\chi(N^{\Phi}_{r})$.

We can thus again distinguish two cases:

Case 1: $x\in\chi(N^{\Phi}_{l})$. Since $N_{l}$ must have a join tree height
of $h^{\prime}\leq h$ and because $(N^{\Phi},p^{\Phi})$ and hence also
$(X^{\Phi},p_{X}^{\Phi})$ is a modular extension of
$(N^{\Phi}_{l},p^{\Phi}_{l})$, by the induction hypothesis, we know that
$\forall
m_{l}\in\mathcal{M}^{Q_{l}}_{H}:m_{l}(v)=m^{\prime}(v)\Rightarrow\exists(m_{l},\phi_{l})\in\mathcal{C}(p_{l}^{\Phi}):\phi_{l}\geq\psi$,
where $Q_{l}$ is the query subgraph associated with $p_{l}$.

For any such $(m_{l},\phi_{l})\in\mathcal{C}(p_{l}^{\Phi})$, by the
construction of $N^{\Phi}$, the semantics of the RETE nodes in $RPS_{l}$,
$\mathcal{C}$ being consistent for all nodes in $V^{N^{\Phi}}$ and hence also
for all nodes in $V^{N^{\Phi}_{l}}$, and since $\phi_{l}\geq\psi>h+1$, it then
follows that
$(m_{l}|_{Q_{v^{\prime}}},h+1)\in\mathcal{C}([\phi:=h+1]^{\Phi}_{l})$, with
$[\phi:=h+1]^{\Phi}_{l}$ the marking assignment node in $RPS_{l}$ and
$Q_{v^{\prime}}=(\\{v^{\prime}\\},\emptyset,\emptyset,\emptyset)$ the query
subgraph associated with $[\phi:=h+1]^{\Phi}_{l}$.

Because $[\phi:=h+1]^{\Phi}_{l}$ is a dependency of some extension point
$x_{r}\in\chi(N^{\Phi}_{r})$ and $x_{r}$ is a marking-sensitive union node, it
follows that there must be some tuple
$(m_{l}|_{Q_{v^{\prime}}},\psi_{r})\in\mathcal{C}(x_{r})$, with $\psi_{r}\geq
h+1$. By the induction hypothesis and since $v^{\prime}\in V^{Q_{l}}\cap
V^{Q_{r}}$, where $Q_{r}$ is the query subgraph associated with $p_{r}$, it
then follows that $\forall
m_{r}\in\mathcal{M}^{Q_{r}}_{H}:m_{r}(v^{\prime})=m_{l}(v^{\prime})\Rightarrow\exists(m_{r},\phi_{r})\in\mathcal{C}(p^{\Phi}_{r}):\phi_{r}\geq\psi_{r}$.

Because $v^{\prime}\in Q_{\cap}$ with $p^{\Phi}=[\bowtie_{Q_{\cap}}]^{\Phi}$,
it must then hold that $\forall
m_{r}\in\mathcal{M}^{Q_{r}}_{H}:m_{r}|_{Q_{\cap}}=m_{l}|_{Q_{\cap}}\Rightarrow\exists(m_{r},\phi_{r})\in\mathcal{C}(p^{\Phi}_{r}):\phi_{r}\geq\psi_{r}$.
By the semantics of the marking-sensitive join node and Lemma 2, and because
$\phi_{l}\geq\psi$, it then follows that $\forall
m\in\mathcal{M}^{Q}_{H}:m|_{Q_{l}}=m_{l}\Rightarrow\exists(m,\phi)\in\mathcal{C}(p^{\Phi}):\phi\geq\psi$.
Since $Q_{l}\subseteq Q$, which entails that $\forall
m\in\mathcal{M}^{Q}_{H}:\exists
m_{l}\in\mathcal{M}^{Q_{l}}_{H}:m|_{Q_{l}}=m_{l}$, and because $\forall
m_{l}\in\mathcal{M}^{Q_{l}}_{H}:m_{l}(v)=m^{\prime}(v)\Rightarrow\exists(m_{l},\phi_{l})\in\mathcal{C}(p_{l}^{\Phi}):\phi_{l}\geq\psi$,
it must finally follow that $\forall
m\in\mathcal{M}^{Q}_{H}:m(v)=m^{\prime}(v)\Rightarrow\exists(m,\phi)\in\mathcal{C}(p^{\Phi}):\phi\geq\psi$.

Case 2: $x\in\chi(N^{\Phi}_{r})$. The proof works analogously to the proof for
Case 1.

Thus, the induction step holds.

From the correctness of the base case and the induction step then follows the
correctness of the lemma.

###### Lemma 2

Let $n^{\Phi}=[\bowtie_{Q_{\cap}}]^{\Phi}\in V^{N^{\Phi}}$ be a marking-
sensitive join with associated subgraph $Q$ and dependencies $n^{\Phi}_{l}$
and $n^{\Phi}_{r}$ with associated subgraphs $Q_{l}$ respectively $Q_{r}$, $H$
a graph, $H_{p}\subseteq H$, $\mathcal{C}$ a configuration, and
$(m_{l},\phi_{l})\in\mathcal{C}(n^{\Phi}_{l})$. If $\forall
m_{r}\in\mathcal{M}^{Q_{r}}_{H}:m_{r}|_{Q_{\cap}}=m_{l}|_{Q_{\cap}}\Rightarrow\exists\phi_{r}\in\overline{\mathbb{N}}:(m_{r},\phi_{r})\in\mathcal{C}(n^{\Phi}_{r})$,
it then holds that $\forall
m\in\mathcal{M}^{Q}_{H}:m|_{Q_{l}}=m_{l}\Rightarrow\exists(m,\phi)\in\mathcal{R}^{\Phi}(n^{\Phi},N^{\Phi},H,H_{p},\mathcal{C}):\phi\geq\phi_{l}$.

###### Proof

Since $Q=Q_{l}\cup Q_{r}$, any match $m\in\mathcal{M}^{Q}_{H}$ with
$m|_{Q_{l}}=m_{l}$ can be represented as a union of two matches $m=m_{l}\cup
m_{r}$, with $m_{r}\in\mathcal{M}^{Q_{r}}_{H}$. For $m_{r}$, it must then hold
that $m_{l}|_{Q_{\cap}}=m_{r}|_{Q_{\cap}}$.

By assumption, there exist a tuple
$(m_{l},\phi_{l})\in\mathcal{C}(n^{\Phi}_{l})$ and a tuple
$(m_{r},\phi_{r})\in\mathcal{C}(n^{\Phi}_{r})$. From the definition of the
marking-sensitive join node, it follows that
$(m,max(\phi_{l},\phi_{r}))\in\mathcal{R}^{\Phi}(n^{\Phi},N^{\Phi},H,H_{p},\mathcal{C})$.
Thus, it must hold that $\forall
m\in\mathcal{M}^{Q}_{H}:m|_{Q_{l}}=m_{l}\Rightarrow\exists(m,\phi)\in\mathcal{R}^{\Phi}(n^{\Phi},N^{\Phi},H,H_{p},\mathcal{C}):\phi\geq\phi_{l}$.

###### Lemma 3

Let $H$ be a graph, $H_{p}\subseteq H$, $(N,p)$ a well-formed RETE net with
join tree height $h>0$, and $\mathcal{C}$ a consistent configuration for the
localized RETE net $(N^{\Phi},[\bowtie_{Q_{\cap}}]^{\Phi})=localize((N,p))$.
Furthermore, let $(N_{l},p_{l})$ and $(N_{r},p_{r})$ be the RETE subnets under
the dependencies of the join node $p$, $Q_{l}$ and $Q_{r}$ the associated
query subgraphs of $p_{l}$ respectively $p_{r}$, and
$(N^{\Phi}_{l},p^{\Phi}_{l})=localize((N_{l},p_{l}))$ and
$(N^{\Phi}_{r},p^{\Phi}_{r})=localize((N_{r},p_{r}))$ the associated RETE
subnets in $(N^{\Phi},[\bowtie_{Q_{\cap}}]^{\Phi})$. Finally, let
$(m_{l},\phi_{l})\in\mathcal{C}(p^{\Phi}_{l})$ such that $\phi_{l}>h$. It then
holds that $\forall
m_{r}\in\mathcal{M}^{Q_{r}}_{H}:m_{l}|_{Q_{\cap}}=m_{r}|_{Q_{\cap}}\Rightarrow\exists(m_{r},\phi_{r})\in\mathcal{C}(p^{\Phi}_{r}):\phi_{r}\geq
h$.

###### Proof

By the construction of $(N^{\Phi},[\bowtie_{Q_{\cap}}]^{\Phi})$, there must be
an marking-sensitive union node extension point
$[\cup]_{v}^{\Phi}\in\chi(N^{\Phi}_{r})$ that has a dependency on the marking
assignment node $[\phi:=h]^{\Phi}_{l}$ in the request projection structure
$RPS_{l}$ in $N^{\Phi}$. According to the semantics of the RETE nodes in
$RPS_{l}$, it must also hold that $\forall
m_{v}\in\mathcal{M}^{Q_{v}}_{H}:m_{v}(v)=m_{l}(v)\Rightarrow(m_{v},h)\in\mathcal{C}([\phi:=h]^{\Phi}_{l})$,
where $Q_{v}=(\\{v\\},\emptyset,\emptyset,\emptyset)$ is the query subgraph
associated with $[\phi:=h]^{\Phi}_{l}$. By the semantics of the marking-
sensitive union node, it must then also hold that $\forall
m_{v}\in\mathcal{M}^{Q_{v}}_{H}:m_{v}(v)=m_{l}(v)\Rightarrow\exists\psi\in\overline{\mathbb{N}}:(m_{v},\phi_{\cup})\in\mathcal{C}([\cup]_{v}^{\Phi})\wedge\phi_{\cup}\geq
h$.

Because $h^{\prime}<h$, where $h^{\prime}$ is the height of the join tree
$N_{r}$, by Lemma 1, we then know that $\forall
m_{r}\in\mathcal{M}^{Q_{r}}_{H}:m_{r}(v)=m_{l}(v)\Rightarrow\exists(m_{r},\phi_{r})\in\mathcal{C}(p^{\Phi}):\phi_{r}\geq
h$. Since $Q_{v}\subseteq Q_{\cap}$, it then follows that $\forall
m_{r}\in\mathcal{M}^{Q_{r}}_{H}:m_{l}|_{Q_{\cap}}=m_{r}|_{Q_{\cap}}\Rightarrow\exists(m_{r},\phi_{r})\in\mathcal{C}(p^{\Phi}_{r}):\phi_{r}\geq
h$.

###### Lemma 4

Let $H$ a graph, $H_{p}\subseteq H$, $(N,p)$ a well-formed RETE net with join-
tree height $h$, $\psi\in\overline{\mathbb{N}}$ such that $\psi>h$,
$(N^{\Phi},p^{\Phi})=localize((N,p))$, $(X^{\Phi},p_{X}^{\Phi})$ a modular
extension of $(N^{\Phi},p^{\Phi})$, $\mathcal{C}_{0}$ a configuration for
$(X^{\Phi},p^{\Phi})$ that is consistent for all nodes in $V^{N^{\Phi}}$ with
respect to $H$ and $H_{p}$, and $\mathcal{C}_{1}$ a configuration with
$\forall n\in V^{N^{\Phi}}:\mathcal{C}_{1}(n)=\mathcal{C}_{0}(n)$ and $\forall
n_{X}\in V^{X^{\Phi}}:(\exists e\in E^{X^{\Phi}}:t^{X^{\Phi}}=n_{X}\wedge
s^{X^{\Phi}}\in
V^{N^{\Phi}})\Rightarrow\forall(m,\phi)\in(\mathcal{C}_{1}(n_{X})\setminus\mathcal{C}_{0}(n_{X}))\cup(\mathcal{C}_{0}(n_{X})\setminus\mathcal{C}_{1}(n_{X})):\phi\leq\psi$.
Under the assumption that the execution order
$order(localize((N^{\prime},p^{\prime})))$ is robust under modular extension
for any well-formed RETE net $(N^{\prime},p^{\prime})$ with join tree height
$h^{\prime}<h$, it then holds for the configuration
$\mathcal{C}_{2}=execute(order(N^{\Phi},p^{\Phi}),X^{\Phi},H,H_{p},\mathcal{C}_{1})$
that
$\forall(m,\phi)\in(\mathcal{C}_{2}(p^{\Phi})\setminus\mathcal{C}_{1}(p^{\Phi}))\cup(\mathcal{C}_{1}(p^{\Phi})\setminus\mathcal{C}_{2}(p^{\Phi})):\phi\leq\psi$.

###### Proof

We show the correctness of the lemma by induction over the height $h$ of the
join tree $N$.

In the base case of $h$ = 0, $N$ consists of a single edge input $p$ and the
localized RETE net is thus given by
$(N^{\Phi},p^{\Phi})=(LNS(p),[\cup]^{\Phi})$, with $LNS(p)$ consisting of
nodes $[v]^{\Phi}$, $[w]^{\Phi}$, $[\cup]^{\Phi}_{v}$, $[\cup]^{\Phi}_{w}$,
$[v\rightarrow_{n}w]^{\Phi}$, $[w\leftarrow_{n}v]^{\Phi}$, and
$[\cup]^{\Phi}$. Without loss of generality, we assume the execution order
$order(LNS(p))=[v]^{\Phi},[w]^{\Phi},[\cup]^{\Phi}_{v},[\cup]^{\Phi}_{w},[v\rightarrow_{n}w]^{\Phi},[w\leftarrow_{n}v]^{\Phi},[\cup]^{\Phi}$.

By the semantics of the marking-sensitive vertex input node, we know that
$\mathcal{C}_{1.1}=execute(O_{1},X^{\Phi},H,H_{p},\mathcal{C}_{1})=\mathcal{C}_{1}$,
with $O_{1}=[v]^{\Phi},[w]^{\Phi}$.

By Lemma 5 and the assumption regarding the difference between current result
sets in $\mathcal{C}_{0}$ and $\mathcal{C}_{1}$ for dependencies from $LNS(p)$
into $X^{\Phi}$, it follows for
$\mathcal{C}_{1.2}=execute(O_{2},X^{\Phi},H,H_{p},\mathcal{C}_{1.1})$ and
$O_{2}=[\cup]^{\Phi}_{v},[\cup]^{\Phi}_{w}$ that
$\forall(m,\phi)\in(\mathcal{C}_{1.2}([\cup]^{\Phi}_{v})\setminus\mathcal{C}_{1}([\cup]^{\Phi}_{v}))\cup(\mathcal{C}_{1}([\cup]^{\Phi}_{v})\setminus\mathcal{C}_{1.2}([\cup]^{\Phi}_{v})):\phi\leq\psi$,
which holds analogously for $[\cup]^{\Phi}_{w}$.

By Lemmata 7 and 8, the same holds for
$\mathcal{C}_{1.3}=execute(O_{3},X^{\Phi},H,H_{p},\mathcal{C}_{1.2})$ and the
nodes $[v\rightarrow_{n}w]^{\Phi}$ and $[w\leftarrow_{n}v]^{\Phi}$, with
$O_{3}=[v\rightarrow_{n}w]^{\Phi},[w\leftarrow_{n}v]^{\Phi}$.

Finally, by Lemma 5 and the assumption regarding the difference between
current result sets in $\mathcal{C}_{0}$ and $\mathcal{C}_{1}$ for
dependencies from $LNS(p)$ into $X^{\Phi}$ then follows the satisfaction of
the base case for
$\mathcal{C}_{2}=execute([\cup]^{\Phi},X^{\Phi},H,H_{p},\mathcal{C}_{1.3})$.

For the induction step, we show that if the lemma holds for all join trees of
height less than or equal to $h$, it follows that the lemma holds for any join
tree $N$ of height $h+1$.

Since $h+1\geq 1$, $p$ is a join node with dependencies $p_{l}$ and $p_{r}$
and the localized RETE net is thus given by
$(N^{\Phi},p^{\Phi})=(N^{\Phi}_{\bowtie}\cup N^{\Phi}_{l}\cup N^{\Phi}_{r}\cup
RPS_{l}\cup RPS_{r},p^{\Phi})$, with
$(N^{\Phi}_{l},p^{\Phi}_{l})=localize((N_{l},p_{l}))$ and
$(N^{\Phi}_{r},p^{\Phi}_{r})=localize((N_{r},p_{r}))$. Consequently, the
execution order of $N^{\Phi}$ is given by $order(N^{\Phi})=order(RPS_{r})\circ
order(N^{\Phi}_{l})\circ order(RPS_{l})\circ order(N^{\Phi}_{r})\circ
order(RPS_{r})\circ order(N^{\Phi}_{l})\circ N^{\Phi}_{\bowtie}$.

By definition, the marking filter nodes, marking-sensitive projection nodes,
and marking assignment nodes in $RPS_{l}$ and $RPS_{r}$ must have exactly one
dependency and the marking-sensitive join node in $N^{\Phi}_{\bowtie}$ must
have exactly two dependencies. By the construction of $N^{\Phi}$, in the
modular extension $X^{\Phi}$, all nodes in $RPS_{l}$, $RPS_{r}$ and
$N^{\Phi}_{\bowtie}$ may thus only depend on nodes in $N^{\Phi}$.

Since $\forall n\in V^{N^{\Phi}}:\mathcal{C}_{1}(n)=\mathcal{C}_{0}(n)$ and
because $\mathcal{C}_{0}$ is consistent for all nodes in $V^{N^{\Phi}}$,
$\mathcal{C}_{1}$ is then consistent for all nodes in $V^{RPS_{r}}$. Thus,
$\mathcal{C}_{1.1}=execute(order(RPS_{r}),X^{\Phi},H,H_{p},\mathcal{C}_{1})=\mathcal{C_{1}}$.

Since $(N^{\Phi},p^{\Phi})$ is a modular extension of
$(N^{\Phi}_{l},p^{\Phi}_{l})$ and $(N^{\Phi}_{r},p^{\Phi}_{r})$,
$(X^{\Phi},p_{X}^{\Phi})$ must be a modular extension of
$(N^{\Phi}_{l},p^{\Phi}_{l})$ and $(N^{\Phi}_{r},p^{\Phi}_{r})$. Furthermore,
since $\forall n\in V^{N^{\Phi}}:\mathcal{C}_{1}(n)=\mathcal{C}_{0}(n)$ and
$\forall n_{X}\in V^{X^{\Phi}}:(\exists e\in
E^{X^{\Phi}}:t^{X^{\Phi}}=n_{X}\wedge s^{X^{\Phi}}\in
V^{N^{\Phi}})\Rightarrow\forall(m,\phi)\in(\mathcal{C}_{1}(n_{X})\setminus\mathcal{C}_{0}(n_{X}))\cup(\mathcal{C}_{0}(n_{X})\setminus\mathcal{C}_{1}(n_{X})):\phi\leq\psi$,
it also holds for $N^{\Phi}_{l}$ and analogously for $N^{\Phi}_{r}$ that
$\forall n\in V^{N^{\Phi}_{l}}:\mathcal{C}_{1}(n)=\mathcal{C}_{0}(n)$ and
$\forall n_{X}\in V^{X^{\Phi}}:(\exists e\in
E^{X^{\Phi}}:t^{X^{\Phi}}=n_{X}\wedge s^{X^{\Phi}}\in
V^{N^{\Phi}_{l}})\Rightarrow\forall(m,\phi)\in(\mathcal{C}_{1}(n_{X})\setminus\mathcal{C}_{0}(n_{X}))\cup(\mathcal{C}_{0}(n_{X})\setminus\mathcal{C}_{1}(n_{X})):\phi\leq\psi$.

Thus, for configuration
$\mathcal{C}_{1.2}=execute(order(N^{\Phi}_{l}),X^{\Phi},H,H_{p},\mathcal{C}_{1.1})$,
by the induction hypothesis it holds that
$\forall(m,\phi)\in(\mathcal{C}_{1.2}(p^{\Phi}_{l})\setminus\mathcal{C}_{0}(p^{\Phi}_{l}))\cup(\mathcal{C}_{0}(p^{\Phi}_{l})\setminus\mathcal{C}_{1.2}(p^{\Phi}_{l})):\phi\leq\psi$.
Furthermore, since $N_{l}$ must have join tree height $h^{\prime}<h+1$ and by
the entailed assumption of robustness of $order(N^{\Phi}_{l})$ under modular
extension, $\mathcal{C}_{1.2}$ must be consistent for all nodes in
$V^{N^{\Phi}_{l}}$.

Since $\psi\geq h+1$, by the semantics of the marking assignment node
$[\phi:=h+1]_{l}^{\Phi}$, it follows that
$\forall(m,\phi)\in(\mathcal{C}_{1.3}([\phi:=h+1]_{l}^{\Phi})\setminus\mathcal{C}_{0}([\phi:=h+1]_{l}^{\Phi}))\cup(\mathcal{C}_{0}([\phi:=h+1]_{l}^{\Phi})\setminus\mathcal{C}_{1.3}([\phi:=h+1]_{l}^{\Phi})):\phi\leq\psi$.

By the construction of $N^{\Phi}$, it then holds that $\forall n\in
V^{N^{\Phi}_{r}}:\mathcal{C}_{1.3}(n)=\mathcal{C}_{0}(n)$ and $\forall
n_{X}\in V^{X^{\Phi}}:(\exists e\in E^{X^{\Phi}}:t^{X^{\Phi}}=n_{X}\wedge
s^{X^{\Phi}}\in
V^{N^{\Phi}_{r}})\Rightarrow\forall(m,\phi)\in(\mathcal{C}_{1.3}(n_{X})\setminus\mathcal{C}_{0}(n_{X}))\cup(\mathcal{C}_{0}(n_{X})\setminus\mathcal{C}_{1.3}(n_{X})):\phi\leq\psi$.
Hence, by the induction hypothesis, it holds for
$\mathcal{C}_{1.4}=execute(order(N^{\Phi}_{r}),X^{\Phi},H,H_{p},\mathcal{C}_{1.3})$
that
$\forall(m,\phi)\in(\mathcal{C}_{1.4}(p^{\Phi}_{r})\setminus\mathcal{C}_{0}(p^{\Phi}_{r}))\cup(\mathcal{C}_{0}(p^{\Phi}_{r})\setminus\mathcal{C}_{1.4}(p^{\Phi}_{r})):\phi\leq\psi$.
Furthermore, since $N_{r}$ must have join tree height $h^{\prime}<h+1$ and by
the entailed assumption of robustness of $order(N^{\Phi}_{r})$ under modular
extension, $\mathcal{C}_{1.4}$ must be consistent for all nodes in
$V^{N^{\Phi}_{r}}$.

By the semantics of the marking assignment node $[\phi:=h+1]_{r}^{\Phi}$ in
$RPS_{r}$, for
$\mathcal{C}_{1.5}=execute(order(RPS_{r}),X^{\Phi},H,H_{p},\mathcal{C}_{1.4})$
it must then hold that
$\forall(m,\phi)\in(\mathcal{C}_{1.5}([\phi:=h+1]_{r}^{\Phi})\setminus\mathcal{C}_{0}([\phi:=h+1]_{r}^{\Phi}))\cup(\mathcal{C}_{1.4}([\phi:=h+1]_{r}^{\Phi})\setminus\mathcal{C}_{1.5}([\phi:=h+1]_{r}^{\Phi})):\phi=h+1$.

Since $V^{N^{\Phi}_{l}}\cap(V^{N^{\Phi}_{r}}\cup V^{RPS_{l}}\cup
V^{RPS_{r}})=\emptyset$, it then follows that $\forall n\in
V^{N^{\Phi}_{l}}:\mathcal{C}_{1.5}(n)=\mathcal{C}_{1.2}(n)$. Because no node
in $V^{N^{\Phi}_{l}}$ may depend on any node in the sequence
$order(RPS_{l})\circ order(N^{\Phi}_{r})\circ order(RPS_{r})$ other than
$[\phi:=h]_{r}^{\Phi}$, it also follows that $\forall n_{X}\in
V^{X^{\Phi}}:(\exists e\in E^{X^{\Phi}}:t^{X^{\Phi}}=n_{X}\wedge
s^{X^{\Phi}}\in
V^{N^{\Phi}_{l}})\Rightarrow\forall(m,\phi)\in(\mathcal{C}_{1.5}(n_{X})\setminus\mathcal{C}_{1.2}(n_{X}))\cup(\mathcal{C}_{1.2}(n_{X})\setminus\mathcal{C}_{1.5}(n_{X})):\phi=h+1$.
Because $\mathcal{C}_{1.2}$ is consistent for all nodes in $V^{N^{\Phi}_{l}}$
and $N_{l}$ must have a join tree height $h^{\prime}\leq h+1$, for
$\mathcal{C}_{1.6}=execute(order(N^{\Phi}_{l}),X^{\Phi},H,H_{p},\mathcal{C}_{1.5})$,
it then follows by the induction hypothesis that
$\forall(m,\phi)\in(\mathcal{C}_{1.6}(p^{\Phi}_{l})\setminus\mathcal{C}_{1.2}(p^{\Phi}_{l}))\cup(\mathcal{C}_{1.2}(p^{\Phi}_{l})\setminus\mathcal{C}_{1.6}(p^{\Phi}_{l})):\phi\leq
h+1$.

Thus, it holds that
$\forall(m,\phi)\in(\mathcal{C}_{1.6}(p^{\Phi}_{l})\setminus\mathcal{C}_{0}(p^{\Phi}_{l}))\cup(\mathcal{C}_{0}(p^{\Phi}_{l})\setminus\mathcal{C}_{1.6}(p^{\Phi}_{l})):\phi\leq\psi$.
Furthermore, since $p^{\Phi}_{r}\notin(V^{N^{\Phi}_{l}}\cup V^{RPS_{r}})$, it
also holds that
$\forall(m,\phi)\in(\mathcal{C}_{1.6}(p^{\Phi}_{r})\setminus\mathcal{C}_{0}(p^{\Phi}_{r}))\cup(\mathcal{C}_{0}(p^{\Phi}_{r})\setminus\mathcal{C}_{1.6}(p^{\Phi}_{r})):\phi\leq\psi$.

By the assumption regarding the robustness under modular extension of
$order(N^{\Phi}_{l})$, $\mathcal{C}_{1.6}$ must be consistent with all nodes
in $V^{N^{\Phi}_{l}}$. Since $V^{N^{\Phi}_{l}}$, $V^{N^{\Phi}_{r}}$,
$V^{RPS_{l}}$, and $V^{RPS_{r}}$ are pairwise disjoint and since the modular
extension $X^{\Phi}$ cannot introduce additional dependencies between nodes in
$N^{\Phi}$, it follows by the construction of $N^{\Phi}$ that
$\mathcal{C}_{1.6}$ must also be consistent for all nodes in
$V^{N^{\Phi}_{r}}$ and $V^{RPS_{r}}$. By the semantics of
$[\phi>h+1]_{l}^{\Phi}$ and because
$\forall(m,\phi)\in(\mathcal{C}_{1.6}(p^{\Phi}_{l})\setminus\mathcal{C}_{1.3}(p^{\Phi}_{l}))\cup(\mathcal{C}_{1.3}(p^{\Phi}_{l})\setminus\mathcal{C}_{1.6}(p^{\Phi}_{l})):\phi\leq
h+1$, we also know that $\mathcal{C}_{1.6}$ is consistent for all nodes in
$V^{RPS_{l}}$.

Because $V^{N^{\Phi}_{\bowtie}}=\\{p^{\Phi}\\}$ with $p^{\Phi}$ a marking
sensitive join with dependencies $p^{\Phi}_{l}$ and $p^{\Phi}_{r}$, by Lemma
11 it follows for
$\mathcal{C}_{2}=execute(order(N^{\Phi}_{\bowtie}),X^{\Phi},H,H_{p},\mathcal{C}_{1.6})$
that
$\forall(m,\phi)\in(\mathcal{C}_{2}(p^{\Phi})\setminus\mathcal{C}_{1}(p^{\Phi}))\cup(\mathcal{C}_{1}(p^{\Phi})\setminus\mathcal{C}_{2}(p^{\Phi})):\phi\leq\psi$.

From the correctness of the base case and the induction step then follows the
correctness of the lemma.

###### Lemma 5

Let $n^{\Phi}$ be a marking-sensitive union node with dependencies
$N^{\Phi}_{\alpha}$ in some marking-sensitive RETE net $(N^{\Phi},p^{\Phi})$.
Let $\mathcal{C}_{0}$ and $\mathcal{C}$ furthermore be configurations for
$(N^{\Phi},p^{\Phi})$ such that $\mathcal{C}_{0}$ is consistent for $n^{\Phi}$
and it holds for all $n^{\Phi}_{\alpha}\in N^{\Phi}_{\alpha}$ that
$\forall(m,\phi)\in\mathcal{C}_{0}(n^{\Phi}_{\alpha})\setminus\mathcal{C}(n^{\Phi}_{\alpha}):\phi\leq
h$ and
$\forall(m,\phi)\in\mathcal{C}(n^{\Phi}_{\alpha})\setminus\mathcal{C}_{0}(n^{\Phi}_{\alpha}):\phi\leq
h$. It then holds for host graph $H$ and partial host graph $H_{p}$ that
$\forall(m,\phi)\in\mathcal{C}_{0}(n^{\Phi})\setminus\mathcal{R}^{\Phi}(n^{\Phi},N^{\Phi},H,H_{p},\mathcal{C}):\phi\leq
h$ and
$\forall(m,\phi)\in\mathcal{R}^{\Phi}(n^{\Phi},N^{\Phi},H,H_{p},\mathcal{C})\setminus\mathcal{C}_{0}(n^{\Phi}):\phi\leq
h$.

###### Proof

Let
$(m,\phi)\in\mathcal{R}^{\Phi}(n^{\Phi},N^{\Phi},H,H_{p},\mathcal{C})\setminus\mathcal{C}_{0}(n^{\Phi})$.
We can then distinguish two cases:

Case 1: It may hold that
$\nexists(m^{\prime},\phi^{\prime})\in\mathcal{C}_{0}(n^{\Phi}):m=m^{\prime}$.
In this case, by the semantics of the marking-sensitive union node, there must
be some $n^{\Phi}_{\alpha}\in N^{\Phi}_{\alpha}$ such that
$(m,\phi)\in\mathcal{C}(n^{\Phi}_{\alpha})\setminus\mathcal{C}_{0}(n^{\Phi}_{\alpha})$.
Since
$\forall(m,\phi)\in\mathcal{C}(n^{\Phi}_{\alpha})\setminus\mathcal{C}_{0}(n^{\Phi}_{\alpha}):\phi\leq
h$, it thus holds that $\phi\leq h$.

Case 2: Otherwise, there must be a tuple
$(m^{\prime},\phi^{\prime})\in\mathcal{C}_{0}(n^{\Phi}):m=m^{\prime}$. If
$\phi^{\prime}<\phi$, there again must be some $n^{\Phi}_{\alpha}\in
N^{\Phi}_{\alpha}$ such that
$(m,\phi)\in\mathcal{C}(n^{\Phi}_{\alpha})\setminus\mathcal{C}_{0}(n^{\Phi}_{\alpha})$,
and thus $\phi\leq h$. If $\phi^{\prime}>\phi$, there must instead be some
$n^{\Phi}_{\alpha}\in N^{\Phi}_{\alpha}$ such that
$(m,\phi^{\prime})\in\mathcal{C}_{0}(n^{\Phi}_{\alpha})\setminus\mathcal{C}(n^{\Phi}_{\alpha})$.
Because
$\forall(m,\phi^{\prime})\in\mathcal{C}_{0}(n^{\Phi}_{\alpha})\setminus\mathcal{C}(n^{\Phi}_{\alpha}):\phi^{\prime}\leq
h$, it then also follows that $\phi\leq h$.

It thus follows that $\phi\leq h$.

Let
$(m,\phi)\in\mathcal{C}_{0}(n^{\Phi})\setminus\mathcal{R}^{\Phi}(n^{\Phi},N^{\Phi},H,H_{p},\mathcal{C})$.
We can then distinguish two cases:

Case 1: It may hold that
$\nexists(m^{\prime},\phi^{\prime})\in\mathcal{R}^{\Phi}(n^{\Phi},N^{\Phi},H,H_{p},\mathcal{C}):m=m^{\prime}$.
In this case, by the semantics of the marking-sensitive union node, there must
be some $n^{\Phi}_{\alpha}\in N^{\Phi}_{\alpha}$ such that
$(m,\phi)\in\mathcal{C}_{0}(n^{\Phi}_{\alpha})\setminus\mathcal{C}(n^{\Phi}_{\alpha})$.
Since
$\forall(m,\phi)\in\mathcal{C}_{0}(n^{\Phi}_{\alpha})\setminus\mathcal{C}(n^{\Phi}_{\alpha}):\phi\leq
h$, it thus holds that $\phi\leq h$.

Case 2: Otherwise, there must be a tuple
$(m^{\prime},\phi^{\prime})\in\mathcal{R}^{\Phi}(n^{\Phi},N^{\Phi},H,H_{p},\mathcal{C}):m=m^{\prime}$.
If $\phi^{\prime}<\phi$, there again must be some $n^{\Phi}_{\alpha}\in
N^{\Phi}_{\alpha}$ such that
$(m,\phi)\in\mathcal{C}_{0}(n^{\Phi}_{\alpha})\setminus\mathcal{C}(n^{\Phi}_{\alpha})$,
and thus $\phi\leq h$. If $\phi^{\prime}>\phi$, there must instead be some
$n^{\Phi}_{\alpha}\in N^{\Phi}_{\alpha}$ such that
$(m,\phi^{\prime})\in\mathcal{C}(n^{\Phi}_{\alpha})\setminus\mathcal{C}_{0}(n^{\Phi}_{\alpha})$.
Because
$\forall(m,\phi^{\prime})\in\mathcal{C}(n^{\Phi}_{\alpha})\setminus\mathcal{C}_{0}(n^{\Phi}_{\alpha}):\phi^{\prime}\leq
h$, it then also follows that $\phi\leq h$.

It thus follows that $\phi\leq h$.

###### Lemma 6

Let $n^{\Phi}$ be a marking-sensitive projection node with dependency
$n^{\Phi}_{\alpha}$ in some marking-sensitive RETE net $(N^{\Phi},p^{\Phi})$.
Let $\mathcal{C}_{0}$ and $\mathcal{C}$ furthermore be configurations for
$(N^{\Phi},p^{\Phi})$ such that $\mathcal{C}_{0}$ is consistent for $n^{\Phi}$
and it holds that
$\forall(m,\phi)\in\mathcal{C}_{0}(n^{\Phi}_{\alpha})\setminus\mathcal{C}(n^{\Phi}_{\alpha}):\phi\leq
h$ and
$\forall(m,\phi)\in\mathcal{C}(n^{\Phi}_{\alpha})\setminus\mathcal{C}_{0}(n^{\Phi}_{\alpha}):\phi\leq
h$. It then holds for host graph $H$ and partial host graph $H_{p}$ that
$\forall(m,\phi)\in\mathcal{C}_{0}(n^{\Phi})\setminus\mathcal{R}^{\Phi}(n^{\Phi},N^{\Phi},H,H_{p},\mathcal{C}):\phi\leq
h$ and
$\forall(m,\phi)\in\mathcal{R}^{\Phi}(n^{\Phi},N^{\Phi},H,H_{p},\mathcal{C})\setminus\mathcal{C}_{0}(n^{\Phi}):\phi\leq
h$.

###### Proof

Let
$(m,\phi)\in\mathcal{R}^{\Phi}(n^{\Phi},N^{\Phi},H,H_{p},\mathcal{C})\setminus\mathcal{C}_{0}(n^{\Phi})$.
We can then distinguish two cases:

Case 1: It may hold that
$\nexists(m^{\prime},\phi^{\prime})\in\mathcal{C}_{0}(n^{\Phi}):m=m^{\prime}$.
In this case, by the semantics of the marking-sensitive projection node, there
must be some match $m^{\prime\prime}$ such that
$(m^{\prime\prime},\phi)\in\mathcal{C}(n^{\Phi}_{\alpha})\setminus\mathcal{C}_{0}(n^{\Phi}_{\alpha})$.
Since
$\forall(m^{\prime\prime},\phi)\in\mathcal{C}(n^{\Phi}_{\alpha})\setminus\mathcal{C}_{0}(n^{\Phi}_{\alpha}):\phi\leq
h$, it thus holds that $\phi\leq h$.

Case 2: Otherwise, there must be a tuple
$(m^{\prime},\phi^{\prime})\in\mathcal{C}_{0}(n^{\Phi}):m=m^{\prime}$. If
$\phi^{\prime}<\phi$, there again must be some match $m^{\prime\prime}$ such
that
$(m^{\prime\prime},\phi)\in\mathcal{C}(n^{\Phi}_{\alpha})\setminus\mathcal{C}_{0}(n^{\Phi}_{\alpha})$,
and thus $\phi\leq h$. If $\phi^{\prime}>\phi$, there must instead be a match
$m^{\prime\prime}$ such that
$(m^{\prime\prime},\phi^{\prime})\in\mathcal{C}_{0}(n^{\Phi}_{\alpha})\setminus\mathcal{C}(n^{\Phi}_{\alpha})$.
Because
$\forall(m^{\prime\prime},\phi^{\prime})\in\mathcal{C}_{0}(n^{\Phi}_{\alpha})\setminus\mathcal{C}(n^{\Phi}_{\alpha}):\phi^{\prime}\leq
h$, it then also follows that $\phi\leq h$.

It thus follows that $\phi\leq h$.

Let
$(m,\phi)\in\mathcal{C}_{0}(n^{\Phi})\setminus\mathcal{R}^{\Phi}(n^{\Phi},N^{\Phi},H,H_{p},\mathcal{C})$.
We can then distinguish two cases:

Case 1: It may hold that
$\nexists(m^{\prime},\phi^{\prime})\in\mathcal{R}^{\Phi}(n^{\Phi},N^{\Phi},H,H_{p},\mathcal{C}):m=m^{\prime}$.
In this case, by the semantics of the marking-sensitive projection node, there
must be some match $m^{\prime\prime}$ such that
$(m^{\prime\prime},\phi)\in\mathcal{C}_{0}(n^{\Phi}_{\alpha})\setminus\mathcal{C}(n^{\Phi}_{\alpha})$.
Since
$\forall(m^{\prime\prime},\phi)\in\mathcal{C}_{0}(n^{\Phi}_{\alpha})\setminus\mathcal{C}(n^{\Phi}_{\alpha}):\phi\leq
h$, it thus holds that $\phi\leq h$.

Case 2: Otherwise, there must be a tuple
$(m^{\prime},\phi^{\prime})\in\mathcal{R}^{\Phi}(n^{\Phi},N^{\Phi},H,H_{p},\mathcal{C}):m=m^{\prime}$.
If $\phi^{\prime}<\phi$, there again must be some match $m^{\prime\prime}$
such that
$(m^{\prime\prime},\phi)\in\mathcal{C}_{0}(n^{\Phi}_{\alpha})\setminus\mathcal{C}(n^{\Phi}_{\alpha})$,
and thus $\phi\leq h$. If $\phi^{\prime}>\phi$, there must instead be a match
$m^{\prime\prime}$ such that
$(m,\phi^{\prime})\in\mathcal{C}(n^{\Phi}_{\alpha})\setminus\mathcal{C}_{0}(n^{\Phi}_{\alpha})$.
Because
$\forall(m,\phi^{\prime})\in\mathcal{C}(n^{\Phi}_{\alpha})\setminus\mathcal{C}_{0}(n^{\Phi}_{\alpha}):\phi^{\prime}\leq
h$, it then also follows that $\phi\leq h$.

It thus follows that $\phi\leq h$.

###### Lemma 7

Let $n^{\Phi}$ be a forward navigation node with dependency
$n^{\Phi}_{\alpha}$ in some marking-sensitive RETE net $(N^{\Phi},p^{\Phi})$.
Let $\mathcal{C}_{0}$ and $\mathcal{C}$ furthermore be configurations for
$(N^{\Phi},p^{\Phi})$ such that $\mathcal{C}_{0}$ is consistent for $n^{\Phi}$
and it holds that
$\forall(m,\phi)\in\mathcal{C}_{0}(n^{\Phi}_{\alpha})\setminus\mathcal{C}(n^{\Phi}_{\alpha}):\phi\leq
h$ and
$\forall(m,\phi)\in\mathcal{C}(n^{\Phi}_{\alpha})\setminus\mathcal{C}_{0}(n^{\Phi}_{\alpha}):\phi\leq
h$. It then holds for host graph $H$ and partial host graph $H_{p}$ that
$\forall(m,\phi)\in\mathcal{C}_{0}(n^{\Phi})\setminus\mathcal{R}^{\Phi}(n^{\Phi},N^{\Phi},H,H_{p},\mathcal{C}):\phi\leq
h$ and
$\forall(m,\phi)\in\mathcal{R}^{\Phi}(n^{\Phi},N^{\Phi},H,H_{p},\mathcal{C})\setminus\mathcal{C}_{0}(n^{\Phi}):\phi\leq
h$.

###### Proof

Let
$(m,\phi)\in\mathcal{R}^{\Phi}(n^{\Phi},N^{\Phi},H,H_{p},\mathcal{C})\setminus\mathcal{C}_{0}(n^{\Phi})$.
It must then hold that
$\exists(m^{\prime},\phi)\in\mathcal{C}(n^{\Phi}_{\alpha})\setminus\mathcal{C}_{0}(n^{\Phi}_{\alpha})$.
Since
$\forall(m^{\prime},\phi)\in\mathcal{C}(n^{\Phi}_{\alpha})\setminus\mathcal{C}_{0}(n^{\Phi}_{\alpha}):\phi\leq
h$, it follows that $\phi\leq h$.

Let
$(m,\phi)\in\mathcal{C}_{0}(n^{\Phi})\setminus\mathcal{R}^{\Phi}(n^{\Phi},N^{\Phi},H,H_{p},\mathcal{C})$.
It must then hold that
$\exists(m^{\prime},\phi)\in\mathcal{C}_{0}(n^{\Phi}_{\alpha})\setminus\mathcal{C}(n^{\Phi}_{\alpha})$.
Since
$\forall(m^{\prime},\phi)\in\mathcal{C}_{0}(n^{\Phi}_{\alpha})\setminus\mathcal{C}(n^{\Phi}_{\alpha}):\phi\leq
h$, it follows that $\phi\leq h$.

###### Lemma 8

Let $n^{\Phi}$ be a backward navigation node with dependency
$n^{\Phi}_{\alpha}$ in some marking-sensitive RETE net $(N^{\Phi},p^{\Phi})$.
Let $\mathcal{C}_{0}$ and $\mathcal{C}$ furthermore be configurations for
$(N^{\Phi},p^{\Phi})$ such that $\mathcal{C}_{0}$ is consistent for $n^{\Phi}$
and it holds that
$\forall(m,\phi)\in\mathcal{C}_{0}(n^{\Phi}_{\alpha})\setminus\mathcal{C}(n^{\Phi}_{\alpha}):\phi\leq
h$ and
$\forall(m,\phi)\in\mathcal{C}(n^{\Phi}_{\alpha})\setminus\mathcal{C}_{0}(n^{\Phi}_{\alpha}):\phi\leq
h$. It then holds for host graph $H$ and partial host graph $H_{p}$ that
$\forall(m,\phi)\in\mathcal{C}_{0}(n^{\Phi})\setminus\mathcal{R}^{\Phi}(n^{\Phi},N^{\Phi},H,H_{p},\mathcal{C}):\phi\leq
h$ and
$\forall(m,\phi)\in\mathcal{R}^{\Phi}(n^{\Phi},N^{\Phi},H,H_{p},\mathcal{C})\setminus\mathcal{C}_{0}(n^{\Phi}):\phi\leq
h$.

###### Proof

Let
$(m,\phi)\in\mathcal{R}^{\Phi}(n^{\Phi},N^{\Phi},H,H_{p},\mathcal{C})\setminus\mathcal{C}_{0}(n^{\Phi})$.
It must then hold that
$\exists(m^{\prime},\phi)\in\mathcal{C}(n^{\Phi}_{\alpha})\setminus\mathcal{C}_{0}(n^{\Phi}_{\alpha})$.
Since
$\forall(m^{\prime},\phi)\in\mathcal{C}(n^{\Phi}_{\alpha})\setminus\mathcal{C}_{0}(n^{\Phi}_{\alpha}):\phi\leq
h$, it follows that $\phi\leq h$.

Let
$(m,\phi)\in\mathcal{C}_{0}(n^{\Phi})\setminus\mathcal{R}^{\Phi}(n^{\Phi},N^{\Phi},H,H_{p},\mathcal{C})$.
It must then hold that
$\exists(m^{\prime},\phi)\in\mathcal{C}_{0}(n^{\Phi}_{\alpha})\setminus\mathcal{C}(n^{\Phi}_{\alpha})$.
Since
$\forall(m^{\prime},\phi)\in\mathcal{C}_{0}(n^{\Phi}_{\alpha})\setminus\mathcal{C}(n^{\Phi}_{\alpha}):\phi\leq
h$, it follows that $\phi\leq h$.

###### Lemma 9

Let $n^{\Phi}$ be a marking-sensitive vertex input node in some marking-
sensitive RETE net $(N^{\Phi},p^{\Phi})$. Let $\mathcal{C}_{0}$ and
$\mathcal{C}$ furthermore be configurations for $(N^{\Phi},p^{\Phi})$ such
that $\mathcal{C}_{0}$ is consistent for $n^{\Phi}$. It then holds for host
graph $H$ and partial host graph $H_{p}$ that
$\mathcal{R}^{\Phi}(n^{\Phi},N^{\Phi},H,H_{p},\mathcal{C})=\mathcal{C}_{0}(n^{\Phi})$.

###### Proof

Follows trivially from the semantics of the marking-sensitive vertex input
node.

###### Lemma 10

Let $n^{\Phi}$ be a marking filter node with dependency $n^{\Phi}_{\alpha}$ in
a marking-sensitive RETE net $(N^{\Phi},p^{\Phi})$. Let $\mathcal{C}_{0}$ and
$\mathcal{C}$ furthermore be configurations for $(N^{\Phi},p^{\Phi})$ such
that $\mathcal{C}_{0}$ is consistent for $n^{\Phi}$ and it holds that
$\forall(m,\phi)\in\mathcal{C}_{0}(n^{\Phi}_{\alpha})\setminus\mathcal{C}(n^{\Phi}_{\alpha}):\phi\leq
h$ and
$\forall(m,\phi)\in\mathcal{C}(n^{\Phi}_{\alpha})\setminus\mathcal{C}_{0}(n^{\Phi}_{\alpha}):\phi\leq
h$. It then holds for host graph $H$ and partial host graph $H_{p}$ that
$\forall(m,\phi)\in\mathcal{C}_{0}(n^{\Phi})\setminus\mathcal{R}^{\Phi}(n^{\Phi},N^{\Phi},H,H_{p},\mathcal{C}):\phi\leq
h$ and
$\forall(m,\phi)\in\mathcal{R}^{\Phi}(n^{\Phi},N^{\Phi},H,H_{p},\mathcal{C})\setminus\mathcal{C}_{0}(n^{\Phi}):\phi\leq
h$.

###### Proof

Let
$(m,\phi)\in\mathcal{R}^{\Phi}(n^{\Phi},N^{\Phi},H,H_{p},\mathcal{C})\setminus\mathcal{C}_{0}(n^{\Phi})$.
It must then hold that
$\exists(m^{\prime},\phi)\in\mathcal{C}(n^{\Phi}_{\alpha})\setminus\mathcal{C}_{0}(n^{\Phi}_{\alpha})$.
Since
$\forall(m^{\prime},\phi)\in\mathcal{C}(n^{\Phi}_{\alpha})\setminus\mathcal{C}_{0}(n^{\Phi}_{\alpha}):\phi\leq
h$, it follows that $\phi\leq h$.

Let
$(m,\phi)\in\mathcal{C}_{0}(n^{\Phi})\setminus\mathcal{R}^{\Phi}(n^{\Phi},N^{\Phi},H,H_{p},\mathcal{C})$.
It must then hold that
$\exists(m^{\prime},\phi)\in\mathcal{C}_{0}(n^{\Phi}_{\alpha})\setminus\mathcal{C}(n^{\Phi}_{\alpha})$.
Since
$\forall(m^{\prime},\phi)\in\mathcal{C}_{0}(n^{\Phi}_{\alpha})\setminus\mathcal{C}(n^{\Phi}_{\alpha}):\phi\leq
h$, it follows that $\phi\leq h$.

###### Lemma 11

Let $H$ a graph, $H_{p}\subseteq H$, $(N,p)$ a well-formed RETE net with join-
tree height $h\geq 1$, $\psi\in\overline{\mathbb{N}}$ such that $\psi\geq h$,
and $(X^{\Phi},p^{\Phi}_{X})$ a modular extension of
$(N^{\Phi},p^{\Phi})=localize((N,p))=(N^{\Phi}_{\bowtie}\cup N^{\Phi}_{l}\cup
N^{\Phi}_{r}\cup RPS_{l}\cup RPS_{r},p^{\Phi})$, with
$(N^{\Phi}_{l},p^{\Phi}_{l})=localize((N_{l},p_{l}))$ and
$(N^{\Phi}_{r},p^{\Phi}_{r})=localize((N_{r},p_{r}))$, where $p_{l}$ is the
left dependency of the join node $p$ with associated subtree $N_{l}$ and
$p_{r}$ is the right dependency of $p$ with associated subtree $N_{r}$. Let
$\mathcal{C}_{0}$ and $\mathcal{C}_{1}$ furthermore be configurations for
$(X^{\Phi},p^{\Phi}_{X})$ such that with respect to $H$, $\mathcal{C}_{0}$ is
consistent for all nodes in $V^{N^{\Phi}}$, $\mathcal{C}_{1}$ is consistent
for all nodes in $V^{N^{\Phi}}\setminus\\{p^{\Phi}\\}$, and it holds that
$\forall(m,\phi)\in(\mathcal{C}_{0}(n^{\Phi}_{l})\setminus\mathcal{C}_{1}(n^{\Phi}_{l}))\cup(\mathcal{C}_{1}(n^{\Phi}_{l})\setminus\mathcal{C}_{0}(n^{\Phi}_{l})):\phi\leq\psi$
and
$\forall(m,\phi)\in(\mathcal{C}_{0}(n^{\Phi}_{r})\setminus\mathcal{C}_{1}(n^{\Phi}_{r}))\cup(\mathcal{C}_{1}(n^{\Phi}_{r})\setminus\mathcal{C}_{0}(n^{\Phi}_{r})):\phi\leq
h$. It then holds for
$\mathcal{C}_{2}=execute(p^{\Phi},X^{\Phi},H,H_{p},\mathcal{C}_{1})$ that
$\forall(m,\phi)\in(\mathcal{C}_{0}(p^{\Phi})\setminus\mathcal{C}_{2}(p^{\Phi}))\cup(\mathcal{C}_{2}(p^{\Phi})\setminus\mathcal{C}_{0}(p^{\Phi})):\phi\leq\psi$.

###### Proof

Let $(m,\phi)$ be a tuple in
$\mathcal{C}_{0}(p^{\Phi})\setminus\mathcal{C}_{2}(p^{\Phi})$. Because
$\mathcal{C}_{0}$ is consistent for $p^{\Phi}$, there must be tuples
$(m_{l},\phi_{l})\in\mathcal{C}_{0}(p^{\Phi}_{l})$ and
$(m_{r},\phi_{r})\in\mathcal{C}_{0}(p^{\Phi}_{r})$ with
$m_{l}|_{Q_{\cap}}=m_{r}|_{Q_{\cap}}$, where
$[\bowtie_{Q_{\cap}}]^{\Phi}=p^{\Phi}$ and $max(\phi_{l},\phi_{r})=\phi$.
Since $(m,\phi)\notin\mathcal{C}_{2}(p^{\Phi})$, it must also hold that
$(m_{l},\phi_{l})\notin\mathcal{C}_{1}(p^{\Phi}_{l})$ or
$(m_{r},\phi_{r})\notin\mathcal{C}_{1}(p^{\Phi}_{r})$.

_Case 1_ : We assume that
$(m_{l},\phi_{l})\notin\mathcal{C}_{1}(p^{\Phi}_{l})$ and
$(m_{r},\phi_{r})\in\mathcal{C}_{1}(p^{\Phi}_{r})$. If $\phi_{l}\geq\phi_{r}$,
it immediately follows that $\phi\leq\psi$. If $\phi_{l}<\phi_{r}$, by Lemma 3
and $\mathcal{C}_{1}$ being consistent for all nodes in
$V^{N^{\Phi}}\setminus\\{p^{\Phi}\\}$, it follows that
$\exists(m_{l}^{\prime},\phi_{l}^{\prime})\in\mathcal{C}_{1}(p^{\Phi}_{l}):m_{l}^{\prime}|_{Q_{\cap}}=m_{r}|_{Q_{\cap}}$.
Due to Lemma 12 and since
$\forall(m^{\prime},\phi^{\prime})\in\mathcal{C}_{1}(n^{\Phi}_{l})\setminus\mathcal{C}_{0}(n^{\Phi}_{l}):\phi^{\prime}\leq\psi$,
it must then follow that $\phi_{r}\leq\psi$, since otherwise, it would follow
that $(m,\phi)\in\mathcal{C}_{2}(p^{\Phi})$, which is a contradiction.

Case 2: We assume that $(m_{l},\phi_{l})\in\mathcal{C}_{1}(p^{\Phi}_{l})$ and
$(m_{r},\phi_{r})\notin\mathcal{C}_{1}(p^{\Phi}_{r})$. Analogously to Case 1,
it then follows that $\phi\leq\psi$.

Case 3: We assume that $(m_{l},\phi_{l})\notin\mathcal{C}_{1}(p^{\Phi}_{l})$
and $(m_{r},\phi_{r})\notin\mathcal{C}_{1}(p^{\Phi}_{r})$. In this case, since
$\forall(m^{\prime},\phi^{\prime})\in\mathcal{C}_{0}(n^{\Phi}_{l})\setminus\mathcal{C}_{1}(n^{\Phi}_{l}):\phi^{\prime}\leq\psi$
and
$\forall(m^{\prime},\phi^{\prime})\in\mathcal{C}_{0}(n^{\Phi}_{r})\setminus\mathcal{C}_{1}(n^{\Phi}_{r}):\phi^{\prime}\leq\psi$,
it immediately follows that $\phi\leq\psi$.

It thus follows that $\phi\leq\psi$.

Let $(m,\phi)$ be a tuple in
$\mathcal{C}_{2}(p^{\Phi})\setminus\mathcal{C}_{0}(p^{\Phi})$. It then follows
that there must be tuples $(m_{l},\phi_{l})\in\mathcal{C}_{1}(p^{\Phi}_{l})$
and $(m_{r},\phi_{r})\in\mathcal{C}_{1}(p^{\Phi}_{r})$ with
$m_{l}|_{Q_{\cap}}=m_{r}|_{Q_{\cap}}$, where
$[\bowtie_{Q_{\cap}}]^{\Phi}=p^{\Phi}$ and $max(\phi_{l},\phi_{r})=\phi$.
Since $(m,\phi)\notin\mathcal{C}_{0}(p^{\Phi})$, it must also hold that
$(m_{l},\phi_{l})\notin\mathcal{C}_{0}(p^{\Phi}_{l})$ or
$(m_{r},\phi_{r})\notin\mathcal{C}_{0}(p^{\Phi}_{r})$..

Case 1: We assume that $(m_{l},\phi_{l})\notin\mathcal{C}_{0}(p^{\Phi}_{l})$
and $(m_{r},\phi_{r})\in\mathcal{C}_{0}(p^{\Phi}_{r})$. If
$\phi_{l}\geq\phi_{r}$, it immediately follows that $\phi\leq\psi$. If
$\phi_{l}<\phi_{r}$, by Lemma 3 and $\mathcal{C}_{1}$ being consistent for all
nodes in $V^{N^{\Phi}}\setminus\\{p^{\Phi}\\}$, it follows that
$\exists(m_{l}^{\prime},\phi_{l}^{\prime})\in\mathcal{C}_{1}(p^{\Phi}_{l}):m_{l}^{\prime}|_{Q_{\cap}}=m_{r}|_{Q_{\cap}}$.
Due to Lemma 12 and since
$\forall(m^{\prime},\phi^{\prime})\in\mathcal{C}_{0}(n^{\Phi}_{l})\setminus\mathcal{C}(n^{\Phi}_{l}):\phi^{\prime}\leq\psi$,
it must then follow that $\phi\leq\psi$, since otherwise, it would follow that
$(m,\phi)\in\mathcal{C}_{0}(p^{\Phi})$, which is a contradiction.

Case 2: We assume that $(m_{l},\phi_{l})\in\mathcal{C}_{0}(p^{\Phi}_{l})$ and
$(m_{r},\phi_{r})\notin\mathcal{C}_{0}(p^{\Phi}_{r})$. Analogously to Case 1,
it then follows that $\phi\leq\psi$.

Case 3: We assume that $(m_{l},\phi_{l})\in\mathcal{C}_{0}(p^{\Phi}_{l})$ and
$(m_{r},\phi_{r})\in\mathcal{C}_{0}(p^{\Phi}_{r})$. In this case, since
$\forall(m^{\prime},\phi^{\prime})\in\mathcal{C}_{1}(n^{\Phi}_{l})\setminus\mathcal{C}_{0}(n^{\Phi}_{l}):\phi^{\prime}\leq\psi$
and
$\forall(m^{\prime},\phi^{\prime})\in\mathcal{C}_{1}(n^{\Phi}_{r})\setminus\mathcal{C}_{0}(n^{\Phi}_{r}):\phi^{\prime}\leq\psi$,
it immediately follows that $\phi\leq\psi$

It thus follows that $\phi\leq\psi$.

###### Lemma 12

Let $(N,p)$ be a well-formed RETE net and $(X^{\Phi},p^{\Phi}_{X})$ a modular
extension of $(N^{\Phi},p^{\Phi})=localize((N,p))$. It then holds for any
configuration $\mathcal{C}$ of $(X^{\Phi},p^{\Phi}_{X})$ that is consistent
for all nodes in $V^{N^{\Phi}}$ that
$\forall(m,\phi),(m^{\prime},\phi^{\prime})\in\mathcal{C}(p^{\Phi}):m=m^{\prime}\Rightarrow\phi=\phi^{\prime}$.

###### Proof

We show the correctness of the lemma via induction over the height $h$ of the
join tree $N$.

In the base case of $h=0$, $(N^{\Phi},p^{\Phi})=(LNS(p),[\cup]^{\Phi})$. By
the semantics of $[\cup]^{\Phi}$ and $\mathcal{C}$ being consistent for
$[\cup]^{\Phi}$, it follows that