# On-The-Fly Static Analysis via Dynamic Bidirected Dyck Reachability

Shankaranarayanan Krishna  0000-0003-0925-398X IIT BombayIndia
<EMAIL_ADDRESS>,  Aniket Lal  IIT BombayIndia
<EMAIL_ADDRESS>,  Andreas Pavlogiannis  0000-0002-8943-0722 Aarhus
UniversityAabogade 34Aarhus8200Denmark<EMAIL_ADDRESS>and  Omkar Tuppe
IIT BombayIndia<EMAIL_ADDRESS>
###### Abstract.

Dyck reachability is a principled, graph-based formulation of a plethora of
static analyses. Bidirected graphs are used for capturing dataflow through
mutable heap data, and are usual formalisms of demand-driven points-to and
alias analyses. The best (offline) algorithm runs in $O(m+n\cdot\alpha(n))$
time, where $n$ is the number of nodes and $m$ is the number of edges in the
flow graph, which becomes $O(n^{2})$ in the worst case.

In the everyday practice of program analysis, the analyzed code is subject to
continuous change, with source code being added and removed. On-the-fly static
analysis under such continuous updates gives rise to _dynamic Dyck
reachability_ , where reachability queries run on a dynamically changing
graph, following program updates. Naturally, executing the _offline_ algorithm
in this _online_ setting is inadequate, as the time required to process a
single update is prohibitively large.

In this work we develop a novel dynamic algorithm for bidirected Dyck
reachability that has $O(n\cdot\alpha(n))$ worst-case performance per update,
thus beating the $O(n^{2})$ bound, and is also optimal in certain settings. We
also implement our algorithm and evaluate its performance on on-the-fly data-
dependence and alias analyses, and compare it with two best known
alternatives, namely (i) the optimal offline algorithm, and (ii) a fully
dynamic Datalog solver. Our experiments show that our dynamic algorithm is
consistently, and by far, the top performing algorithm, exhibiting speedups in
the order of 1000X. The running time of each update is almost always
unnoticeable to the human eye, making it ideal for the on-the-fly analysis
setting.

CFL reachability, static analysis, dynamic algorithms

††journal: PACMPL††journalnumber: POPL††journalyear: 2024††ccs: Software and
its engineering Software verification and validation††ccs: Theory of
computation Theory and algorithms for application domains††ccs: Theory of
computation Program analysis

##  1\. Introduction

Dyck reachability in static analysis. Dyck reachability is an elegant and
widespread graph-based formulation of a plethora of static analyses. The
reachability problem is phrased on labeled directed graphs $G=(V,E)$, where
$V$ is a set of nodes and $E$ is a set of edges, labeled with opening and
closing parenthesis symbols. Given two nodes $u$ and $v$, the task is to
determine whether $v$ is reachable from $u$ by means of a path $P$, such that
the sequence of labels of the edges of $P$ produce a parenthesis string that
is properly balanced (Yannakakis, 1990). In the static analysis domain, $G$
serves as the program model, where nodes represent basic program constructs
such as program variables, pointers, or statements, and edges capture data
flow between these constructs. Effectively, program executions carrying data
flow between distant program points are captured by paths in $G$. Naturally,
as $G$ is an approximate model of the program, it may have paths that do not
correspond to any valid program execution, leading to spurious data flow and
thus to false positive warnings. In order to increase the precision of the
analysis, parenthesis symbols are used to model certain restrictions in the
data flow, such as sensitivity to calling contexts and field accesses (Reps,
1997, 2000; Späth et al., 2019). Focusing on Dyck reachability on $G$ (as
opposed to plain reachability) thus filters out paths that are guaranteed to
not correspond to valid program executions, thereby increasing the precision
of the analysis.

As a modeling formalism, Dyck reachability strikes a remarkable balance
between simplicity and expressiveness, and has been used to drive a wide range
of static analyses, such as interprocedural data-flow analysis (Reps et al.,
1995), slicing (Reps et al., 1994), shape analysis (Reps, 1995a), impact
analysis (Arnold, 1996), type-based flow analysis (Rehof and Fähndrich, 2001),
taint analysis (Huang et al., 2015), data-dependence analysis (Tang et al.,
2017), alias/points-to analysis (Lhoták and Hendren, 2006; Zheng and Rugina,
2008; Xu et al., 2009), to only name a few. In practice, widely-used analysis
tools, such as Wala (Wal, 2003) and Soot (Bodden, 2012) equip Dyck-
reachability techniques to perform the analysis. From a complexity
perspective, answering a single Dyck-reachability query “is $v$ reachable from
$u$?” takes $O(n^{3})$ time, where $n$ is the number of nodes of $G$, and
although some slight improvements are possible (Chaudhuri, 2008), this cubic
dependency is often considered prohibitive (Heintze and McAllester, 1997).

Bidirectedness. One important and practically motivated variant of Dyck
reachability is that of _bidirectedness_. Intuitively, a bidirected graph $G$
has the property that every (directed) edge is present in both directions with
complementary labels: an edge $x\xrightarrow{(}y$ is present in $G$ if and
only if $y\xrightarrow{)}x$ is also present in $G$. Bidirectedness makes
reachability an _equivalence relation_ : if $v$ is reachable from $u$ via a
properly balanced path, the same path backwards (i.e., from $v$ to $u$) is
also properly balanced, thereby witnessing the reachability of $u$ from $v$.
Thus, the nodes of $G$ can be partitioned into equivalence classes of inter-
reachable nodes, called _Dyck Strongly Connected Components_ (or _DSCCs_ , for
short). For example, in Figure 1 the bidirected graph $G$ (top right)
corresponds to the input program, and nodes $c$ and $d$ are inter-reachable
via the paths $c\xrightarrow{L}f\xrightarrow{\overline{L}}d$ and
$d\xrightarrow{L}f\xrightarrow{\overline{L}}c$, and thus they belong to the
same DSCC.

From a _semantics_ perspective, bidirectedness has been a standard approach to
handle mutable heap data (Sridharan and Bodík, 2006; Xu et al., 2009; Lu and
Xue, 2019; Zhang and Su, 2017) – though it can sometimes be relaxed for read-
only accesses (Milanova, 2020), and the de-facto formulation of demand-driven
points-to analyses (Sridharan et al., 2005; Zheng and Rugina, 2008; Shang et
al., 2012; Yan et al., 2011; Vedurada and Nandivada, 2019). From an
_algorithmic_ perspective, bidirectedness allows Dyck reachability to be
computed more efficiently (Yuan and Eugster, 2009; Zhang et al., 2013), with
the fastest algorithm running in $O(m+n\cdot\alpha(n))$ time (Chatterjee et
al., 2018), where $n$ is the number of nodes, $m$ is the number of edges, and
$\alpha(n)$ is the inverse Ackermann function111For all practical purposes,
$\alpha(n)\leq 5$, i.e., the function behaves as a constant.. Compared to the
cubic bound of directed Dyck reachability, bidirectedness thus allows for a
large speedup in the order of $n^{2}$. Due to this algorithmic benefit,
bidirectedness also serves as an overapproximation to directed reachability,
and has been suggested as a mechanism to speed up challenging static analysis
and verification problems (Li et al., 2020; Ganardi et al., 2022b; Ganardi et
al., 2022a).

⬇

class ATree {

ATree L;

ATree R;

}

void main(){

ATree c,d,e;

ATree f,g,h;

g.L=e;

$\,-\,\,\,$d=f.L; $2$

h.L=f;

f.L=c;

$\,+\,\,\,$h=d.R; $1$

c.R=g;

e=f.L

}

after
insert(d,h,$\overline{R}$)$c$$d$$e$$f$$g$$h$$\overline{L}$$\overline{L}$$\overline{L}$$\overline{R}$$\overline{L}$$\overline{L}$after
delete(f,d,$\overline{L}$)$c$$d$$e$$f$$g$$h$$\overline{L}$$\overline{L}$$\overline{L}$$\overline{R}$$\overline{R}$$\overline{L}$$\overline{L}$$c$$d$$e$$f$$g$$h$$\overline{L}$$\overline{L}$$\overline{R}$$\overline{R}$$\overline{L}$$\overline{L}$

Figure 1. An input program (left), to which two updates are made, an insertion
$1$ and a deletion $2$ , and the corresponding flow graphs for field-sensitive
alias analysis after each update (right). The edges are labeled
$L,\overline{L},R,\overline{R}$ and correspond to the fields of ATree. For
notational convenience, we only draw the edges labeled with closing
parentheses, the reverse edges with opening parentheses are implied by
bidirectedness. On the initial program (before $1$ and $2$ ), bidirected Dyck-
reachability reports four DSCCs: $\\{c,d,e\\},\\{f\\},\\{g\\},$ and $\\{h\\}$.
The addition $1$ inserts the edge $d\xrightarrow{\overline{R}}h$ in the flow
graph, which now has two DSSCs:$\\{c,d,e,f\\}$ and $\\{g,h\\}$. The deletion
$2$ deletes the edge $f\xrightarrow{\overline{L}}d$ in the flow graph, leaving
it with five DSCCs: $\\{c,e\\},\\{d\\},\\{f\\},\\{g\\},$ and $\\{h\\}$.

On-the-fly static analysis. In the everyday practice of program analysis, the
analyzed code base is not static but rather subject to perpetual change;
source-code lines are added and removed following patches, new modules and
libraries, and bug fixes. In an even more demanding setting, lightweight
static analyzers are embedded inside the IDE and run on-the-fly, so as to
enable faster, more robust and more productive development. As has been
observed in the literature, a major computational challenge in static analyses
is in their apparent inability to adapt to these continuous changes
efficiently (Zadeck, 1984; Arzt and Bodden, 2014). Existing works approach
this challenge mostly by tweaking the offline analyses and adapting them to
the dynamic setting. Typically, such adaptations only focus on incremental
updates (i.e., only the addition of code lines) and are based on some form of
caching (Burke and Ryder, 1990; Arzt and Bodden, 2014; Szabó et al., 2016; Liu
et al., 2019; Pacak et al., 2020). Decremental updates (i.e., the deletion of
code lines) is much more difficult, intuitively, due to the fixpoint nature of
static analyses. As such, analyses that fully follow all code changes (both
incremental and decremental) thus far offer no efficiency guarantees. This
paper tackles this challenge of on-the-fly, full dynamic analyses formulated
as bidirected Dyck reachability in a rigorous and provably efficient way.
Figure 1 illustrates the use of dynamic bidirected Dyck reachability for on-
the-fly field-sensitive alias analysis on a small example.

Our contributions. We consider the problem of maintaining the DSCCs of a
dynamic graph $G$, representing the on-the-fly static analysis of a program,
where source code changes are both incremental and decremental. In particular,
an incremental update inserts an edge in $G$, while a decremental update
deletes edges from $G$, and the task is to restore the DSCCs of $G$ after each
such update. To this end, we develop an algorithm
$\operatorname{DynamicAlgo}$, with guarantees as stated in the following
theorem.

###### Theorem 1.1.

Given a bidirected graph $G$ of $n$ nodes, $\operatorname{DynamicAlgo}$
correctly maintains the DSCCs of $G$ across edge insertions and edge
deletions, and uses at most $O(n\cdot\alpha(n))$ time for each update.

Observe that in general this is much faster than the optimal offline algorithm
of (Chatterjee et al., 2018), as the latter spends time that is at least
proportional to the number of edges $m$ (which can be up to
$m=\Theta(n^{2})$). On the other hand, it can be easily shown that a single
update (either edge insertion or deletion) can affect $\Theta(n)$ DSCCs. Thus
$\operatorname{DynamicAlgo}$ is effectively optimal, at least in the natural
setting where DSCCs have to be explicitly maintained at all times.

We have implemented our dynamic algorithm and evaluated its performance on
Dyck graphs that arise on data-dependence analysis and alias analysis, on
standard benchmarks. Our experiments show that our dynamic algorithm is
consistently, and by far, the top performing algorithm compared to (i) the
optimal offline algorithm for the problem, and (ii) a fully dynamic Datalog
solver, arguably the two most relevant approaches to our problem setting. In
particular, our dynamic algorithm exhibits speedups that are between
100X-1000X for data-dependence analysis and 1000X for alias analysis (which is
also the more demanding of the two), compared to the best alternative.
Although its theoretical worst-case complexity is linear in $n$, its average
running time is barely (if at all) noticeable for all practical purposes,
making it suitable for the on-the-fly analysis setting that runs continuously
during development.

A note on earlier approaches. Dynamic bidirected Dyck reachability was studied
recently in (Li et al., 2022). To this end, that work claims a dynamic
algorithm with $O(n\cdot\alpha(n))$ running time per update operation,
similarly to our Theorem 1.1. Unfortunately, both the complexity and the
correctness of (Li et al., 2022) overlook certain cases. In particular, that
algorithm exhibits $\Omega(n^{2})$ running time, as opposed to the claimed
(nearly) linear bound. This quadratic behavior arises even on sparse graphs
(i.e., with $m=O(n)$ edges), for which the vanilla offline algorithm runs in
$O(n\cdot\alpha(n))$ time. Hence on such graphs, processing a single line
deletion in the source code is $n$ times slower than performing the whole
analysis from scratch. Moreover, that algorithm also suffers from correctness
issues, as it fails to detect that certain nodes become unreachable after
updates. In such cases, the on-the-fly static analysis returns wrong results.
We provide further details in Appendix B.

Intuition behind our approach. In high-level, our approach works as follows.
First, we observe that the component graph (i.e., the graph with a single node
representing each DSCC) is sparse. Each edge insertion can then be handled by
executing the offline algorithm of (Chatterjee et al., 2018) not from scratch,
but directly on the already constructed component graph, yielding
$O(n\cdot\alpha(n))$ running time. The main difficulty arises in edge
deletions, as each deletion seemingly requires repeating all the computation
from scratch, i.e., operating on the initial graph, which might be dense and
thus incur $O(n^{2})$ running time. We leverage techniques from dynamic
undirected connectivity, together with some sparsification ideas that are
specific to our richer bidirected setting, to start the recomputation not from
scratch, but from a suitable preliminary component graph, called the _primary
component graph_ , that is already sparse, thereby recovering the
$O(n\cdot\alpha(n))$ running time. Maintaining the primary component graph
efficiently is the main technical challenge.

##  2\. Preliminaries

In this section we develop general notation on labeled graphs, Dyck
reachability, and fully-dynamic reachability queries. As this is somewhat
standard material, our exposition follows closely that of related works (e.g.,
(Zhang et al., 2013; Chatterjee et al., 2018; Kjelstrøm and Pavlogiannis,
2022)).

###  2.1. Dyck Reachability on Bidirected Graphs

Dyck Languages. Hereinafter, we fix a natural number $k\in\mathbb{N}$. Let
$[k]$ denote $\\{1,\dots,k\\}$. A Dyck alphabet is a set
$\Sigma=\\{\alpha_{i},\overline{\alpha}_{i}\\}_{i\in[k]}$ of $k$ matched
symbols, usually referred to as parentheses, where
$\operatorname{Open}(\Sigma)=\\{\alpha_{i}\\}_{i\in k}$ and
$\operatorname{Close}(\Sigma)=\\{\overline{\alpha}_{i}\\}_{i\in k}$ are the
sets of opening parenthesis symbols and closing parenthesis symbols of
$\Sigma$, respectively222We use Greek letters such as $\alpha,\beta$ to
represent opening parenthesis symbols, and
$\overline{\alpha},\overline{\beta}$ for their matching closing parentheses..
The Dyck language $\mathcal{D}$ is the set of strings over $\Sigma^{*}$
produced by the following grammar with initial non-terminal $\mathcal{I}$:

$\mathcal{I}\to\mathcal{I}\leavevmode\nobreak\ \mathcal{I}\leavevmode\nobreak\
|\leavevmode\nobreak\
\alpha_{1}\mathcal{I}\overline{\alpha}_{1}\leavevmode\nobreak\
|\leavevmode\nobreak\ \cdots\leavevmode\nobreak\ |\leavevmode\nobreak\
\alpha_{k}\mathcal{I}\overline{\alpha}_{k}\leavevmode\nobreak\
|\leavevmode\nobreak\ \epsilon$

For example,
$\alpha_{1}\alpha_{2}\overline{\alpha}_{2}\alpha_{3}\overline{\alpha}_{3}\overline{\alpha}_{1}\in\mathcal{D}$,
but
$\alpha_{1}\alpha_{2}\alpha_{3}\overline{\alpha}_{3}\overline{\alpha}_{1}\overline{\alpha}_{2}\not\in\mathcal{D}$.
Finally, given a string $\sigma=\gamma_{1}\dots\gamma_{m}\in\Sigma^{*}$, we
let
$\overline{\sigma}=\overline{\gamma}_{1}\dots\overline{\gamma}_{m}\in\Sigma^{*}$,
where $\overline{\gamma}_{i}$ is a closing parenthesis symbol if $\gamma_{i}$
is an opening parenthesis symbol, and vice versa. For example, if
$\sigma=\alpha_{1}\alpha_{2}\overline{\alpha}_{2}\alpha_{3}\overline{\alpha}_{3}\overline{\alpha}_{1}$
then
$\overline{\sigma}=\overline{\alpha}_{1}\overline{\alpha}_{2}\alpha_{2}\overline{\alpha}_{3}\alpha_{3}\alpha_{1}$.

Graphs and Dyck reachability. We consider labeled directed graphs $G=(V,E)$
where $V$ is a set of nodes and $E$ is a set of labeled edges $(u,v,l)$, where
$u,v\in V$ and $l\in\Sigma\cup\\{\epsilon\\}$. For notational convenience,
given an edge $e$, we will refer to its label as $\lambda(e)$. We occasionally
are not interested in the label of an edge, in which case we will simply
denote it with its endpoints, e.g., $e=(u,v)$. We also adopt the pictorial
notation $u\xrightarrow{l}v$ to denote the existence of an edge $(u,v,l)$, and
write $u\xrightarrow{l}\cdot$ to denote the existence of an edge outgoing $u$
and labeled with $l$. Given a set $X$, we sometimes write $u\xrightarrow{l}X$
to denote that there exists some $v\in X$ such that $u\xrightarrow{l}v$. We
also use similar notation for incoming, instead of outgoing edges (e.g.,
$X\xrightarrow{l}v$). A path is a sequence of edges
$P=(u_{1},v_{1},l_{1}),\dots,(u_{r},v_{r},l_{r})$ such that, for each
$i\in[r-1]$, we have $u_{i+1}=v_{i}$. The label of $P$ is
$\lambda(P)=l_{1}\dots l_{r}$, that is, it is the concatenation of the labels
of its edges. A path can also be an empty sequence of edges, in which case its
label is $\epsilon$. We often write $P\colon u\rightsquigarrow v$ to denote a
path from node $u$ to node $v$. Naturally, we say that $v$ is reachable from
$u$ if such a path exists. Moreover, we say that $v$ is Dyck-reachable from
$u$ if there exists a path $P\colon u\rightsquigarrow v$ such that
$\lambda(P)\in\mathcal{D}$, in which case we call $P$ a Dyck path.

In alignment to existing literature ((Zhang et al., 2013; Chatterjee et al.,
2018)), we consider that the number of parenthesis types is constant compared
to the size of $G$ (i.e., $k=O(1)$). From a theoretical standpoint this is not
an oversimplification, as any Dyck graph with arbitrary $k$ can be transformed
to one with $k=O(1)$, while preserving the reachability relationships (see
e.g., (Chistikov et al., 2022)).

Bidirected Graphs and Dyck SCCs. We call a graph $G=(V,E)$ bidirected if every
edge in $E$ appears in both ways with complementary labels. Formally, let
$\overline{\epsilon}=\epsilon$, and we have:

$(u,v,s)\in E\qquad\iff\qquad(v,u,\overline{s})\in E$

Bidirectedness turns reachability into an equivalence relation, similarly to
plain undirected graphs. To realize this, notice that every path $P\colon
u\rightsquigarrow v$ has a reverse version $\overline{P}\colon
v\rightsquigarrow u$ with $\lambda(P)=\lambda(\overline{P})$. Hence, if $P$
witnesses the Dyck reachability of $v$ from $u$, then $\overline{P}$ witnesses
the Dyck reachability of $u$ from $v$. Naturally, the nodes of $G$ are
partitioned into strongly-connected components (SCCs), which are maximal sets
of pairwise Dyck-inter-reachable nodes. We will call such sets Dyck strongly
connected components, or DSCCs, for short. Note that, in contrast to standard
SCCs, paths witnessing the Dyck reachability of two nodes in the same DSCC
might have to traverse nodes outside the DSCC. For example, in Figure 1 (top
right), the paths witnessing the Dyck reachability of nodes $c$ to $d$ and $d$
to $c$ go via node $f$, which is outside the DSCC $\\{c,d\\}$. Given a node
$u$, we let $\operatorname{DSCC}(u)$ be the DSCC in which $u$ appears.

For notational convenience, hereinafter we represent bidirected graphs by only
explicitly denoting their edges labeled with closing parentheses, with the
understanding that the reverse edges (labeled with an opening parentheses) are
also present. In our figures, when a graph contains edges of different labels,
we color-code the edges for easier visual representation.

The efficiency of DSCC computation. In Dyck-reachability formulations of
static analyses, the analysis queries are phrased as Dyck-reachability queries
in the underlying graph. As we have seen above, the nodes of bidirected graphs
are partitioned into DSCCs. Thus, reachability queries can be handled by first
computing these DSCCs. Then, given a reachability query on two nodes $u,v$, we
answer that they are inter-reachable iff they are found in the same DSCC,
which costs a simple lookup of constant time. Computing Dyck reachability on
general (non-bidirected) graphs takes cubic time $O(n^{3})$ even for a single
pair. On the other hand, it is known that the DSCCs of bidirected graphs can
be computed efficiently.

###### Theorem 2.1 ((Chatterjee et al., 2018)).

Given a graph $G$ of $n$ nodes and $m$ edges, the DSCCs of $G$ can be computed
in $O(m+n\cdot\alpha(n))$ time, where $\alpha(n)$ is the inverse Ackermann
function.

###  2.2. Dynamic Reachability

Dynamic reachability on bidirected graphs. As the program source is being
developed, the underlying graph model changes shape due to the addition and
removal of nodes and edges. The goal of the fully dynamic setting is to
maintain Dyck-reachability information on the fly under such changes, so that
analysis queries can be performed fast. More formally, we are processing a
sequence of operations $\mathcal{S}=(o_{1},o_{2},\dots,o_{r})$, where each
operation $o_{i}$ has one of the following types.

  1. (1)

$\operatorname{insert}(u,v,\overline{\alpha})$, which inserts an edge
$u\xrightarrow{\overline{\alpha}}v$ (as well as the implicit inverse edge
$v\xrightarrow{\alpha}u$).

  2. (2)

$\operatorname{delete}(u,v,\overline{\alpha})$, which deletes the edge
$u\xrightarrow{\overline{\alpha}}v$ (as well as the implicit inverse edge
$v\xrightarrow{\alpha}u$).

  3. (3)

$\operatorname{DSCCRepr}(u)$, which returns a representative node of the DSCC
of $u$ that is the same for all nodes $v\in\operatorname{DSCC}(u)$.

This sequence of operations creates a sequence of graphs
$(G_{i}=(V,E_{i}))_{i\in[r]}$, where $G_{1}$ is the initial graph, and
$G_{i+1}$ is obtained from $G_{i}$ by performing the operation $o_{i}$
(naturally, if $o_{i}=\operatorname{DSCCRepr}(u)$ is a query operation,
$G_{i+1}=G_{i}$). Note that we have kept the node set identical across all
$G_{i}$. Indeed, this is a standard approach for studying such problems: we
may simply assume that $V$ contains all nodes that are ever added to the
graph, and instead of deleting a node, we can delete all its adjacent edges.
Finally, the reachability of $v$ from $u$ can be checked with two successive
queries, i.e., testing whether
$\operatorname{DSCCRepr}(u)=\operatorname{DSCCRepr}(v)$.

Although in general there might be a spectrum of trade offs in the time taken
between operations modifying the graph
($\operatorname{insert}(u,v,\overline{\alpha})$,
$\operatorname{delete}(u,v,\overline{\alpha})$) and reachability queries
($\operatorname{DSCCRepr}(u)$), the linear upper bounds we establish here for
updates means that query operations can be done in constant time $O(1)$. This
holds because, in theory, after every update operation we can easily, in
$O(n)$ time (which is within the upper bound we establish for processing the
update operations), retrieve the DSCC of each node to a simple lookup table
that will lead to subsequent queries taking $O(1)$ time each. In practice, of
course, this approach is to be avoided, as dynamic updates cost much less than
$O(n)$ time, hence building the full lookup table causes an unnecessary cost.
Moreover, even without a lookup table, queries cost $O(\alpha(n))$ time, which
is constant for all practical purposes.

Dynamic reachability on undirected graphs. Problems of dynamic reachability
have been studied extensively on plain graphs (i.e., without the restriction
on Dyck paths), both for directed and undirected variants. However, the richer
semantics of Dyck reachability makes the Dyck setting quite more intricate.
Our solution to the problem uses as a black box a data structure for dynamic
reachability on undirected graphs. Although there exist several results in
this direction, Table 1 shows two standard data structures that are relevant
to our work. The one developed in (Eppstein et al., 1997) offers standard
worst-case guarantees for the time to perform each update (i.e.,
inserting/deleting an undirected edge) and query (i.e., obtaining the
component of a node $u$). The one developed in (Holm et al., 2001) offers
amortized guarantees for the respective tasks. That is, some operations might
exceed the stated time bounds, but this excess is balanced in later
operations, so that the average time per operation is the one stated. As we
will see later, we will be using the former technique to establish our bound
in Theorem 1.1, but the latter in our experiments.

Table 1.  Classic results on dynamic undirected reachability.  Reference | Update time | Query time | Guarantee
---|---|---|---
(Eppstein et al., 1997) | $O(\sqrt{n})$ | $O(1)$ | Worst-case
(Holm et al., 2001) | $O(\log^{2}n)$ | $O(\log n)$ | Amortized

##  3\. Efficient Dynamic Bidirected Dyck Reachability

In this section we present our dynamic algorithm for bidirected Dyck
reachability. As this is the main technical section of our paper, we provide
here an outline of its structure to guide the reader.

  1. (1)

In Section 3.1 we present the key algorithmic intuition for solving Dyck
reachability on bidirected graphs, and revisit the offline algorithm for the
problem, as presented in (Chatterjee et al., 2018). Some aspects of the
offline algorithm (in particular, its fixpoint computation) will also be used
later in our dynamic algorithm.

  2. (2)

In Section 3.2 we present the main technical challenges for handling dynamic
updates efficiently, and the key concepts our algorithm uses for handling each
challenge. This section is filled with examples that illustrate how each
concept is used, and what data structure is used to support it.

  3. (3)

In Section 3.3 we present $\operatorname{DynamicAlgo}$ in detail, with
pseudocode followed by a high-level description of each of its blocks. The
pseudocode is also heavy in comments to guide the reader.

  4. (4)

In Section 3.4 we give a step-by-step execution of the algorithm on the
running example of Figure 1.

  5. (5)

Finally, in Section 3.5, we establish the correctness and complexity of
$\operatorname{DynamicAlgo}$. We state its main invariants, together with some
intuition around them and how they are used towards the correctness and
complexity lemmas, while we delegate the proofs to Appendix A.

###  3.1. Offline Reachability

We start with the optimal offline algorithm for computing bidirected Dyck
reachability (Chatterjee et al., 2018), i.e., for obtaining Theorem 2.1. This
will allow us to build some intuition about the problem. Moreover, our data
structure for handling graph updates later will use some components of the
offline algorithm.

Intuitive description. The principle of operation of the algorithm behind
Theorem 2.1 (initially observed in (Zhang et al., 2013)) is as follows. Assume
that we have computed a DSCC $S_{1}$ that has two nodes $u,v\in S_{1}$, and
further, $G$ has two edges $u\xrightarrow{\overline{\alpha}}x$ and
$v\xrightarrow{\overline{\alpha}}y$. Here $u$ and $v$ are not necessarily
distinct, meaning that possibly $u=v$. Then we can conclude that $x$ and $y$
also belong to the same DSCC, witnessed by the path

$x\xrightarrow{\alpha}u\rightsquigarrow v\xrightarrow{\overline{\alpha}}y$

where the intermediate path $u\rightsquigarrow v$ is one witnessing the
reachability of $v$ from $u$ – such a path exists since $u$ and $v$ belong to
the same DSCC. In fact, any node $x^{\prime}$ in the DSCC of $x$ can reach any
node $y^{\prime}$ in the DSCC of $y$, via the path

$x^{\prime}\rightsquigarrow x\xrightarrow{\alpha}u\rightsquigarrow
v\xrightarrow{\overline{\alpha}}y\rightsquigarrow y^{\prime}$

Thus the DSCCs of $x$ and $y$ can be merged into one DSCC $S_{2}$. We can now
repeat the above process to discover Dyck paths that go through $S_{2}$, and
so on, up to a fixpoint. Figure 2 illustrates this process on a small example.

$u$$z$$w$$x$$y$$v$$\overline{\alpha}$$\overline{\alpha}$$\overline{\beta}$$\overline{\beta}$$\overline{\gamma}$$\overline{\gamma}$$u$$z$$w$$x$$y$$v$$\overline{\alpha}$$\overline{\alpha}$$\overline{\beta}$$\overline{\beta}$$\overline{\gamma}$$\overline{\gamma}$$u$$z$$w$$x$$y$$v$$\overline{\alpha}$$\overline{\alpha}$$\overline{\beta}$$\overline{\beta}$$\overline{\gamma}$$\overline{\gamma}$$u$$z$$w$$x$$y$$v$$\overline{\alpha}$$\overline{\alpha}$$\overline{\beta}$$\overline{\beta}$$\overline{\gamma}$$\overline{\gamma}$

Figure 2.  Illustration of the fixpoint computation of DSCCs. Initially, every
node forms its own DSCC. We have $u\xrightarrow{\overline{\alpha}}x$ and
$u\xrightarrow{\overline{\alpha}}y$, forming a DSCC $S_{1}=\\{x,y\\}$,
witnessed by the paths
$x\xrightarrow{\alpha}u\xrightarrow{\overline{\alpha}}y$ and
$y\xrightarrow{\alpha}u\xrightarrow{\overline{\alpha}}x$. In turn, the two
edges $z\xrightarrow{\overline{\beta}}y$ and
$z\xrightarrow{\overline{\beta}}v$ enlarge this DSCC to $S_{1}=\\{x,y,v\\}$.
Finally, the two edges $x\xrightarrow{\overline{\gamma}}z$ and
$v\xrightarrow{\overline{\gamma}}w$ form another DSCC $S_{2}=\\{z,w\\}$.

Algorithm $\operatorname{OfflineAlgo}$. The above insights are made formal in
Algorithm 1, which is an adaptation of the algorithm as appeared initially in
(Chatterjee et al., 2018). The first insight that $\operatorname{OfflineAlgo}$
rests on is that, since DSCCs are equivalence classes that only merge together
during the fixpoint computation, they can be maintained efficiently using a
disjoint-sets data structure that supports
$\operatorname{Union}/\operatorname{Find}$ operations. The second insight is
to use linked lists for storing the edges outgoing each DSCC and labeled with
a given symbol $\overline{\alpha}$. When two DSCCs are merged into one, the
algorithm also merges the corresponding linked lists, which can be done very
efficiently, in $O(1)$ time (using simple pointers). In particular,
$\operatorname{OfflineAlgo}$ performs two big steps. First, it initializes a
disjoint-sets data structure
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}$
and a worklist $\mathcal{Q}$ (function Initialization() in Algorithm 1). Then,
it uses
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}$
and $\mathcal{Q}$ to compute the fixpoint (function Fixpoint() in Algorithm
1), achieving the running time of $O(m+n\cdot\alpha(n))$. As the correctness
and complexity are established in (Chatterjee et al., 2018), we do not re-
establish them here.

Input: A bidirected graph $G=(V,E)$

Output: A
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}$
map of the DSCCs of $G$

1 $\operatorname{Initialization}()$ // Initialize the fixpoint computation

2 $\operatorname{Fixpoint}()$ // Compute the fixpoint

3 function  _Initialization(__)_

4 $\mathcal{Q}\leftarrow$ an empty queue over $V^{*}$ // A worklist over edges
for computing the fixpoint

5
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}\leftarrow$
a map $V\times\operatorname{Close}(\Sigma)\to V^{*}$ as a linked list // The
outgoing edges of each node

6
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}\leftarrow$
a disjoint-sets data structure over $V$

7 foreach  _$u\in V$_ do

8
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}.\operatorname{MakeSet}(u)$
// constructs the singleton set $\\{u\\}$

9 foreach  _label $\overline{\alpha}\in\operatorname{Close}(\Sigma)$_ do

10
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[u][\overline{\alpha}]\leftarrow(v:\leavevmode\nobreak\
(u,v,\overline{\alpha})\in E)$

11 if
_$|{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[u][\overline{\alpha}]|\geq
2$_ then Insert $(u,\overline{\alpha})$ in $\mathcal{Q}$

12 // The two edges must merge their endpoints

13function  _Fixpoint(__)_

14 while  _$\mathcal{Q}$ is not empty_ do // Repeat until fixpoint

15 Extract $(u,\overline{\alpha})$ from $\mathcal{Q}$ // We merge components
connected via $u$’s component

16 if
_$u={\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}.\operatorname{Find}(u)$_
then // $u$ is the root of its component

17
$S\leftarrow\\{{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}.\operatorname{Find}(w):w\in{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[u][\overline{\alpha}]\\}$
// The components to be merged

18 if  _$|S|\geq 2$_ then

19 $x\leftarrow$ some arbitrary element of $S\setminus\\{u\\}$ // $x$ will be
the root of the merged component

20 Make
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}.\operatorname{Union}(S,x)$
// All components merge to $x$’s component

21 foreach  _label $\overline{\beta}\in\operatorname{Close}(\Sigma)$_ do //
Process each label separately

22 foreach  _$v\in S\setminus\\{x\\}$_ do

23 if  _$u\neq v$ or $\overline{\alpha}\neq\overline{\beta}$_ then //
$(v,\overline{\beta})$ is not the $(u,\overline{\alpha})$ we extracted from
$\mathcal{Q}$

24 Move
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[v][\overline{\beta}]$
to
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[x][\overline{\beta}]$
// In $O(1)$ time, using pointers

25

26 else

27 Append $(x)$ to
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[x][\overline{\beta}]$
// All
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[u][\overline{\alpha}]$
merged to a self-loop $x\xrightarrow{\overline{\alpha}}x$

28 if
_$|{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[x][\overline{\beta}]|\geq
2$_ then Insert $(x,\overline{\beta})$ in $\mathcal{Q}$

29 // More components to be merged

30 else

31 Let $x\leftarrow$ the single node in $S$

32 if  _$u\not\in S$ or $|S|=1$_ then
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[u][\overline{\alpha}]\leftarrow(x)$
// $u$’s component now points to $x$’s component

33

34

Algorithm 1 $\operatorname{OfflineAlgo}$

###  3.2. Main Concepts and Intuition

Having outlined the basic algorithm for offline reachability, we now turn our
attention to the data structure for dynamic reachability. In high level, our
data structure will use the same components as $\operatorname{OfflineAlgo}$,
in particular, the representation of DSCCs using the
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}$
data structure, the
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}$
linked lists for storing the outgoing edges of each component, and the
$\operatorname{Fixpoint}()$ function for computing the DSCCs as a fixpoint
after every graph update. However, instead of starting the computation from
scratch,
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}$
and
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}$
(as well as the worklist $\mathcal{Q}$ of $\operatorname{Fixpoint}()$) will be
at a state that represent some DSCCs that are guaranteed to exist in the
updated graph, and thus need not be recomputed. The key technical challenge we
have to solve is in computing a non-trivial such state, and doing so
efficiently.

In this section we introduce the main concepts of our dynamic algorithm and
provide the necessary intuition around them. The precise algorithm is
presented in the next section.

High-level description of the dynamic algorithm. The main components that are
new to our dynamic algorithm compared to the offline algorithm of Section 3.1
are geared towards handling edge deletions. Assume that we have computed the
DSCCs of a graph $G$, and we now have to process an operation
$\operatorname{delete}(u,v,\overline{\alpha})$. This will, in general, result
in splitting some DSCCs into smaller ones. In high level, we handle such edge
deletion in three steps.

  1. (1)

We compute a sound overapproximation of the DSCCs that are affected by the
edge deletion, i.e., those that might have to be split into smaller
components. We compute this overapproximation by effectively performing a
forward search starting from $\operatorname{DSCC}(v)$ and repeatedly
proceeding to neighboring DSCCs of $G$. In particular given a current DSCC
$S$, we proceed to those DSCCs $S^{\prime}$ that have at least two incoming
edges of the form $x\xrightarrow{\overline{\beta}}y$, with $x\in S$ and $y\in
S^{\prime}$, and some label $\overline{\beta}$. This is because $S^{\prime}$
might have been formed through $S$ and the corresponding edges
$x\xrightarrow{\overline{\beta}}y$. Although this traversal might end up
touching $\Theta(n)$ DSCCs, we expect that in practice it will perform much
better, as the effect of an average edge deletion is usually very local.

  2. (2)

At this point, it would suffice to split all nodes $t$ in the previously
discovered DSCCs $S^{\prime}$ into singleton components, gather in the
worklist $\mathcal{Q}$ (see Algorithm 1) all pairs $(s,\overline{\beta})$
corresponding to incoming edges $s\xrightarrow{\overline{\beta}}t$ where $t$
is the unique node of such a singleton component, and restart the fixpoint
computation using $\operatorname{Fixpoint}()$. Unfortunately, this would
require $\Theta(n^{2})$ time, which is beyond our target bound, as there can
be $\Theta(n^{2})$ such edges $s\xrightarrow{\overline{\beta}}t$, and
Algorithm 1 of Algorithm 1 would iterate over all of them (where $u=s$ and
$w=t$ in the algorithm). To circumvent this difficulty, we introduce the novel
notion of _primary DSCCs_ (or _PDSCCs_), which, intuitively, are connected
components of small size. We keep track of the formation of PDSCCs dynamically
by leveraging techniques from undirected dynamic reachability (see e.g., Table
1). Now, instead of splitting each previously discovered DSCC $S^{\prime}$
into _singleton components_ , we split it into its _PDSCCs_. This allows us to
re-initiate the fixpoint computation of the function
$\operatorname{Fixpoint}()$ after only traversing $O(n)$ edges of the form
$s\xrightarrow{\overline{\beta}}t$ (where $t$ now is a node in a PDSCC). In
practice and due to the previous step, we typically traverse much fewer edges
than $n$. In turn, this implies that $\operatorname{Fixpoint}()$ will converge
after $O(n)$ iterations, leading to the desired time bound.

  3. (3)

We execute the fixpoint computation, similarly to Algorithm 1.

We now describe the above concepts in detail.

$u$$v$$x$$y$$z$$w$$q$$r$$s$$t$$\overline{\alpha}$$\overline{\alpha}$$\overline{\alpha}$$\overline{\beta}$$\overline{\beta}$$\overline{\gamma}$$\overline{\gamma}$$\overline{\gamma}$$\overline{\gamma}$$u$$v$$x$$y$$z$$w$$q$$r$$s$$t$

Figure 3.  A bidirected graph $G$ (left) and the corresponding primal graph
$H$ (right). There are two non-singleton PDSCCs in $G$ (marked), corresponding
to non-singleton connected subgraphs of $H$.

Primal graphs and primary DSCCs. Consider a bidirected graph $G=(V,E)$. The
_primal_ graph $H=(V,L)$ is an unlabeled, undirected graph with the same node
set, and edge set defined as:

$L=\\{(x,y)\colon\exists u\in V.\leavevmode\nobreak\
\exists\overline{\alpha}\in\Sigma^{C}.\leavevmode\nobreak\
u\xrightarrow{\overline{\alpha}}x,u\xrightarrow{\overline{\alpha}}y\in E\\}$

In words, $x$ and $y$ share an edge in $H$ if they are connected in $G$ via a
Dyck path of length $2$. A _primary DSCC (PDSCC)_ of $G$ is a (maximal)
connected component of the primal graph $H$. It is not hard to see that the
PDSCC partitioning of $G$ is a refinement of its DSCC partitioning, i.e., each
DSCC contains one or more PDSCCs. See Figure 3 for an illustration. Similarly
to the case of DSCCs, given a node $u$, we let $\operatorname{PDSCC}(u)$ be
the PDSCC in which $u$ belongs, while $\operatorname{PDSCCRepr}(u)$ returns a
representative of $\operatorname{PDSCC}(u)$ that is common for all nodes
$v\in\operatorname{PDSCC}(u)$. Hence, two nodes $u$, $w$ are in the same PDSCC
iff $\operatorname{PDSCCRepr}(u)=\operatorname{PDSCCRepr}(v)$.

Since the PDSCCs of $G$ have a direct representation as connected components
in the undirected graph $H$, we can leverage existing techniques from dynamic
undirected connectivity (see, e.g., Table 1) to maintain them efficiently.
PDSCCs serve the following function. When an edge is deleted, some DSCCs $S$
of $G$ have to be split to smaller DSCCs. This can lead to effectively
repeating the fixpoint computation from scratch in $G$. However, this approach
would require $\Theta(n^{2})$ running time, which is beyond our complexity
bound. Instead, maintaining the PDSCCs allows us to split $S$ to its PDSCCs
(as opposed to individual nodes), and thus avoid recomputing the PDSCCs from
scratch. In turn, this allows us to achieve the desired $O(n\cdot\alpha(n))$
bound for edge deletions.

$\operatorname{insert}(u,x,\overline{\alpha})$$G_{1}$$u$$x$$y$$z$$\overline{\alpha}$$\overline{\alpha}$$H_{1}$$u$$x$$y$$z$$\operatorname{delete}(u,y,\overline{\alpha})$$G_{2}$$u$$x$$y$$z$$\overline{\alpha}$$\overline{\alpha}$$\overline{\alpha}$$H_{2}$$u$$x$$y$$z$$G_{3}$$u$$x$$y$$z$$\overline{\alpha}$$\overline{\alpha}$$H_{3}$$u$$x$$y$$z$

Figure 4.  Sparsification for the maintenance of the PDSCCs of $G_{i}$ across
edge insertions and deletions (top), by maintaining connected components in
the corresponding primal graphs $H_{i}$ (bottom).

A sparsification approach for maintaining the PDSCCs. Since each PDSCC
corresponds to a connected component of the undirected primal graph $H$, we
will maintain PDSCCs dynamically, by using any data structure for dynamic
reachability on undirected graphs (see Table 1). We call this data structure
for undirected reachability
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{PrimCompDS}}$.

An operation $o=\operatorname{insert}(u,v,\overline{\alpha})$ inserts between
$0$ and $n-1$ undirected edges in the primal graph $H$. Indeed, we have an
edge $(x,v)$ for every node $x\neq v$ for which already
$u\xrightarrow{\overline{\alpha}}x$, and there may be $n-1$ such nodes $x$.
Note, however, that if there already exist two such nodes, $x,y$, with
$u\xrightarrow{\overline{\alpha}}x$ and $u\xrightarrow{\overline{\alpha}}y$,
then $x$ and $y$ already appear in the same PDSCC of $G$. Hence, we can
faithfully maintain the PDSCCs of $G$ by only adding _one_ of the two primal
edges $(v,x)$ and $(v,y)$ in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{PrimCompDS}}$.
This has the desirable effect of maintaining PDSCCs after edge insertions by
inserting $O(1)$ undirected edges in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{PrimCompDS}}$,
as opposed to $O(n)$. This kind of technique is known as _sparsification_
(Eppstein et al., 1997), in that we manage to represent the full connectivity
of the primal graph $H$ while only storing a subset of its edges. In
particular, we achieve this effect by maintaining the outgoing edges of $u$
labeled with $\overline{\alpha}$ in a linked list
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[u][\overline{\alpha}]=(x_{1},\dots,x_{r})$,
and only inserting in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{PrimCompDS}}$
edges $(x_{i},x_{i+1})$, i.e., between consecutive nodes in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[u][\overline{\alpha}]$.
Distant nodes become connected transitively in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{PrimCompDS}}$.

Conversely, an operation $o=\operatorname{delete}(u,v,\overline{\alpha})$
deletes between $0$ and $n-1$ undirected edges in the primal graph $H$, with
reasoning similar to the one above. However, because of the above invariant,
we can restore the PDSCCs of $G$ by removing the edges $(a,v)$ and $(v,b)$ in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{PrimCompDS}}$,
where $a$ and $b$ are the neighbors of $v$ in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[u][\overline{\alpha}]$.
Moreover, as $a$ and $b$ are no longer connected in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{PrimCompDS}}$,
we restore their connectivity by inserting the edge $(a,b)$ in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{PrimCompDS}}$.
Figure 4 illustrates this sparsification technique on a small example. The
update $\operatorname{insert}(u,x,\overline{\alpha})$ creates two edges in the
primal graph $H_{2}$, namely $(x,y)$ and $(x,z)$. However, the dashed edge
$(x,z)$ is not stored explicitly in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{PrimCompDS}}$,
as $x$ and $y$ are already connected via $z$. The update
$\operatorname{delete}(u,y,\overline{\alpha})$ removes the edges $(x,y)$ and
$(y,z)$ from the primal graph $H_{3}$. To preserve the connectivity of $x$ and
$z$, the dashed edge $(x,z)$ is restored in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{PrimCompDS}}$.

Maintaining the neighbors of PDSCCs. The maintenance of the PDSCCs allows us
to efficiently identify the incoming neighbors of a PDSCC, in $O(n)$ worst-
case time, although the graph might have $\Theta(n^{2})$ edges. This fact
stems from the following observation. For a given node $u$ and label
$\overline{\alpha}$, if there are two edges
$u\xrightarrow{\overline{\alpha}}x$ and $u\xrightarrow{\overline{\alpha}}y$,
then $x$ and $y$ are in the same PDSCC. In other words, for every such $u$ and
$\overline{\alpha}$, there is at most one PDSCC that $u$ is a neighbor of via
a $\overline{\alpha}$-labeled edge. Thus, given a set of PDSCCs (as described
in Item (2) above), we can obtain all edges incoming to them in $O(n)$ time,
by iterating over all nodes $u$ and labels $\overline{\alpha}$. Though this is
sufficient towards our linear time bound, it can become unnecessarily slow
when the number of such PDSCCs is small. Instead, we follow a different
approach, which retains the $O(n)$ worst-case behavior but is faster in
practice.

For every node $x$ and label $\overline{\alpha}$, we maintain a set
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[x][\overline{\alpha}]$,
which stores nodes $u$ that have an edge $u\xrightarrow{\overline{\alpha}}x$.
We maintain the invariant that $x$ will be the _only_ node in
$\operatorname{PDSCC}(x)$ with
$u\in{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[x][\overline{\alpha}]$,
even though there might be other nodes $y\in\operatorname{PDSCC}(x)$ also
having an edge $u\xrightarrow{\overline{\alpha}}y$. To identify the neighbors
of each PDSCC, it now suffices to iterate over its nodes $x$, and for each
label $\overline{\alpha}$, collect the nodes from
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[x][\overline{\alpha}]$.
The invariant guarantees that every neighbor $u$ will be accessed exactly once
per label $\overline{\alpha}$, retaining the $O(n)$ worst-case running time.

The sets
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[x][\overline{\alpha}]$,
together with their invariant, can be maintained as follows. Upon inserting an
edge $\operatorname{insert}(u,x,\overline{\alpha})$, if $u$ does not have any
other outgoing edges labeled with $\overline{\alpha}$, we insert $u$ in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[x][\overline{\alpha}]$.
Otherwise, there exists another edge $u\xrightarrow{\overline{\alpha}}y$, with
already
$u\in{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[y][\overline{\alpha}]$.
The existence of the two edges $u\xrightarrow{\overline{\alpha}}x$ and
$u\xrightarrow{\overline{\alpha}}y$ implies that
$\operatorname{PDSCC}(x)=\operatorname{PDSCC}(y)$, hence it is sound to not
insert $u$ in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[x][\overline{\alpha}]$,
as $u$ is retrievable via $y$. Similarly, upon deleting an edge
$\operatorname{delete}(u,x,\overline{\alpha})$, if
$u\in{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[x][\overline{\alpha}]$,
we move $u$ to another set
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[y][\overline{\alpha}]$
for which there exists an edge $u\xrightarrow{\overline{\alpha}}y$. Figure 5
illustrates the maintenance of
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}$
on a small example.

$\operatorname{insert}(u,x,\overline{\alpha})$$G_{1}$$u$$x$$y$$z$$\operatorname{insert}(u,y,\overline{\alpha})$$\operatorname{insert}(u,z,\overline{\alpha})$$G_{2}$$u$$x$$y$$z$$\overline{\alpha}$$\overline{\alpha}$$\operatorname{delete}(u,x,\overline{\alpha})$$G_{3}$$u$$x$$y$$z$$\overline{\alpha}$$\overline{\alpha}$$\overline{\alpha}$$\overline{\alpha}$$G_{4}$$u$$x$$y$$z$$\overline{\alpha}$$\overline{\alpha}$$\overline{\alpha}$

Figure 5.  Maintenance of the sets
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}$
(shown in orange dashed) along edge insertions and deletions. The first edge
insertion $u\xrightarrow{\overline{\alpha}}x$ leads to
$u\in{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[x][\overline{\alpha}]$.
The following two edge insertions $u\xrightarrow{\overline{\alpha}}y$ and
$u\xrightarrow{\overline{\alpha}}z$ do not modify
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}$,
as $x$, $y$ and $z$ belong to the same PDSCC, thus $u$ can be retrieved as a
$\overline{\alpha}$-neighbor via the set
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[x][\overline{\alpha}]$.
When processing deleting the edge $u\xrightarrow{\overline{\alpha}}x$, we move
$u$ to
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[y][\overline{\alpha}]$,
thus $u$ can still be retrieved as a $\overline{\alpha}$-neighbor of the PDSCC
$\\{y,z\\}$.

Processing a delete operation. We are now in position to outline our approach
for processing a delete operation
$\operatorname{delete}(u,v,\overline{\alpha})$. As the edge
$u\xrightarrow{\overline{\alpha}}v$ might be used to connect $v$ to other
nodes in $\operatorname{DSCC}(v)$, this operation might split
$\operatorname{DSCC}(v)$ into smaller DSCCs. As nodes become disconnected in
$\operatorname{DSCC}(v)$, other DSCCs might also be split, if the paths
connecting their nodes passed through $\operatorname{DSCC}(v)$, resulting in a
cascading effect. For instance, consider Figure 1 (middle), having two
$\operatorname{DSCC}$s $\\{c,d,e,f\\}$ and $\\{g,h\\}$. On deleting the edge
$f\xrightarrow{\overline{L}}d$, the node $d$ splits from the
$\operatorname{DSCC}$ $\\{c,d,e,f\\}$. In turn, the $\operatorname{DSCC}$
$\\{g,h\\}$ splits into $\\{g\\},\\{h\\}$ since they were held together by
$c,d$ being in the same $\operatorname{DSCC}$. The split of $\\{g,h\\}$
results in pulling out $f$ from $\operatorname{DSCC}(e)$. Thus, deleting the
edge $f\xrightarrow{\overline{L}}d$ results in splitting
$\operatorname{DSCC}$s $\\{c,d,e,f\\}$ and $\\{g,h\\}$ resulting in
$\operatorname{DSCC}$s $\\{c,e\\}$, $\\{d\\},\\{f\\},\\{g\\},\\{h\\}$.

Thus, a single edge deletion may have an effect which propagates to the whole
graph; however, we can obtain a sound overapproximation of the DSCCs affected
by the initial edge deletion using the following observation. If the split of
a DSCC $S$ leads to the immediate split of another DSCC $S^{\prime}$, then
there exist two distinct edges $x_{i}\xrightarrow{\overline{\beta}}y_{i}$, for
$i\in[2]$, such that $x_{i}\in S$ and $y_{i}\in S^{\prime}$. Thus, for
$\operatorname{delete}(u,v,\overline{\alpha})$, we can obtain our
overapproximation by starting a forward search from $\operatorname{DSCC}(v)$:
given a current DSCC $S$, we iterate over all labels $\overline{\beta}$ such
that $S$ has at least two $\overline{\beta}$-labeled outgoing edges, and
proceed to the resulting DSCC $S^{\prime}$ (note that there can be at most one
such $S^{\prime}$).

After the overapproximation of the set of potentially splitting DSCCs has been
performed, each such DSCC $S$ is split to its constituent PDSCCs, using the
undirected connectivity data structure
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{PrimCompDS}}$.
Note that this splitting is an underapproximation of the set of the final
DSCCs, as some PDSCCs have to be merged again. We will discover this by
running the fixpoint computation again, up to convergence. For this, we re-
insert in the worklist $\mathcal{Q}$ (see function $\operatorname{Fixpoint}()$
in Algorithm 1) node-label pairs
$(\operatorname{DSCCRepr}(y),\overline{\beta})$ that represent edges
$y\xrightarrow{\overline{\beta}}\cdot$ that might lead to further component
merging. Due to the efficient maintenance of neighbors of PDSCCs (see the
previous paragraph), this can be achieved by iterating over all nodes $x$ of
the PDSCCs, and for each label $\overline{\beta}\in\Sigma^{C}$, insert in
$\mathcal{Q}$, the pair $(\operatorname{DSCCRepr}(w),\overline{\beta})$
corresponding to
$w\in{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[x][\overline{\beta}]$
if
$|{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[\operatorname{DSCCRepr}(w)][\overline{\beta}]|\geq
2$. Finally we continue with the fixpoint computation as in
$\operatorname{OfflineAlgo}$ with the guarantee that upon convergence,
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}$
will contain the DSCCs of the new graph after deleting the edge
$u\xrightarrow{\overline{\alpha}}v$.

$S_{1}$$S_{2}$$S_{3}$$S_{4}$$\operatorname{delete}(c,d,\overline{\gamma})$,
initializing new fixpoint
computation$a$$b$$c$$d$$e$$f$$g$$h$$u$$v$$x$$y$$\overline{\alpha}$$\overline{\alpha}$$\overline{\beta}$$\overline{\beta}$$\overline{\gamma}$$\overline{\gamma}$$\overline{\alpha}$$\overline{\beta}$$\overline{\alpha}$$\overline{\beta}$$\overline{\gamma}$$\overline{\gamma}$$\overline{\gamma}$$\overline{\alpha}$$\overline{\alpha}$$\overline{\beta}$$\overline{\beta}$$\overline{\gamma}$$\overline{\gamma}$after
fixpoint
computation$a$$b$$c$$d$$e$$f$$g$$h$$u$$v$$x$$y$$\overline{\alpha}$$\overline{\alpha}$$\overline{\beta}$$\overline{\beta}$$\overline{\gamma}$$\overline{\alpha}$$\overline{\beta}$$\overline{\alpha}$$\overline{\beta}$$\overline{\gamma}$$\overline{\gamma}$$\overline{\gamma}$$\overline{\alpha}$$\overline{\alpha}$$\overline{\beta}$$\overline{\beta}$$\overline{\gamma}$$\overline{\gamma}$$a$$b$$c$$d$$e$$f$$g$$h$$u$$v$$x$$y$$\overline{\alpha}$$\overline{\alpha}$$\overline{\beta}$$\overline{\beta}$$\overline{\gamma}$$\overline{\alpha}$$\overline{\beta}$$\overline{\alpha}$$\overline{\beta}$$\overline{\gamma}$$\overline{\gamma}$$\overline{\gamma}$$\overline{\alpha}$$\overline{\alpha}$$\overline{\beta}$$\overline{\beta}$$\overline{\gamma}$$\overline{\gamma}$

Figure 6.  Illustration of handling
$\operatorname{delete}(c,d,\overline{\gamma})$, showing the state of the
algorithm before deletion (top), after preparing the new fixpoint computation
(middle) and after completing the fixpoint computation (bottom).

Example. Figure 6 illustrates the above process on a small example, processing
an update $\operatorname{delete}(c,d,\overline{\gamma})$. Before the deletion
(top), the graph has four DSCCs, namely $S_{1},S_{2},S_{3},S_{4}$ (marked). In
the first step, we perform a forward search from $S_{2}$, following pairs of
same-label edges, which discovers $S_{2}$, $S_{3}$ and $S_{4}$ as the set of
DSCCs that are potentially affected by the delete operation. Observe that
$S_{1}$ does not have to be split, and the algorithm avoids recomputation on
$S_{1}$. Then, $S_{2}$, $S_{3}$ and $S_{4}$ are split to their constituent
PDSCCs (middle). Observe that $S_{4}$ is only partly split, as its subset
$\\{u,v,y\\}$ is a PDSCC (with $y=\operatorname{PDSCCRepr}(u)$) in the new
graph (after deletion). Hence the algorithm avoids recomputing $S_{4}$ from
scratch. Afterwards, the algorithm uses the
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}$
data structure to collect the set of pairs
$\mathcal{L}=\\{(g,\overline{\gamma}),(h,\overline{\gamma}),(c,\overline{\gamma}),(d,\overline{\alpha}),(e,\overline{\alpha}),(d,\overline{\beta}),(y,\overline{\alpha}),(y,\overline{\beta}),(y,\overline{\gamma}),(f,\overline{\beta})\\}$,
i.e., the pairs $(\operatorname{DSCCRepr}(x),\overline{\beta})$ such that
$\operatorname{DSCC}(x)\xrightarrow{\overline{\beta}}\operatorname{PDSCC}(r)$,
where $r$ is a node in the newly formed $\operatorname{PDSCC}$s. Observe that
the pair $(f,\overline{\gamma})$ is not collected in $\mathcal{L}$ even though
$f\xrightarrow{\overline{\gamma}}c$, as this edge is incoming to DSCC $S_{1}$
which was deemed as not affected by the edge deletion. Note that some of these
$\operatorname{PDSCC}$s can be merged during the $\operatorname{Fixpoint}$
computation to obtain the new set of $\operatorname{DSCC}$s post deletion. For
this, a pair $(x,\overline{\alpha})\in\mathcal{L}$ is added to $\mathcal{Q}$,
if there are two outgoing edges on $\overline{\alpha}$ from $x$’s component.
In this example, only $(y,\overline{\gamma})$ is added in $\mathcal{Q}$ since
there are two edges on $\overline{\gamma}$ from $y$’s component, namely
$u\xrightarrow{\overline{\gamma}}e$ and $v\xrightarrow{\overline{\gamma}}f$.
$\operatorname{Fixpoint}$ takes this $\mathcal{Q}$ and converges to the final
DSCCs (bottom), merging the $\operatorname{PDSCC}$s $\\{e\\}$ and $\\{f\\}$,
thereby partially restoring $S_{2}$.

###  3.3. The Dynamic Algorithm

We now make the concepts of the previous section formal, by developing precise
algorithms for handling each insert and delete operation. In a static analysis
context, the edges of the underlying graph correspond to statements in the
analyzed source code. This means that a certain edge might be inserted several
times in the graph, if, for example, it comes from a repeating program
statement. Note, however, that only the presence of the edge impacts the
reachability analysis and not its multiplicity. To handle multiple edges, we
maintain simple counters in a list data structure
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Count}}$,
so that
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Count}}[u][v][\overline{\alpha}]$
holds the number of $u\xrightarrow{\overline{\alpha}}v$ edges currently in the
graph.

1
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Count}}[u][v][\overline{\alpha}]\leftarrow{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Count}}[u][v][\overline{\alpha}]+1$
// Update the edge counter

2 if
_${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Count}}[u][v][\overline{\alpha}]\geq
2$_ then return

3 // Edge exists already, no change in reachability if
_$|{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[u][\overline{\alpha}]|=0$_
then // $v$ is the first $\overline{\alpha}$-neighbor of $u$

4 Insert $u$ in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[v][\overline{\alpha}]$
// The fact that $u\xrightarrow{\overline{\alpha}}\operatorname{PDSCC}(v)$ is
retrievable via
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[v][\overline{\alpha}]$

5

6else

7 Let $y\leftarrow$ the head of
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[u][\overline{\alpha}]$
// The most recent $\overline{\alpha}$-neighbor of $u$

8
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{PrimCompDS}}.\operatorname{insert}(v,y)$
// Update the PDSCCs with the edge $(v,y)$

9

10Insert $v$ as the head of
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[u][\overline{\alpha}]$
// $v$ is a node in the PDSCC formed by
$u\xrightarrow{\overline{\alpha}}\cdot$ edges

11
$x\leftarrow{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}.\operatorname{Find}(u)$
// $x$ is the root of the component of $u$

12 Insert $v$ in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[x][\overline{\alpha}]$
// The component of $u$ has an extra outgoing edge

13 if
_$|{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[x][\overline{\alpha}]|\geq
2$ _ then // Potentially some component merging occurs, compute new fixpoint

14 Insert $(x,\overline{\alpha})$ in $\mathcal{Q}$ // Prepare the new fixpoint
computation

15 $\operatorname{Fixpoint}()$ // Compute the new fixpoint due to the new edge

16

Algorithm 2 $\operatorname{insert}(u,v,\overline{\alpha})$

Operation $\operatorname{insert}(u,v,\overline{\alpha})$. Algorithm 2 handles
each $\operatorname{insert}(u,v,\overline{\alpha})$ operation. In words, the
algorithm first implements the logic for sparsely maintaining the PDSCCs
(Algorithm 2 to Algorithm 2). In particular, if $v$ is the first
$\overline{\alpha}$-neighbor of $u$, then $u$ is marked as a
$\overline{\alpha}$-neighbor of $\operatorname{PDSCC}(v)$ via $v$, by
inserting $u$ in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[v][\overline{\alpha}]$
(Algorithm 2). Otherwise, $u$ is already marked via some existing
$\overline{\alpha}$-neighbor $y$ of $u$, which is also in
$\operatorname{PDSCC}(v)$. Then the algorithm inserts an edge $(v,y)$ in the
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{PrimCompDS}}$
data structure (which maintains undirected connectivity) to reflect the change
in $v$’s PDSCC.

The second step of Algorithm 2 (Algorithm 2 to Algorithm 2) prepares the
fixpoint computation that might be triggered due to the new edge. For this, it
marks that $v$ is a new $\overline{\alpha}$-neighbor of
$\operatorname{DSCC}(u)$ (Algorithm 2, as the DSCC is represented by its root
node $x$). If there already exists another $\overline{\alpha}$-labeled edge
out of $\operatorname{DSCC}(u)$, then the pair $(x,\overline{\alpha})$ is
inserted in $\mathcal{Q}$, and the $\operatorname{Fixpoint}()$ is called to
continue the fixpoint computation for merging the DSCCs (in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}$)
(note that $\operatorname{Fixpoint}()$ is also used by
$\operatorname{OfflineAlgo}$ and defined in Algorithm 1).

1
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Count}}[u][v]\overline{\alpha}]\leftarrow{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Count}}[u][v][\overline{\alpha}]-1$
// Update the edge counter

2 if
_${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Count}}[u][v][\overline{\alpha}]\geq
1$_ then return

3 // Edge still exists, no change in reachability if  _$v$ is the tail of
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[u][\overline{\alpha}]$_
then // $v$ was the earliest node to have an edge
$u\xrightarrow{\overline{\alpha}}\cdot$

4 Remove $u$ from
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[v][\overline{\alpha}]$

5 if
_$|{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[u][\overline{\alpha}]|\geq
2$_ then // There is another $u\xrightarrow{\overline{\alpha}}\cdot$ edge

6 Let $w\leftarrow$ the penultimate node in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[u][\overline{\alpha}]$

7 Insert $u$ in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[w][\overline{\alpha}]$
// $u\xrightarrow{\overline{\alpha}}\operatorname{PDSCC}(w)$ is now
retrievable via
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[w][\overline{\alpha}]$

8

9 Let $a,b\leftarrow\bot,\bot$

10 if  _$v$ is neither the head nor the tail of
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[u][\overline{\alpha}]$_
then

11 Let $a,b\leftarrow$ the two neighbors of $v$ in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[u][\overline{\alpha}]$
// We will have to reconnect $a$ and $b$

12 foreach  _neighbor $x$ of $v$ in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[u][\overline{\alpha}]$_
do // At most two neighbors

13
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{PrimCompDS}}.\operatorname{delete}(v,x)$
// The primal graph loses the edge $(v,x)$

14Remove $v$ from
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[u][\overline{\alpha}]$
// $v$ no longer has undirected edges due to $\overline{\alpha}$ via $u$

15 if  _$a\neq\bot$ and $b\neq\bot$_ then // $v$ had two neighbors in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[u][\overline{\alpha}]$

16
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{PrimCompDS}}.\operatorname{insert}(a,b)$
// $a$ and $b$ no longer connected via $v$, connect them directly

17 $\operatorname{MakePrimary}()$ // Prepare the state for the dynamic
fixpoint

$\operatorname{Fixpoint}()$ // Compute the fixpoint from the current state

Algorithm 3 $\operatorname{delete}(u,v,\overline{\alpha})$

Operation $\operatorname{delete}(u,v,\overline{\alpha})$. Algorithm 3 handles
each $\operatorname{delete}(u,v,\overline{\alpha})$ operation. Similarly to
Algorithm 2, Algorithm 3 first implements the logic for sparsely maintaining
the PDSCCs (Algorithm 3 to Algorithm 3). In particular, if $v$ is the tail of
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[u][\overline{\alpha}]$
then $u$ is currently retrievable as a $\overline{\alpha}$-neighbor of
$\operatorname{PDSCC}(v)$ via $v$. Since $u$ will no longer be a
$\overline{\alpha}$-neighbor of $v$, the algorithm removes $u$ from
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[v][\overline{\alpha}]$,
and makes $u$ retrievable via $w$ (Algorithm 3), which is the new last
$\overline{\alpha}$-neighbor of $u$ (after removing $v$ in Algorithm 3). Then,
the algorithm deletes the edge $(a,v)$ and $(b,v)$ in the
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{PrimCompDS}}$
data structure, where $a$ and $b$ are the neighbors of $v$ in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[u][\overline{\alpha}]$
to reflect the change in $\operatorname{PDSCC}(v)$ (Algorithm 3). After
removing $v$ from
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[u][\overline{\alpha}]$
(Algorithm 3), $a$ and $b$ become neighboring nodes in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[u][\overline{\alpha}]$,
and thus the algorithm inserts a new edge $(a,b)$ in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{PrimCompDS}}$,
to reflect the fact that $a$ and $b$ are now directly connected in the sparse
representation of PDSCCs (Algorithm 3). As the edge deletion might lead to the
splitting of some DSCCs, the second step of Algorithm 3 splits some of the
previously computed DSCCs and re-initiates the fixpoint computation (Algorithm
3 and Algorithm 3).

// 1\. A forward search from $\operatorname{DSCC}(u)$ to gather the DSCCs
potentially affected by $\operatorname{delete}(u,v,\overline{\alpha})$

1 $\mathcal{S}\leftarrow$ an empty queue over $V$ // A simple queue to perform
the forward search

2 $\mathcal{Z}\leftarrow$ an empty set over $V$ // Stores the roots of DSCCs
potentially affected by $\operatorname{delete}(u,v,\overline{\alpha})$

3 Insert
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}.\operatorname{Find}(v)$
in $\mathcal{Z}$ and $\mathcal{S}$ // Mark $\operatorname{DSCC}(v)$ as
potentially affected by the delete

4 while  _$\mathcal{S}$ is not empty_ do // Start the forward search from
$\operatorname{DSCC}(v)$

5 Extract $x$ from $\mathcal{S}$ // Proceed the search to
$\operatorname{DSCC}(x)$

6 foreach  _label $\overline{\beta}\in\Sigma^{C}$_ do

7 if  _exist nodes $s\neq t$ with
$\operatorname{DSCC}(x)\xrightarrow{\overline{\beta}}s$ and
$\operatorname{DSCC}(x)\xrightarrow{\overline{\beta}}t$_ then // Note that
$\operatorname{DSCC}(s)=\operatorname{DSCC}(t)$

8
$z\leftarrow{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}.\operatorname{Find}(t)$
// The root representative of $t$’s component

9 if  _$z\not\in\mathcal{Z}$_ then // This is the first time we encounter
$\operatorname{DSCC}(z)$

10 Insert $z$ in $\mathcal{Z}$ and $\mathcal{S}$ // Mark
$\operatorname{DSCC}(z)$ as potentially affected by the delete

11

12

13

// 2\. Every DSCC potentially affected is split to its PDSCCs

14 $\mathcal{R}\leftarrow$ an empty set over $V$ // Gathers the roots of the
PDSCCs that DSCCs are split to

15 foreach  _$z\in\mathcal{Z}$_ do

16 foreach  _node $t$ in the component of $z$_ do // Iterate over the nodes of
the affected DSCCs

17 foreach  _label $\overline{\beta}\in\Sigma^{C}$_ do

18 foreach
_$s\in{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[t][\overline{\beta}]$_
do // Incoming neighbor to the affected $\operatorname{DSCC}(z)$

19
$x\leftarrow{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}.\operatorname{Find}(s)$
// The root representative of $\operatorname{DSCC}(s)$

20 if  _$x\not\in\mathcal{Z}$_ then // $\operatorname{DSCC}(x)$ is unaffected
by the delete

21 Reinitialize
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[x][\overline{\beta}]$
to an empty list // Will be re-populated later in Algorithm 4

22

23 Split the nodes of $z$’s component in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}$
to its PDSCCs, using
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{PrimCompDS}}$

24 Insert the roots of the new components in $\mathcal{R}$ // Some of the
PDSCCs might merge again

25 foreach  _label $\overline{\beta}\in\Sigma^{C}$_ do

26 Reinitialize
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[z][\overline{\beta}]$
to an empty list // $z$ no longer represents a component in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}$

// 3\. Gather edges incoming to the newly initialized components for new
fixpoint computation

27 $\mathcal{L}\leftarrow$ an empty set over $V\times\Sigma^{C}$ // Gathers
pairs $(x,\overline{\beta})$ for which
$\operatorname{DSCC}(x)\xrightarrow{\overline{\beta}}\operatorname{PDSCC}(r)$,
for $r\in\mathcal{R}$

28 foreach  _$r\in\mathcal{R}$_ do // Iterate over the roots of the newly
split components

29 foreach  _node $t$ in the component of $r$_ do // Iterate over the nodes of
each newly split component

30 foreach  _label $\overline{\beta}\in\Sigma^{C}$_ do

31 foreach
_$s\in{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[t][\overline{\beta}]$_
do // Retrieve that $s\xrightarrow{\overline{\beta}}\operatorname{PDSCC}(t)$

32
$x\leftarrow{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}.\operatorname{Find}(s)$
// The root representative of $s$’s component

33 Insert $t$ in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[x][\overline{\beta}]$
// The component of $s$ has an outgoing edge to $t$

34 Insert $(x,\overline{\beta})$ in $\mathcal{L}$ // Mark that we have
inserted edges in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[x][\overline{\beta}]$

35

36 if
_$|{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[t][\overline{\beta}]|\geq
1$_ then // $t$ has a $\overline{\beta}$ out-neighbor

37 $y\leftarrow$ the first node in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[t][\overline{\beta}]$
// An arbitrary $\overline{\beta}$ out-neighbor of $t$

38 if
_${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}.\operatorname{Find}(y)\not\in\mathcal{R}$_
then // The component of $y$ is not splitting

39 Insert $y$ in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[r][\overline{\beta}]$
// The component of $t$ has a $\overline{\beta}$ edge to $y$

40

41

42

43foreach  _$(x,\overline{\beta})\in\mathcal{L}$_ do // Re-initialize the
queue $\mathcal{Q}$ for the new fixpoint

44 if
_$|{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[x][\overline{\beta}]|\geq
2$_ then // There are two outgoing $\overline{\beta}$-labeled edges from $x$’s
component

45 Insert $(x,\overline{\beta})$ in $\mathcal{Q}$

46

47

Algorithm 4 $\operatorname{MakePrimary}()$

Function $\operatorname{MakePrimary}()$. Algorithm 4 prepares the new fixpoint
computation by partially splitting some DSCCs to their constituent PDSCCs. In
words, the algorithm first computes an overapproximation of the splitting
DSCCs by running a forward graph search from $\operatorname{DSCC}(v)$
(Algorithm 4 to Algorithm 4), every time transitioning to new DSCCs by
following pairs of same-label edges outgoing the current DSCC. This
transitioning reflects the intuition that such pairs of edges might have used
to form the neighboring DSCC – by splitting the current one, we might have to
split the neighbor as well. It begins the forward search by populating
$\operatorname{DSCCRepr}(v)$ in a set $\mathcal{Z}$ and a queue $\mathcal{S}$.
Eventually, after Algorithm 4 to Algorithm 4, $\mathcal{Z}$ will contain the
roots of all affected $\operatorname{DSCC}$s (including
$\operatorname{DSCC}(v)$) while $\mathcal{S}$ helps with the forward search of
affected $\operatorname{DSCC}$s.

The second step (Algorithm 4 to Algorithm 4) of Algorithm 4 splits these
potentially affected DSCCs to their constituent PDSCCs. In Algorithm 4, the
algorithm performs this split in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}$
by iterating over the nodes of the DSCCs stored in $\mathcal{Z}$.
$\mathcal{R}$ holds the roots of all the newly formed $\operatorname{PDSCC}$s
after splitting (Algorithm 4). Then
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[z][\cdot]$
is reset, where $z$ is either the root node of an affected DSCC (Algorithm 4)
or is the root node of an unaffected DSCC which has an outgoing edge entering
one of the affected $\operatorname{DSCC}$s (Algorithm 4). The re-
initialization is done keeping in mind the split of the affected
$\operatorname{DSCC}$s. These will be re-populated in the third step with
edges outgoing or entering the nodes of the newly formed
$\operatorname{PDSCC}$s. Although we are guaranteed that these
$\operatorname{DSCC}$s do not have to be split below their
$\operatorname{PDSCC}$s, it may be the case that certain
$\operatorname{PDSCC}$s have to merge again.

In its third step, Algorithm 4 identifies the edges incoming to these
$\operatorname{PDSCC}$s, and inserts them in the set $\mathcal{L}$ (Algorithm
4 to Algorithm 4). $\mathcal{L}$ is later used to decide whether two
$\operatorname{PDSCC}$s must be merged or not. It also populates
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}$
with (i) edges incoming to the $\operatorname{PDSCC}$s (lines Algorithm 4 to
Algorithm 4) as well as with (ii) edges (Algorithm 4 to Algorithm 4) outgoing
from the $\operatorname{PDSCC}$s, and entering an unaffected
$\operatorname{DSCC}$ (those whose roots are not in $\mathcal{R}$). Note that
edges coming out of a $\operatorname{PDSCC}$ and entering an affected
$\operatorname{DSCC}$ (those whose roots are in $\mathcal{R}$) are covered by
Algorithm 4 to Algorithm 4.

To merge PDSCCs, the worklist $\mathcal{Q}$ is populated using relevant
entries of $\mathcal{L}$ to drive the new fixpoint computation (Algorithm 4 to
Algorithm 4). In more detail, the algorithm iterates over all PDSCCs
(Algorithm 4), and for each node $t$ in each PDSCC (Algorithm 4) and label
$\overline{\beta}$ (Algorithm 4), it identifies the edges
$s\xrightarrow{\overline{\beta}}t$ by iterating over the nodes
$s\in{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[t][\overline{\beta}]$
(Algorithm 4). It then identifies the root node $x$ of $s$’s component
(Algorithm 4), and inserts $t$ in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[x][\overline{\beta}]$
as well as the pair $(x,\overline{\beta})$ in $\mathcal{L}$, to record that we
have an incoming edge $\cdot\xrightarrow{\overline{\beta}}t$ to a PDSCC that
the fixpoint computation needs to process. Then, Algorithm 4 inserts in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[r][\overline{\beta}]$
the edges $t\xrightarrow{\overline{\beta}}y$ that outgo $t$’s component
(rooted at $r$) and for which $y$ is not in a breaking component. Finally, the
algorithm identifies the pairs $(x,\overline{\beta})$ in $\mathcal{L}$ for
which it has recorded at least two $\overline{\beta}$ neighbors out of $x$’s
component, and inserts them in $\mathcal{Q}$ to be processed by the fixpoint
algorithm later (Algorithm 4).

By structuring $\operatorname{MakePrimary}$ this way we have the following
benefits: (i) we spend no time in the non-affected DSCCs, and (ii) because we
maintain the PDSCCs, the time cost is only linear in the number of _nodes_ of
these affected DSCCs (and hence $O(n)$ in the worst case), as opposed to
linear in the number of the _edges_ incoming to these affected DSCCs (which
would be $O(n^{2})$). This ensures that
$\ell=\sum_{x,\overline{\alpha}}|{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[x][\overline{\alpha}]|=O(n)$
at the end of $\operatorname{MakePrimary}$ before calling
$\operatorname{Fixpoint}$; as shown in (Chatterjee et al., 2018, Lemma 3.4,
Lemma 3.5), a call to $\operatorname{Fixpoint}()$ takes time
$O(\ell\cdot\alpha(n))$.

###  3.4. Example

Here we give a step-by-step illustration of $\operatorname{DynamicAlgo}$ on
the example of Figure 1. We start with a description of the contents of the
various data structures before handling the edge insertion.

Let us fix some notations. Let $(v_{1},v_{2},\overline{R})\colon k$ denote
that there are $k$ edges from $v_{1}$ to $v_{2}$ labeled $\overline{R}$. The
elements of the set
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Count}}$
will contain entries of this kind. Likewise, let
$(v,\overline{L})\colon[v_{1},v_{2},\dots,v_{k}]$ represent that there are out
edges labeled $\overline{L}$ from $v$ to $v_{1},\dots,v_{k}$.
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}$
contains entries of this kind. We let
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}$
to contain entries of the kind $(v,\overline{L}):[v_{1},\dots,v_{k}]$ to
denote that there are edges labeled $\overline{L}$ from each of
$v_{1},\dots,v_{k}$ to $v$. The components in the
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}$
and
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{PrimCompDS}}$
data structures are listed as sequences of nodes $\\{(a),b,c,\dots\\}$, where
the node in the parenthesis denotes the component representative.

  1. (1)

${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Count}}:\\{(c,g,\overline{R})\colon
1,\,(f,c,\overline{L})\colon 1,\,(f,e,\overline{L})\colon
1,\,(f,d,\overline{L})\colon 1,\,(g,e,\overline{L})\colon
1,\,(h,f,\overline{L})\colon 1\\}$

  2. (2)

${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}:\\{(f,\overline{L})\colon[e,c,d],\,(g,\overline{L})\colon[e],\,(h,\overline{L})\colon[f],\,(c,\overline{R})\colon[g]\\}$

  3. (3)

${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}:\\{(d,\overline{L})\colon[f],\,(e,\overline{L})\colon[g],\,(f,\overline{L})\colon[h],\,(g,\overline{R})\colon[c]\\}$

  4. (4)

${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}:\\{(f,\overline{L}):[c],\,(c,\overline{R}):[g],\,(g,\overline{L}):[e],\,(h,\overline{L}):[f]\\}$

  5. (5)

${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}:\\{(c),d,e\\},\,\\{(g)\\},\,\\{(f)\\},\,\\{(h)\\}$

  6. (6)

${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{PrimCompDS}}-\operatorname{PDSCC}:\\{(c),d,e\\},\\{(g)\\},\\{(f)\\},\,\\{(h)\\}$

  7. (7)

$\mathcal{Q}:\emptyset$

We now describe the development of the data structures during the edge
insertion $(d,h,\overline{R})$.

  1. (1)

${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Count}}[d][h][\overline{R}]=1$.

  2. (2)

Since
$|{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[d][\overline{R}]|==0$,
the algorithm adds $d$ to the
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[h][\overline{R}]$.
Then, the algorithm inserts $h$ as the head of
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[d][\overline{R}]$.

  3. (3)

Get the root of $\operatorname{DSCC}$ containing $d$ , i.e.
$c={\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}.\operatorname{Find}(d)$.
Then add $h$ to
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[c][\overline{R}]$.
So, updated
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[c][\overline{R}]=(g,h)$.

  4. (4)

Since,
$|{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[c][\overline{R}]|\geq
2$. The algorithm inserts $(c,\overline{R})$ in $\mathcal{Q}$ and invokes
$\operatorname{Fixpoint}()$.

  5. (5)

Inside $\operatorname{Fixpoint}()$: First, we extract $(c,\overline{R})$ from
$\mathcal{Q}$. Then we get the set $S=\\{g,h\\}$. Since $|S|\geq 2$, the
algorithm merges $\operatorname{DSCC}$s $[(g)],[(h)]$ into single
$\operatorname{DSCC}[(h),g]$. Then, moves
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[g][\overline{L}]$
to
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[h][\overline{L}]$.
Now, since
$|{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[h][\overline{L}]|\geq
2$, insert $(h,\overline{L})$ to $\mathcal{Q}$. This will lead to merging of
$\operatorname{DSCC}$s $[(c),d,e]$ and $[(f)]$ into $\operatorname{DSCC}$
$[(f),c,d,e]$. This finishes the fixpoint.

After the insertion, the data structures are in the following state.

  1. (1)

${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Count}}$:
new entry $(d,h,\overline{R})\colon 1$;
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}$:
new entry $(d,\overline{R})\colon[h]$;
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}$:
new entry $(h,\overline{R})\colon[d]$; $\mathcal{Q}:\emptyset$

  2. (2)

${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}:\\{(f,\overline{L}):[c],\,(f,\overline{R}):[h],\,(h,\overline{L}):[f]$

  3. (3)

${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}:\\{(f),c,d,e\\},\,\\{(h),g\\}$

  4. (4)

${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{PrimCompDS}}-\operatorname{PDSCC}:\\{(c),d,e\\},\,\\{(g)\\},\,\\{(f)\\},\,\\{(h)\\}$

We now describe the development of the data structures during the edge
deletion $(f,d,\overline{L})$.

  1. (1)

${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Count}}[f][d][\overline{L}]=0$.
Since $d$ is at tail of
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[f][\overline{L}]$,
remove $f$ from
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[d][\overline{L}]$.

  2. (2)

In
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[f][\overline{L}]$,
$c$ is penultimate element. Hence, the algorithm inserts $f$ in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[c][\overline{L}]$.

  3. (3)

Remove edge $(c,d)$ from
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{PrimCompDS}}$.

  4. (4)

Remove $d$ from
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[f][\overline{L}]$.

  5. (5)

Invoke $\operatorname{MakePrimary}()$:

    1. (1)

Insert $f=\operatorname{DSCCRepr}(d)$ to $\mathcal{S}$ and $\mathcal{Z}$.

    2. (2)

In the loop from Algorithm 4 to Algorithm 4 the algorithm inserts
$h=\operatorname{DSCCRepr}(g)$ to $\mathcal{S}$ and $\mathcal{Z}$.

    3. (3)

$\mathcal{Z}$ contains $f,h$ and by following
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}$,
algorithm re-initializes
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[f][\overline{L}]$,
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[f][\overline{R}]$
and
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[h][\overline{L}]$
to an empty list.

    4. (4)

Since $\mathcal{Z}$ contains $f$ and $h$, we split $\operatorname{DSCC}(f)$
and $\operatorname{DSCC}(h)$ to their $\operatorname{PDSCC}$s. Then the
algorithm inserts roots of new components in $\mathcal{R}$. So, we get
$\mathcal{R}=\\{c,d,f,g,h\\}$.

    5. (5)

In the next step the algorithm gathers edges for fixpoint computations. For
each root $r$ in $\mathcal{R}$, the algorithm iterate over all nodes in
$\operatorname{DSCC}(r)$. For each node $t$ in $\operatorname{DSCC}(r)$ and
each edge type $\overline{\beta}\in\\{\overline{L},\overline{R}\\}$ the
algorithm checks if there exists node
$s\in{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[t][\overline{\beta}]$.
For all such nodes $s$, the algorithm inserts $t$ in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[\operatorname{DSCCRepr}(s)][\overline{\beta}]$
and $(\operatorname{DSCCRepr}(s),\overline{\beta})$ in $\mathcal{L}$ (lines
Algorithm 4 to Algorithm 4) . In lines Algorithm 4 \- Algorithm 4 the
algorithm checks if
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[t][\overline{\beta}]\geq
1$. If yes, then inserts $x=$ first node of
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[t][\overline{\beta}]$
in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[r][\overline{\beta}]$.

So after Algorithm 4 the updated
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}$
and $\mathcal{L}$ will be:

      1. (1)

${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}:\\{(c,\overline{R})\colon[g],\,(f,\overline{L})\colon[c],\,(h,\overline{L})\colon[f],\,(g,\overline{L})\colon[e],(d,\overline{R})\colon[h]$.

      2. (2)

$\mathcal{L}:(d,\overline{R}),(f,\overline{L}),(c,\overline{R}),(g,\overline{L}),(h,\overline{L})$.

Then the algorithm iterates over all $(x,\overline{\beta})$ $\in\mathcal{L}$,
and checks if
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[x][\overline{\beta}]\geq
2$. If yes, then inserts $(x,\overline{\beta})$ in $\mathcal{Q}$. So, for the
$\mathcal{L}$, computed in above step, no element will be added to the
$\mathcal{Q}$.

  6. (6)

Since $\mathcal{Q}$ is empty, the call to $\operatorname{Fixpoint}()$ will not
merge any components.

After the deletion, the data structures are in the following state.

  1. (1)

${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Count}}:\\{(c,g,\overline{R})\colon
1,\,(f,c,\overline{L})\colon 1,\,(f,e,\overline{L})\colon
1,\,(f,d,\overline{L})\colon 0,\,(g,e,\overline{L})\colon
1,\,(h,f,\overline{L})\colon 1,\,(d,h,\overline{R})\colon 1\\}$,

  2. (2)

${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}:\\{(f,\overline{L})\colon[e,c],\,(g,\overline{L})\colon[e],\,(h,\overline{L})\colon[f],\,(c,\overline{R})\colon[g],\,(d,\overline{R})\colon[h]\\}$,

  3. (3)

${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}:\\{(c,\overline{L})\colon[f],\,(e,\overline{L})\colon[g],\,(f,\overline{L})\colon[h],\,(g,\overline{R})\colon[c],\,(h,\overline{R})\colon[d]\\}$

  4. (4)

${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}:\\{(c,\overline{R}):[g],\,(f,\overline{L}):[c],\,(h,\overline{L}):[f],\,(g,\overline{L}):[e],\,(d,\overline{R}):[h]\\}$

  5. (5)

${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}:\\{(c),e\\},\\{(d)\\},\\{(g)\\},\\{(f)\\},\\{(h)\\}$

  6. (6)

${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{PrimCompDS}}-\operatorname{PDSCC}:\\{(c),e\\},\\{(d)\\},\\{(g)\\},\\{(f)\\},\\{(h)\\}$

  7. (7)

$\mathcal{Q}:\emptyset$

###  3.5. Correctness and Complexity

Finally, we state the correctness and complexity of
$\operatorname{DynamicAlgo}$.

See 1.1

Next, we state the main invariants that $\operatorname{DynamicAlgo}$ maintains
which support its correctness and complexity, as well as some intuition behind
them. For proofs, we refer to Appendix A.

Correctness. The basis of the correctness of $\operatorname{DynamicAlgo}$ is a
number of invariants that are maintained along edge insertions and deletions.
Observe that
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[u][\overline{\alpha}]$
is, at all times, a linked list representation of the edge set
$u\xrightarrow{\overline{\alpha}}\cdot$.

Our first invariant concerns the correct maintenance of the PDSCCs of $G$ in
the
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{PrimCompDS}}$
data structure maintaining undirected connectivity. To prove the invariant, we
argue that $\operatorname{DynamicAlgo}$ inserts and removes sufficient and
necessary undirected edges in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{PrimCompDS}}$
to (sparsely) represent the connected components of the corresponding primal
graph. This follows directly from the sparsification approach outlined in
Section 3.2 and Figure 4. Indeed, the algorithm maintains in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{PrimCompDS}}$
a set of edges that connect neighboring nodes in each linked list
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[u][\overline{\alpha}]$.
Thus, the omitted edges (i.e., between non-neighboring nodes in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[u][\overline{\alpha}]$)
are anyway transitively connected in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{PrimCompDS}}$.
Formally, we have the following lemma.

###### Lemma 3.1.

After every insert and delete operation, the connected components in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{PrimCompDS}}$
are precisely the PDSCCs of $G$.

The next invariant concerns the correct maintenance of the
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}$
data structure, and is established in Lemma 3.2 and Lemma 3.3. In words, the
invariant states that
$x\in{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[z][\overline{\beta}]$
iff we have an edge $x\xrightarrow{\overline{\beta}}z$ and $z$ is the last
node in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[x][\overline{\beta}]$.
Thus, when $\operatorname{MakePrimary}()$ constructs the PDSCCs and discovers
their incoming edges, the edge
$x\xrightarrow{\overline{\beta}}\operatorname{PDSCC}(z)$ is correctly
discovered by finding that
$x\in{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[z][\overline{\beta}]$
(Algorithm 4).

Lemma 3.2 is concerned with the soundness, and is straightforward. Any time
the algorithm inserts
$x\in{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[z][\overline{\beta}]$,
this is followed by inserting $z$ in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[x][\overline{\beta}]$
(in the case of edge insertions, Algorithm 2 and Algorithm 2 in Algorithm 2).
In the case of edge deletions, the insertion
$x\in{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[z][\overline{\beta}]$
is preceded by inserting $z$ to
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[x][\overline{\beta}]$
in a previous update (Algorithm 3 and Algorithm 3 in Algorithm 3). In this
case,
$x\in{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[z][\overline{\beta}]$
takes place when $z$ becomes the last node in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[x][\overline{\beta}]$
after deletion of edges $x\xrightarrow{\overline{\beta}}v$, where $v$ appeared
later than $z$ in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[x][\overline{\beta}]$.

###### Lemma 3.2.

After every insert and delete operation, for every two nodes $x,z\in V$ and
label $\overline{\beta}\in\Sigma^{C}$, if
$x\in{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[z][\overline{\beta}]$
then $x\xrightarrow{\overline{\beta}}z$ and $z$ is the last node in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[x][\overline{\beta}]$.

Similarly, for Lemma 3.3, if
$x\xrightarrow{\overline{\beta}}\operatorname{PDSCC}(y)$, then the last node
$z$ in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[x][\overline{\beta}]$
is also in $\operatorname{PDSCC}(y)$, while the algorithm maintains that
$x\in{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[z][\overline{\beta}]$.
Hence, the fact that $x\xrightarrow{\overline{\beta}}\operatorname{PDSCC}(y)$
is recoverable via discovering that
$x\in{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[z][\overline{\beta}]$.

###### Lemma 3.3.

After every insert and delete operation, for every pair of nodes $x,y\in V$
and label $\overline{\beta}\in\Sigma^{C}$, if
$x\xrightarrow{\overline{\beta}}\operatorname{PDSCC}(y)$ then there exists a
node $z\in\operatorname{PDSCC}(y)$ such that
$x\in{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[z][\overline{\beta}]$.

The next lemma captures the correctness of $\operatorname{MakePrimary}()$ and
the invariants concerning the state that it passes on to function
$\operatorname{Fixpoint}()$ for the final fixpoint computation after
processing a $\operatorname{delete}(u,v,\overline{\alpha})$ update. Recall
that $\operatorname{MakePrimary}()$ identifies an overapproximation of the
DSCCs that have to be split and rebuilt as a result of this edge deletion. The
lemma has two parts. Item (1) states that the components that
$\operatorname{MakePrimary}()$ passes on to $\operatorname{Fixpoint}()$ (i.e.,
those found in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}$)
are a refinement of the DSCC decomposition of $G$ after the deletion, i.e., it
suffices to merge some of them in order to arrive at the correct DSCC-
decomposition of the graph after the edge deletion. The
$\operatorname{Fixpoint}()$ function will perform this merging by processing
the edges found in the
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}$
data structure. Item (2) states that $\operatorname{MakePrimary}()$ populates
the
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}$
data structure with sufficiently many edges for $\operatorname{Fixpoint}()$ to
process and arrive at the correct DSCC decomposition of $G$.

###### Lemma 3.4.

At the end of $\operatorname{MakePrimary}()$, the following assertions hold.

  1. (1)

Every component in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}$
is a (not necessarily maximal) DSCC of $G$.

  2. (2)

For every component in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}$
rooted in some node $x$, the following hold.

    1. (a)

For every node $y$ and label $\overline{\beta}$, if
$y\in{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[x][\overline{\beta}]$
then there is an edge $z\xrightarrow{\overline{\beta}}w$, where $z$ is a node
in the component of $x$, and $w$ is a node in the component of $y$ in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}$.

    2. (b)

For every node $z$ and label $\overline{\beta}$ such that (i) $z$ is in the
component rooted at node $x$ in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}$,
and (ii) there is an edge $z\xrightarrow{\overline{\beta}}w$, there exists a
node $y$ in the component of $w$ in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}$
such that
$y\in{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[x][\overline{\beta}]$.

Given the above invariants, $\operatorname{MakePrimary}$ creates a correct
state of the worklist $\mathcal{Q}$ and the
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}$
linked lists for the $\operatorname{Fixpoint}()$ call of Algorithm 3
(Algorithm 3) to compute the correct DSCC decomposition. This leads ot the
correctness of $\operatorname{DynamicAlgo}$.

###### Lemma 3.5.

After every $\operatorname{insert}(u,v,\overline{\alpha})$ and
$\operatorname{delete}(u,v,\overline{\alpha})$,
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}$
contains the DSCCs of $G$.

Complexity. We now turn our attention to the complexity bound of Theorem 1.1.
We always start with a graph of $n$ nodes but without any edges, for which the
initialization of all data structures takes $O(n)$ time. In practice, the
initial graph might already have some edges, which can be thought of being
inserted one-by-one.

In high level, the time $\operatorname{DynamicAlgo}$ spends in each edge
insertion and deletion is the sum of two parts: (i) the time taken for
maintaining the PDSCCs in the
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{PrimCompDS}}$
data structure, and (ii) the time taken for all other computations. Regarding
(i), so far we have not specified the precise data structure for implementing
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{PrimCompDS}}$,
as $\operatorname{DynamicAlgo}$ treats
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{PrimCompDS}}$
as a black box. The theoretical guarantees of Theorem 1.1 can be obtained by
using the data structure of (Eppstein et al., 1997) for undirected
connectivity (see Table 1). Although this guarantees $O(\sqrt{n})$ and $O(1)$
time for edge insertions/deletions and queries, respectively, here we only use
the fact that both bounds are less than $n$. Regarding (ii), the algorithm
spends $O(n\cdot\alpha(n))$ for each operation, which stems from the fact that
the algorithm encounters each node of $G$ across all data structures a
constant number of times (recall that we have $k=O(1)$ labels in $G$). In
particular, we have the following lemma.

###### Lemma 3.6.

Every $\operatorname{insert}(u,v,\overline{\alpha})$ and
$\operatorname{delete}(u,v,\overline{\alpha})$ operation is processed in
$O(n\cdot\alpha(n))$ time.

###### Proof.

After every insert and delete operation, $\operatorname{Fixpoint}()$ is
invoked for merging the DSCCs (in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}$).
As shown in (Chatterjee et al., 2018, Lemma 3.4, Lemma 3.5), a call to
$\operatorname{Fixpoint}()$ takes time $O(\ell\cdot\alpha(n))$, where
$\ell=\sum_{u,\overline{\alpha}}|{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[x][\overline{\alpha}]|$
is the total number of nodes stored in the
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}$
linked lists, and $\alpha(n)$ is the inverse Ackermann function. After
$\operatorname{Fixpoint}()$ has completed, we have
$|{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[x][\overline{\alpha}]|\leq
1$ for each $x$ and $\overline{\alpha}$. Thus to prove Lemma 3.6, it suffices
to argue that every operation takes $O(n)$ time before calling
$\operatorname{Fixpoint}()$. This implies that $\ell=O(n)$ before the call,
and thus $\operatorname{Fixpoint}()$ takes $O(n\cdot\alpha(n))$ time, yielding
$O(n)+O(n\cdot\alpha(n))=O(n\cdot\alpha(n))$ total time.

Edge insertions. Consider the processing of an operation
$\operatorname{insert}(u,v,\overline{\alpha})$ by Algorithm 2. Observe that
the algorithm has no loops, thus the running time is dominated by the time
taken to access the various data structures that the algorithm maintains. In
particular,
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}$
is a simple linked list, and checking its length (Algorithm 2), as well as
accessing and inserting in the head (Algorithm 2 and Algorithm 2) takes
constant time. Similarly, the data structures
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}$
and
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}$
are simple sets and linked lists with $O(1)$ accesses. As we have already
argued in Section 2.2, performing a
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}.\operatorname{Find}(v)$
operation (Algorithm 2) takes $O(1)$ time. Finally, inserting the edge $(v,y)$
in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{PrimCompDS}}$
takes $O(\sqrt{n})$ time (Eppstein et al., 1997).

Edge deletions. Consider the processing of an operation
$\operatorname{delete}(u,v,\overline{\alpha})$ by Algorithm 3. The time spent
in the body of Algorithm 3 is $O(n)$, by an analysis very similar to Algorithm
2 for edge deletions, and we will not repeat it here. Instead, we focus on the
time spent in the call to $\operatorname{MakePrimary}()$, which is the more
complex part of processing the edge deletion (Algorithm 4). In the first step
(Algorithm 4 to Algorithm 4), for each iteration of the while loop of
Algorithm 4, the condition in Algorithm 4 can be checked in
$O(|\operatorname{DSCC}(x)|)$ time, by iterating over all nodes of
$\operatorname{DSCC}(x)$. Observe that $\operatorname{DSCC}(x)$ is examined
only once throughout this loop of Algorithm 4, and since the DSCCs partition
the node set, total time for running this loop is $O(n)$.

The time spent in the second step (Algorithm 4 to Algorithm 4) is the sum of
two parts. The first part corresponds to the time spent in the nested loops,
which is proportional to the number of times the inner-most loop in Algorithm
4 is taken. That is, the number of nodes $x$ that exist in the lists
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[t][\overline{\beta}]$
of nodes $t$ in the components represented by their roots in $\mathcal{Z}$. It
suffices to argue that there do not exist nodes $x,s_{1},s_{2}$ and label
$\overline{\beta}$ such that
$x\in{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[s_{1}][\overline{\beta}]$
and
$x\in{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[s_{2}][\overline{\beta}]$.
Indeed, by Lemma 3.2, if
$x\in{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[s_{1}][\overline{\beta}]$
then $s_{1}$ is the last node in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[x][\overline{\beta}]$.
Clearly, as a linked list,
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[x][\overline{\beta}]$
can have at most one last node, hence
$x\not\in{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[s_{2}][\overline{\beta}]$.
Thus, for every label $\overline{\beta}$, the loop in Algorithm 4 is executed
at most once per node $x$ leading to $O(n)$ total iterations. The second part
corresponds to the total time spent in Algorithm 4. In Algorithm 4, the
algorithm splits the potentially affected DSCCs (in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{DisjointSets}}$)
into its PDSCCs. This takes $O(n)$ time as the algorithm simply iterates over
the nodes of the DSCCs stored in $\mathcal{Z}$. For each such node, the
algorithm performs a single membership query to
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{PrimCompDS}}$,
which takes $O(1)$ time (Eppstein et al., 1997).

Finally, we consider the time spent by $\operatorname{MakePrimary}()$ in the
third step (Algorithm 4 to Algorithm 4). Note that the time spent in these
nested loops is proportional to the number of times the inner-most loop
(Algorithm 4) is executed. Again, it suffices to argue that there do not exist
nodes $x,s_{1},s_{2}$ and label $\overline{\beta}$ such that
$x\in{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[s_{1}][\overline{\beta}]$
and
$x\in{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[s_{2}][\overline{\beta}]$.
Indeed, by Lemma 3.2, if
$x\in{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[s_{1}][\overline{\beta}]$
then $s_{1}$ is the last node in
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{OutEdges}}[x][\overline{\beta}]$,
hence
$x\not\in{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{InPrimary}}[s_{2}][\overline{\beta}]$.
Thus, for every label $\overline{\beta}$, the loop in Algorithm 4 is executed
at most once per node $x$, leading to $O(n)$ total iterations. In the end, the
loop in Algorithm 4 runs for $|\mathcal{L}|$ iterations, which is bounded by
the iterations of the previous loop.

Since for every label $\overline{\beta}$ and node $x$ the loop in Algorithm 4
is executed at most once, it follows that Algorithm 4 will be executed $O(n)$
times. This leads to total $O(n)$ new entries to
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}$
at Algorithm 4. Similarly, Algorithm 4 is executed $O(n)$ times leading to
$O(n)$ new entries to
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}$.
Therefore, at the end of $\operatorname{MakePrimary}()$ we have
$\sum_{x,\overline{\alpha}}|{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[x][\overline{\alpha}]|=O(n)$.
The loop in Algorithm 4 runs for $|\mathcal{L}|=O(n)$ iterations. This leads
to $O(n)$ entries in $\mathcal{Q}$. Thus, at the end of
$\operatorname{MakePrimary}()$, $|\mathcal{Q}|=O(n)$. Thus before calling
$\operatorname{Fixpoint}()$ we have
$\sum_{u,\overline{\alpha}}|{\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{Edges}}[u][\overline{\alpha}]|=O(n)$
and $|\mathcal{Q}|=O(n)$. ∎

##  4\. Experiments

In this section we report on an implementation of $\operatorname{DynamicAlgo}$
algorithm behind Theorem 1.1, and an evaluation of its performance on various
datasets on real-world static analyses. To some extent, our experimental
setting follows (Li et al., 2022).

Compared algorithms. We compare three standard approaches to bidirected Dyck
reachability333Since the algorithm of (Li et al., 2022) has complexity and
correctness issues, we have not included it in our evaluation..

  1. (1)

$\operatorname{OfflineAlgo}$, as developed and implemented in (Chatterjee et
al., 2018). For each graph update (edge insertion/deletion), the algorithm is
invoked from scratch to handle the updated graph.

  2. (2)

Our $\operatorname{DynamicAlgo}$, which is implemented in C/C++, and closely
follows the pseudocode presented in Section 3. $\operatorname{DynamicAlgo}$
uses as a black box a data structure
${\color[rgb]{0,.5,.5}\definecolor[named]{pgfstrokecolor}{rgb}{0,.5,.5}\operatorname{PrimCompDS}}$
for dynamic undirected connectivity (see Table 1). Although the one developed
in (Eppstein et al., 1997) works best towards the complexity guarantees of
Theorem 1.1, in our implementation we use the one developed in (Holm et al.,
2001) (and implemented in (Tseng, 2020)), as it is conceptually simpler and
well-performing in practice.

  3. (3)

A declarative approach in which the production rules of Dyck reachability are
encoded as Datalog constraints and dispatched to a Datalog solver (Reps,
1995b). Datalog-based static analyses have been popularized in the Flix
programming language (Madsen and Lhoták, 2020) and the Doop framework
(Bravenboer and Smaragdakis, 2009). Our bidirected setting allows us to
optimize the Datalog program by explicitly focusing only on closing-
parentheses edges, in similar style to $\operatorname{OfflineAlgo}$ and
$\operatorname{DynamicAlgo}$. To be fair in our comparison, we follow this
approach here. In particular, we use the following Datalog program.

⬇

Reaches(u,u)

Close(x,u,$\overline{\alpha}$):- Edge(x,u,$\overline{\alpha}$)

Close(x,u,$\overline{\alpha}$):- Edge(y,u,$\overline{\alpha}$), Reaches(x,y)

Reaches(u,v):- Close(x,u,$\overline{\alpha}$), Close(x,v,$\overline{\alpha}$)

Reaches(u,v):- Reaches(u,x), Reaches(x,v)

To handle our dynamic setting, we rely on an efficient, fully dynamic Datalog
solver (Ryzhyk and Budiu, 2019), as opposed to solving the Datalog program
from scratch every time.

The two algorithms ($\operatorname{OfflineAlgo}$ and dynamic Datalog) that
support our experimental comparison serve as very fitting baselines.
$\operatorname{OfflineAlgo}$ is an algorithm dedicated to the _problem_ we are
solving (i.e., bidrected Dyck reachability) but not dedicated to the _setting_
we are solving it in (i.e., under dynamic updates). On the other hand, the
dynamic-Datalog approach is dedicated to the dynamic setting, but not
dedicated to the bidirected Dyck-reachability problem. As such, both
algorithms are theoretically of worse complexity that our
$\operatorname{DynamicAlgo}$, yet still the closest that exist in the
literature for this problem and setting. Our experiments aim to highlight to
what extent the theoretical superiority of $\operatorname{DynamicAlgo}$ is
realized in practice.

Benchmarks. We evaluate the above algorithms on two popular static analyses.

  1. (1)

Context-sensitive data dependence analysis as formulated in (Tang et al.,
2015), and evaluated on benchmark programs from (SPE, 2008). In this case the
parenthesis labels represent calling contexts, and a properly-balanced-
parenthesis path represents an interprocedurally-valid dataflow via parameter-
passing in function invocation and return.

  2. (2)

Field-sensitive alias analysis for Java as formulated in (Yan et al., 2011;
Zhang et al., 2013), and evaluated on DaCapo benchmarks (Blackburn et al.,
2006). In this case the parenthesis labels represent field accesses on
composite objects, as illustrated in Figure 1 of Section 1.

Our graph models for the above analyses and benchmarks are obtained from (Li
et al., 2022).

On-the-fly formulation and update sequences. To simulate the on-the-fly
setting where the source code undergoes a sequence of changes, for each
benchmark graph $G$, we generate three sequences $\mathcal{S}_{G}$ of updates
(edge insertions/deletions), as follows.

  1. (1)

_Incremental setting:_ We randomly select a set $E^{+}$ of 90% of the edges of
$G$ and remove them from the graph. We create a sequence of edge insertions
$\mathcal{S}^{\mathsf{inc}}_{G}$ as a random permutation of $E^{+}$. This is a
fully incremental setting, where code lines are only added but never removed
in the program.

  2. (2)

_Decremental setting:_ We randomly select a set $E^{-}$ of 90% of the edges of
$G$. We create a sequence of edge deletions $\mathcal{S}^{\mathsf{dec}}_{G}$
as a random permutation of $E^{-}$. This is a fully decremental setting, where
code lines are only removed but never added in the program.

  3. (3)

_Mixed setting:_ We randomly split the edges of $G$ into two sets $E^{+}$ and
$E^{-}$, with proportion 10% to 90%, and start with an initial graph
containing the edges of $E^{-}$. We create a sequence of mixed operations
(both insertions and deletions) $\mathcal{S}^{\mathsf{dec}}_{G}$ by repeated
stochastic sampling: in each step, we randomly choose the next operation as an
edge insertion/edge deletion. In the former case, we randomly select an edge
from $E^{+}$, move it to $E^{-}$, and insert it in $G$. In the latter case, we
randomly select an edge from $E^{-}$, move it to $E^{+}$, and delete it from
$G$. The length of the sequence is equal to 90% of the number of edges in $G$.

In each case, for each benchmark we report the amortized time that each
algorithm took to handle the whole sequence: that is, the total running time
over the whole sequence divided by the length of the sequence. To gain more
confidence in our results, we repeat the above process three times and report
the average numbers. We run our experiments on a conventional laptop with a
2.6GHz CPU and 16GBs of memory, which was always sufficient for the analysis.
As a sanity check, we have verified that all three algorithms give the same
results on each benchmark and update sequence.

$S_{1}$$S_{2}$$S_{3}$$S_{4}$btreecheckcompilercompresscryptoderbyhelloworldmpegaudiomushroomparsersamplescimarkstartupsunflowxml$10^{0}$$10^{2}$$10^{4}$microsecsData
Dependence AnalysisOfflineDDlogDynamic

(a) Incremental updates.

$S_{1}$$S_{2}$$S_{3}$$S_{4}$antlrbloatcharteclipsefophsqldbjythonluindexlusearchpmdxalan$10^{2}$$10^{4}$$10^{6}$microsecsAlias
AnalysisOfflineDDlogDynamic

(b) Incremental updates.

$S_{1}$$S_{2}$$S_{3}$$S_{4}$btreecheckcompilercompresscryptoderbyhelloworldmpegaudiomushroomparsersamplescimarkstartupsunflowxml$10^{0}$$10^{2}$$10^{4}$microsecsOfflineDDlogDynamic

(c) Decremental updates.

$S_{1}$$S_{2}$$S_{3}$$S_{4}$antlrbloatcharteclipsefophsqldbjythonluindexlusearchpmdxalan$10^{2}$$10^{4}$$10^{6}$microsecsOfflineDDlogDynamic

(d) Decremental updates.

$S_{1}$$S_{2}$$S_{3}$$S_{4}$btreecheckcompilercompresscryptoderbyhelloworldmpegaudiomushroomparsersamplescimarkstartupsunflowxml$10^{0}$$10^{2}$$10^{4}$microsecsOfflineDDlogDynamic

(e) Mixed updates.

$S_{1}$$S_{2}$$S_{3}$$S_{4}$antlrbloatcharteclipsefophsqldbjythonluindexlusearchpmdxalan$10^{2}$$10^{4}$$10^{6}$microsecsOfflineDDlogDynamic

(f) Mixed updates.

Figure 7.  The average time to handle a single update on on-the-fly data-
dependence analysis (7(a), 7(c), 7(e)) and on-the-fly alias analysis (7(b),
7(d), 7(f)) for sequence files generated with 90-10 split of original graph.
Note that all results are in log-scale.

Results on data-dependence analysis. Our experimental results on on-the-fly
the data-dependence analysis are shown in Figure 7 (left column). We see that
in all three settings (incremental/decremental/mixed), the dynamic-Datalog
approach is measurably faster than $\operatorname{OfflineAlgo}$. Although, in
the worst case, the Datalog solver has worse complexity than
$\operatorname{OfflineAlgo}$, the nature of the updates on the analyses graphs
allows an efficient Datalog solver dedicated to dynamic updates to perform
faster, as it never exhibits its worst-case performance. Still, the time spent
by the Datalog solver is typically quite large, given that we are looking at
updates by a _single edge_ (i.e., a single source-code line).

On the other hand, our $\operatorname{DynamicAlgo}$ spends much less time than
both $\operatorname{OfflineAlgo}$ and the dynamic Datalog solver, leading to
typical speedups between two and three orders of magnitude. The only
difference is in xml, where $\operatorname{DynamicAlgo}$ appears to spend more
time than in the rest of the benchmarks. We have identified that this
benchmark has a disproportionately large number of parenthesis symbols, which
is the likely cause of this behavior. Still, $\operatorname{DynamicAlgo}$ is
by far the fastest approach also on this benchmark. Naturally, decremental
updates yield the least speedup on average. This is expected given how much
more complex our procedure for handling deletions is compared to that of
handling insertions. Indeed, when processing a
$\operatorname{insert}(u,v,\overline{\alpha})$ update, our algorithm only
merges DSCCs, while processing a
$\operatorname{delete}(u,v,\overline{\alpha})$ update both splits and merges
DSCCs. Nevertheless, the speedups are still in the range of two orders of
magnitude, enough to render $\operatorname{DynamicAlgo}$ the clear best
approach overall.

Results on alias analysis. Our experimental results on on-the-fly the alias
analysis are shown in Figure 7 (right column). In contrast to the data-
dependence analysis, here the dynamic-Datalog approach is always a bit worse
that $\operatorname{OfflineAlgo}$, indicating that reachability patterns in
these graphs are more challenging; enough so to push the dynamic-Datalog
solver to worse performance than the from-scratch
$\operatorname{OfflineAlgo}$. Note, also, that the analysis times here are
considerably larger than in the case of data-dependence analysis.

$\operatorname{DynamicAlgo}$ is again the best-performing approach by far,
consistently by three orders of magnitude. In several benchmarks, its running
time is not visible despite the log-scale of the plots. Finally, we again
observe that decremental updates are overall more challenging that incremental
updates.

In summary. Our experiments clearly show that $\operatorname{DynamicAlgo}$ is
the right approach to on-the-fly static analyses formulated as bidirected Dyck
reachability, giving several orders of magnitude speedups over both (i) the
offline algorithm that is dedicated (and optimal) for bidirected Dyck
reachability, and (ii) the dynamic Datalog approach that is dedicated to
dynamic updates (but agnostic to the setting of bidirected Dyck reachability).
Although the worst-case running time of $\operatorname{DynamicAlgo}$ is
linear, we rarely observed this in our experiments. Instead, the time cost of
each update is barely (if at all) noticeable to the human eye, and thus the
algorithm is suitable for continuous analysis, e.g., integrated inside an IDE.

##  5\. Related Work

The importance of Dyck reachability in static analyses has lead to a
systematic study of its complexity in various settings. The problem has a
simple $O(n^{3})$ upper bound (Yannakakis, 1990), which has resisted
improvements beyond logarithmic (Chaudhuri, 2008). Due to this reason, the
complexity of Dyck reachability has also been studied in terms of lower
bounds. Even for a single-pair query, the problem has been known to be 2NPDA-
hard (Heintze and McAllester, 1997), while its combinatorial cubic hardness
persists even on constant-treewidth graphs (Chatterjee et al., 2018). All-
pairs Dyck reachability was recently shown to have a conditional $n^{2.5}$
lower bound based on popular complexity-theoretic hypotheses (Koutris and
Deep, 2023). Despite the cubic hardness of the general problem, it is known to
have sub-cubic certificates for both positive and negative instances
(Chistikov et al., 2022). All-pairs reachability with $k=1$ parenthesis (aka
one-counter systems) was recently shown to admit an
$O(n^{\omega}\cdot\log^{2}n)$ bound (Mathiasen and Pavlogiannis, 2021), where
$\omega$ is the matrix multiplication exponent, which is also tight even for
single-pair queries (Cetti Hansen et al., 2021). We refer to (Pavlogiannis,
2023) for a recent survey on this rich problem.

The technique developed in this work for on-the-fly bidirected Dyck
reachability is motivated by the same setting on undirected connectivity,
which has been studied extensively. We leverage the data structure developed
in (Eppstein et al., 1997) for maintaining the PDSCCs of a graph as connected
components of the underlying primary graph (which is indeed undirected), as
well as a sparsification technique that is specific to our setting (even
though the concept of sparsification was developed in (Eppstein et al., 1997)
to handle undirected connectivity). It would be interesting to investigate
whether techniques from undirected connectivity can be used further in our
setting so as to reduce the complexity to sublinear (as is the status quo in
undirected connectivity). However, as a single update can create or merge
$\Theta(n)$ DSCCs, sublinear complexity can only arise in the amortized sense,
or by not requiring the explicit maintenance of DSCCs throughout updates.
Though we can easily obtain an $O(\alpha(n))$ amortized insertion cost for our
technique (by amortizing over the linear cost of deletes), tighter bounds
appear non-trivial and are open to interesting future work.

Bidirected Dyck reachability is very similar to unification closure, though
the later problem is typically phrased with labels on the nodes as opposed to
the edges of the input graph (Kanellakis and Revesz, 1989). Unification
closure has found widespread applications in programming languages, such as in
efficient binding-time analysis (Henglein, 1991), simple first-order type-
inference (Møller and Schwartzbach, 2018), efficient dynamic type inference
for LISP (Henglein, 1992), as well as Steensgaard’s famous pointer analysis
(Steensgaard, 1996). The insights developed here for the on-the-fly setting
are likely extendable to these applications, though this merits further
investigation.

In this work we have focused on online analyses where the analyzed source code
changes frequently. Another “on-the-fly” style of analysis is that of _on-
demand_ analysis. Here the analyzed program remains unchanged, but the task is
to answer a sequence of analysis queries that is not known in advance. This
setting has been studied a lot in the context of pointer analysis (Heintze and
Tardieu, 2001; Sridharan et al., 2005; Zheng and Rugina, 2008; Yan et al.,
2011) and data flow analysis (Horwitz et al., 1995; Naeem et al., 2010; Lerch
et al., 2015); the latter have also been efficiently parameterized by
treewidth (Chatterjee et al., 2015, 2016, 2020) and treedepth (Goharshady and
Zaher, 2023).

##  6\. Conclusion

On-the-fly analysis is a very appealing feature to static analyzers, in order
to run in real-time during code development and incorporate the constant