11institutetext: Department of Computer Science, University of Münster,
Germany

# A Navigation Logic for Recursive Programs with Dynamic Thread Creation

Roman Lakenbrink  Markus Müller-Olm  Christoph Ohrem  Jens Gutsfeld

###### Abstract

Dynamic Pushdown Networks (DPNs) are a model for multithreaded programs with
recursion and dynamic creation of threads. In this paper, we propose a
temporal logic called NTL for reasoning about the call- and return- as well as
thread creation behaviour of DPNs. Using tree automata techniques, we
investigate the model checking problem for the novel logic and show that its
complexity is not higher than that of LTL model checking against pushdown
systems despite a more expressive logic and a more powerful system model. The
same holds true for the satisfiability problem when compared to the
satisfiability problem for a related logic for reasoning about the call- and
return-behaviour of pushdown systems. Overall, this novel logic offers a
promising approach for the verification of recursive programs with dynamic
thread creation.

###### Keywords:

Concurrency, Dynamic Pushdown Networks, Navigation Logic,
Model Checking, Satisfiability, Tree Automata

##  1 Introduction

Model Checking is an established technique for the verification of hardware
and software systems. Conceptually, it consists of checking whether a property
given in a specification logic holds for a model of a system. While logics
such as LTL or CTL and finite Kripke models were considered early on [12, 22],
later more expressive logics as well as infinite state systems have been
studied. The use of pushdown systems, for instance, allows for a more precise
analysis of recursive software systems due to the presence of a call stack of
a program while still retaining a decidable model checking problem against LTL
specifications [8]. In the context of pushdown systems, an example of a logic
more expressive than LTL is the logic CaRet [4] which extends LTL by operators
for non-regular properties of the call and return behaviour of pushdown
systems. This extension does not lead to increased complexity for the model
checking problem against pushdown systems compared to LTL.

However, there are even more powerful system models than pushdown systems for
which model checking of variants of LTL is decidable. In this paper, we
consider Dynamic Pushdown Networks (DPNs) [9], a model for software systems
that cannot model only recursion, but also multithreading with dynamic thread
creation. So far, the model checking problem for DPNs has only been considered
for single indexed LTL, a variant of LTL for multithreaded systems in which an
LTL formula is assigned to each thread [26]. Here, we consider the model
checking problem for a more expressive logic. More specifically, we propose a
fixpoint calculus with CaRet-like operators for the verification of DPNs via
model checking. The logic allows to specify non-regular properties concerning
the call and return behaviour of the different execution threads of a DPN.
Unlike CaRet, it can additionally specify properties concerning the thread-
spawn behaviour of programs. For example, consider a scenario where a program
has a method for bookkeeping information about spawned threads and it is
required that new threads be only spawned from this method in order to keep
the bookkeeping consistent. The property
$\mathcal{G}^{r}(\bigcirc^{c}\psi\rightarrow\mathcal{F}^{-}\textit{pr})$
specified in our new logic expresses that in all positions of all threads
(expressed through the modality $\mathcal{G}^{r}$), new threads fulfilling the
property $\psi$ are only spawned (expressed through $\bigcirc^{c}\psi$) when
the procedure pr is in the call stack (expressed through
$\mathcal{F}^{-}\textit{pr}$). This formalises the requirement. Properties
regarding such relationships between parent and child threads cannot be
expressed in the variant of LTL from [26] or other specification logics for
DPNs we are aware of. Our logic thus constitutes the first specification logic
able to reason about the thread spawning behaviour of DPNs.

Contributions and structure of the paper. After introducing some notation and
results (Section 2), we present a semantics for DPNs based on graphs (Section
3). As our first main contribution, we then introduce a novel specification
logic called Navigation Temporal Logic (NTL) with the ability to reason about
the call/return and thread creation behaviour of DPNs (Section 4). We discuss
some example properties and applications of our logic in Section 5. Towards
algorithmic verification, we then switch from a semantics based on graphs to a
semantics based on trees (Section 6). As our second main contribution, we then
investigate the model checking and satisfiability problems for the new logic
(Section 7). In particular, we show that the model checking problem is
decidable in time exponential in the size of the specification and polynomial
in the size of the system model, i.e. the same as for LTL model checking
against pushdown systems, and that the satisfiability problem is solvable in
time exponential in the size of the specification, i.e. the same as for the
satisfiability problem for $\mathit{VP}$-$\mu$-$\mathit{TL}$ [10], a temporal
logic subsuming CaRet and subsumed by our logic. For both problems, we
establish matching lower bounds. Section 8 concludes the paper. Due to lack of
space, some technical proofs can be found in an appendix.

Related work. There are several specification logics related to the logic we
present in this paper. The temporal logic LTL was considered for model
checking finite state systems [22] as well as pushdown systems [8]. For
pushdown models, CaRet was developed with different successor types that allow
the inspection of the call and return behaviour of the system [4]. Also,
variants of CaRet have been studied in the literature [3, 2, 11, 17]. As
mentioned, CaRet is one inspiration for the logic presented in this paper and
we adopt and complement its successor types in our logic. Other inspirations
are the linear time $\mu$-calculus from [28] and the logic
$\mathit{VP}$-$\mu$-$\mathit{TL}$ from [10]. In these logics, fixpoint
operators can be used to express arbitrary $\omega$-regular (resp.
$\omega$-visibly pushdown) properties on paths, which makes them more
expressive than LTL and CaRet, respectively. From these logics, we take
fixpoint operators. There is also a plethora of work on dynamic pushdown
networks. The model was first introduced in [9]. Different methods for
reachability analysis of DPNs have been proposed [9, 20]. Additionally,
different variants of the model were investigated. [24] and [19] consider
variants of DPNs that communicate via locks. Another variant is the model of
Dynamic Networks of concurrent pushdown systems from [7] in which threads can
communicate via global variables. However, none of the above works on DPNs is
concerned with model checking. The only approach to model checking DPNs we are
aware of consists of checking different variants of DPNs against a variant of
LTL called single indexed LTL [26, 13]. Compared to NTL, this variant cannot
specify properties concerning the call and return behaviour of a thread or the
relationship between different threads. In Section 5, we show that single
indexed LTL can be embedded into NTL.

##  2 Preliminaries

Without further ado, we introduce tools and notation used throughout the
paper. This section can be skipped on first reading and be consulted for
reference later.

Trees. An $\mathbb{N}_{0}$-tree $T$ is a prefix-closed subset of
$\mathbb{N}_{0}^{*}$, i.e. for all nodes $t\in\mathbb{N}_{0}^{*}$ and
directions $d\in\mathbb{N}_{0}$, $t\cdot d\in T$ implies $t\in T$. Moreover,
we require that $t\cdot d\in T$ for some $d\in\mathbb{N}_{0}$ implies $t\cdot
d^{\prime}\in T$ for all $d^{\prime}\leq d$. We call an element $t\in T$ a
node of $T$ with special node $\varepsilon$, which we call the root. A node of
the form $t\cdot d$ is called a child of $t$ and $t$ is called the parent of
$t\cdot d$. Additionally, for sequences $w\in\mathbb{N}_{0}^{*}$, we call
$t\cdot w$ a descendant of $t$ and $t$ an ancestor of $t\cdot w$. Nodes $t\in
T$ that have no children are called leaves. A path in a tree $T$ is a finite
or infinite sequence $t_{0}t_{1}\dots$ of nodes such that $t_{0}=\varepsilon$
and for all $i\in\mathbb{N}_{0}$, $t_{i+1}$ is a child of $t_{i}$. An
$\mathbb{N}_{0}$-tree that is a subset of $\\{0,1\\}^{*}$ is also called a
binary tree. In this case, we call a node of the form $t\cdot 0$ the left
child of $t$ and a node of the form $t\cdot 1$ the right child of $t$. Let
$\Sigma$ be a finite set of labels and $\mathit{ar}\colon\Sigma\to\\{0,1,2\\}$
be a function assigning an arity to each of these labels. A
$(\Sigma,\mathit{ar})$-labelled binary tree is a pair $(T,l)$ such that $T$ is
a binary tree and $l\colon T\to\Sigma$ is a labelling function such that each
node $t\in T$ has exactly $\mathit{ar}(l(t))$ children.

2-way alternating tree automata. For a finite set $X$, let
$\mathcal{B}^{+}(X)$ be the set of positive boolean combinations over $X$,
i.e. boolean formulae built with elements of $X$, conjunction and disjunction.
For $Y\subseteq X$ and $\vartheta\in\mathcal{B}^{+}(X)$, we say that $Y$
satisfies $\vartheta$ iff assigning the value $\mathit{true}$ to the elements
of $Y$ and $\mathit{false}$ to the elements of $X\setminus Y$ makes the
formula $\vartheta$ true. Let $\mathsf{Dir}=\\{0,1,\varepsilon,\uparrow\\}$ be
the set of moves in the tree with directions $0$ for the left child, $1$ for
the right child, $\varepsilon$ for standing still and $\uparrow$ for moving
upwards. We define $u\cdot\varepsilon=u$ and $u\cdot d\ \cdot\uparrow\ =u$ for
all $u\in\\{0,1\\}^{*}$ and $d\in\\{0,1\\}$. A 2-way alternating tree
automaton (2ATA) [29] over $(\Sigma,\mathit{ar})$-labelled binary trees is a
tuple $\mathcal{A}=(Q,q_{0},\rho,\Omega)$ where $Q$ is a finite set of states,
$q_{0}\in Q$ is an initial state, $\rho\colon
Q\times\Sigma\to\mathcal{B}^{+}(\mathsf{Dir}\times Q)$ is a transition
function and $\Omega\colon Q\to\\{0,\dots,k\\}$ is a priority mapping. The
size $|\mathcal{A}|$ of a 2-way alternating tree automaton is defined as the
sum of the sizes of its constituents. We sometimes also refer to the size of
individual constituents of an automaton. In particular, we refer to the number
of states, i.e. $|Q|$, and the size of the acceptance condition, i.e. $k$. If
the transition function of a 2-way alternating tree automaton uses only
symbols from $\\{0,1\\}$ instead of $\mathsf{Dir}$ and additionally maps all
nodes $t$ either to $\mathit{true}$ or to disjunctions over conjunctions that
consist of exactly one pair $(d,q)$ for each $d<\mathit{ar}(l(t))$, it is
called a nondeterministic parity tree automaton (NPTA).

For a $(\Sigma,\mathit{ar})$-labelled binary tree $\mathcal{T}=(T,l)$, a node
$t\in T$ and a state $q\in Q$, a $(t,q)$-run of $\mathcal{A}$ over
$\mathcal{T}$ is a pair $(T_{r},r)$ such that $T_{r}$ is an
$\mathbb{N}_{0}$-tree and $r\colon T_{r}\to T\times Q$ assigns a pair of a
node of $T$ and a state of $\mathcal{A}$ to all nodes in $T_{r}$.
Additionally, $(T_{r},r)$ has to satisfy the following conditions: (i)
$r(\varepsilon)=(t,q)$ and (ii) for all nodes $y\in T_{r}$ with $r(y)=(x,s)$
and $\rho(s,l(x))=\vartheta$, there is a set $Y\subseteq\mathsf{Dir}\times Q$
satisfying $\vartheta$ and for all $(d,s^{\prime})\in Y$, there is
$n\in\mathbb{N}_{0}$ such that $y\cdot n\in T_{r}$ and $r(y\cdot n)=(x\cdot
d,s^{\prime})$. In particular, for all leaves $y\in T_{r}$ with $r(y)=(x,s)$,
we thus require $\rho(s,l(x))=\mathit{true}$. A $(t,q)$-run $(T_{r},r)$ is
accepting iff on each infinite path in $T_{r}$ the lowest priority occurring
infinitely often is even. If $\mathcal{A}$ is a nondeterministic parity tree
automaton, a minimal set $Y$ satisfying $\rho(s,l(x))$ in the above definition
moves to each child of the current node $x$ in the tree $T$. For an
$(\varepsilon,q)$-run, we can thus simply identify $T$ with $T_{r}$ and
consider a map $r_{A}\colon T\to Q$ as an $(\varepsilon,q)$-run over
$\mathcal{A}$. The set of nodes $t\in T$ such that there is an accepting
$(t,q)$-run of $\mathcal{A}$ over $\mathcal{T}$ is denoted by
$\mathcal{L}_{q}^{\mathcal{T}}(\mathcal{A})$. We say that $\mathcal{A}$
accepts a tree $\mathcal{T}$ iff there is an accepting
$(\varepsilon,q_{0})$-run of $\mathcal{A}$ over $\mathcal{T}$. The set of
trees accepted by $\mathcal{A}$ is denoted by $\mathcal{L}(\mathcal{A})$. We
use the following theorems:

######  Proposition 1 ([29])

For every 2ATA $\mathcal{A}$, there is an equivalent NPTA
$\mathcal{A}^{\prime}$. The number of states in $\mathcal{A}^{\prime}$ is at
most exponential in the number of states of $\mathcal{A}$ and the size of the
acceptance condition of $\mathcal{A}^{\prime}$ is linear in the size of the
acceptance condition of $\mathcal{A}$.

######  Proposition 2 ([14, 18, 25])

The emptiness problem for NPTA can be solved in time polynomial in the number
of states and exponential in the size of the acceptance condition.

###### Proposition 3

  1. (i)

For any two NPTA $\mathcal{A}_{1}$ and $\mathcal{A}_{2}$, there is a NPTA
$\mathcal{A}$ with
$\mathcal{L}(\mathcal{A})=\mathcal{L}(\mathcal{A}_{1})\cap\mathcal{L}(\mathcal{A}_{2})$.

  2. (ii)

If either acceptance condition is trivial, the size of $\mathcal{A}$ is in
$\mathcal{O}(|\mathcal{A}_{1}|\cdot|\mathcal{A}_{2}|)$.

Proposition 3 (i) can be found e.g. in [23]. For (ii), a straightforward
product construction can be used and yields an automaton of the size claimed.

Dynamic Pushdown Networks. Let $\mathit{AP}$ be a set of atomic propositions,
$\Gamma$ be a finite set of stack symbols and $\bot\notin\Gamma$ be a special
bottom of stack symbol. A Dynamic Pushdown Network (DPN) [9] is a tuple
$\mathcal{M}=(S,s_{0},\gamma_{0},\Delta,L)$ where $S$ is a finite set of
control locations, $s_{0}\in S$ is an initial control location,
$\gamma_{0}\in\Gamma$ is an initial stack symbol and $L\colon S\times\Gamma\to
2^{\mathit{AP}}$ is a labelling function. The transition relation
$\Delta=\Delta_{I}\overset{.}{\cup}\Delta_{C}\overset{.}{\cup}\Delta_{R}\overset{.}{\cup}\Delta_{S}$
is a finite set of internal rules ($\Delta_{I}$), calling rules
($\Delta_{C}$), returning rules ($\Delta_{R}$) and spawning rules
($\Delta_{S}$). Internal rules $s\gamma\rightarrow
s^{\prime}\gamma^{\prime}\in\Delta_{I}\subseteq S\Gamma\times S\Gamma$, call
rules $s\gamma\rightarrow
s^{\prime}\gamma^{\prime}\gamma^{\prime\prime}\in\Delta_{C}\subseteq
S\Gamma\times S\Gamma^{2}$ or returning rules $s\gamma\rightarrow
s^{\prime}\in\Delta_{R}\subseteq S\Gamma\times S$ enable transitions of a
single pushdown process in control location $s$ with top of stack $\gamma$ to
the new control location $s^{\prime}$ with new top of stack $\gamma^{\prime}$,
$\gamma^{\prime}\gamma^{\prime\prime}$ and $\varepsilon$, respectively. A
spawning rule $s\gamma\rightarrow s^{\prime}\gamma^{\prime}\triangleright
s_{n}\gamma_{n}\in\Delta_{S}\subseteq S\Gamma\times S\Gamma\times S\Gamma$ is
an internal rule with the additional side effect of spawning a new process in
control location $s_{n}$ and stack content $\gamma_{n}$. We formally develop a
semantics for DPNs in Section 3.

##  3 Graph Semantics of Dynamic Pushdown Networks

The semantics of DPNs is often defined as an interleaving semantics. In such
semantics, a configuration of a DPN is a collection of local configurations of
the underlying pushdown systems representing the currently active threads. A
step in this semantics consists of a step of one of the active threads,
possibly adding a configuration of a new thread to the collection. This way,
the semantics accurately reflects different interleavings of the steps of the
threads issued by arbitrary schedulers, hence the name. For our intents,
interleaving semantics has some drawbacks, however. First, an encoding of the
intersection problem for contextfree languages is often possible in
interleaving semantics, which leads to undecidability of the investigated
verification problem. Second, we are mostly interested in temporal properties
of individual threads, not necessarily temporal properties of interleavings.
This is because the behaviour of a thread is in most cases independent of what
types of steps other threads currently make in a specific interleaving. Third,
we want to reason about the parent-child relationship of threads which is lost
in most formalisations of interleaving semantics.

We thus instead adopt a semantics based on graphs. Intuitively, in an
execution graph, each thread is modelled by a linear sequence of positions
connected by $\mathit{int}$-, $\mathit{call}$\- and $\mathit{ret}$-edges based
on the types of transitions taken in the thread. In order to model the parent-
child relationship between threads, a position where a spawn-transition is
taken is connected to the first position of the spawned thread via a
$\mathit{spawn}$-edge. This is analogous to the notion of action trees from
[20, 15]. Additionally, similar to nested words [5], calls and their matching
returns are connected via nesting edges. We formalise these graphs in the next
paragraph.

Execution graphs. Let
$\mathsf{Moves}=\\{\mathit{int},\mathit{call},\mathit{ret},\mathit{spawn}\\}$
be the set of moves for dynamic pushdown networks, $V$ be a set of nodes,
$l\colon V\to 2^{\mathit{AP}}$ be a labelling function, $\rightarrow^{d}\
\subseteq V^{2}$ be a transition relation for all $d\in\mathsf{Moves}$ and
$\curvearrowright\ \subseteq V^{2}$ be a nesting relation. For $x,y\in V$, we
call $y$ a ($d$)-successor of $x$ and $x$ a ($d$)-predecessor of $y$ if
$x\rightarrow^{d}y$ for some $d\in\mathsf{Moves}$. A tuple
$G=(V,l,(\rightarrow^{d})_{d\in\mathsf{Moves}},\curvearrowright)$ is called an
_execution graph_ , iff the following conditions hold:

  1. 1.

Every node has exactly one predecessor with respect to
$\bigcup\\{\rightarrow^{d}\mid d\in\mathsf{Moves}\\}$ except for a special
node $v_{0}$ without predecessor.

  2. 2.

For all $x\in V$ we have $(v_{0},x)\in(\bigcup\\{\rightarrow^{d}\mid
d\in\mathsf{Moves}\\})^{*}$.

  3. 3.

Every node either has (a) exactly one $\mathit{int}$-successor and at most one
$\mathit{spawn}$-successor, (b) exactly one $\mathit{call}$-successor, (c)
exactly one $\mathit{ret}$-successor or (d) no successors.

  4. 4.

On every finite path starting in $v_{0}$ or a node with a
$\mathit{spawn}$-predecessor and following only
$\mathsf{Moves}\setminus\\{\mathit{spawn}\\}$-successors, the number of
$\mathit{call}$-moves on that path is greater than or equal to the number of
$\mathit{ret}$-moves on that path.

  5. 5.

For all $x\in V$ having a $\mathit{call}$-successor, let $A_{x}$ be the set of
nodes $y\neq x$ such that there is a path $\pi$ from $x$ to $y$ following only
$\mathsf{Moves}\setminus\\{\mathit{spawn}\\}$-successors where the number of
$\mathit{call}$-moves on $\pi$ is equal to the number of $\mathit{ret}$-moves
on $\pi$. Then we have $x\curvearrowright y$ for a node $y\in V$ iff $y$ is a
node in $A_{x}$ such that the witnessing path has minimal length.

The set of execution graphs is denoted by $\mathsf{ExGraphs}$.

An example of an execution graph can be found in Fig. 1. In this example, a
main thread spawns two additional threads. Additionally, there are two nested
procedure calls in the main thread and one procedure call in a spawned thread.

$v_{0}$………$\mathit{int}$$\mathit{int}$$\mathit{call}$$\mathit{call}$$\mathit{ret}$$\mathit{int}$$\mathit{int}$$\mathit{ret}$$\mathit{int}$$\mathit{spawn}$$\mathit{int}$$\mathit{call}$$\mathit{ret}$$\mathit{int}$$\mathit{spawn}$$\mathit{int}$$\mathit{int}$$\mathit{int}$$\mathit{int}$

Figure 1: Example of an execution graph. Labelled edges represent edges
$\rightarrow^{d}$ for $d\in\mathsf{Moves}$ and dashed edges represent nesting
edges $\curvearrowright$.

Graph semantics. In most cases, we care only about graphs generated by a given
DPN instead of arbitrary execution graphs. This is formalised in the graph
semantics of DPN. In the definition of this semantics, we make use of
configurations of the processes of a given DPN
$\mathcal{M}=(S,s_{0},\gamma_{0},\Delta,L)$. Formally, a configuration of a
pushdown process of $\mathcal{M}$ is a pair $c=(s,u)$ where $s\in S$ is a
control location and $u\in\Gamma^{*}\bot$ is a stack content ending in $\bot$.
We define successor relations on configurations corresponding to the different
types of transition rules of DPNs. For this purpose, let $c=(s,u)$,
$c^{\prime}=(s^{\prime},u^{\prime})$ and
$c^{\prime\prime}=(s^{\prime\prime},u^{\prime\prime})$ be configurations. We
call $c^{\prime}$ an internal successor of $c$, denoted by
$c\rightarrow_{\mathit{int}}c^{\prime}$, if there is a transition
$s\gamma\rightarrow s^{\prime}\gamma^{\prime}\in\Delta_{I}$ and $u=\gamma w$,
$u^{\prime}=\gamma^{\prime}w$ for some stack content $w\in\Gamma^{*}\bot$. We
call $c^{\prime}$ a call successor of $c$, denoted by
$c\rightarrow_{\mathit{call}}c^{\prime}$, if there is a transition
$s\gamma\rightarrow
s^{\prime}\gamma^{\prime}\gamma^{\prime\prime}\in\Delta_{C}$ and $u=\gamma w$,
$u^{\prime}=\gamma^{\prime}\gamma^{\prime\prime}w$ for some stack content
$w\in\Gamma^{*}\bot$. We call $c^{\prime}$ a return successor of $c$, denoted
by $c\rightarrow_{\mathit{ret}}c^{\prime}$, if there is a transition
$s\gamma\rightarrow s^{\prime}\in\Delta_{R}$ and $u=\gamma w$, $u^{\prime}=w$
for some stack content $w\in\Gamma^{*}\bot$. Finally, we call $c^{\prime}$ a
successor of $c$ with spawned process $c^{\prime\prime}$, denoted
$c\rightarrow c^{\prime}\triangleright c^{\prime\prime}$, if there is a
transition $s\gamma\rightarrow s^{\prime}\gamma^{\prime}\triangleright
s^{\prime\prime}\gamma^{\prime\prime}\in\Delta_{S}$ and $u=\gamma w$,
$u^{\prime}=\gamma^{\prime}w$ for some stack content $w\in\Gamma^{*}\bot$ as
well as $u^{\prime\prime}=\gamma^{\prime\prime}\bot$. Using the notion of
configurations and the successor relations just introduced, we now define the
graph semantics. We say that an execution graph
$(V,l,(\rightarrow^{d})_{d\in\mathsf{Moves}},\curvearrowright)$ _is generated_
by $\mathcal{M}$ if there is an assignment $\mathit{as}\colon V\to
S\times\Gamma^{*}\bot$ satisfying (i)
$\mathit{as}(v_{0})=(s_{0},\gamma_{0}\bot)$ and (ii) for all $x\in V$, we have
$l(x)=L(s,\gamma)$ where $\mathit{as}(x)=(s,\gamma w)$ for some control
location $s\in S$, stack symbol $\gamma\in\Gamma$ and stack content
$w\in\Gamma^{*}\bot$ and

  * •

if $x$ has only one $d$-successor $y$ with
$d\in\\{\mathit{int},\mathit{call},\mathit{ret}\\}$, then
$\mathit{as}(x)\rightarrow_{d}\mathit{as}(y)$,

  * •

if $x$ has an $\mathit{int}$-successor $y$ and a $\mathit{spawn}$-successor
$z$, then
$\mathit{as}(x)\rightarrow\mathit{as}(y)\triangleright\mathit{as}(z)$ and

  * •

if $x$ has no successor, then $\mathit{as}(x)$ has no successor.

The set of execution graphs generated by $\mathcal{M}$ is denoted by
$\llbracket\mathcal{M}\rrbracket$.

Successor functions. On execution graphs
$G=(V,l,(\rightarrow^{d})_{d\in\mathsf{Moves}},\curvearrowright)$, we define
multiple successor functions $\mathit{succ}^{G}_{g}$,
$\mathit{succ}^{G}_{\uparrow}$, $\mathit{succ}^{G}_{a}$,
$\mathit{succ}^{G}_{-}$, $\mathit{succ}^{G}_{p}$ and $\mathit{succ}^{G}_{c}$
with signature $V\rightsquigarrow V$, i.e. partial functions from $V$ to $V$.
The first four of these successor functions come from logics like CaRet [4]
and allow us to progress single threads and their call-return behaviour in
different ways. The latter two functions are new and give means to reason
about the thread spawning behaviour of DPNs. For $x\in V$, the functions are
defined as follows:

  * •

The _global successor_ $\mathit{succ}^{G}_{g}(x)$ of $x$ is the
$\mathit{int}$-, $\mathit{call}$\- or $\mathit{ret}$-successor of $x$, if it
exists, and undefined otherwise.

  * •

The _global predecessor_ $\mathit{succ}^{G}_{\uparrow}(x)$ of $x$ is the
$\mathit{int}$-, $\mathit{call}$\- or $\mathit{ret}$-predecessor of $x$, if it
exists, and undefined otherwise.

  * •

The _abstract successor_ $\mathit{succ}^{G}_{a}(x)$ of $x$ is the node $y$
with $x\curvearrowright y$ or $x\rightarrow^{\mathit{int}}y$, if it exists,
and undefined otherwise.

  * •

The _caller_ $\mathit{succ}^{G}_{-}(x)$ of $x$ is the node $y$ with a
$\mathit{call}$-successor $y^{\prime}$ such that there is a path from
$y^{\prime}$ to $x$ following abstract successors, if it exists, and undefined
otherwise.

  * •

The _parent_ $\mathit{succ}^{G}_{p}(x)$ of $x$ is the node $y$ with a
$\mathit{spawn}$-successor $z$ such that there is a path from $z$ to $x$ with
only $\mathsf{Moves}\setminus\\{\mathit{spawn}\\}$-transitions, if it exists,
and undefined otherwise.

  * •

The _child_ $\mathit{succ}^{G}_{c}(x)$ of $x$ is the
$\mathit{spawn}$-successor of $x$, if it exists, and undefined otherwise.

We illustrate these successor functions for parts of the execution graph from
Fig. 1 in Fig. 2(a) and Fig. 2(b). Abstract successors (seen in dashdotted red
in Fig. 2(a)) follow the execution of a procedure on the same stack level and
skip over executions of additional procedures via nesting edges. If a
procedure is left in the next step, i.e. if the next step is a return, the
abstract successor is undefined. Callers (seen in dotted blue in Fig. 2(a))
are defined if the stack level is at least one in a configuration and move to
the latest previous call on a lower stack level. Parents (seen in dotted green
in Fig. 2(b)) are defined in every branch of an execution graph representing a
thread except for the thread starting in $v_{0}$ and move to the position in
the graph where the current thread was spawned. Children (seen in dashdotted
yellow in Fig. 2(b)) are defined only if the current thread currently executes
a spawn transition and move to the initial position of the spawned thread.

$v_{0}$………$\mathit{int}$$\mathit{int}$$\mathit{call}$$\mathit{call}$$\mathit{ret}$$\mathit{int}$$\mathit{int}$$\mathit{ret}$$\mathit{int}$$\mathit{spawn}$$\mathit{spawn}$

(a) Abstract successors (red, dashdotted) and callers (blue, dotted).
Irrelevant edges are gray and some internal edges coinciding with abstract
successors are omitted to improve readability.

$v_{0}$……$\mathit{int}$$\mathit{int}$$\mathit{spawn}$$\mathit{int}$$\mathit{call}$$\mathit{ret}$$\mathit{int}$

(b) Parents (green, dotted) and children (yellow, dashdotted). Irrelevant
edges are gray to improve readability.

Figure 2: Successor types in parts of the execution graph from Fig. 1.

##  4 A Navigation Logic for Dynamic Pushdown Networks

Syntax. We now define the new logic Navigation Temporal Logic (NTL) for
expressing properties of execution graphs. As mentioned in the introduction,
we have three main inspirations. From the logics CaRet [4] and
$\mathit{VP}$-$\mu$-$\mathit{TL}$ [10], we take different next operators
inspecting the call and return behaviour of a thread. We complement these by
additional next operators expressing parent and child relationships between
different processes. From the linear time $\mu$-calculus [28] and logics like
$\mathit{VP}$-$\mu$-$\mathit{TL}$ [10], we take fixpoint operators for
additional expressivity beyond LTL modalities. First, we define the syntax of
NTL.

######  Definition 1 (Syntax of NTL)

The syntax of NTL formulae is defined by

$\displaystyle\varphi::=$
$\displaystyle\quad\mathit{ap}\mid\lnot\varphi\mid\varphi_{1}\lor\varphi_{2}\mid
X\mid\bigcirc^{f}\varphi\mid\mu X.\varphi$

where $\mathit{ap}\in AP$ is an atomic proposition, $X$ is a fixpoint variable
and $f\in\\{g,\uparrow,a,-,p,c\\}$ is a successor type.

An NTL formula $\varphi$ is called _closed_ , if every fixpoint variable $X$
is bound in $\varphi$, i.e. it only appears in a subformula of the form $\mu
X.\psi$. A formula $\varphi$ is called _well-formed_ , if every fixpoint
variable $X$ occurring in $\varphi$ (i) is bound by only one fixpoint formula
which we then denote by $\mathit{fp}(X)$, (ii) appears only in the scope of an
even number of negations inside $\mathit{fp}(X)$ and (iii) is in scope of at
least one next operator inside $\mathit{fp}(X)$. We use
$\mathit{Sub}(\varphi)$ for the set of subformulae of a formula $\varphi$. The
size $|\varphi|$ of a formula $\varphi$ is defined as the number of its
distinct subformulae. We also need a notion of substitution:
$\varphi[\varphi^{\prime}/X]$ is the formula that is obtained from $\varphi$
by replacing every occurrence of the fixpoint variable $X$ with
$\varphi^{\prime}$.

Let us explain the intuition behind each construct. Atomic formulae
$\mathit{ap}$ express that $\mathit{ap}\in\mathit{AP}$ holds in the current
node of the graph. Next operators $\bigcirc^{f}\varphi$ can be used to
navigate and express that the corresponding successor exists in the current
node and additionally satisfies $\varphi$. Negation and disjunction are
interpreted as usual. Finally, we have fixpoint variables $X$ and least
fixpoint operators $\mu X.\varphi$ for more involved properties. Intuitively,
$\mu X.\varphi$ is the least fixpoint of a function that unrolls the formula
by replacing $\mu X.\varphi$ with $\varphi[\mu X.\varphi/X]$.

We use some common syntactic sugar such as
$\mathit{true}\equiv\mathit{ap}\lor\lnot\mathit{ap}$,
$\mathit{false}\equiv\lnot\mathit{true}$,
$\varphi_{1}\land\varphi_{2}\equiv\lnot(\lnot\varphi_{1}\lor\lnot\varphi_{2})$,
$\varphi_{1}\rightarrow\varphi_{2}\equiv\lnot\varphi_{1}\lor\varphi_{2}$,
$\varphi_{1}\leftrightarrow\varphi_{2}\equiv(\varphi_{1}\rightarrow\varphi_{2})\land(\varphi_{2}\rightarrow\varphi_{1})$
and $\nu X.\varphi\equiv\lnot\mu X.\lnot\varphi[\lnot X/X]$. We also introduce
a dual operator
$\bigcirc^{\overline{f}}\varphi\equiv\lnot\bigcirc^{f}\lnot\varphi$ of
$\bigcirc^{f}\varphi$ for each successor type $f\in\\{g,\uparrow,a,-,p,c\\}$
which is needed for a special form in the next paragraph. It is necessary to
explicitly define these dual operators since $\lnot\bigcirc^{f}\varphi$ is not
equivalent to $\bigcirc^{f}\lnot\varphi$ as the corresponding successors can
be undefined for certain nodes in an execution graph. Unlike
$\bigcirc^{f}\varphi$, $\bigcirc^{\overline{f}}\varphi$ is equivalent to
$\mathit{true}$ for nodes that do not have an $f$-successor. We also introduce
some variants of LTL modalities as derived operators. In particular we use
$\varphi_{1}\ \mathcal{U}^{f}\varphi_{2}\equiv\mu
X.(\varphi_{2}\lor(\varphi_{1}\land\bigcirc^{f}X))$,
$\mathcal{F}^{f}\varphi\equiv\mathit{true}\ \mathcal{U}^{f}\varphi$ and
$\mathcal{G}^{f}\varphi\equiv\lnot\mathcal{F}^{f}\lnot\varphi$ for
$f\in\\{g,\uparrow,a,-,p,c\\}$. For $f=g$, we sometimes omit the superscript
and write $\mathcal{F}\varphi$ etc. Intuitively, these modalities correspond
to the usual LTL modalities evaluated on the path starting in the current
position and taking $f$-successors. Additionally, we introduce modalities
$\mathcal{F}^{r}\varphi\equiv\mu
X.(\varphi\lor\bigcirc^{g}X\lor\bigcirc^{c}X)$ and
$\mathcal{G}^{r}\varphi\equiv\lnot\mathcal{F}^{r}\lnot\varphi$ to express that
$\varphi$ holds in some position or all positions, respectively, reachable
from the current position. Using these abbreviations, dual operators and the
equivalence $\lnot\lnot\varphi\equiv\varphi$ we can transform every well-
formed formula into an equivalent formula in which negation only appears in
front of atomic propositions. We call this form _positive normal form_ and
assume formulae to be given in this form in the algorithms presented in this
paper.

Semantics. We now formally define the semantics of NTL. It is defined with
respect to an execution graph
$G=(V,l,(\rightarrow^{d})_{d\in\mathsf{Moves}},\curvearrowright)$ and a
fixpoint variable assignment $\mathcal{V}$ assigning sets of nodes of $G$ to
fixpoint variables. Intuitively,
$\llbracket\varphi\rrbracket^{G}_{\mathcal{V}}$ is the set of nodes of $G$
satisfying $\varphi$ when each free fixpoint variable $X$ is interpreted to
hold at nodes $\mathcal{V}(X)$. In the following, for a fixpoint variable
assignment $\mathcal{V}$, a fixpoint variable $X$ and a set of nodes
$M\subseteq V$, we write $\mathcal{V}[X\mapsto M]$ for the fixpoint variable
assignment with $\mathcal{V}[X\mapsto M](X)=M$ and $\mathcal{V}[X\mapsto
M](Y)=\mathcal{V}(Y)$ for all variables $Y\neq X$.

######  Definition 2 (Semantics of NTL)

Let $G=(V,l,(\rightarrow^{d})_{d\in\mathsf{Moves}},\curvearrowright)$ be an
execution graph and $\mathcal{V}$ be a fixpoint variable assignment. The
semantics of an NTL formula with respect to $G$ and $\mathcal{V}$ is defined
by

$\displaystyle\llbracket\mathit{ap}\rrbracket_{\mathcal{V}}^{G}:=$
$\displaystyle\quad\\{x\in V\mid\mathit{ap}\in l(x)\\}$
$\displaystyle\llbracket\lnot\varphi\rrbracket_{\mathcal{V}}^{G}:=$
$\displaystyle\quad V\setminus\llbracket\varphi\rrbracket_{\mathcal{V}}^{G}$
$\displaystyle\llbracket\varphi_{1}\lor\varphi_{2}\rrbracket_{\mathcal{V}}^{G}:=$
$\displaystyle\quad\llbracket\varphi_{1}\rrbracket_{\mathcal{V}}^{G}\cup\llbracket\varphi_{2}\rrbracket_{\mathcal{V}}^{G}$
$\displaystyle\llbracket X\rrbracket_{\mathcal{V}}^{G}:=$
$\displaystyle\quad\mathcal{V}(X)$
$\displaystyle\llbracket\bigcirc^{f}\varphi\rrbracket_{\mathcal{V}}^{G}:=$
$\displaystyle\quad\\{x\in V\mid\mathit{succ}^{G}_{f}(x)\text{ is defined and
}\mathit{succ}^{G}_{f}(x)\in\llbracket\varphi\rrbracket_{\mathcal{V}}^{G}\\}$
$\displaystyle\llbracket\mu X.\varphi\rrbracket_{\mathcal{V}}^{G}:=$
$\displaystyle\quad\bigcap\\{M\subseteq
V\mid\llbracket\varphi\rrbracket_{\mathcal{V}[X\mapsto M]}^{G}\subseteq M\\}$

where $\mathit{ap}\in\mathit{AP}$ is an atomic proposition, $X$ is a fixpoint
variable and $f\in\\{g,\uparrow,a,-,p,c\\}$ is a successor type.

In this semantics definition, two remarks are in order. First, it is easy to
see using Knaster-Tarski’s fixpoint theorem [27] that for formulae $\varphi$
in positive normal form, $\llbracket\mu X.\varphi\rrbracket_{\mathcal{V}}^{G}$
characterises the least fixpoint of the monotone function $\alpha_{S}\colon
2^{V}\to 2^{V}$ with
$\alpha_{S}(M)=\llbracket\varphi\rrbracket^{G}_{\mathcal{V}[X\mapsto M]}$ for
$S=(G,\mathcal{V},X,\varphi)$. Second, for closed NTL formulae $\varphi$, the
semantics does not depend on the fixpoint variable assignment. For such
formulae, we introduce additional semantic notations. We write
$\llbracket\varphi\rrbracket^{G}$ for
$\llbracket\varphi\rrbracket_{\mathcal{V}}^{G}$ where $\mathcal{V}$ is an
arbitrary fixpoint variable assignment and set
$\llbracket\varphi\rrbracket:=\\{G\in\mathsf{ExGraphs}\mid
v_{0}\in\llbracket\varphi\rrbracket^{G}\\}$. For an execution graph $G$, we
write $G\models\varphi$ for $G\in\llbracket\varphi\rrbracket$. Finally, for a
DPN $\mathcal{M}$, we write $\mathcal{M}\models\varphi$, iff $G\models\varphi$
for all $G\in\llbracket\mathcal{M}\rrbracket$.

In this paper, we consider the following decision problems for NTL:

  * •

_Model Checking:_ Given a DPN $\mathcal{M}$ and a closed well-formed NTL
formula $\varphi$, does $\mathcal{M}\models\varphi$ hold?

  * •

_DPN Satisfiability:_ Given a closed well-formed NTL formula $\varphi$, is
there a DPN $\mathcal{M}$ such that $\mathcal{M}\models\varphi$?

  * •

_Graph Satisfiability:_ Given a closed well-formed NTL formula $\varphi$, is
there an execution graph $G$ such that $G\models\varphi$?

##  5 Example properties

We motivate the introduction of our new logic with some examples.

Locking policies. In programming languages like Java, mutual exclusion between
different threads on certain procedures or code blocks is realised via
synchronized procedures or blocks. Internally, this feature works by acquiring
a lock upon entering a synchronized procedure or block that is released when
leaving the synchronized part of the code [1]. Locks are thus acquired and
released in a nested manner. In DPNs, this synchronization mechanism can be
modelled by including symbols for locks in the stack alphabet that are pushed
onto the stack when acquiring a lock and removed from the stack when releasing
it. A call or return of a synchronized procedure is then modelled by taking
two $\mathit{call}$\- or $\mathit{ret}$-transitions of the DPN, respectively,
one for pushing or popping the lock symbol and another one as usual. We also
include the lock symbols as atomic propositions that are assigned to
corresponding configuration heads. In this setup, the formula
$\varphi_{l}:=\mathcal{F}^{-}l$ expresses that the lock $l$ is currently held
using the caller modality $\mathcal{F}^{-}$. This form of modelling also works
for reentrant locks, i.e. locks that can be acquired multiple times. When
threads acquire multiple locks, problems with deadlocks can occur when
different threads acquire locks in a different order. Assume, for example,
that we have two locks where thread one acquires lock one first and then lock
two and thread two acquires lock two first and then lock one. In this case, a
deadlock can occur when the threads are scheduled such that thread one
acquires lock one and thread two acquires lock two. A common policy to avoid
deadlocks is to ensure that all threads acquire locks in the same order. The
formula $\varphi_{ij}:=\mathcal{F}^{-}(l_{i}\land\mathcal{G}^{-}\lnot l_{j})$
expresses that lock $l_{i}$ is currently held and when it was acquired, lock
$l_{j}$ was not held. It can be used in the formula
$\mathcal{G}^{r}(\varphi_{l_{i}}\land\varphi_{l_{j}})\rightarrow\varphi_{ij}$
to express that $l_{i}$ is always acquired before $l_{j}$, if both locks are
held. The disjunction
$\mathcal{G}^{r}(\varphi_{l_{i}}\land\varphi_{l_{j}})\rightarrow\varphi_{ij}\lor\mathcal{G}^{r}(\varphi_{l_{i}}\land\varphi_{l_{j}})\rightarrow\varphi_{ji}$
then expresses the existence of a global order for locks $l_{i}$ and $l_{j}$
and the existence of a global order for all locks can be expressed by a
boolean combination of a quadratic number of variants of this formula. Another
problem with locking arises when certain threads wait for a lock that is held
by another thread for an infinite amount of time, e.g. if a synchronized
method is never left. A policy addressing this problem is to ensure that all
locks that are acquired are released at some point in the future. We can
express this using the formula
$\mathcal{G}^{r}\bigwedge_{l\in\mathit{Locks}}\varphi_{l}\rightarrow\mathcal{F}\lnot\varphi_{l}$.
Under these two policies, a necessary and sufficient condition for mutual
exclusion of two program points labelled $s_{1}$ and $s_{2}$ is that a common
lock is held at the two program points. This can also be expressed in a
formula from our logic:
$\bigvee_{l\in\mathit{Locks}}\mathcal{G}^{r}((s_{1}\rightarrow\varphi_{l})\land(s_{2}\rightarrow\varphi_{l}))$.

Behaviour of main and worker threads. We elaborate on a motivating example for
single indexed LTL from [26] expressible in NTL. In this example, a main
thread of a server processes requests from clients by starting a worker thread
responding to the specific request. Then, the main thread should repeatedly
accept new requests, expressed by the formula
$\mathcal{G}^{r}(\mathit{main}\rightarrow\mathcal{G}\mathcal{F}\mathit{accept})$.
Also, each worker thread should respond with a correct acknowledgement to each
type of request, i.e. it should respond exactly with $\mathit{ack}$ to
$\mathit{req}$ and exactly with $\mathit{ack^{\prime}}$ to
$\mathit{req^{\prime}}$. This is expressed by the formula
$\mathcal{G}^{r}(\mathit{worker}\rightarrow(\mathit{req}\rightarrow(\mathcal{F}\mathit{ack}\land\mathcal{G}\lnot\mathit{ack^{\prime}})\land\mathit{req^{\prime}}\rightarrow(\mathcal{F}\mathit{ack^{\prime}}\land\mathcal{G}\lnot\mathit{ack})))$.
Such requirements were already expressible in single indexed LTL. However,
using the different types of successor operators in NTL, we can further expand
on this scenario and express properties not expressible in single indexed LTL.
For example, it is a reasonable requirement that worker threads are only
spawned by the main thread and only if the main thread has accepted a request.
This requirement can be expressed in the formula
$\mathcal{G}^{r}(\mathit{worker}\rightarrow\bigcirc^{p}(\mathit{main}\land\mathit{accept}))$.
Another desirable property in this scenario is a variant of the property from
the introduction. In particular, we may want worker threads to only be spawned
from a procedure $\mathit{pr}$ which performs bookkeeping about the currently
active worker threads. This is expressed by the formula
$\mathcal{G}^{r}(\bigcirc^{c}\mathit{worker}\rightarrow\mathcal{F}^{-}\mathit{pr})$.

Single indexed LTL model checking. It is no surprise that the previous
motivating example for single indexed LTL is expressible in NTL. Indeed, we
show that the full approach of single indexed LTL DPN model checking from [26]
can also be handled using our logic. We first sketch their setup. In [26], a
DPN $\mathcal{M}=\\{\mathcal{P}_{1},\dots,\mathcal{P}_{n}\\}$ is defined as a
set of pushdown systems $\mathcal{P}_{i}$ with the ability to spawn threads
executing one of the pushdown systems of $\mathcal{M}$. A single indexed LTL
formula is a conjunction $\varphi=\bigwedge_{i=1}^{n}\varphi_{i}$ of LTL
formulae $\varphi_{i}$ that are each assigned to a specific pushdown system
$\mathcal{P}_{i}$. Then, $\mathcal{M}\models\varphi$ holds iff $\mathcal{M}$
has a global run such that for all $i$, every local run of $\mathcal{P}_{i}$
in the global run satisfies $\varphi_{i}$. In our setup, their global runs
correspond to execution graphs and their local runs correspond to the paths in
the execution graph starting in positions where new threads are spawned and
following the global successors. Since in single indexed LTL model checking,
the existence of a global run is checked, whereas in NTL model checking, it is
checked that all execution graphs satisfy a property, we can check that
$\mathcal{M}\not\models\varphi$ for a single indexed LTL formula
$\varphi=\bigwedge_{i=1}^{n}\varphi_{i}$ using NTL model checking. This is
done as follows. We model the partition of a DPN $\mathcal{M}$ from their
setup into its pushdown systems $\mathcal{P}_{i}$ by labelling every control
location of $\mathcal{P}_{i}$ with a fresh atomic proposition $p_{i}$ in its
translation $\bar{\mathcal{M}}$ in our setup. LTL formulae $\varphi_{i}$ can
trivially be translated to NTL by encoding until operators using least
fixpoints. Then, the NTL formula
$\bar{\varphi}=(p_{1}\land\lnot\varphi_{1})\lor\mathcal{F}^{r}(\bigvee_{i=1}^{n}\bigcirc^{c}(p_{i}\land\lnot\varphi_{i}))$
expresses that there is a local run of $\mathcal{P}_{i}$ for some $i$ that
does not satisfy $\varphi_{i}$. In this formula, the disjunct
$(p_{1}\land\lnot\varphi_{1})$ identifies a violation by the root process
$\mathcal{P}_{1}$ and the disjunct
$\mathcal{F}^{r}(\bigvee_{i=1}^{n}\bigcirc^{c}(p_{i}\land\lnot\varphi_{i}))$
identifies violations by spawned processes. Accordingly,
$\mathcal{M}\models\varphi$ (in the single indexed LTL setup) iff
$\bar{\mathcal{M}}\not\models\bar{\varphi}$ (in our setup).

##  6 From Graph Semantics to Tree Semantics

In order to enable algorithmic verification with tree automata, we introduce
an additional structure called execution tree. In a nutshell, these trees are
obtained from execution graphs by keeping the same set of nodes and adjusting
the edge relation a little. In particular, we discard $\mathit{ret}$-edges. In
order to properly interpret left and right children in this adjusted
structure, we add labels $(l,d,p)$ where $l$ represents the label of the
current node, $d$ represents the transition types from this node to its
children and $p$ represents the transition type from the parent to this node.
This yields us a structure simpler than execution graphs that still contains
the same information and can be analysed using tree automata.

Execution trees. Let
$G=(V,l,(\rightarrow^{d})_{d\in\mathsf{Moves}},\curvearrowright)$ be an
execution graph. We inductively define a map $\delta_{G}\colon
V\to\\{0,1\\}^{*}$ assigning a tree node to each graph node $x\in V$ as
follows.

  * •

If $x=v_{0}$, we set $\delta_{G}(x):=\varepsilon$.

  * •

If $x$ has a $\mathit{call}$\- or $\mathit{int}$-predecessor $y$, we set
$\delta_{G}(x):=\delta_{G}(y)\cdot 0$. In this case, we also call
$\delta_{G}(x)$ a $\mathit{call}$\- or $\mathit{int}$-child of
$\delta_{G}(y)$, respectively.

  * •

If there is $y\in V$ such that $y$ is a $\mathit{spawn}$-predecessor of $x$ or
$y\curvearrowright x$, we set $\delta_{G}(x):=\delta_{G}(y)\cdot 1$. If $y$ is
a $\mathit{spawn}$-predecessor of $x$, we also call $\delta_{G}(x)$ a
$\mathit{spawn}$-child of $\delta_{G}(y)$ and if $y\curvearrowright x$, we
also call $\delta_{G}(x)$ a $\mathit{ret}$-child of $\delta_{G}(y)$.

Additionally, for a subset $M\subseteq\mathsf{Moves}$ and nodes $x,y\in V$, we
call $\delta_{G}(y)$ an $M$-descendant of $\delta_{G}(x)$ and $\delta_{G}(x)$
an $M$-ancestor of $\delta_{G}(y)$, if there is a path from $\delta_{G}(x)$ to
$\delta_{G}(y)$ in the tree following only $M$-children.

Let
$\mathit{TL}=2^{\mathit{AP}}\times\\{\mathit{int},\mathit{call},\mathit{callRet},\mathit{spawn},\mathit{ret},\mathit{end}\\}\times(\mathsf{Moves}\cup\\{\bot\\})$
be the set of labels for tree nodes and the arity function
$\mathit{ar}\colon\mathit{TL}\to\\{0,1,2\\}$ be defined by
$\mathit{ar}(l,\mathit{ret},p)=\mathit{ar}(l,\mathit{end},p)=0$,
$\mathit{ar}(l,\mathit{int},p)=\mathit{ar}(l,\mathit{call},p)=1$ and
$\mathit{ar}(l,\mathit{callRet},p)=\mathit{ar}(l,\mathit{spawn},p)=2$. The
tree representation $\mathcal{T}(G)$ of $G$ is the
$(\mathit{TL},\mathit{ar})$-labelled binary tree $(\mathsf{im}(\delta_{G}),r)$
where $\mathsf{im}(\delta_{G})=\\{\delta_{G}(x)\mid x\in V\\}$ denotes the
image of $\delta_{G}$ and for all $x\in V$ we have
$r(\delta_{G}(x))=(l(x),d(x),p(x))$ where (i) either $p(x)\neq\bot$ and $x$
has a $p(x)$-predecessor or $p(x)=\bot$ and $x=v_{0}$ and (ii) one of the
following conditions hold:

  * •

$x$ has only one $d(x)$-successor and
$d(x)\in\\{\mathit{int},\mathit{ret}\\}$.

  * •

$x$ has only one $\mathit{int}$\- and one $\mathit{spawn}$-successor and
$d(x)=\mathit{spawn}$.

  * •

$x$ has only one $\mathit{call}$-successor, there is no $y\in V$ with
$x\curvearrowright y$, and $d(x)=\mathit{call}$.

  * •

$x$ has only one $\mathit{call}$-successor, there is $y\in V$ with
$x\curvearrowright y$, and $d(x)=\mathit{callRet}$.

  * •

$x$ has no successors and $d(x)=\mathit{end}$.

A tree representation of an execution graph is also called an execution tree.
An example of an execution tree can be found in Fig. 3.

$\varepsilon$$(l,\mathit{spawn},\mathit{int})$$(l,\mathit{callRet},\mathit{int})$$(l,\mathit{ret},\mathit{call})$………$0$$0$$0$$0$$0$$0$$0$$1$$1$$1$$0$$0$$0$$1$$1$$0$$0$$0$$0$

Figure 3: Execution tree for the execution graph in Fig. 1. An edge from node
$t$ to node $t^{\prime}$ labelled $d$ means that $t^{\prime}=t\cdot d$. Labels
are depicted for nodes $0$, $00$ and $0000$. Gray edges exist in the execution
graph but not in the execution tree.

Adapted successor functions. We adapt the successor functions previously
defined on execution graphs to execution trees in order to allow us to check
the satisfaction of formulae directly on execution trees. Specifically, we
define multiple successor functions $\mathit{succ}_{g}^{\mathcal{T}}$,
$\mathit{succ}_{\uparrow}^{\mathcal{T}}$, $\mathit{succ}_{a}^{\mathcal{T}}$,
$\mathit{succ}_{-}^{\mathcal{T}}$, $\mathit{succ}_{p}^{\mathcal{T}}$ and
$\mathit{succ}_{c}^{\mathcal{T}}$ with signature $T\rightsquigarrow T$ for
execution trees $\mathcal{T}=(T,r)$. For $t\in T$ with $r(t)=(l,d,p)$, the
successor functions are given as follows:

  * •

The _abstract successor_ $\mathit{succ}_{a}^{\mathcal{T}}(t)$ of $t$ is
defined as the left child of $t$, if $d\in\\{\mathit{int},\mathit{spawn}\\}$,
the right child of $t$, if $d=\mathit{callRet}$, and undefined else.

  * •

The _caller predecessor_ $\mathit{succ}_{-}^{\mathcal{T}}(t)$ of $t$ is
defined as the parent node of $t$, if $p=\mathit{call}$, the caller
predecessor of its parent node, if $p\in\\{\mathit{int},\mathit{ret}\\}$ and
this is defined, and undefined else.

  * •

The _global successor_ $\mathit{succ}_{g}^{\mathcal{T}}(t)$ of $t$ is defined
as the left child of $t$, if
$d\in\\{\mathit{int},\mathit{call},\mathit{callRet},\mathit{spawn}\\}$,
$\mathit{succ}_{a}^{\mathcal{T}}(\mathit{succ}_{-}^{\mathcal{T}}(t))$, if
$d=\mathit{ret}$, and undefined else.

  * •

The _global predecessor_ $\mathit{succ}_{\uparrow}^{\mathcal{T}}(t)$ of $t$ is
defined as the parent node of $t$, if $p\in\\{\mathit{int},\mathit{call}\\}$,
the $\\{\mathit{int},\mathit{ret}\\}$-descendant leaf of the left child of its
parent node, if $p=\mathit{ret}$, and undefined else.

  * •

The _parent predecessor_ $\mathit{succ}_{p}^{\mathcal{T}}(t)$ of $t$ is
defined as the parent node of $t$, if $p\\!=\\!\mathit{spawn}$, the parent
predecessor of its parent node, if
$p\in\\{\mathit{int},\mathit{call},\mathit{ret}\\}$ and this is defined, and
undefined else.

  * •

The _child successor_ $\mathit{succ}_{c}^{\mathcal{T}}(t)$ of $t$ is defined
as the right child of $t$, if $d=\mathit{spawn}$, and undefined else.

We show in the following lemma that these adapted successor functions behave
exactly like their counterparts on execution graphs.

###### Lemma 1

Let $G=(V,l,(\rightarrow^{d})_{d\in\mathsf{Moves}},\curvearrowright)$ be an
execution graph with $\mathcal{T}(G)=\mathcal{T}$. For all
$f\in\\{g,\uparrow,a,-,p,c\\}$ we have
$\delta_{G}\circ\mathit{succ}^{G}_{f}=\mathit{succ}_{f}^{\mathcal{T}}\circ\delta_{G}$,
i.e. for all nodes $x\in V$, $\delta_{G}(\mathit{succ}^{G}_{f}(x))$ is defined
iff $\mathit{succ}_{f}^{\mathcal{T}}(\delta_{G}(x))$ is defined and in this
case
$\delta_{G}(\mathit{succ}^{G}_{f}(x))=\mathit{succ}_{f}^{\mathcal{T}}(\delta_{G}(x))$.

A detailed proof of this lemma can be found in Appendix 0.D.

##  7 Model Checking and Satisfiability

We now use execution trees to decide the model checking and satisfiability
problems for NTL. For this, we construct three tree automata: one automaton
for checking whether a tree is an execution tree, a second automaton for
checking whether an execution graph (given by its tree representation)
satisfies a given formula, and another automaton for checking whether a tree
represents an execution graph generated by a given DPN.

An automaton for execution trees. We first construct a nondeterministic parity
tree automaton that checks whether a $(\mathit{TL},\mathit{ar})$-labelled
binary tree is an execution tree. At each node labelled by $(l,d,p)$, the
automaton needs to ensure that the node is a $p$-child, if $p\neq\bot$, and
that it is the root, if $p=\bot$. Moreover, if $d=\mathit{callRet}$, it has to
check that its $\mathit{call}$-child does have an
$\\{\mathit{int},\mathit{ret}\\}$-descendant leaf. Finally, it has to ensure
that for leaves $t$ labelled by $(l,d,p)$ we have $d=\mathit{ret}$ iff $t$ is
the $\\{\mathit{int},\mathit{ret}\\}$-descendant leaf of a
$\mathit{call}$-child of a node labelled by
$(l^{\prime},\mathit{callRet},p^{\prime})$ for some $l^{\prime}\in
2^{\mathit{AP}}$ and $p^{\prime}\in\mathsf{Moves}\cup\\{\bot\\}$. Thus, we can
define the automaton as $\mathcal{A}_{\mathsf{ET}}=(Q,q_{0},\rho,\Omega)$ with
state set $Q=(\mathsf{Moves}\cup\\{\bot\\})\times\\{0,1\\}$ and initial state
$q_{0}=(\bot,0)$. Intuitively, in a state $(p,c)$, $p$ denotes the parent edge
type and the bit $c$ indicates whether the current node is an
$\\{\mathit{int},\mathit{ret}\\}$-descendant of a $\mathit{call}$-child of a
node labelled by $(l^{\prime},\mathit{callRet},p^{\prime})$ for some
$l^{\prime}\in 2^{\mathit{AP}}$ and
$p^{\prime}\in\mathsf{Moves}\cup\\{\bot\\}$. The transition function $\rho$ is
defined by

$\displaystyle\rho((p,c),(l,d,p^{\prime})):=\begin{cases}(0,(\mathit{int},c))&\text{
if }d=\mathit{int}\\\ (0,(\mathit{call},0))&\text{ if }d=\mathit{call}\text{
and }c=0\\\ (0,(\mathit{call},1))\land(1,(\mathit{ret},c))&\text{ if
}d=\mathit{callRet}\\\ (0,(\mathit{int},c))\land(1,(\mathit{spawn},0))&\text{
if }d=\mathit{spawn}\\\ \mathit{true}&\text{ if
}(d,c)\in\\{(\mathit{ret},1),(\mathit{end},0)\\}\end{cases}$

for $p=p^{\prime}$ and $\rho((p,c),(l,d,p^{\prime})):=\mathit{false}$ in all
other cases. The priority assignment is given by $\Omega(p,c)=c$ for all
$(p,c)\in Q$.

We establish the following theorem. A proof can be found in Appendix 0.E.

###### Theorem 7.1

One can construct a NPTA $\mathcal{A}_{\mathsf{ET}}$ over
$(\mathit{TL},\mathit{ar})$-labelled binary trees with a constant size such
that $\mathcal{L}(\mathcal{A}_{\mathsf{ET}})=\\{\mathcal{T}(G)\mid G\text{ is
an execution graph}\\}$.

An automaton for formulae. For the next automaton, we define a 2-way
alternating tree automaton evaluating $\varphi$ on execution trees, intersect
it with the automaton recognising execution trees and then transform this
automaton into a nondeterministic parity tree automaton. In the following, let
$\varphi$ be a closed, well-formed NTL formula in positive normal form. We
define the automaton for $\varphi$ as
$\tilde{\mathcal{A}}_{\varphi}=(Q,q_{0},\rho,\Omega)$ where $Q$, $q_{0}$,
$\rho$ and $\Omega$ are described in more detail in the following paragraphs.

The states of the automaton are given by

$\displaystyle Q=$ $\displaystyle\ \mathit{Sub}(\varphi)\cup Q_{1}\cup
Q_{2}\text{ where }$ $\displaystyle Q_{1}=$ $\displaystyle\
\\{\bigcirc^{-}\bigcirc^{a}\psi,\bigcirc^{a}\psi\mid\bigcirc^{g}\psi\in\mathit{Sub}(\varphi)\text{
or }\bigcirc^{\overline{g}}\psi\in\mathit{Sub}(\varphi)\\}\text{ and }$
$\displaystyle Q_{2}=$ $\displaystyle\
\\{\mathit{call},\mathit{leaf}\\}\times\\{\psi\mid\bigcirc^{\uparrow}\psi\in\mathit{Sub}(\varphi)\text{
or }\bigcirc^{\overline{\uparrow}}\psi\in\mathit{Sub}(\varphi)\\}$

with initial state $q_{0}=\varphi$. Since we use another automaton to check
that the given tree indeed represents an execution graph, we care only about
execution trees as inputs in this construction. Intuitively, being in a state
$\psi\in\mathit{Sub}(\varphi)\cup Q_{1}$ at the position $\delta_{G}(x)$ in
the input execution tree $\mathcal{T}(G)$, the automaton checks whether the
node $x$ satisfies $\psi$, i.e. whether $x\in\llbracket\psi\rrbracket^{G}$.
The states in $Q_{2}$ are used to handle the global predecessor next modality
and its dual version. We use states of the form $(\mathit{call},\psi)$ to
denote that we should move to the $\mathit{call}$-child of the current node
and switch to state $(\mathit{leaf},\psi)$; states of the form
$(\mathit{leaf},\psi)$ denote that we should check $\psi$ for the
$\\{\mathit{int},\mathit{ret}\\}$-descendant leaf of the current node.

The transition function $\rho$ is defined as described next. Recall that
$\tilde{\mathcal{A}}_{\varphi}$ operates on execution trees which are labelled
by triples $(l,d,p)$ where $l\in 2^{\mathit{AP}}$ are the atomic propositions,
$d\in\\{\mathit{int},\mathit{call},\mathit{callRet},\mathit{spawn},\mathit{ret},\mathit{end}\\}$
specifies the successor types of the current node and
$p\in\mathsf{Moves}\cup\\{\bot\\}$ denotes the type of its predecessor. If the
current state is an atomic proposition or a negation of an atomic proposition,
we can check directly whether the tree node is labelled by this proposition
and thus determine whether the formula holds:

$\displaystyle\rho(\mathit{ap},(l,d,p)):=\begin{cases}\mathit{true}\text{ if
}\mathit{ap}\in l\\\ \mathit{false}\text{ if }\mathit{ap}\notin l\end{cases}$
$\displaystyle\rho(\lnot\mathit{ap},(l,d,p)):=\begin{cases}\mathit{false}\text{
if }\mathit{ap}\in l\\\ \mathit{true}\text{ if }\mathit{ap}\notin
l.\end{cases}$

For a disjunction or conjunction of two formulae, we can use the power of
alternation and set

$\displaystyle\rho(\psi_{1}\lor\psi_{2},\sigma):=(\varepsilon,\psi_{1})\lor(\varepsilon,\psi_{2})\text{
and
}\rho(\psi_{1}\land\psi_{2},\sigma):=(\varepsilon,\psi_{1})\land(\varepsilon,\psi_{2}).$

For a formula of the form $\bigcirc^{f}\psi$, we move to the corresponding
successor of the given node and then switch to state $\psi$. In most cases,
the according transitions can be defined straightforwardly using the
characterisation from the successor functions on execution trees:

$\displaystyle\rho(\bigcirc^{g}\psi,(l,d,p)):=\begin{cases}(0,\psi)\text{ if
}d\in\\{\mathit{int},\mathit{call},\mathit{callRet},\mathit{spawn}\\}\\\
(\varepsilon,\bigcirc^{-}\bigcirc^{a}\psi)\text{ if }d=\mathit{ret}\\\
\mathit{false}\text{ if }d=\mathit{end}\end{cases}$
$\displaystyle\rho(\bigcirc^{a}\psi,(l,d,p))$
$\displaystyle\rho(\bigcirc^{-}\psi,(l,d,p))$
$\displaystyle:=\begin{cases}(0,\psi)\text{ if
}d\in\\{\mathit{int},\mathit{spawn}\\}\\\ (1,\psi)\text{ if
}d=\mathit{callRet}\\\ \mathit{false}\text{ if
}d\in\\{\mathit{call},\mathit{ret},\mathit{end}\\}\end{cases}$
$\displaystyle:=\begin{cases}(\uparrow,\psi)\text{ if }p=\mathit{call}\\\
(\uparrow,\bigcirc^{-}\psi)\text{ if }p\in\\{\mathit{int},\mathit{ret}\\}\\\
\mathit{false}\text{ if }p\in\\{\mathit{spawn},\bot\\}\end{cases}$
$\displaystyle\rho(\bigcirc^{p}\psi,(l,d,p))$
$\displaystyle\rho(\bigcirc^{c}\psi,(l,d,p))$
$\displaystyle:=\begin{cases}(\uparrow,\psi)\text{ if }p=\mathit{spawn}\\\
(\uparrow,\bigcirc^{p}\psi)\text{ if
}p\in\\{\mathit{int},\mathit{call},\mathit{ret}\\}\\\ \mathit{false}\text{ if
}p=\bot\end{cases}$ $\displaystyle:=\begin{cases}(1,\psi)\text{ if
}d=\mathit{spawn}\\\ \mathit{false}\text{ if }d\neq\mathit{spawn}\end{cases}$

In the above definition, we move to $\mathit{false}$ when we see that the
desired successor does not exist and the formula is not satisfied. The
transition function for dual next operators is defined analogously but moves
to $\mathit{true}$ instead of $\mathit{false}$ in case the successor does not
exist.

For the global predecessor, we additionally use states of the form
$(\mathit{call},\psi)$ and $(\mathit{leaf},\psi)$ for moving to the
$\\{\mathit{int},\mathit{ret}\\}$-descendant leaf of the $\mathit{call}$-child
of the parent of a node in cases where the global predecessor is defined this
way:

$\displaystyle\rho(\bigcirc^{\uparrow}\psi,(l,d,p))$
$\displaystyle\rho((\mathit{leaf},\psi),(l,d,p))$
$\displaystyle:=\begin{cases}(\uparrow,\psi)\text{ if
}p\in\\{\mathit{int},\mathit{call}\\}\\\ (\uparrow,(\mathit{call},\psi))\text{
if }p=\mathit{ret}\\\ \mathit{false}\text{ if
}p\in\\{\mathit{spawn},\bot\\},\end{cases}$
$\displaystyle:=\begin{cases}(0,(\mathit{leaf},\psi))\text{ if
}d\in\\{\mathit{int},\mathit{spawn}\\}\\\ (1,(\mathit{leaf},\psi))\text{ if
}d=\mathit{callRet}\\\ (\varepsilon,\psi)\text{ if
}d\in\\{\mathit{ret},\mathit{call},\mathit{end}\\}\\\ \end{cases}$
$\displaystyle\text{and
}\rho((\mathit{call},\psi),\sigma):=(0,(\mathit{leaf},\psi)).$

Note that if we are in a state $(\mathit{leaf},\psi)$ at position
$\delta_{G}(x)$ in the tree, $d(x)\in\\{\mathit{call},\mathit{end}\\}$ cannot
hold if the tree represents an execution graph since in this case $x$ lies on
the path between nodes $y$ and $z$ following
$\mathsf{Moves}\setminus\\{\mathit{spawn}\\}$-successors with
$y\curvearrowright z$ and $x\neq z$.

Finally, fixpoint formulae lead to loops:

$\displaystyle\rho(\lambda X.\psi,\sigma):=(\varepsilon,\psi)\text{ for
}\lambda\in\\{\mu,\nu\\}\text{ and
}\rho(X,\sigma):=(\varepsilon,\mathit{fp}(X)).$

The acceptance condition specifies whether a fixpoint formula may be visited
at most a finite number of times or an infinite number of visits is allowed.
In this definition, higher priorities are assigned to fixpoint formulae
binding variables which depend on other fixpoint variables. Formally, we say
that a fixpoint variable $X^{\prime}$ depends on the variable $X$ in
$\varphi$, written $X\prec_{\varphi}X^{\prime}$, if $X$ is a free variable in
$\mathit{fp}(X^{\prime})$. We consider all maximal chains
$X_{1}\prec_{\varphi}...\prec_{\varphi}X_{n}$ of fixpoint variables appearing
in $\varphi$. If $\mathit{fp}(X_{1})$ is a formula of the form $\mu X.\psi$,
we set $\Omega(\mathit{fp}(X_{1}))=1$, otherwise we set
$\Omega(\mathit{fp}(X_{1}))=0$. Then, we move through the chains and assign
this priority to $\mathit{fp}(X_{i})$ as long as the fixpoint type does not
change. In that case, we increase the currently assigned priority by one and
keep going. Then, we set $\Omega(q)$ to the highest priority assigned so far
for all other states $q$.

We establish the following theorem.

###### Theorem 7.2

Let $\varphi$ be a closed, well-formed NTL formula, $G$ be an execution graph
and $\tilde{\mathcal{A}}_{\varphi}$ be the 2ATA defined above. Then
$\tilde{\mathcal{A}}_{\varphi}$ accepts $\mathcal{T}(G)$ iff
$G\in\llbracket\varphi\rrbracket$.

######  Proof (Proof Sketch)

The proof is by induction on the structure of $\varphi$. Therefore, we also
have to deal with non-closed subformulae and consider valuations to decide
whether a subformula is satisfied. In order to do this in a formal way, we
consider automata with special states $X_{1},\dots,X_{n}$, called _holes_
[21], that can be filled with sets of nodes $L_{1},\dots,L_{n}$ of a given
tree. Intuitively, such an automaton can operate on a tree as before, but when
a hole $X_{i}$ is encountered during a run and we are at the tree node $t$,
then we do not continue on the current path and say that it is accepting iff
$t\in L_{i}$. By
$\mathcal{L}_{q}^{\mathcal{T}}(\mathcal{A}[X_{1}:L_{1},\dots,X_{n}:L_{n}])$ we
denote the set of nodes $t\in T$ such that there is an accepting $(t,q)$-run
over $\mathcal{A}$ where the states $X_{1},\dots,X_{n}$ are holes filled by
$L_{1},\dots,L_{n}$.

For the inductive proof, we assume that the free variables of the current
formula $\psi\in\mathit{Sub}(\varphi)$ are holes in the automaton and show
that the language of this automaton corresponds to the semantics of $\psi$.
Intuitively, we fill the holes in the automaton, i.e. the free variables of
$\psi$, with the same sets of nodes as specified by a given valuation that we
consider for the semantics of $\psi$. More formally, the holes are filled by
sets of tree nodes that correspond to given sets of graph nodes in the
valuation.

We consider the case for subformulae of the form $\psi\equiv\mu
X.\psi^{\prime}$ with free variables $X_{1},\dots,X_{n}$. Let $\mathcal{V}$ be
a fixpoint variable assignment, $\mathcal{T}(G)=\mathcal{T}=(T,r)$ and $R$ be
a $(t,\psi)$-run over $\mathcal{\tilde{A}}_{\varphi}$ for a $t\in T$, where
the states $X_{1},\dots,X_{n}$ are holes filled by
$\delta_{G}(L_{1}),\dots,\delta_{G}(L_{n})$ with $L_{i}=\mathcal{V}(X_{i})$.
We observe that $R$ can only visit states $\varphi^{\prime}$ of the form $\mu
X.\psi^{\prime\prime}$ or $\nu X.\psi^{\prime\prime}$ if $\varphi^{\prime}$ is
a subformula of $\psi$. Therefore, $\Omega(\psi)$ is the lowest priority
occurring in the run so that the state $\psi$ can only be visited finitely
often if the run is accepting. This means we can characterize
$\mathcal{L}_{\psi}^{\mathcal{T}}(\mathcal{\tilde{A}}_{\varphi}[X_{1}:{\delta}_{G}(L_{1}),\dots,X_{n}:{\delta}_{G}(L_{n})])$
as the least fixpoint of the function $f:2^{T}\to 2^{T}$ with
$f({\delta}_{G}(L)):=\mathcal{L}_{\psi^{\prime}}^{\mathcal{T}}(\mathcal{\tilde{A}}_{\varphi}[X_{1}:{\delta}_{G}(L_{1}),\dots,X_{n}:{\delta}_{G}(L_{n}),X:{\delta}_{G}(L)])$.
Thus, we can use the induction hypothesis and the fixpoint characterization of
the semantics of $\psi$ obtained by Knaster-Tarski’s fixpoint theorem to get
the desired result in this inductive step.

Since $\varphi$ is closed, the induction establishes in particular that
$\tilde{\mathcal{A}}_{\varphi}$ accepts $\mathcal{T}(G)$ iff
$G\in\llbracket\varphi\rrbracket$. Details of this proof can be found in
Appendix 0.E. ∎

As mentioned, we do not use this automaton directly but instead intersect it
with $\mathcal{A}_{\mathsf{ET}}$ from Theorem 7.1 and then transform it into a
nondeterministic parity tree automaton using Proposition 1. We obtain:

###### Corollary 1

Let $\varphi$ be a closed, well-formed NTL formula. Then we can construct an
NPTA $\mathcal{A}_{\varphi}$ over $(\mathit{TL},\mathit{ar})$-labelled binary
trees with a number of states exponential and an acceptance condition linear
in $|\varphi|$ such that
$\mathcal{L}(\mathcal{A}_{\varphi})=\\{\mathcal{T}(G)\mid G\text{ is an
execution graph with }G\in\llbracket\varphi\rrbracket\\}$.

An automaton for DPNs. We proceed with an automaton for a DPN
$\mathcal{M}=(S,s_{0},\gamma_{0},\Delta,L)$. We define
$\mathcal{A}_{\mathcal{M}}$ as an NPTA that checks whether an execution tree
represents an execution graph generated by $\mathcal{M}$. We set
$\mathcal{A}_{\mathcal{M}}:=(Q,q_{0},\rho,\Omega)$ where $Q$, $q_{0}$, $\rho$
and $\Omega$ are described in more detail next.

The state set is given by
$Q=S\times\Gamma\times((S\times\Gamma)\cup\\{\bot\\})$ with initial state
$q_{0}=(s_{0},\gamma_{0},\bot)$. Being in a state $(s,\gamma,c)\in Q$ at the
position $\delta_{G}(x)$ in the tree labelled by $(l,d,p)$ means that there is
a suitable assignment $\mathit{as}$ assigning configurations to the graph
nodes whose corresponding tree nodes have been visited so far where
$\mathit{as}(x)=(s,\gamma w)$ for some stack content $w\in\Gamma^{*}\bot$. If
$d=\mathit{callRet}$, we also have to know the configuration assigned to the
global predecessor of the $\mathit{ret}$-child of the current node to check
that we can extend $\mathit{as}$ suitably for the children of the current
node. We thus guess this configuration in this case and use $c\in
S\times\Gamma$ to indicate that we must assign $c$ to the
$\\{\mathit{int},\mathit{ret}\\}$-descendant leaf of the call successor of the
current node in order to fulfill the requirements for the assignment
$\mathit{as}$. Note that the $\\{\mathit{int},\mathit{ret}\\}$-descendant leaf
exists in this case, if the input tree is an execution tree. The transition
function $\rho$ then checks that (i) $l=L(\mathit{as}(x))$, (ii) if $c\in
S\times\Gamma$, then the configuration $c$ is assigned to the
$\\{\mathit{int},\mathit{ret}\\}$-descendant leaf of $\delta_{G}(x)$ and (iii)
the assignment $\mathit{as}$ can be properly extended to the children of
$\delta_{G}(x)$. We set

$\displaystyle\rho((s,\gamma,c),(l,\mathit{int},p)):=$
$\displaystyle\bigvee\\{(0,(s^{\prime},\gamma^{\prime},c))\mid
s\gamma\rightarrow s^{\prime}\gamma^{\prime}\in\Delta_{I}\\},$
$\displaystyle\rho((s,\gamma,\bot),(l,\mathit{call},p)):=$
$\displaystyle\bigvee\\{(0,(s^{\prime},\gamma^{\prime},\bot))\mid\exists\gamma^{\prime\prime}\in\Gamma\text{
s.t. }s\gamma\rightarrow
s^{\prime}\gamma^{\prime}\gamma^{\prime\prime}\in\Delta_{C}\\},$
$\displaystyle\rho((s,\gamma,c),(l,\mathit{callRet},p)):=$
$\displaystyle\bigvee\\{(0,(s^{\prime},\gamma^{\prime},(s_{r},\gamma_{r})))\land(1,(s^{\prime\prime},\gamma^{\prime\prime},c))\mid$
$\displaystyle s\gamma\rightarrow
s^{\prime}\gamma^{\prime}\gamma^{\prime\prime}\in\Delta_{C}\text{ and
}s_{r}\gamma_{r}\rightarrow s^{\prime\prime}\in\Delta_{R}\\},$
$\displaystyle\rho((s,\gamma,c),(l,\mathit{spawn},p)):=$
$\displaystyle\bigvee\\{(0,(s^{\prime},\gamma^{\prime},c))\land(1,(s_{n},\gamma_{n},\bot))\mid$
$\displaystyle s\gamma\rightarrow s^{\prime}\gamma^{\prime}\vartriangleright
s_{n}\gamma_{n}\in\Delta_{S}\\},$
$\displaystyle\rho((s,\gamma,(s,\gamma)),(l,\mathit{ret},p)):=$
$\displaystyle\ \mathit{true}\text{ and}$
$\displaystyle\rho((s,\gamma,\bot),(l,\mathit{end},p)):=$
$\displaystyle\begin{cases}\mathit{true}\text{ if there is no transition for
}s\gamma\text{ in }\Delta\\\ \mathit{false}\text{ else}\end{cases}$

for $l=L(s,\gamma)$ and $\rho((s,\gamma,c),(l,d,p)):=\mathit{false}$ in all
other cases. Since we are only concerned with execution trees as inputs, all
conditions necessary to determine if the input tree is generated by
$\mathcal{M}$ are already checked by the transition function of
$\mathcal{A}_{\mathcal{M}}$. We thus set $\Omega(q):=0$ for all $q\in Q$. We
establish the following theorem. A detailed proof can be found in Appendix
0.E.

###### Theorem 7.3

Let $\mathcal{M}$ be a DPN. We can construct an NPTA
$\mathcal{A}_{\mathcal{M}}$ over $(\mathit{TL},\mathit{ar})$-labelled binary
trees with a number of states quadratic in $|\mathcal{M}|$ and a trivial
acceptance condition such that for all execution graphs $G$,
$\mathcal{T}(G)\in\mathcal{L}(\mathcal{A}_{\mathcal{M}})$ iff
$G\in\llbracket\mathcal{M}\rrbracket$.

Complexity of Model Checking and Satisfiability. These automata constructions
can be used to obtain a decision procedure for the model checking and
satisfiability problems. For the former, we obtain the following theorem:

###### Theorem 7.4

The model checking problem for NTL is $\mathsf{EXPTIME}$-complete. For fixed
formulae, the problem is in $\mathsf{PTIME}$.

###### Proof

For the upper bound, we construct an automaton for the negation of the formula
using Corollary 1 and intersect it with an automaton for the DPN from Theorem
7.3. Since the acceptance condition of the latter is trivial, the resulting
automaton is quadratic in the size of the DPN and exponential in the size of
the formula by Proposition 3 (ii). It is tested for emptiness using
Proposition 2 in time exponential in $|\varphi|$ and polynomial in
$|\mathcal{M}|$ to answer the model checking problem.

The lower bound follows by a reduction from the $\mathit{LTL}$ pushdown model
checking problem which was shown to be $\mathsf{EXPTIME}$-hard in [8]. The
reduction is trivial since $\mathit{LTL}$ is a sublogic of NTL for single
threads and pushdown systems can be trivially embedded into DPNs with a single
thread. ∎

For satisfiability, we can show that the two problems defined in Section 4 are
equivalent and thus only need to solve one of the problems by a direct
procedure.

###### Theorem 7.5

The graph and DPN satisfiability problems are equivalent.

###### Proof

For the first direction, assume that a formula $\varphi$ is satisfiable by a
DPN $\mathcal{M}$. Then $G\models\varphi$ for all
$G\in\llbracket\mathcal{M}\rrbracket$. Since
$\llbracket\mathcal{M}\rrbracket\neq\emptyset$ (this indeed holds for all
DPNs), we can thus choose an arbitrary graph
$G\in\llbracket\mathcal{M}\rrbracket$ to show that $\varphi$ is satisfiable by
a graph.

For the other direction, assume that a formula $\varphi$ is satisfiable by a
graph $G$. By Corollary 1, we know that
$\mathcal{T}(G)\in\mathcal{L}(\mathcal{A}_{\varphi})$. Since
$\mathcal{L}(\mathcal{A}_{\varphi})$ is a nonempty $\omega$-regular tree
language, we know that $\mathcal{T}\in\mathcal{L}(\mathcal{A}_{\varphi})$ for
a regular tree $\mathcal{T}=(T,r)$, i.e. a tree with only finitely many non-
isomorphic subtrees (see e.g. Cor 8.20. in [16]). Let $x_{1},\dots,x_{n}$ be
the finitely many classes of nodes associated with the roots of the distinct
subtrees of $T$ such that $x_{1}$ is the class of $\varepsilon$ and let
$(l_{i},d_{i},p_{i})$ be the label of the nodes from class $x_{i}$. We
construct a DPN $\mathcal{M}=(\\{s\\},s,x_{1},\Delta,L)$ with stack alphabet
$\Gamma=\\{x_{1},\dots,x_{n}\\}$. The labeling $L$ is defined such that
$L(s,x_{i})=l_{i}$. Transition rules are defined from the parent-child
relationships between the different classes of nodes: (i) if
$d_{i}=\mathit{int}$, then nodes of class $x_{i}$ have exactly one child of
class $x_{j}$ and we include $sx_{i}\rightarrow sx_{j}\in\Delta$, (ii) if
$d_{i}=\mathit{spawn}$, then nodes of class $x_{i}$ have exactly one left
child of class $x_{j}$ and one right child of class $x_{k}$ and we include
$sx_{i}\rightarrow sx_{j}\triangleright sx_{k}\in\Delta$, (iii) if
$d_{i}=\mathit{callRet}$, then nodes of class $x_{i}$ have exactly one left
child of class $x_{j}$ and one right child of class $x_{k}$ and we include
$sx_{i}\rightarrow sx_{j}x_{k}\in\Delta$, (iv) if $d_{i}=\mathit{call}$, then
nodes of class $x_{i}$ have exactly one child of class $x_{j}$ and we include
$sx_{i}\rightarrow sx_{j}x_{i}\in\Delta$, (v) if $d_{i}=\mathit{ret}$, then
nodes of class $x_{i}$ have no children and we include $sx_{i}\rightarrow
s\in\Delta$ and (vi) if $d_{i}=\mathit{end}$, then nodes of class $x_{i}$ have
no children and we do not include a transition. It is easy to see that
$\llbracket\mathcal{M}\rrbracket$ is a singleton set since $\mathcal{M}$ is
deterministic. We show that $\llbracket\mathcal{M}\rrbracket=\\{H\\}$ where
$\mathcal{T}=\mathcal{T}(H)$ and thus $\mathcal{M}\models\varphi$. For this,
let $\mathcal{T}(H)=(T_{H},r_{H})$.

We show by induction on the length of $x$ that for all $x\in\\{0,1\\}^{*}$,
$x\in T$ iff $x\in T_{H}$ and in that case (a) $r(x)=r_{H}(x)$ and (b) if $x$
belongs to class $x_{i}$, then the configuration in $\delta_{G}^{-1}(x)$ is
$(s,x_{i}w)$ for some stack content $w$. In the base case, we know that
$\varepsilon\in T$ and $\varepsilon\in T_{H}$. We know that
$r(\varepsilon)=(l_{1},d_{1},p_{1})$ since $T$ is rooted in $x_{1}$ and
$p_{1}=\bot$ since $\mathcal{T}$ is an execution tree. Let
$r_{H}(\varepsilon)=(l,d,p)$. Since $(s,x_{1}\bot)$ is the starting
configuration of $\mathcal{M}$, we know that it is also the configuration in
$\delta_{G}^{-1}(\varepsilon)$ and that $l=l_{1}$. Additionally, we can show
that $d=d_{1}$ by a case distinction on $d_{1}$. We only sketch the case
$d_{1}=\mathit{int}$, the other cases are similar. In this case, the only
enabled transition in $(s,x_{1}\bot)$ is $sx_{1}\rightarrow sx_{j}$, an
internal transition. Thus, $\delta_{G}^{-1}(\varepsilon)$ has exactly one
$\mathit{int}$-successor in $H$ which means that $d=\mathit{int}$. Finally,
since $\mathcal{T}(H)$ is an execution tree, we have $p=\bot$.

In the inductive step, we consider $x\cdot d$ for $d\in\\{0,1\\}$. From the
induction hypothesis, we know that the claim holds for $x$. If $x\not\in T$
and $x\not\in T_{H}$, then also $x\cdot d\not\in T$ and $x\cdot d\not\in
T_{H}$ since trees are prefix-closed. In the other case, let $x_{i}$ be the
class of $x$. We have $x\in T$ and $x\in T_{H}$ with
$r(x)=r_{H}(x)=(l_{i},d_{i},p_{i})$ and the configuration in
$\delta_{G}^{-1}(x)$ is $(s,x_{i}w)$ for some stack content $w$. We
distinguish cases based on $d_{i}$. We consider the most involved case where
$d_{i}=\mathit{callRet}$. Since $\mathcal{T}$ is an execution tree, we know
that $x\cdot d\in T$ for $d\in\\{0,1\\}$. Let $x_{j}$ be the class of $x\cdot
0$ and $x_{k}$ be the class of $x\cdot 1$. We know that the only enabled
transition in $(s,x_{i}w)$ is $sx_{i}\rightarrow sx_{j}x_{k}$. Since
$d_{i}=\mathit{callRet}$ and since $\mathcal{T}(G)$ is an execution tree, we
know that $\delta_{G}^{-1}(x\cdot 0)$ continues with the configuration after
this call transition and $\delta_{G}^{-1}(x\cdot 1)$ continues with the
configuration after the matching return transition (which exists in this
case). Thus, the configuration in $\delta_{G}^{-1}(x\cdot 0)$ is
$(s,x_{j}x_{k}w)$ and the configuration in $\delta_{G}^{-1}(x\cdot 1)$ is
$(s,x_{k}w)$, establishing this part of the claim. We now establish that
$r(x\cdot d)=r_{H}(x\cdot d)$. For the first and second component, this is
established by the fact that the configuration in $\delta_{G}^{-1}(x\cdot d)$
determines both the label and the unique enabled transition. For the third
component, this follows from the fact that both $\mathcal{T}$ and
$\mathcal{T}(H)$ are execution trees and the fact that $r(x)$ and $r_{H}(x)$
match in the second component. ∎

We obtain the following theorem for the two satisfiability problems:

###### Theorem 7.6

The graph and DPN satisfiability problems for NTL are
$\mathsf{EXPTIME}$-complete.

###### Proof

Since the two problems are equivalent by Theorem 7.5, we need to only give an
upper and lower bound for the graph satisfiability problem.

For the upper bound, we can construct an automaton for the formula using
Corollary 1 and test it for emptiness using Proposition 2 in time exponential
in $|\varphi|$ for an answer to the graph satisfiability problem.

The lower bound follows by a reduction from the
$\mathit{VP}$-$\mu$-$\mathit{TL}$ satisfiability problem which was shown to be
$\mathsf{EXPTIME}$-hard in [10]. The reduction is straightforward since
$\mathit{VP}$-$\mu$-$\mathit{TL}$ is a sublogic of NTL and we can easily
extract a nested word satisfying a formula interpreted in
$\mathit{VP}$-$\mu$-$\mathit{TL}$ from the execution graph satisfying the same
formula interpreted in NTL. ∎

##  8 Conclusion

We introduced a novel specification logic called NTL for reasoning about the
call-return and thread creation behaviour of dynamic pushdown networks. We
showed that a variety of interesting properties regarding the behaviour of
multithreaded software is expressible in NTL. Further, the model checking and
satisfiability problems were investigated. The complexity of these problems is
not higher than that of the corresponding problems for related logics for
pushdown systems despite a more powerful logic and system model. For future
work, it would be interesting to consider more powerful variants of DPNs that
allow communication and synchronization of different threads via locking or
messages.

## References

  * [1] Oracle Java docs: Intrinsic locks and synchronization, https://docs.oracle.com/javase/tutorial/essential/concurrency/locksync.html
  * [2] Alur, R., Arenas, M., Barceló, P., Etessami, K., Immerman, N., Libkin, L.: First-order and temporal logics for nested words. Log. Methods Comput. Sci. 4(4) (2008). https://doi.org/10.2168/LMCS-4(4:11)2008, https://doi.org/10.2168/LMCS-4(4:11)2008
  * [3] Alur, R., Chaudhuri, S., Madhusudan, P.: A fixpoint calculus for local and global program flows. In: Morrisett, J.G., Jones, S.L.P. (eds.) Proceedings of the 33rd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2006, Charleston, South Carolina, USA, January 11-13, 2006. pp. 153–165. ACM (2006). https://doi.org/10.1145/1111037.1111051, https://doi.org/10.1145/1111037.1111051
  * [4] Alur, R., Etessami, K., Madhusudan, P.: A temporal logic of nested calls and returns. In: Jensen, K., Podelski, A. (eds.) Tools and Algorithms for the Construction and Analysis of Systems, 10th International Conference, TACAS 2004, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2004, Barcelona, Spain, March 29 - April 2, 2004, Proceedings. Lecture Notes in Computer Science, vol. 2988, pp. 467–481. Springer (2004). https://doi.org/10.1007/978-3-540-24730-2_35, https://doi.org/10.1007/978-3-540-24730-2_35
  * [5] Alur, R., Madhusudan, P.: Adding nesting structure to words. In: Ibarra, O.H., Dang, Z. (eds.) Developments in Language Theory, 10th International Conference, DLT 2006, Santa Barbara, CA, USA, June 26-29, 2006, Proceedings. Lecture Notes in Computer Science, vol. 4036, pp. 1–13. Springer (2006). https://doi.org/10.1007/11779148_1, https://doi.org/10.1007/11779148_1
  * [6] Apt, K.R., Plotkin, G.D.: Countable nondeterminism and random assignment. J. ACM 33(4), 724–767 (1986). https://doi.org/10.1145/6490.6494, https://doi.org/10.1145/6490.6494
  * [7] Atig, M.F., Bouajjani, A., Qadeer, S.: Context-bounded analysis for concurrent programs with dynamic creation of threads. Log. Methods Comput. Sci. 7(4) (2011). https://doi.org/10.2168/LMCS-7(4:4)2011, https://doi.org/10.2168/LMCS-7(4:4)2011
  * [8] Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: Mazurkiewicz, A.W., Winkowski, J. (eds.) CONCUR ’97: Concurrency Theory, 8th International Conference, Warsaw, Poland, July 1-4, 1997, Proceedings. Lecture Notes in Computer Science, vol. 1243, pp. 135–150. Springer (1997). https://doi.org/10.1007/3-540-63141-0_10, https://doi.org/10.1007/3-540-63141-0_10
  * [9] Bouajjani, A., Müller-Olm, M., Touili, T.: Regular symbolic analysis of dynamic networks of pushdown systems. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005 - Concurrency Theory, 16th International Conference, CONCUR 2005, San Francisco, CA, USA, August 23-26, 2005, Proceedings. Lecture Notes in Computer Science, vol. 3653, pp. 473–487. Springer (2005). https://doi.org/10.1007/11539452_36, https://doi.org/10.1007/11539452_36
  * [10] Bozzelli, L.: Alternating automata and a temporal fixpoint calculus for visibly pushdown languages. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007 – Concurrency Theory. pp. 476–491. Springer Berlin Heidelberg, Berlin, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74407-8_32
  * [11] Bozzelli, L., Lanotte, R.: Hybrid and first-order complete extensions of CaRet. In: Brünnler, K., Metcalfe, G. (eds.) Automated Reasoning with Analytic Tableaux and Related Methods - 20th International Conference, TABLEAUX 2011, Bern, Switzerland, July 4-8, 2011. Proceedings. Lecture Notes in Computer Science, vol. 6793, pp. 58–72. Springer (2011). https://doi.org/10.1007/978-3-642-22119-4_7, https://doi.org/10.1007/978-3-642-22119-4_7
  * [12] Clarke, E.M., Emerson, E.A.: Design and synthesis of synchronization skeletons using branching-time temporal logic. In: Kozen, D. (ed.) Logics of Programs, Workshop, Yorktown Heights, New York, USA, May 1981. Lecture Notes in Computer Science, vol. 131, pp. 52–71. Springer (1981). https://doi.org/10.1007/BFb0025774, https://doi.org/10.1007/BFb0025774
  * [13] Diaz, M., Touili, T.: Model checking dynamic pushdown networks with locks and priorities. In: Podelski, A., Taïani, F. (eds.) Networked Systems - 6th International Conference, NETYS 2018, Essaouira, Morocco, May 9-11, 2018, Revised Selected Papers. Lecture Notes in Computer Science, vol. 11028, pp. 240–251. Springer (2018). https://doi.org/10.1007/978-3-030-05529-5_16, https://doi.org/10.1007/978-3-030-05529-5_16
  * [14] Emerson, E.A., Jutla, C.S.: The complexity of tree automata and logics of programs (extended abstract). In: 29th Annual Symposium on Foundations of Computer Science, White Plains, New York, USA, 24-26 October 1988. pp. 328–337. IEEE Computer Society (1988). https://doi.org/10.1109/SFCS.1988.21949, https://doi.org/10.1109/SFCS.1988.21949
  * [15] Gawlitza, T.M., Lammich, P., Müller-Olm, M., Seidl, H., Wenner, A.: Join-lock-sensitive forward reachability analysis for concurrent programs with dynamic process creation. In: Jhala, R., Schmidt, D.A. (eds.) Verification, Model Checking, and Abstract Interpretation - 12th International Conference, VMCAI 2011, Austin, TX, USA, January 23-25, 2011. Proceedings. Lecture Notes in Computer Science, vol. 6538, pp. 199–213. Springer (2011). https://doi.org/10.1007/978-3-642-18275-4_15, https://doi.org/10.1007/978-3-642-18275-4_15
  * [16] Grädel, E., Thomas, W., Wilke, T. (eds.): Automata, Logics, and Infinite Games: A Guide to Current Research [outcome of a Dagstuhl seminar, February 2001], Lecture Notes in Computer Science, vol. 2500. Springer (2002). https://doi.org/10.1007/3-540-36387-4, https://doi.org/10.1007/3-540-36387-4
  * [17] Gutsfeld, J.O., Müller-Olm, M., Nordhoff, B.: A branching time variant of CaRet. In: Gallardo, M., Merino, P. (eds.) Model Checking Software - 25th International Symposium, SPIN 2018, Malaga, Spain, June 20-22, 2018, Proceedings. Lecture Notes in Computer Science, vol. 10869, pp. 153–170. Springer (2018). https://doi.org/10.1007/978-3-319-94111-0_9, https://doi.org/10.1007/978-3-319-94111-0_9
  * [18] Kupferman, O., Vardi, M.Y.: Weak alternating automata and tree automata emptiness. In: Vitter, J.S. (ed.) Proceedings of the Thirtieth Annual ACM Symposium on the Theory of Computing, Dallas, Texas, USA, May 23-26, 1998. pp. 224–233. ACM (1998). https://doi.org/10.1145/276698.276748, https://doi.org/10.1145/276698.276748
  * [19] Lammich, P., Müller-Olm, M., Seidl, H., Wenner, A.: Contextual locking for dynamic pushdown networks. In: Logozzo, F., Fähndrich, M. (eds.) Static Analysis - 20th International Symposium, SAS 2013, Seattle, WA, USA, June 20-22, 2013. Proceedings. Lecture Notes in Computer Science, vol. 7935, pp. 477–498. Springer (2013). https://doi.org/10.1007/978-3-642-38856-9_25, https://doi.org/10.1007/978-3-642-38856-9_25
  * [20] Lammich, P., Müller-Olm, M., Wenner, A.: Predecessor sets of dynamic pushdown networks with tree-regular constraints. In: Bouajjani, A., Maler, O. (eds.) Computer Aided Verification, 21st International Conference, CAV 2009, Grenoble, France, June 26 - July 2, 2009. Proceedings. Lecture Notes in Computer Science, vol. 5643, pp. 525–539. Springer (2009). https://doi.org/10.1007/978-3-642-02658-4_39, https://doi.org/10.1007/978-3-642-02658-4_39
  * [21] Lange, M.: Weak automata for the linear time $\mu$-calculus. In: Cousot, R. (ed.) Verification, Model Checking, and Abstract Interpretation. pp. 267–281. Springer Berlin Heidelberg, Berlin, Heidelberg (2005). https://doi.org/10.1007/978-3-540-30579-8_18, https://doi.org/10.1007/978-3-540-30579-8_18
  * [22] Lichtenstein, O., Pnueli, A.: Checking that finite state concurrent programs satisfy their linear specification. In: Deusen, M.S.V., Galil, Z., Reid, B.K. (eds.) Conference Record of the Twelfth Annual ACM Symposium on Principles of Programming Languages, New Orleans, Louisiana, USA, January 1985. pp. 97–107. ACM Press (1985). https://doi.org/10.1145/318593.318622, https://doi.org/10.1145/318593.318622
  * [23] Löding, C.: Automata on infinite trees. In: Pin, J. (ed.) Handbook of Automata Theory, pp. 265–302. European Mathematical Society Publishing House, Zürich, Switzerland (2021). https://doi.org/10.4171/Automata-1/8, https://doi.org/10.4171/Automata-1/8
  * [24] Nordhoff, B., Müller-Olm, M., Lammich, P.: Iterable forward reachability analysis of Monitor-DPNs. In: Banerjee, A., Danvy, O., Doh, K., Hatcliff, J. (eds.) Semantics, Abstract Interpretation, and Reasoning about Programs: Essays Dedicated to David A. Schmidt on the Occasion of his Sixtieth Birthday, Manhattan, Kansas, USA, 19-20th September 2013. EPTCS, vol. 129, pp. 384–403 (2013). https://doi.org/10.4204/EPTCS.129.24, https://doi.org/10.4204/EPTCS.129.24
  * [25] Pnueli, A., Rosner, R.: On the synthesis of an asynchronous reactive module. In: Ausiello, G., Dezani-Ciancaglini, M., Rocca, S.R.D. (eds.) Automata, Languages and Programming, 16th International Colloquium, ICALP89, Stresa, Italy, July 11-15, 1989, Proceedings. Lecture Notes in Computer Science, vol. 372, pp. 652–671. Springer (1989). https://doi.org/10.1007/BFb0035790, https://doi.org/10.1007/BFb0035790
  * [26] Song, F., Touili, T.: Model checking dynamic pushdown networks. Formal Aspects Comput. 27(2), 397–421 (2015). https://doi.org/10.1007/s00165-014-0330-y, https://doi.org/10.1007/s00165-014-0330-y
  * [27] Tarski, A.: A lattice-theoretical fixpoint theorem and its applications. Pacific J. Math. 5(2), 285–309 (1955), https://projecteuclid.org:443/euclid.pjm/1103044538
  * [28] Vardi, M.Y.: A temporal fixpoint calculus. In: POPL. pp. 250–259. ACM Press (1988). https://doi.org/10.1145/73560.735822, https://doi.org/10.1145/73560.73582
  * [29] Vardi, M.Y.: Reasoning about the past with two-way automata. In: Larsen, K.G., Skyum, S., Winskel, G. (eds.) Automata, Languages and Programming, 25th International Colloquium, ICALP’98, Aalborg, Denmark, July 13-17, 1998, Proceedings. Lecture Notes in Computer Science, vol. 1443, pp. 628–641. Springer (1998). https://doi.org/10.1007/BFb0055090, https://doi.org/10.1007/BFb0055090

##  Appendix 0.A Fixpoint Theory

In some of the proofs in this paper, we need results from fixpoint theory. We
provide the necessary definitions and results in this section. A partial order
is a pair $(L,\sqsubseteq)$ such that $\sqsubseteq$ is a reflexive, transitive
and antisymmetric binary relation on $L$. For $X\subseteq L$ and $x\in L$, we
call $x$ a lower bound on $X$ iff $x\sqsubseteq x^{\prime}$ for all
$x^{\prime}\in X$. Similarly, $x$ is called an upper bound on $X$ iff
$x^{\prime}\sqsubseteq x$ for all $x^{\prime}\in X$. A lower bound $x$ of $X$
is called the greatest lower bound of $X$, denoted $x=\bigsqcap X$, iff
$x^{\prime}\sqsubseteq x$ for all lower bounds $x^{\prime}$ of $X$.
Analogously, an upper bound $x$ of $X$ is called the least upper bound of $X$,
denoted $x=\bigsqcup X$, iff $x\sqsubseteq x^{\prime}$ for all upper bounds
$x^{\prime}$ of $X$. A partial order $(L,\sqsubseteq)$ is called a complete
lattice iff the least upper bound $\bigsqcup X$ exists for every set
$X\subseteq L$. For a function $f\colon L\to L^{\prime}$ on partial orders
$(L,\sqsubseteq)$ and $(L^{\prime},\sqsubseteq^{\prime})$, we call $f$
monotone iff $x\sqsubseteq x^{\prime}$ implies
$f(x)\sqsubseteq^{\prime}f(x^{\prime})$ for all $x,x^{\prime}\in L$. For
$(L,\sqsubseteq)=(L^{\prime},\sqsubseteq^{\prime})$, a fixpoint of $f$ is an
element $x\in L$ with $f(x)=x$. We call a fixpoint $x$ of $f$ the least
fixpoint of $f$, denoted $\mu f$, iff $x\sqsubseteq x^{\prime}$ for all
fixpoints $x^{\prime}$ of $f$. Analogously, a fixpoint $x$ is called the
greatest fixpoint of $f$, denoted $\nu f$, iff $x^{\prime}\sqsubseteq x$ for
all fixpoints $x^{\prime}$ of $f$. We use the classical Knaster-Tarski
fixpoint theorem:

######  Proposition 4 ([27])

Let $(L,\sqsubseteq)$ be a complete lattice and $f\colon L\to L$ be a monotone
function. Then $f$ has a least fixpoint that is characterised by $\mu
f=\bigsqcap\\{x\in L\mid f(x)\sqsubseteq x\\}$.

Additionally, we need a lemma about the relationship of least fixpoints in
different partial orders. This lemma is a variant of a similar transfer lemma
found e.g. in [6].

###### Lemma 2

Let $(L,\sqsubseteq)$ and $(L^{\prime},\sqsubseteq^{\prime})$ be partial
orders with functions $f\colon L\to L$, $f^{\prime}\colon L^{\prime}\to
L^{\prime}$ and $\mu f$ be the least fixpoint of $f$. Let further $h\colon
L\to L^{\prime}$ be a bijective, monotone function with $h\circ
f=f^{\prime}\circ h$. Then $\mu f^{\prime}=h(\mu f)$.

###### Proof

We first show that $h(\mu f)$ is a fixpoint of $f^{\prime}$. Since $\mu f$ is
a fixpoint of $f$, we have $f^{\prime}(h(\mu f))=f^{\prime}\circ h(\mu
f)=h\circ f(\mu f)=h(f(\mu f))=h(\mu f)$, i.e. $h(\mu f)$ is a fixpoint of
$f^{\prime}$.

It remains to show that $h(\mu f)$ is the _least_ fixpoint of $f^{\prime}$.
Therefore, let $y$ be an arbitrary fixpoint of $f^{\prime}$. We show that
$h(\mu f)\sqsubseteq y$. Since $y$ is a fixpoint of $f^{\prime}$, we have
$f(h^{-1}(y))=h^{-1}\circ h\circ f\circ h^{-1}(y)=h^{-1}\circ f^{\prime}\circ
h\circ h^{-1}(y)=h^{-1}(f^{\prime}(y))=h^{-1}(y)$, i.e. $h^{-1}(y)$ is a
fixpoint of $f$. Since $\mu f$ is the least fixpoint of $f$, we have $\mu
f\sqsubseteq h^{-1}(y)$. Since $h$ is monotone, we infer that $h(\mu
f)\sqsubseteq^{\prime}h(h^{-1}(y))=y$. Since $y$ was an arbitrary fixpoint of
$f^{\prime}$, the fixpoint $h(\mu f)$ must be the least fixpoint of
$f^{\prime}$. ∎

In this paper, we consider complete lattices of the form $(2^{A},\subseteq)$
for a set $A$. In these lattices, greatest lower and least upper bounds are
given by intersections and unions over sets, respectively.

##  Appendix 0.B Proofs from Section 4

###### Lemma 3

Let $S=(G,\mathcal{V},X,\varphi)$ where
$G=(V,l,(\rightarrow^{d})_{d\in\mathsf{Moves}},\curvearrowright)$ is an
execution graph, $\mathcal{V}$ is a fixpoint variable assignment, $X$ is a
fixpoint variable and $\varphi$ is a well-formed NTL formula in positive
normal form. Then, the function $\alpha_{S}:2^{V}\to 2^{V}$ with
$\alpha_{S}(M)=\llbracket\varphi\rrbracket^{G}_{\mathcal{V}[X\mapsto M]}$ is
monotone.

###### Proof

The proof is by induction on the structure of $\varphi$.

  * •

$\varphi=\mathit{ap}$ for $\mathit{ap}\in\mathit{AP}$: Since $\alpha_{S}$ is
constant in this case, we have $\alpha_{S}(M)=\alpha_{S}(M^{\prime})$ for
$M\subseteq M^{\prime}$.

  * •

$\varphi=\lnot\mathit{ap}$ for $\mathit{ap}\in\mathit{AP}$: Analogous to the
previous case.

  * •

$\varphi=Y$ for a fixpoint variable $Y$: For $Y\neq X$, $\alpha_{S}$ is
constant in this case, and we have $\alpha_{S}(M)=\alpha_{S}(M^{\prime})$ for
$M\subseteq M^{\prime}$. For $Y=X$, we have $\alpha_{S}(M)=M\subseteq
M^{\prime}=\alpha_{S}(M^{\prime})$ for $M\subseteq M^{\prime}$.

  * •

$\varphi=\varphi_{1}\lor\varphi_{2}$: Let
$S_{1}=(G,\mathcal{V},X,\varphi_{1})$ and
$S_{2}=(G,\mathcal{V},X,\varphi_{2})$. We have
$\alpha_{S}(M)=\alpha_{S_{1}}(M)\cup\alpha_{S_{2}}(M)\subseteq\alpha_{S_{1}}(M^{\prime})\cup\alpha_{S_{2}}(M^{\prime})=\alpha_{S}(M^{\prime})$
for $M\subseteq M^{\prime}$ by the induction hypothesis.

  * •

$\varphi=\varphi_{1}\land\varphi_{2}$: Analogous to the previous case.

  * •

$\varphi=\bigcirc^{f}\varphi_{1}$ for $f\in\\{g,\uparrow,a,-,p,c\\}$: Let
$S_{1}=(G,\mathcal{V},X,\varphi_{1})$. We have

$\displaystyle\alpha_{S}(M)$ $\displaystyle=\\{x\in
V\mid\mathit{succ}_{f}^{G}(x)\textit{ is defined and
}\mathit{succ}_{f}^{G}(x)\in\alpha_{S_{1}}(M)\\}$
$\displaystyle\subseteq\\{x\in V\mid\mathit{succ}_{f}^{G}(x)\textit{ is
defined and }\mathit{succ}_{f}^{G}(x)\in\alpha_{S_{1}}(M^{\prime})\\}$
$\displaystyle=\alpha_{S}(M^{\prime})$

for $M\subseteq M^{\prime}$ by the induction hypothesis.

  * •

$\varphi=\bigcirc^{\bar{f}}\varphi_{1}$ for $f\in\\{g,\uparrow,a,-,p,c\\}$:
Analogous to the previous case.

  * •

$\varphi=\mu Y.\varphi_{1}$: For $Y=X$, $\alpha_{S}$ is constant and we have
$\alpha_{S}(M)=\alpha_{S}(M^{\prime})$ for $M\subseteq M^{\prime}$. For $Y\neq
X$, let $S_{1}^{M^{\prime\prime}}=(G,\mathcal{V}[Y\mapsto
M^{\prime\prime}],X,\varphi_{1})$. We have

$\displaystyle\alpha_{S}(M)$
$\displaystyle=\bigcap\\{M^{\prime\prime}\subseteq
V\mid\llbracket\varphi_{1}\rrbracket_{\mathcal{V}[X\mapsto M][Y\mapsto
M^{\prime\prime}]}^{G}\subseteq M^{\prime\prime}\\}$
$\displaystyle=\bigcap\\{M^{\prime\prime}\subseteq
V\mid\alpha_{S_{1}^{M^{\prime\prime}}}(M)\subseteq M^{\prime\prime}\\}$
$\displaystyle\overset{(*)}{\subseteq}\bigcap\\{M^{\prime\prime}\subseteq
V\mid\alpha_{S_{1}^{M^{\prime\prime}}}(M^{\prime})\subseteq
M^{\prime\prime}\\}$ $\displaystyle=\bigcap\\{M^{\prime\prime}\subseteq
V\mid\llbracket\varphi_{1}\rrbracket_{\mathcal{V}[X\mapsto
M^{\prime}][Y\mapsto M^{\prime\prime}]}^{G}\subseteq M^{\prime\prime}\\}$
$\displaystyle=\alpha_{S}(M^{\prime})$

for $M\subseteq M^{\prime}$. In step $(*)$, the induction hypothesis implies
$\alpha_{S_{1}^{M^{\prime\prime}}}(M)\subseteq\alpha_{S_{1}^{M^{\prime\prime}}}(M^{\prime})$
for all $M^{\prime\prime}\subseteq V$, which then means that
$\\{M^{\prime\prime}\subseteq
V\mid\alpha_{S_{1}^{M^{\prime\prime}}}(M)\subseteq
M^{\prime\prime}\\}\supseteq\\{M^{\prime\prime}\subseteq
V\mid\alpha_{S_{1}^{M^{\prime\prime}}}(M^{\prime})\subseteq
M^{\prime\prime}\\}$ which in turn implies the inclusion $(*)$.

  * •

$\varphi=\nu Y.\varphi_{1}$: Analogous to the previous case. ∎

Using Proposition 4, a corollary from this lemma is:

###### Corollary 2

Let $S=(G,\mathcal{V},X,\varphi)$ where
$G=(V,l,(\rightarrow^{d})_{d\in\mathsf{Moves}},\curvearrowright)$ is an
execution graph, $\mathcal{V}$ is a fixpoint variable assignment, $X$ is a
fixpoint variable and $\varphi$ is a well-formed NTL formula in positive
normal form. Then, $\llbracket\mu X.\varphi\rrbracket_{\mathcal{V}}^{G}$ is
the least fixpoint of $\alpha_{S}$.

##  Appendix 0.C Properties of Successor Functions

We establish some properties of the successor functions defined on execution
graphs that are used in some of the proofs in this paper.

###### Lemma 4

Let $G=(V,l,(\rightarrow^{d})_{d\in\mathsf{Moves}},\curvearrowright)$ be an
execution graph.

  1. (i)

For all $y\in V$, there is $z\in V$ with $z\curvearrowright y$ iff $y$ has a
$\mathit{ret}$-predecessor $x$. In this case we have
$z=\mathit{succ}^{G}_{-}(x)$.

  2. (ii)

For all $x,y\in V$ with $y=\mathit{succ}^{G}_{a}(x)$, the caller of $x$ is
defined iff the caller of $y$ is defined and in this case
$\mathit{succ}^{G}_{-}(x)=\mathit{succ}^{G}_{-}(y)$.

  3. (iii)

For all $x,y\in V$ with $x\rightarrow^{\mathit{int}}y$,
$x\rightarrow^{\mathit{call}}y$ or $x\curvearrowright y$, the parent of $x$ is
defined iff the parent of $y$ is defined and in this case
$\mathit{succ}^{G}_{p}(x)=\mathit{succ}^{G}_{p}(y)$.

###### Proof

  1. (i)

Let $y\in V$ be a node.

For the first direction, assume that there is a node $z\in V$ with
$z\curvearrowright y$. Then there is a path from $z$ to $y$ following only
$\mathsf{Moves}\setminus\\{\mathit{spawn}\\}$-successors such that the number
$n$ of $\mathit{call}$-moves on that path is equal to the number of
$\mathit{ret}$-moves on that path. Since $y\neq z$ and $z$ has a
$\mathit{call}$-successor, we have $n>0$. Since $y$ is defined as the node
such that this path has minimal length, the predecessor of $y$ must be a
$\mathit{ret}$-predecessor.

For the other direction, assume that $y$ has a $\mathit{ret}$-predecessor $x$.
Since $(v_{0},y)\in(\bigcup\limits_{d\in\mathsf{Moves}}\rightarrow^{d})^{*}$,
there is a node $u\in V$ that is either $v_{0}$ or has a
$\mathit{spawn}$-predecessor such that there is a path $\pi$ from $u$ to $y$
following only $\mathsf{Moves}\setminus\\{\mathit{spawn}\\}$-successors. Since
$y$ is a $\mathit{ret}$-successor and the number of $\mathit{call}$-moves on
$\pi$ has to be greater or equal to the number of $\mathit{ret}$-moves on
$\pi$, we can consider the last node $z$ on $\pi$ with a
$\mathit{call}$-successor $z^{\prime}$ such that the number of
$\mathit{call}$-moves on the path $\pi$ between $z$ and $y$ is equal to the
number of $\mathit{ret}$-moves on $\pi$ between $z$ and $y$. Then we have
$z\curvearrowright y$.

It remains to show that $z=\mathit{succ}^{G}_{-}(x)$. Let $n$ be the number of
$\mathit{call}$-transitions on the path $\pi$ from the
$\mathit{call}$-successor $z^{\prime}$ of $z$ to $x$ following only
$\mathsf{Moves}\setminus\\{\mathit{spawn}\\}$-transitions. Since
$z\curvearrowright y$, $z^{\prime}$ is the $\mathit{call}$-successor of $z$
and $y$ is the $\mathit{ret}$-successor of $x$, this is also the number of
$\mathit{ret}$-transitions on $\pi$. We now show by induction on $n$ that we
can transform the path $\pi$ to a path $\pi^{\prime}$ from $z^{\prime}$ to $x$
following abstract successors. Since $z\rightarrow^{\mathit{call}}z^{\prime}$,
this implies in particular that $z=\mathit{succ}^{G}_{-}(x)$.

If $n=0$, the path $\pi$ follows only $\mathit{int}$-successors, i.e. it is
also a path following abstract successors.

If $n>0$, let $c$ and $c^{\prime}$ be the first nodes on the path $\pi$ with
$c\rightarrow^{\mathit{call}}c^{\prime}$. Since the number of
$\mathit{call}$-moves on $\pi$ is equal to the number of $\mathit{ret}$-moves
on $\pi$, there is a node $r\in V$ on the path $\pi$ between $c$ and $x$ with
$c\curvearrowright r$. Thus, $\pi$ can be written as
$\pi=\pi_{1}\pi_{2}\pi_{3}$ for paths $\pi_{1}$ from $z^{\prime}$ to $c$,
$\pi_{2}$ from $c$ to $r$ and $\pi_{3}$ from $r$ to $x$ following
$\mathsf{Moves}\setminus\\{\mathit{spawn}\\}$-transitions. By construction,
there are no $\mathit{call}$-moves on $\pi_{1}$. Moreover, there are no
$\mathit{ret}$-moves on $\pi_{1}$ since this would imply $z\curvearrowright v$
for a node $v\neq y$. Thus, $\pi_{1}$ is also a path following abstract
successors. Moreover, the number $m$ of $\mathit{call}$-moves on $\pi_{3}$ is
also equal to the number of $\mathit{ret}$-moves on $\pi_{3}$, since the same
holds true for $\pi$, $\pi_{1}$ and $\pi_{2}$. Since we clearly have $m<n$, we
can transform $\pi_{3}$ to a path $\pi_{a}$ from $r$ to $x$ following abstract
successors by the induction hypothesis. Since $r$ is the abstract successor of
$c$, the concatenation of the paths $\pi_{1}$ and $\pi_{a}$ is thus a path
from $z^{\prime}$ to $x$ following abstract successors.

  2. (ii)

$\mathit{succ}^{G}_{-}(x)$ is defined iff there is a node $z\in V$ with a
$\mathit{call}$-successor $z^{\prime}$ such that there is a path from
$z^{\prime}$ to $x$ following abstract successors. Since
$y=\mathit{succ}^{G}_{a}(x)$ and abstract successors are uniquely determined,
we can demand equivalently that there is a node $z\in V$ with a
$\mathit{call}$-successor $z^{\prime}$ such that there is a path from
$z^{\prime}$ to $y$ following abstract successors, i.e.
$\mathit{succ}^{G}_{-}(y)$ is defined and in this case
$\mathit{succ}^{G}_{-}(y)=z=\mathit{succ}^{G}_{-}(x)$.

  3. (iii)

$\mathit{succ}^{G}_{p}(x)$ is defined iff there is a node $z\in V$ with a
$\mathit{spawn}$-successor $z^{\prime}$ such that there is a path $\pi$ from
$z^{\prime}$ to $x$ following only
$\mathsf{Moves}\setminus\\{\mathit{spawn}\\}$-transitions. If
$x\curvearrowright y$, there is also a path $\pi^{\prime}$ from $x$ to $y$
following only $\mathsf{Moves}\setminus\\{\mathit{spawn}\\}$-transitions. This
also holds trivially if $x\rightarrow^{\mathit{int}}y$ or
$x\rightarrow^{\mathit{call}}y$. Thus, since
$\mathsf{Moves}\setminus\\{\mathit{spawn}\\}$-successors are uniquely
determined, we can demand equivalently that there is a node $z\in V$ with a
$\mathit{spawn}$-successor $z^{\prime}$ such that there is a path $\pi$ from
$z^{\prime}$ to $y$ following only
$\mathsf{Moves}\setminus\\{\mathit{spawn}\\}$-transitions, i.e.
$\mathit{succ}^{G}_{p}(y)$ is defined and in this case
$\mathit{succ}^{G}_{p}(y)=z=\mathit{succ}^{G}_{p}(x)$. ∎

##  Appendix 0.D Proofs from Section 6

######  Proof (Proof of Lemma 1)

Let $x\in V$ be an arbitrary node. Since $\delta_{G}(y)$ is defined for all
nodes $y\in V$, we only have to show that $\mathit{succ}_{f}^{G}(x)$ is
defined iff $\mathit{succ}_{f}^{\mathcal{T}}(\delta_{G}(x))$ is defined and
that
$\delta_{G}(\mathit{succ}_{f}^{G}(x))=\mathit{succ}_{f}^{\mathcal{T}}(\delta_{G}(x))$
holds in this case. In order to improve readability, we also write
$\mathit{succ}^{G}_{f}(x)=\mathit{succ}^{G}_{f}(y)$ for
$f\in\\{g,\uparrow,a,-,p,c\\}$ and $y\in V$, if both
$\mathit{succ}^{G}_{f}(x)$ and $\mathit{succ}^{G}_{f}(y)$ are undefined. We
show the claim for each successor type separately.

  * •

$\underline{f=a:}$ The claim is shown by a case distinction on $d(x)$.

If $d(x)\in\\{\mathit{int},\mathit{spawn}\\}$, then $x$ has an
$\mathit{int}$-successor $y$, i.e. $\mathit{succ}^{G}_{a}(x)=y$. Moreover, we
have $\delta_{G}(y)=\delta_{G}(x)\cdot 0$ and thus
$\mathit{succ}_{a}^{\mathcal{T}}(\delta_{G}(x))=\delta_{G}(x)\cdot
0=\delta_{G}(y)=\delta_{G}(\mathit{succ}^{G}_{a}(x))$.

If $d(x)=\mathit{callRet}$, there is $y\in V$ with $x\curvearrowright y$, i.e.
$\mathit{succ}^{G}_{a}(x)=y$. Moreover, we have
$\delta_{G}(y)=\delta_{G}(x)\cdot 1$ and thus
$\mathit{succ}_{a}^{\mathcal{T}}(\delta_{G}(x))=\delta_{G}(x)\cdot
1=\delta_{G}(y)=\delta_{G}(\mathit{succ}^{G}_{a}(x))$.

If $d(x)\in\\{\mathit{call},\mathit{ret},\mathit{end}\\}$, there is no $y\in
V$ with $x\curvearrowright y$ and $x$ has no $\mathit{int}$-successor, i.e.
$\mathit{succ}^{G}_{a}(x)$ is undefined. Moreover,
$\mathit{succ}_{a}^{\mathcal{T}}(\delta_{G}(x))$ is also undefined in this
case.

Thus, we have established
$\delta_{G}\circ\mathit{succ}^{G}_{a}(x)=\mathit{succ}_{a}^{\mathcal{T}}\circ\delta_{G}(x)$
in each of the cases.

  * •

$\underline{f=-:}$ Since $G$ is an execution graph, we have
$(v_{0},x)\in(\bigcup\limits_{d\in\mathsf{Moves}}\rightarrow^{d})^{*}$. Thus,
let $\pi$ be a path from $v_{0}$ to $x$ following $\mathsf{Moves}$-successors.
We show the claim by induction on the length $n$ of $\pi$.

If $n=0$, we have $x=v_{0}$. In this case $x$ has no predecessor and
$\mathit{succ}^{G}_{-}(x)$ is undefined. Moreover, we have $p(x)=\bot$ and
thus $\mathit{succ}_{-}^{\mathcal{T}}(\delta_{G}(x))$ is also undefined.

If $n>0$, let $y$ be the predecessor node of $x$ in $\pi$. We show the claim
by a case distinction based on what type of predecessor $y$ is.

If $y\rightarrow^{\mathit{call}}x$, we have $\mathit{succ}^{G}_{-}(x)=y$ and
$\delta_{G}(x)=\delta_{G}(y)\cdot 0$, i.e. $\delta_{G}(y)$ is the parent node
of $\delta_{G}(x)$. Moreover, we have $p(x)=\mathit{call}$ and hence
$\mathit{succ}_{-}^{\mathcal{T}}(\delta_{G}(x))=\delta_{G}(y)=\delta_{G}(\mathit{succ}^{G}_{-}(x))$.

If $y\rightarrow^{\mathit{int}}x$, then $x=\mathit{succ}^{G}_{a}(y)$. Thus, by
Lemma 4(ii), $\mathit{succ}^{G}_{-}(x)=\mathit{succ}^{G}_{-}(y)$. Moreover, we
have $\delta_{G}(x)=\delta_{G}(y)\cdot 0$, i.e. $\delta_{G}(y)$ is the parent
node of $\delta_{G}(x)$ and we have $p(x)=\mathit{int}$, i.e.
$\mathit{succ}_{-}^{\mathcal{T}}(\delta_{G}(x))=\mathit{succ}_{-}^{\mathcal{T}}(\delta_{G}(y))$.
By the induction hypothesis, we obtain
$\delta_{G}(\mathit{succ}^{G}_{-}(x))=\delta_{G}(\mathit{succ}^{G}_{-}(y))=\mathit{succ}_{-}^{\mathcal{T}}(\delta_{G}(y))=\mathit{succ}_{-}^{\mathcal{T}}(\delta_{G}(x))$.

If $y\rightarrow^{\mathit{ret}}x$, then by Lemma 4(i), there is $z\in V$ with
$z\curvearrowright x$. We then have $x=\mathit{succ}^{G}_{a}(z)$ and
$\delta_{G}(x)=\delta_{G}(z)\cdot 1$, i.e. $\delta_{G}(z)$ is the parent node
of $\delta_{G}(x)$. The claim follows as in the previous case.

If $y\rightarrow^{\mathit{spawn}}x$, then $\mathit{succ}^{G}_{-}(x)$ is
undefined since $x$ has no $\mathit{call}-$, $\mathit{int}$\- or
$\mathit{ret}$-predecessor, i.e. there is no $y\in V$ such that
$x=\mathit{succ}^{G}_{a}(y)$ or $x$ is a $\mathit{call}$-successor of $y$.
Moreover, we have $p(x)=\mathit{spawn}$ and thus
$\mathit{succ}_{-}^{\mathcal{T}}(\delta_{G}(x))$ is also undefined.

Thus, we have established
$\delta_{G}\circ\mathit{succ}^{G}_{-}(x)=\mathit{succ}_{-}^{\mathcal{T}}\circ\delta_{G}(x)$
in each of the cases.

  * •

$\underline{f=g:}$ The claim is shown by a case distinction on $d(x)$.

If $d(x)\in\\{\mathit{int},\mathit{call},\mathit{callRet},\mathit{spawn}\\}$,
then $x$ has an $\mathit{int}$\- or $\mathit{call}$-successor $y$, i.e.
$\mathit{succ}^{G}_{g}(x)=y$. Moreover, we have
$\delta_{G}(y)=\delta_{G}(x)\cdot 0$ and thus
$\mathit{succ}_{g}^{\mathcal{T}}(\delta_{G}(x))=\delta_{G}(x)\cdot
0=\delta_{G}(y)=\delta_{G}(\mathit{succ}^{G}_{g}(x))$.

If $d(x)=\mathit{ret}$, then $x$ has a $\mathit{ret}$-successor $y$, i.e.
$\mathit{succ}^{G}_{g}(x)=y$. By Lemma 4(i), there is a node $z\in V$ with
$z\curvearrowright y$ and $z=\mathit{succ}^{G}_{-}(x)$ and thus
$y=\mathit{succ}^{G}_{a}(z)=\mathit{succ}^{G}_{a}(\mathit{succ}^{G}_{-}(x))$.
Since we have already shown the claim for the abstract successor and the
caller, we conclude that
$\mathit{succ}_{g}^{\mathcal{T}}(\delta_{G}(x))=\mathit{succ}_{a}^{\mathcal{T}}(\mathit{succ}_{-}^{\mathcal{T}}(\delta_{G}(x)))=\mathit{succ}_{a}^{\mathcal{T}}(\delta_{G}(\mathit{succ}^{G}_{-}(x)))=\delta_{G}(\mathit{succ}^{G}_{a}(\mathit{succ}^{G}_{-}(x)))=\\\
\delta_{G}(y)=\delta_{G}(\mathit{succ}^{G}_{g}(x))$.

If $d(x)=\mathit{end}$, then $x$ has no successor, i.e.
$\mathit{succ}^{G}_{g}(x)$ is undefined. Moreover,
$\mathit{succ}_{g}^{\mathcal{T}}(\delta_{G}(x))$ is also undefined in this
case.

Thus, we have established
$\delta_{G}\circ\mathit{succ}^{G}_{g}(x)=\mathit{succ}_{g}^{\mathcal{T}}\circ\delta_{G}(x)$
in each of the cases.

  * •

$\underline{f=\ \uparrow:}$ We show the claim by a case distinction on $p(x)$.

If $p(x)\in\\{\mathit{int},\mathit{call}\\}$, then $x$ has a
$p(x)$-predecessor $y$, i.e. $\mathit{succ}^{G}_{\uparrow}(x)=y$. Moreover,
$\delta_{G}(y)$ is the parent node of $\delta_{G}(x)=\delta_{G}(y)\cdot 0$.
Thus, we have
$\delta_{G}(\mathit{succ}^{G}_{\uparrow}(x))=\delta_{G}(y)=\mathit{succ}_{\uparrow}^{\mathcal{T}}(\delta_{G}(x))$.

If $p(x)=\mathit{ret}$, then $x$ has a $\mathit{ret}$-predecessor $y$, i.e.
$\mathit{succ}^{G}_{\uparrow}(x)=y$, and by Lemma 4(i) there is a node $z\in
V$ with $z\curvearrowright x$ and $\mathit{succ}^{G}_{-}(y)=z$. Using the
claim for $f=-$, which we have already seen, we thus have
$\delta_{G}(z)=\delta_{G}(\mathit{succ}^{G}_{-}(y))=\mathit{succ}^{\mathcal{T}}_{-}(\delta_{G}(y))$.
By definition, the caller predecessor of $\delta_{G}(y)$ has to be a node with
a $\mathit{call}$-child $\delta_{G}(z^{\prime})$ such that
$\delta_{G}(z^{\prime})$ is an $\\{\mathit{int},\mathit{ret}\\}$-ancestor of
$\delta_{G}(y)$. Moreover, since $x$ is a $\mathit{ret}$-successor of $y$, we
have $d(y)=\mathit{ret}$ and hence $\delta_{G}(y)$ is a leaf. Thus,
$\delta_{G}(y)$ is the $\\{\mathit{int},\mathit{ret}\\}$-descendant leaf of
$\delta_{G}(z^{\prime})$, which is the left child of the parent node
$\delta_{G}(z)$ of $\delta_{G}(x)=\delta_{G}(z)\cdot 1$, i.e.
$\mathit{succ}^{\mathcal{T}}_{\uparrow}(\delta_{G}(x))=\delta_{G}(y)$. Hence,
$\delta_{G}(\mathit{succ}^{G}_{\uparrow}(x))=\delta_{G}(y)=\mathit{succ}_{\uparrow}^{\mathcal{T}}(\delta_{G}(x))$.

If $p(x)\in\\{\mathit{spawn},\bot\\}$, then $x$ has no $\mathit{int}$-,
$\mathit{call}$\- or $\mathit{ret}$-predecessor, i.e.
$\mathit{succ}^{G}_{\uparrow}(x)$ is undefined. Moreover,
$\mathit{succ}_{\uparrow}^{\mathcal{T}}(\delta_{G}(x))$ is also undefined in
this case.

Thus, we have established
$\delta_{G}\circ\mathit{succ}^{G}_{\uparrow}(x)=\mathit{succ}_{\uparrow}^{\mathcal{T}}\circ\delta_{G}(x)$
in each of the cases.

  * •

$\underline{f=p:}$ Since $G$ is an execution graph, we have
$(v_{0},x)\in(\bigcup\limits_{d\in\mathsf{Moves}}\rightarrow^{d})^{*}$. Thus,
let $\pi$ be a path from $v_{0}$ to $x$ following $\mathsf{Moves}$-successors.
We show the claim by induction via the length $n$ of $\pi$.

If $n=0$, we have $x=v_{0}$. In this case $x$ has no predecessor and
$\mathit{succ}^{G}_{p}(x)$ is undefined. Moreover, we have $p(x)=\bot$ and
thus $\mathit{succ}_{p}^{\mathcal{T}}(\delta_{G}(x))$ is also undefined.

If $n>0$, let $y$ be the predecessor node of $x$ in $\pi$. We show the claim
by a case distinction based on what type of predecessor $y$ is.

If $y\rightarrow^{\mathit{ret}}x$, by Lemma 4(i), there is $z\in V$ with
$z\curvearrowright x$. Hence, if $y\rightarrow^{\mathit{int}}x$,
$y\rightarrow^{\mathit{call}}x$ or $y\rightarrow^{\mathit{ret}}x$, there is a
node $z\in V$ with $z\rightarrow^{\mathit{int}}x$,
$z\rightarrow^{\mathit{call}}x$ or $z\curvearrowright x$. Thus, by Lemma
4(iii), $\mathit{succ}^{G}_{p}(x)=\mathit{succ}^{G}_{p}(z)$. Moreover,
$\delta_{G}(z)$ is the parent node of $\delta_{G}(x)$ and we have
$p(x)\in\\{\mathit{int},\mathit{call},\mathit{ret}\\}$, i.e.
$\mathit{succ}_{p}^{\mathcal{T}}(\delta_{G}(x))=\mathit{succ}_{p}^{\mathcal{T}}(\delta_{G}(z))$.
By the induction hypothesis, we obtain
$\delta_{G}(\mathit{succ}^{G}_{p}(x))=\delta_{G}(\mathit{succ}^{G}_{p}(z))=\mathit{succ}_{p}^{\mathcal{T}}(\delta_{G}(z))=\mathit{succ}_{p}^{\mathcal{T}}(\delta_{G}(x))$.

If $y\rightarrow^{\mathit{spawn}}x$, we have $\mathit{succ}^{G}_{p}(x)=y$ and
$\delta_{G}(x)=\delta_{G}(y)\cdot 1$, i.e. $\delta_{G}(y)$ is the parent node
of $\delta_{G}(x)$. Moreover, we have $p(x)=\mathit{spawn}$ and hence
$\mathit{succ}_{p}^{\mathcal{T}}(\delta_{G}(x))=\delta_{G}(y)=\delta_{G}(\mathit{succ}^{G}_{p}(x))$.

Thus, we have established
$\delta_{G}\circ\mathit{succ}^{G}_{p}(x)=\mathit{succ}_{p}^{\mathcal{T}}\circ\delta_{G}(x)$
in each of the cases.

  * •

$\underline{f=c:}$ We distinguish two cases for $d(x)$.

If $d(x)=\mathit{spawn}$, then $x$ has a $\mathit{spawn}$-successor $y$, i.e.
we have $\mathit{succ}^{G}_{c}(x)=y$. Moreover, we have
$\delta_{G}(y)=\delta_{G}(x)\cdot 1$ and thus
$\mathit{succ}_{c}^{\mathcal{T}}(\delta_{G}(x))=\delta_{G}(y)=\delta_{G}(\mathit{succ}^{G}_{c}(x))$.

If $d(x)\neq\mathit{spawn}$, then $x$ has no $\mathit{spawn}$-successor, i.e.
$\mathit{succ}^{G}_{c}(x)$ is undefined. Moreover, $\delta_{G}(x)$ is also
undefined in this case.

Thus, we have established
$\delta_{G}\circ\mathit{succ}^{G}_{c}(x)=\mathit{succ}_{c}^{\mathcal{T}}\circ\delta_{G}(x)$
in both cases. ∎

##  Appendix 0.E Proofs from Section 7

######  Proof (Proof of Theorem 7.1)

We first show that $\mathcal{A}_{\mathsf{ET}}$ accepts all execution trees.

For this, let
$G=(V,l,(\rightarrow^{d})_{d\in\mathsf{Moves}},\curvearrowright)$ be an
execution graph and $\mathcal{T}(G)=(T,r)$ be the tree representation of $G$.
We inductively define a map $r_{R}\colon V\to\\{0,1\\}$ as follows. First, we
set $r_{R}(v_{0}):=0$. Then, for each node $x\in V$,

  * •

if there is a node $y\in V$ such that $y$ is an $\mathit{int}$-predecessor of
$x$ or $y\curvearrowright x$ (the latter holds by Lemma 4(i) iff $x$ has a
$\mathit{ret}$-predecessor), we set $r_{R}(x):=r_{R}(y)$,

  * •

if $x$ (i) has a $\mathit{spawn}$-predecessor or (ii) it has a
$\mathit{call}$-predecessor $y$ and there is no node $z\in V$ with
$y\curvearrowright z$, we set $r_{R}(x):=0$ and

  * •

if $x$ has a $\mathit{call}$-predecessor $y$ and there is a node $z\in V$ with
$y\curvearrowright z$, we set $r_{R}(x):=1$.

Next, we define a map $r_{A}\colon T\to Q$ by
$r_{A}(\delta_{G}(x)):=(p(x),r_{R}(x))$ and show the following claim:

Claim: $r_{A}$ is an accepting $(\varepsilon,q_{0})$-run of
$\mathcal{A}_{\mathsf{ET}}$ over $\mathcal{T}(G)$.

We first show that $r_{A}$ is an $(\varepsilon,q_{0})$-run of
$\mathcal{A}_{\mathsf{ET}}$ over $\mathcal{T}(G)$. For the initial node, we
have $p(v_{0})=\bot$ and $r_{R}(v_{0})=0$ and thus
$r_{A}(\varepsilon)=r_{A}(\delta_{G}(v_{0}))=(\bot,0)=q_{0}$.

Let $t=\delta_{G}(x)\in T$ be an arbitrary node with $r(t)=(l(x),d(x),p(x))$
and $r_{A}(t)=(p(x),c)$. By a case distinction on $d(x)$, we show that the
children of $t$ satisfy the transition function in this node.

  * •

If $d(x)=\mathit{int}$, then $x$ has exactly one $\mathit{int}$-successor $y$
with $p(y)=\mathit{int}$, $r_{R}(y)=r_{R}(x)=c$ and $\delta_{G}(y)=t\cdot 0$.
Thus, $\\{(0,r_{A}(t\cdot 0))\\}=\\{(0,(\mathit{int},c))\\}$ satisfies
$\rho((p(x),c),r(t))$.

  * •

If $d(x)=\mathit{call}$, then $x$ has exactly one $\mathit{call}$-successor
$y$ with $p(y)=\mathit{call}$, there is no node $z\in V$ with
$x\curvearrowright z$, i.e. $r_{R}(x)=0$, and $\delta_{G}(y)=t\cdot 0$. Thus
$\\{(0,r_{A}(t\cdot 0))\\}=\\{(0,(\mathit{call},0))\\}$ satisfies
$\rho((p(x),c),r(t))$.

  * •

If $d(x)=\mathit{callRet}$, then $x$ has a $\mathit{call}$-successor $y$ with
$p(y)=\mathit{call}$, there is a node $z\in V$ with $x\curvearrowright z$ and
by Lemma 4(i), there is a node $z^{\prime}\in V$ with
$z^{\prime}\rightarrow^{\mathit{ret}}z$, i.e. $p(z)=\mathit{ret}$. Thus, we
have $r_{R}(y)=1$, $\delta_{G}(y)=t\cdot 0$, $r_{R}(z)=r_{R}(x)=c$, and
$\delta_{G}(z)=t\cdot 1$. Thus, $\\{(0,r_{A}(t\cdot 0)),(1,r_{A}(t\cdot
1))\\}=\\{(0,(\mathit{call},1)),(1,(\mathit{ret},c))\\}$ satisfies
$\rho((p(x),c),r(t))$.

  * •

If $d(x)=\mathit{spawn}$, then $x$ has an $\mathit{int}$-successor $y$ and a
$\mathit{spawn}$-successor $z$ with $p(y)=\mathit{int}$,
$r_{R}(y)=r_{R}(x)=c$, $\delta_{G}(y)=t\cdot 0$, $p(z)=\mathit{spawn}$,
$r_{R}(z)=0$, and $\delta_{G}(z)=t\cdot 1$. Thus, $\\{(0,r_{A}(t\cdot
0)),(1,r_{A}(t\cdot 1))\\}=\\{(0,(\mathit{int},c)),(1,(\mathit{spawn},0))\\}$
satisfies $\rho((p(x),c),r(t))$.

  * •

If $d(x)=\mathit{ret}$, then $x$ has a $\mathit{ret}$-successor $y$. By Lemma
4(i), there is a node $z\in V$ with $z\curvearrowright y$ and
$\mathit{succ}_{-}^{G}(x)=z$, i.e. there is a path from the
$\mathit{call}$-successor $z^{\prime}$ of $z$ to $x$ following abstract
successors. Then we clearly have $c=r_{R}(x)=r_{R}(z^{\prime})=1$ by
construction. Thus, $\emptyset$ satisfies $\mathit{true}=\rho((p(x),c),r(t))$.

  * •

If $d(x)=\mathit{end}$, then $x$ has no successors. Assume towards
contradiction that $r_{R}(x)=1$. Clearly, by construction, there is a node
$z\in V$ with $z\curvearrowright y$ and a path from the
$\mathit{call}$-successor $z^{\prime}$ of $z$ to $x$ following abstract
successors. Thus, $\delta_{G}(x)$ is the
$\\{\mathit{int},\mathit{ret}\\}$-descendant leaf of the left child
$\delta_{G}(z^{\prime})=\delta_{G}(z)\cdot 0$ of the parent node
$\delta_{G}(z)$ of $\delta_{G}(y)=\delta_{G}(z)\cdot 1$. Then we have
$\mathit{succ}_{\uparrow}^{\mathcal{T}(G)}(\delta_{G}(y))=\delta_{G}(x)$.
Using Lemma 1, we obtain
$\delta_{G}(\mathit{succ}_{\uparrow}^{G}(y))=\mathit{succ}_{\uparrow}^{\mathcal{T}(G)}(\delta_{G}(y))=\delta_{G}(x)$
and thus $\mathit{succ}^{G}_{\uparrow}(y)=x$ since $\delta_{G}$ is injective.
This means that $y$ is a successor of $x$, which contradicts our assumption
that $x$ has no successor. Thus, $c=r_{R}(x)=0$, and $\emptyset$ satisfies
$\mathit{true}=\rho((p(x),c),r(t))$.

Thus, $r_{A}$ is an $(\varepsilon,q_{0})$-run of $\mathcal{A}_{\mathsf{ET}}$
over $\mathcal{T}(G)$.

It remains to show that the run is accepting. Assume towards contradiction
that there is an infinite path $\delta_{G}(x_{0})\delta_{G}(x_{1})\dots$ in
$T$ where the priority $0$ occurs only finitely often, i.e. there is a minimal
$i>0$ such that for all $j\geq i$ we have $r_{R}(x_{j})=1$. By construction,
there must be a node $y\in V$ with $x_{i-1}\curvearrowright y$ such that
$x_{i-1}$ is the $\mathit{call}$-predecessor of $x_{i}$ and we have
$r_{R}(y)=r_{R}(x_{i-1})=0$. Thus, there is a finite path in $G$ from
$x_{i-1}$ to $y\neq x_{i-1}$ following only
$\mathsf{Moves}\setminus\\{\mathit{spawn}\\}$-successors such that the number
of $\mathit{call}$-moves on the path is equal to the number of
$\mathit{ret}$-moves on the path. On the other hand, the infinite path in the
tree $T$ up from $\delta_{G}(x_{i})$ cannot contain a $\mathit{spawn}$-child
by construction and thus provides an infinite path in $G$ starting in $x_{i}$
and following only $\mathit{call}$\- or abstract successors and thus also an
infinite path in $G$ starting in $x_{i-1}$ following only
$\mathsf{Moves}\setminus\\{\mathit{spawn}\\}$-successors. Since
$\mathsf{Moves}\setminus\\{\mathit{spawn}\\}$-successors are uniquely
determined, $y$ must be contained in this path. But since the paths between
nodes $z$ and $z^{\prime}$ with $z\curvearrowright z^{\prime}$ are the minimal
paths of length greater than zero from $z$ such that the number of
$\mathit{call}$-moves is equal to the number of $\mathit{ret}$-moves, the
number of $\mathit{call}$-moves on the infinite path up from $x_{i}$ so far is
always greater or equal to the number of $\mathit{ret}$-moves on this path so
far. Since $x_{i}$ is the $\mathit{call}$-successor of $x_{i-1}$, the number
of $\mathit{call}$-moves on the infinite path in $G$ from $x_{i-1}$ so far is
always greater than the number of $\mathit{ret}$-moves on this path so far
after the first move. This contradicts the fact that $y\neq x_{i-1}$ is
contained in this path. Thus, for all infinite paths in $T$, the priority $0$
occurs infinitely often, and the run is accepting.

We now show that all trees accepted by $\mathcal{A}_{\mathsf{ET}}$ are
execution trees. For this, let $\mathcal{T}_{A}=(T,r)$ be a tree accepted by
$\mathcal{A_{\mathsf{ET}}}$, witnessed by the accepting
$(\varepsilon,q_{0})$-run $r_{A}$ of $\mathcal{A}_{\mathsf{ET}}$ over
$\mathcal{T}_{A}$. We define an execution graph
$G=(V,l,(\rightarrow^{d})_{d\in\mathsf{Moves}},\curvearrowright)$ and show
that $\mathcal{T}_{A}$ is the tree representation of $G$.

The components of $G$ are defined as follows. First, we set $V:=T$ and
$l(t):=l_{t}$ where $r(t)=(l_{t},d_{t},p_{t})$. For the definition of the
transitions of $G$, let $t\in V$ be a node with $r_{A}(t)=q$ and
$r(t)=(l^{\prime},d,p)$. Outgoing transitions in $t$ are defined based on $d$.

  * •

If $d\in\\{\mathit{int},\mathit{call}\\}$, then $\mathit{ar}(r(t))=1$, i.e.
$t$ has a child $t\cdot 0$ and we include $t\rightarrow^{d}t\cdot 0$.

  * •

If $d\in\\{\mathit{callRet},\mathit{spawn}\\}$, then $\mathit{ar}(r(t))=2$,
i.e. $t$ has two children $t\cdot 0$ and $t\cdot 1$. For $d=\mathit{callRet}$,
we include $t\rightarrow^{\mathit{call}}t\cdot 0$ and $t\curvearrowright
t\cdot 1$. For $d=\mathit{spawn}$, we include
$t\rightarrow^{\mathit{int}}t\cdot 0$ and $t\rightarrow^{\mathit{spawn}}t\cdot
1$.

In order to define the transition relation $\rightarrow^{\mathit{ret}}$, we
show by induction on the length of $t$ that for all $t\in V$ with
$r_{A}(t)=(p,c)$:

$(*)$ $c=1$ iff there are $t_{1},t_{2},t_{3}\in V$ with
$t_{1}\rightarrow^{\mathit{call}}t_{2}$, $t_{1}\curvearrowright t_{3}$ and
there is a path from $t_{2}$ to $t$ following only $\mathit{int}$\- and
$\mathit{ret}$-children.

In the base case, where $t=\varepsilon$, we have $c=0$ and $t$ has no parent
node and no $\mathit{call}$-predecessor.

In the inductive step, let $t$ be of the form $t^{\prime}\cdot i$ for
$i\in\\{0,1\\}$ with $r_{A}(t^{\prime})=(p^{\prime},c^{\prime})$ and
$r(t^{\prime})=(l^{\prime},d,p^{\prime\prime})$. The claim is shown by a case
distinction on $d$.

  * •

If $d=\mathit{int}$, we have $i=0$ and
$\rho(r_{A}(t^{\prime}),r(t^{\prime}))=(0,(\mathit{int},c^{\prime}))$, i.e.
$c=c^{\prime}$. Since $t=t^{\prime}\cdot 0$ is the $\mathit{int}$-child of
$t^{\prime}$ and $\mathit{int}$\- or $\mathit{ret}$-children are uniquely
determined, the required nodes and the path exist for $t$ iff they exist for
$t^{\prime}$, and the latter holds by induction hypothesis iff
$c=c^{\prime}=1$.

  * •

If $d=\mathit{call}$, we have $i=0$ and
$\rho(r_{A}(t^{\prime}),r(t^{\prime}))=(0,(\mathit{call},0))$, i.e. $c=0$.
Since $t$ is no $\mathit{int}$\- or $\mathit{ret}$-child and there is no node
$\tilde{t}\in V$ with $t^{\prime}\curvearrowright\tilde{t}$, the required
nodes and the path do not exist for $t^{\prime}\cdot 0=t$.

  * •

If $d=\mathit{callRet}$, we have
$\rho(r_{A}(t^{\prime}),r(t^{\prime}))=(0,(\mathit{call},1))\land(1,(\mathit{ret},c^{\prime}))$.
If $i=0$, then $c=1$. Since
$t^{\prime}\rightarrow^{\mathit{call}}t^{\prime}\cdot 0$ and
$t^{\prime}\curvearrowright t^{\prime}\cdot 1$, the nodes $t_{1}=t^{\prime}$,
$t_{2}=t^{\prime}\cdot 0$ and $t_{3}=t^{\prime}\cdot 1$ and the empty path
from $t_{2}=t^{\prime}\cdot 0=t$ to $t$ witness that $(*)$ holds. If $i=1$,
then $c=c^{\prime}$ and $t^{\prime}\curvearrowright t$. Since $\mathit{int}$\-
or $\mathit{ret}$-children are uniquely determined, the required nodes and the
path exist for $t$ iff they exist for $t^{\prime}$, and the latter holds by
induction hypothesis iff $c=1$.

  * •

If $d=\mathit{spawn}$, we have
$\rho(r_{A}(t^{\prime}),r(t^{\prime}))=(0,(\mathit{int},c^{\prime}))\land(1,(\mathit{spawn},0))$.
If $i=0$, then $c=c^{\prime}$. Since
$t^{\prime}\rightarrow^{\mathit{int}}t^{\prime}\cdot 0=t$ and $\mathit{int}$\-
or $\mathit{ret}$-children are uniquely determined, the required nodes and the
path exist for $t$ iff they exist for $t^{\prime}$, and the latter holds by
induction hypothesis iff $c=c^{\prime}=1$. If $i=1$, then $c=0$. Since $t$ is
no $\mathit{int}$\- or $\mathit{ret}$-child and it has no
$\mathit{call}$-predecessor, the required nodes and the path do not exist for
$t^{\prime}\cdot 1=t$.

Given $(*)$, for each node $t\in V$ with $r_{A}(t)=(p,1)$ and
$r(t)=(l^{\prime},\mathit{ret},p^{\prime})$, there are nodes
$t_{1},t_{2},t_{3}\in V$ with $t_{1}\rightarrow^{\mathit{call}}t_{2}$,
$t_{1}\curvearrowright t_{3}$ and there is a path from $t_{2}$ to $t$
following only $\mathit{int}$\- and $\mathit{ret}$-children. We then include
the transition $t\rightarrow^{\mathit{ret}}t_{3}$.

We now show that $G$ is indeed an execution graph. For this, we separately
check each of the conditions from the definition of execution graphs.

  1. 1.

Clearly, the node $\varepsilon$ has no predecessor with respect to
$(\rightarrow^{d})_{d\in\mathsf{Moves}}$. Moreover, every node
$t\neq\varepsilon$ has exactly one predecessor with respect to
$(\rightarrow^{d})_{d\in\mathsf{Moves}\setminus\\{\mathit{ret}\\}}$ and
$\curvearrowright$. Additionally, $t$ can only have a
$\mathit{ret}$-predecessor, if $t$ has a predecessor with respect to
$\curvearrowright$. Now let $t^{\prime}\in V$ be a node with
$t^{\prime}\curvearrowright t$. We show that $t$ has a unique
$\mathit{ret}$-predecessor in this case. We know that $t^{\prime}$ has a
$\mathit{call}$-successor $t^{\prime}\cdot 0\in V$. Now consider the unique
maximal path in $T$ from $t^{\prime}\cdot 0$ following only $\mathit{int}$\-
and $\mathit{ret}$-chlidren. By $(*)$, we have $r_{A}(x)=(p,1)$ for some
$p\in\mathsf{Moves}\cup\\{\bot\\}$ for all nodes $x$ on the path. Since
$\Omega(q)=1$ for all states $q$ visited on the path and the run $r_{A}$ is
accepting, the path cannot be infinite. Thus, there is a node $x$ in the path
that has no $\mathit{int}$\- or $\mathit{ret}$-child. Assume towards
contradiction that $x$ has a $\mathit{call}$-child $y$. For $r_{A}(x)=(p,c)$
and $r(x)=(l^{\prime},d,p^{\prime})$, we must have $d=\mathit{call}$ in this
case. Since $y=x\cdot 0$ has to satisfy
$\rho((p,c),(l^{\prime},\mathit{call},p^{\prime}))$, we thus have $c=0$ which
contradicts our assumption that $x$ is on the given path. Therefore, $x$ also
has no $\mathit{call}$-child, i.e. we have
$d\in\\{\mathit{ret},\mathit{end}\\}$. Since
$\rho(r_{A}(x),r(x))=\rho((p,1),(l^{\prime},d,p))$ must be satisfied by the
children of $x$, we then have $d=\mathit{ret}$, since otherwise we had
$\rho(r_{A}(x),r(x))=\mathit{false}$. Thus, $x\rightarrow^{\mathit{ret}}t$
holds by construction. Clearly, since $\mathit{int}$\- or
$\mathit{ret}$-children are uniquely determined, we can only have
$y\rightarrow^{\mathit{ret}}t$ for a node $y\in T$, if $y$ is on the given
path and it is a leaf, i.e. if $y=x$.

  2. 2.

By construction of $V$, there is a path $\pi$ from $\varepsilon$ to $x$
following only $\mathsf{Moves}\setminus\\{\mathit{ret}\\}$-transitions or
nesting edges for all nodes $x\in V$. Consider the first nodes $y,z$ on the
path $\pi$ with $y\curvearrowright z$, if they exist. As shown in (i), there
is a path $\pi^{\prime}$ from the $\mathit{call}$-successor $y^{\prime}$ of
$y$ to the $\mathit{ret}$-predecessor $z^{\prime}$ of $z$ following only
$\mathit{int}$\- and $\mathit{ret}$-children, i.e. $\mathit{int}$-transitions
and nesting edges. Now include the concatenation of the paths
$y\rightarrow^{\mathit{call}}y^{\prime}$, $\pi^{\prime}$ and
$z^{\prime}\rightarrow^{\mathit{ret}}z$ in the initial path $\pi$ between the
nodes $y$ and $z$ and repeat this construction. If this provided an infinite
procedure, we would obtain an infinite path from $y^{\prime}$ following only
$\mathit{call}$\- or $\mathit{int}$-successors. However, since
$y\curvearrowright z$, all states visited on the path are of the form $(p,1)$,
which contradicts the fact that the run $r_{A}$ is accepting. Thus, the given
procedure terminates and we finally obtain a path from $\varepsilon$ to $x$
following only $\mathsf{Moves}$-transitions.

  3. 3.

By construction, each node clearly either has (a) exactly one
$\mathit{int}$-successor and at most one $\mathit{spawn}$-successor, (b) one
$\mathit{call}$-successor, (c) one $\mathit{ret}$-successor or (d) no
successors.

  4. 4.

Let $x\in V$ be a node. In the construction of the path from $\varepsilon$ to
$x$ following only $\mathsf{Moves}$-transitions in (ii), we never add a
$\mathit{spawn}$-transition on the path between nodes $y$ and $z$ with
$y\curvearrowright z$. Moreover, for each new nesting edge we add one
$\mathit{call}$-transition and one $\mathit{ret}$-transition afterwards on the
path. Thus, on the path from $\varepsilon$ or a node with a
$\mathit{spawn}$-predecessor to $x$, the number of $\mathit{call}$-moves is
greater or equal to the number of $\mathit{ret}$-moves, since we start without
any $\mathit{ret}$-moves in this construction.

  5. 5.

Let $x\in V$ be a node with a $\mathit{call}$-successor. For the first
direction, let $y\in V$ be a node with $x\curvearrowright y$. By the
construction given in (ii), we obtain a path from $x$ to $y$ following only
$\mathsf{Moves}\setminus\\{\mathit{spawn}\\}$-transitions from $x$ to $y$ such
that the number of $\mathit{call}$-moves on the path is equal to the number of
$\mathit{ret}$-moves on the path. Moreover, for all nodes $z$ between $x$ and
$y$, the number of $\mathit{call}$-moves on the path between $x$ and $z$ is
greater than the number of $\mathit{ret}$-moves on this path, i.e. $y$ is
given as the node with the stated property such that the witnessing path has
minimal length.

For the other direction, let $y\in V$ with $y\neq x$ be a node such that there
is a path from $x$ to $y$ following only