1842 LABEL:LastPageJun. 20, 2021Oct. 21, 2022

An abridged version of this paper appeared in TACAS 2021; missing proofs have
been added to create this version.

# General Decidability Results
for Asynchronous Shared-Memory Programs:
Higher-Order and Beyond

Rupak Majumdar  Max Planck Institute for Software Systems (MPI-SWS), Paul-
Ehrlich-Straße, Building G26, Kaiserslautern, Germany 67663.
<EMAIL_ADDRESS>,  Ramanathan S. Thinniyam  and  Georg
Zetzsche

###### Abstract.

The model of asynchronous programming arises in many contexts, from low-level
systems software to high-level web programming. We take a language-theoretic
perspective and show general decidability and undecidability results for
asynchronous programs that capture all known results as well as show
decidability of new and important classes. As a main consequence, we show
decidability of safety, termination and boundedness verification for _higher-
order_ asynchronous programs—such as OCaml programs using Lwt—and
undecidability of liveness verification already for order-2 asynchronous
programs. We show that under mild assumptions, surprisingly, safety and
termination verification of asynchronous programs with handlers from a
language class are decidable _iff_ emptiness is decidable for the underlying
language class. Moreover, we show that configuration reachability and liveness
(fair termination) verification are equivalent, and decidability of these
problems implies decidability of the well-known “equal-letters” problem on
languages. Our results close the decidability frontier for asynchronous
programs.

###### Key words and phrases:

Higher-order asynchronous programs, Higher-order recursion schemes and
Decidability

##  1\. Introduction

_Asynchronous programming_ is a common way to manage concurrent requests in a
system. In this style of programming, rather than waiting for a time-consuming
operation to complete, the programmer can make _asynchronous_ procedure calls
which are stored in a _task buffer_ pending later execution. Each asynchronous
procedure, or _handler_ , is a sequential program. When run, it can change the
_global shared state_ of the program, make internal synchronous procedure
calls, and post further instances of handlers to the task buffer. A scheduler
repeatedly and non-deterministically picks pending handler instances from the
task buffer and executes their code _atomically_ to completion. Asynchronous
programs appear in many domains, such as operating system kernel code, web
programming, or user applications on mobile platforms. This style of
programming is supported natively or through libraries for most programming
environments. The interleaving of different handlers hides latencies of long-
running operations: the program can process a different handler while waiting
for an external operation to finish. However, asynchronous scheduling of tasks
introduces non-determinism in the system, making it difficult to reason about
correctness.

An asynchronous program is _finite-data_ if all program variables range over
finite domains. Finite-data programs are still infinite state transition
systems: the task buffer can contain an unbounded number of pending instances
and the sequential machine implementing an individual handler can have
unboundedly large state (e.g., if the handler is given as a recursive program,
the stack can grow unboundedly). Nevertheless, verification problems for
finite-data programs have been shown to be decidable for several kinds of
handlers [SV06, JM07, CV07, GM12]. Several algorithmic approaches have been
studied, which tailor to (i) the kinds of permitted handler programs and (ii)
the properties that are checked.

#### State of the art

We briefly survey the existing approaches and what is known about the
decidability frontier. The _Parikh approach_ applies to (first-order)
recursive handler programs. Here, the decision problems for asynchronous
programs are reduced to decision problems over Petri nets [GM12]. The key
insight is that since handlers are executed atomically, the order in which a
handler posts tasks to the buffer is irrelevant. Therefore, instead of
considering the sequential order of posted tasks along an execution, one can
equivalently consider its Parikh image. Thus, when handlers are given as
pushdown systems, the behaviors of an asynchronous program can be represented
by a (polynomial sized) Petri net. Using the Parikh approach, safety
(formulated as reachability of a global state), termination (whether all
executions terminate), and boundedness (whether there is an a priori upper
bound on the task buffer) are all decidable for asynchronous programs with
recursive handlers, by reduction to corresponding problems on Petri nets
[SV06, GM12]. Configuration reachability (reachability of a specific global
state and task buffer configuration), fair termination (termination under a
fair scheduler), and fair non-starvation (every pending handler instance is
eventually executed) are also decidable, by separate ad hoc reductions to
Petri net reachability [GM12]. A “reverse reduction” shows that Petri nets can
be simulated by polynomial-sized asynchronous programs (already with finite-
data handlers).

In the _downclosure approach_ , one replaces each handler with a finite-data
program that is equivalent up to “losing” handlers in the task buffer. Of
course, this requires that one can compute equivalent finite-data programs for
a given class of handler programs. This has been applied to checking safety
for recursive handler programs [ABQ09]. Finally, a bespoke _rank-based
approach_ has been applied to checking safety when handlers can perform
restricted higher-order recursion [CV07].

#### Contribution

Instead of studying individual kinds of handler programs, we consider
asynchronous programs in a general language-theoretic framework. The class of
handler programs is given as a language class $\mathcal{C}$: An asynchronous
program over a language class $\mathcal{C}$ is one where each handler defines
a language from $\mathcal{C}$ over the alphabet of handler names, as well as a
transformer over the global state. This view leads to general results: we can
obtain simple characterizations of which classes of handler programs permit
decidability. For example, we do not need the technical assumptions of
computability of equivalent finite-data programs from the Parikh and the
downclosure approach.

Our first result shows that, under a mild language-theoretic assumption,
safety and termination are decidable if and only if the underlying language
class $\mathcal{C}$ has a decidable emptiness problem.111 The “mild language-
theoretic assumption” is that the class of languages forms an effective full
trio: it is closed under intersections with regular languages, homomorphisms,
and inverse homomorphisms. Many language classes studied in formal language
theory and verification satisfy these conditions.  Similarly, we show that
boundedness is decidable iff _finiteness_ is decidable for the language class
$\mathcal{C}$. These results are the best possible: decidability of emptiness
(resp., finiteness) is a requirement for safety and termination verification
already for verifying the safety or termination (resp., boundedness) of one
_sequential_ handler call. As corollaries, we get new decidability results for
all these problems for asynchronous programs over _higher-order recursion
schemes_ , which form the language-theoretic basis for programming in higher-
order functional languages such as OCaml [Kob09, Ong15], as well as other
language classes (lossy channel languages, Petri net languages, etc.).

Second, we show that configuration reachability, fair termination, and fair
starvation are mutually reducible; thus, decidability of any one of them
implies decidability of all of them. We also show decidability of these
problems implies the decidability of a well-known combinatorial problem on
languages: given a language over the alphabet ${\\{\mathtt{a},\mathtt{b}\\}}$,
decide if it contains a word with an equal number of $\mathtt{a}$s and
$\mathtt{b}$s. Viewed contrapositively, we conclude that all these decision
problems are undecidable already for asynchronous programs over order-2
pushdown languages, since the equal-letters problem is undecidable for this
class.

Together, our results “close” the decidability frontier for asynchronous
programs, by demonstrating reducibilities between decision problems heretofore
studied separately and connecting decision problems on asynchronous programs
with decision problems on the underlying language classes of their handlers.

While our algorithms do not assume that downclosures are effectively
computable, we use downclosures to prove their correctness. We show that the
safety, termination, and boundedness problems are invariant under taking
downclosures of runs; this corresponds to taking downclosures of the languages
of handlers.

The observation that safety, termination, and boundedness depend only on the
downclosure suggests a possible route to implementation. If there is an
effective procedure to compute the downclosure for class $\mathcal{C}$, then a
direct verification algorithm would replace all handlers by their (regular)
downclosures, and invoke existing decision procedures for this class. Thus, we
get a direct algorithm based on downclosure constructions for higher-order
recursion schemes, using the string of celebrated recent results on
effectively computing the downclosure of _word schemes_ [Zet15, HKO16,
CPSW16].

We find our general decidability result for asynchronous programs to be
surprising. Already for regular languages, the complexity of safety
verification jumps from ${\mathsf{NL}}$ (NFA emptiness) to
${\mathsf{EXPSPACE}}$ (Petri net coverability): asynchronous programs are far
more expressive than individual handler languages. It is therefore unexpected
that safety and termination remain decidable whenever they are decidable for
individual handler languages.

##  2\. Preliminaries

#### Basic Definitions

We assume familiarity with basic definitions of automata theory (see, e.g.,
[HMU07, Sip97]). If $w$ is a word over $\Sigma$ and $\Gamma\subseteq\Sigma$ is
a subalphabet, then the _projection of $w$ onto $\Gamma$_, denoted
$\mathrm{Proj}_{\Gamma}(w)$, is the word obtained by erasing from $w$ each
symbol that does not belong to $\Gamma$. For a language
$L\subseteq\Sigma^{*}$, define
$\mathrm{Proj}_{\Gamma}(L)={\\{\mathrm{Proj}_{\Gamma}(w)\mid w\in L\\}}$. The
subword order $\sqsubseteq$ on $\Sigma^{*}$ is defined as $w\sqsubseteq
w^{\prime}$ for $w,w^{\prime}\in\Sigma^{*}$ if $w$ can be obtained from
$w^{\prime}$ by deleting some letters from $w^{\prime}$. For example,
$abba\sqsubseteq bababa$ but $abba\not\sqsubseteq baaba$. The downclosure
$\mathord{\downarrow}{w}$ with respect to the subword order, of a word
$w\in\Sigma^{*}$, is defined as
$\mathord{\downarrow}{w}:=\\{w^{\prime}\in\Sigma^{*}\mid w^{\prime}\sqsubseteq
w\\}$. The downclosure $\mathord{\downarrow}{L}$ of a language
$L\subseteq\Sigma^{*}$ is given by
$\mathord{\downarrow}{L}:=\\{w^{\prime}\in\Sigma^{*}\mid\exists w\in L\colon
w^{\prime}\sqsubseteq w\\}$. Recall that the downclosure
$\mathord{\downarrow}{L}$ of any language $L$ is a regular language [Hai69].

A _multiset_ $\mathbf{m}\colon\Sigma\rightarrow{\mathbb{N}}$ over $\Sigma$
maps each symbol of $\Sigma$ to a natural number. Let ${\mathbb{M}[\Sigma]}$
be the set of all multisets over $\Sigma$. We treat sets as a special case of
multisets where each element is mapped onto $0$ or $1$. For example, we write
$\mathbf{m}={\llbracket\mathtt{a},\mathtt{a},\mathtt{c}\rrbracket}$ for the
multiset
$\mathbf{m}\in{\mathbb{M}[{\\{\mathtt{a},\mathtt{b},\mathtt{c},\mathtt{d}\\}}]}$
with $\mathbf{m}(\mathtt{a})=2$,
$\mathbf{m}(\mathtt{b})=\mathbf{m}(\mathtt{d})=0$, and
$\mathbf{m}(\mathtt{c})=1$. We also use the notation
$\lvert{\mathbf{m}}\rvert=\sum_{\sigma\in\Sigma}\mathbf{m}(\sigma)$. The
Parikh image ${\mathsf{Parikh}}(w)\in{\mathbb{M}[\Sigma]}$ of a word
$w\in\Sigma^{*}$ is the multiset such that ${\mathsf{Parikh}}(w)(\mathtt{a})$
is the number of times $\mathtt{a}$ occurs in $w$.

Given two multisets $\mathbf{m},\mathbf{m}^{\prime}\in{\mathbb{M}[\Sigma]}$ we
define the multiset
$\mathbf{m}\oplus\mathbf{m}^{\prime}\in{\mathbb{M}[\Sigma]}$ for which, for
all $\mathtt{a}\in\Sigma$, we have
$(\mathbf{m}\oplus\mathbf{m}^{\prime})(\mathtt{a})=\mathbf{m}(\mathtt{a})+\mathbf{m}^{\prime}(\mathtt{a})$.
We also define the natural order $\preceq$ on ${\mathbb{M}[\Sigma]}$ as
follows: $\mathbf{m}\preceq\mathbf{m}^{\prime}$ iff there exists
$\mathbf{m}^{\Delta}\in{\mathbb{M}[\Sigma]}$ such that
$\mathbf{m}\oplus\mathbf{m}^{\Delta}=\mathbf{m}^{\prime}$. We also define
$\mathbf{m}^{\prime}\ominus\mathbf{m}$ for
$\mathbf{m}\preceq\mathbf{m}^{\prime}$ analogously: for all
$\mathtt{a}\in\Sigma$, we have
$(\mathbf{m}\ominus\mathbf{m}^{\prime})(\mathtt{a})=\mathbf{m}(\mathtt{a})-\mathbf{m}^{\prime}(\mathtt{a})$.
For $\Gamma\subseteq\Sigma$ we regard $\mathbf{m}\in{\mathbb{M}[\Gamma]}$ as a
multiset of ${\mathbb{M}[\Sigma]}$ where undefined values are sent to $0$.

#### Language Classes and Full Trios

A _language class_ is a collection of languages, together with some finite
representation. Examples are the regular (e.g. represented by finite automata)
or the context-free languages (e.g. represented by pushdown automata
($\mathsf{PDA}$)). A relatively weak and reasonable assumption on a language
class is that it is a _full trio_ , that is, it is closed under each of the
following operations: taking intersection with a regular language, taking
homomorphic images, and taking inverse homomorphic images. Equivalently, a
language class is a full trio iff it is closed under rational transductions
[Ber79] as we explain below.

We assume that all full trios $\mathcal{C}$ considered in this paper are
effective: Given a language $L$ from $\mathcal{C}$, a regular language $R$,
and a homomorphism $h$, we can compute a representation of the languages
$L\cap R$, $h(L)$, and $h^{-1}(L)$ in $\mathcal{C}$.

Many classes of languages studied in formal language theory form effective
full trios. Examples include the regular and the context-free languages
[HMU07], the indexed languages [Aho68, DG86], the languages of higher-order
pushdown automata [Mas74], higher-order recursion schemes ($\mathsf{HORS}$)
[Dam82, HMOS08], Petri nets (both coverability and reachability languages)
[Gre78, Jan79], and lossy channel systems (see Section 4.1). (While
$\mathsf{HORS}$ are usually viewed as representing a tree or collection of
trees, one can also view them as representing a word language, as we explain
in Section 5.)

Informally, a language class defined by non-deterministic devices with a
finite-state control that allows $\varepsilon$-transitions and imposes no
restriction between input letter and performed configuration changes (such as
non-deterministic pushdown automata) is always a full trio: The three
operations above can be realized by simple modifications of the finite-state
control. The deterministic context-free languages are a class that is _not_ a
full trio.

An asynchronous transducer $\mathcal{T}$ is a tuple
$\mathcal{T}=(Q,\Gamma,\Sigma,E,q_{0},F)$ with a finite set of states $Q$,
finite output alphabet $\Gamma$, finite input alphabet $\Sigma$, a finite set
of edges $E\subseteq Q\times\Gamma^{*}\times\Sigma^{*}\times Q$, initial state
$q_{0}\in Q$ and set of final states $F\subseteq Q$. We write
$p\xrightarrow{v|u}q$ if $(p,v,u,q)\in E$ and the machine reads $u$ in state
$p$, outputs $v$ and moves to state $q$. We also write
$p\xrightarrow{w|w^{\prime}}q$ if there are states $q_{0},q_{1},\dots,q_{n}$
and words $u_{1},u_{2},\dots,u_{n},v_{1},v_{2},\dots,v_{n}$ such that
$p=q_{0}$, $q=q_{n}$, $w^{\prime}=u_{1}u_{2}\cdots u_{n}$, $w=v_{1}v_{2}\cdots
v_{n}$ and $q_{i-1}\xrightarrow{v_{i}|u_{i}}q_{i}$ for all $0\leq i\leq n$.

The transduction $T\subseteq\Gamma^{*}\times\Sigma^{*}$ generated by the
transducer $\mathcal{T}$ is the set of tuples
$(v,u)\in\Gamma^{*}\times\Sigma^{*}$ such that $q_{0}\xrightarrow{v|u}q_{f}$
for some $q_{f}\in F$. Given a language $L\subseteq\Sigma^{*}$, we define
$TL:=\\{v\in\Gamma^{*}\;|\;\exists u\in L\colon(v,u)\in T\\}$. A transduction
$T\subseteq\Gamma^{*}\times\Sigma^{*}$ is _rational_ if it is generated by
some asynchronous transducer.

A language class $\mathcal{C}$ is a full trio if and only if it is closed
under each of the following operations:

  * •

intersection with a regular language,

  * •

taking homomorphic images, and

  * •

taking inverse homomorphic images.

It is well known that these two concepts are equivalent:

######  Theorem 1 (Berstel [Ber79]).

A language class is closed under rational transductions if and only if it is a
full trio.

#### Asynchronous Programs: A Language-Theoretic View

We use a language-theoretic model for asynchronous shared-memory programs.

Let $\mathcal{C}$ be an (effective) full trio. An _asynchronous program_
($\mathsf{AP}$) over $\mathcal{C}$ is a tuple
$\mathfrak{P}=(D,\Sigma,(L_{c})_{c\in\mathfrak{C}},d_{0},\mathbf{m}_{0})$,
where $D$ is a finite set of _global states_ , $\Sigma$ is an alphabet of
_handler names_ , $(L_{c})_{c\in\mathfrak{C}}$ is a family of languages over
$\Sigma$ from $\mathcal{C}$, one for each $c\in\mathfrak{C}$ where
$\mathfrak{C}=D\times\Sigma\times D$ is the set of contexts, $d_{0}\in D$ is
the _initial state_ , and $\mathbf{m}_{0}\in{\mathbb{M}[\Sigma]}$ is a
multiset of _initial pending handler instances_.

A configuration $(d,\mathbf{m})\in D\times{\mathbb{M}[\Sigma]}$ of
$\mathfrak{P}$ consists of a global state $d$ and a multiset $\mathbf{m}$ of
pending handler instances. For a configuration $c$, we write $c.d$ and
$c.\mathbf{m}$ for the global state and the multiset in the configuration
respectively. The _initial_ configuration $c_{0}$ of $\mathfrak{P}$ is given
by $c_{0}.d=d_{0}$ and $c_{0}.\mathbf{m}=\mathbf{m}_{0}$. The semantics of
$\mathfrak{P}$ is a labeled transition system over the set of configurations,
with the transition relation
$\xrightarrow{\sigma}\subseteq(D\times{\mathbb{M}[\Sigma]})\times(D\times{\mathbb{M}[\Sigma]})$
given by

$\displaystyle(d,\mathbf{m}\oplus{\llbracket\sigma\rrbracket})\xrightarrow{\sigma}(d^{\prime},\mathbf{m}\oplus\mathbf{m}^{\prime})\quad\text{
if{}f }\quad\exists w\in L_{d\sigma
d^{\prime}}\colon{\mathsf{Parikh}}(w)=\mathbf{m}^{\prime}$

Moreover, we write $(d,\mathbf{m})\rightarrow(d^{\prime},\mathbf{m}^{\prime})$
if there exists a $\sigma\in\Sigma$ with
$(d,\mathbf{m})\xrightarrow{\sigma}(d^{\prime},\mathbf{m}^{\prime})$. We use
$\rightarrow^{*}$ to denote the reflexive transitive closure of the relation
$\rightarrow$. A configuration $c$ is said to be _reachable_ in $\mathfrak{P}$
if $(d_{0},\mathbf{m}_{0})\rightarrow^{*}c$.

Intuitively, the set $\Sigma$ of handler names specifies a finite set of
procedures that can be invoked asynchronously. The shared state takes values
in $D$. When a handler is called asynchronously, it gets added to a bag of
pending handler calls (the multiset $\mathbf{m}$ in a configuration). The
language $L_{d\sigma d^{\prime}}$ captures the effect of executing an instance
of $\sigma$ starting from the global state $d$, such that on termination, the
global state is $d^{\prime}$. Each word $w\in L_{d\sigma d^{\prime}}$ captures
a possible sequence of handlers posted during the execution.

Suppose the current configuration is $(d,\mathbf{m})$. A non-deterministic
scheduler picks one of the outstanding handlers $\sigma\in\mathbf{m}$ and
executes it. Executing $\sigma$ corresponds to picking one of the languages
$L_{d\sigma d^{\prime}}$ and some word $w\in L_{d\sigma d^{\prime}}$. Upon
execution of $\sigma$, the new configuration has global state $d^{\prime}$ and
the new bag of pending calls is obtained by taking $\mathbf{m}$, removing an
instance of $\sigma$ from it, and adding the Parikh image of $w$ to it. This
reflects the current set of pending handler calls—the old ones (minus an
instance of $\sigma$) together with the new ones added by executing $\sigma$.
Note that a handler is executed atomically; thus, we atomically update the
global state and the effect of executing the handler.

Let us see some examples of asynchronous programs. It is convenient to present
these examples in a programming language syntax, and to allow each handler to
have _internal actions_ that perform local tests and updates to the global
state. As we describe informally below, and formally in Appendix A, when
$\mathcal{C}$ is a full trio, internal actions can be “compiled away” by
taking an intersection with a regular language of internal actions and
projecting the internal actions away. Thus, we use our simpler model
throughout.

⬇

1global var turn = ref 0 and x = ref 0;

2let rec s1 () = if * then begin post a; s1(); post b end

3let rec s2 () = if * then begin post a; s2(); post b end else post b

4let a () = if !turn = 0 then begin turn := 1; x := !x + 1 end else post a

5let b () = if !turn = 1 then begin turn := 0; x := !x - 1 end else post b

6

7let s3 () = post s3; post s3

8

9global var t = ref 0;

10let c () = if !t = 0 then t := 1 else post c

11let d () = if !t = 1 then t := 2 else post d

12let f () = if !t = 2 then t := 0 else post f

13

14let cc x = post c; x

15let dd x = post d; x

16let ff x = post f; x

17let id x = x

18let h g y = cc (g (dd y))

19let rec produce g x = if * then produce (h g) (ff x) else g x

20let s4 () = produce id ()

Figure 1. Examples of asynchronous programs

#### Examples

Figure 1 shows some simple examples of asynchronous programs in an OCaml-like
syntax. Consider first the asynchronous program in lines 1–5. The alphabet of
handlers is s1, s2, a, and b. The global states correspond to possible
valuations to the global variables turn and x; assuming turn is a Boolean and
x takes values in $\mathbb{N}$, we have that
$D={\\{0,1\\}}\times{\\{0,1,\omega\\}}$, where $\omega$ abstracts all values
other than ${\\{0,1\\}}$. Since $\mathtt{s1}$ and s2 do not touch any
variables, for $d,d^{\prime}\in D$, we have
$L_{d,\mathtt{s1},d}={\\{\mathtt{a}^{n}\mathtt{b}^{n}\mid n\geq 0\\}}$,
$L_{d,\mathtt{s2},d}={\\{\mathtt{a}^{n}\mathtt{b}^{n+1}\mid n\geq 0\\}}$, and
$L_{d,\mathtt{s1},d^{\prime}}=L_{d,\mathtt{s2},d^{\prime}}=\emptyset$ if
$d^{\prime}\neq d$.

For the languages corresponding to a and b, we use syntactic sugar in the form
of _internal actions_ ; these are local tests and updates to the global state.
In our example, we have $L_{(0,0),\mathtt{a},(1,1)}={\\{\varepsilon\\}}$,
$L_{(1,x),\mathtt{a},(1,x)}={\\{\mathtt{a}\\}}$ for all values of $x$, and
similarly for b. The meaning is that, starting from a global state $(0,0)$,
executing the handler will lead to the global state $(1,1)$ and no handlers
will be posted, whereas starting from a global state in which turn is $1$,
executing the handler will keep the global state unchanged but post an
instance of a. Note that all the languages are context-free.

Consider an execution of the program from the initial configuration
$((0,0),{\llbracket\mathtt{s1}\rrbracket})$. The execution of s1 puts $n$ as
and $n$ bs into the bag, for some $n\geq 0$. The global variable turn is used
to ensure that the handlers a and b alternately update x. When turn is $0$,
the handler for a increments x and sets turn to $1$, otherwise it re-posts
itself for a future execution. Likewise, when turn is $1$, the handler for b
decrements x and sets turn back to $0$, otherwise it re-posts itself for a
future execution. As a result, the variable x never grows beyond $1$. Thus,
the program satisfies the _safety_ property that no execution sets x to
$\omega$.

It is possible that the execution goes on forever: for example, if s1 posts an
a and a b, and thereafter only b is chosen by the scheduler. This is not an
“interesting” infinite execution as it is not fair to the pending a. In the
case of a fair scheduler, which eventually always picks an instance of every
pending task, the program terminates: eventually all the as and bs are
consumed when they are scheduled in alternation. However, if instead we
started with ${\llbracket\mathtt{s2}\rrbracket}$, the program will not
terminate even under a fair scheduler: the last remaining b will not be paired
and will keep executing and re-posting itself forever.

Now consider the execution of s3. It has an infinite fair run, where the
scheduler picks an instance of s3 at each step. However, the number of pending
instances grows without bound. We shall study the _boundedness problem_ ,
which checks if the bag can become unbounded along some run. We also study a
stronger notion of fair termination, called _fair non-starvation_ , which asks
that every _instance_ of a posted handler is executed under any fair
scheduler. The execution of s3 is indeed fair, but there can be a specific
instance of s3 that is never picked: we say s3 can _starve_ an instance.

The program in lines 9–20 is _higher-order_ ($\mathtt{produce}$ and
$\mathtt{h}$ take functions as arguments). The language of $\mathtt{s4}$ is
the set ${\\{\mathtt{c}^{n}\mathtt{d}^{n}\mathtt{f}^{n}\mid n\geq 0\\}}$, that
is, it posts an equal number of $\mathtt{c}$s, $\mathtt{d}$s, and
$\mathtt{f}$s. It is an indexed language; we shall see (Section 5) how this
and other higher-order programs can be represented using higher-order
recursion schemes ($\mathsf{HORS}$). Note that the OCaml types of
$\mathtt{produce}:(\mathtt{o}\rightarrow\mathtt{o})\rightarrow\mathtt{o}\rightarrow\mathtt{o}$
and
$\mathtt{h}:(\mathtt{o}\rightarrow\mathtt{o})\rightarrow\mathtt{o}\rightarrow\mathtt{o}$
are higher-order.

The program is similar to the first: the handlers c, d, and f execute in
“round robin” fashion using the global state t to find their turns. Again, we
use internal actions to update the global state for readability. We ask the
same decision questions as before: does the program ever reach a specific
global state and does the program have an infinite (fair) run? We shall see
later that safety and termination questions remain decidable, whereas fair
termination does not.

##  3\. Decision Problems on Asynchronous Programs

We now describe decision problems on runs of asynchronous programs.

#### Runs, preruns, and downclosures

A prerun of an $\mathsf{AP}$
$\mathfrak{P}=(D,\Sigma,(L_{c})_{c\in\mathfrak{C}},d_{0},\mathbf{m}_{0})$ is a
finite or infinite sequence
$\rho=(e_{0},\mathbf{n}_{0}),\sigma_{1},(e_{1},\mathbf{n}_{1}),\sigma_{2},\ldots$
of alternating elements of tuples $(e_{i},\mathbf{n}_{i})\in
D\times{\mathbb{M}[\Sigma]}$ and symbols $\sigma_{i}\in\Sigma$. The set of
preruns of $\mathfrak{P}$ will be denoted $\mathsf{Preruns}(\mathfrak{P})$.
Note that if two asynchronous programs $\mathfrak{P}$ and
$\mathfrak{P}^{\prime}$ have the same $D$ and $\Sigma$, then
$\mathsf{Preruns}(\mathfrak{P})=\mathsf{Preruns}(\mathfrak{P}^{\prime})$. The
_length_ , denoted $|\rho|$, of a finite prerun $\rho$ is the number of
configurations in $\rho$. The $i^{th}$ configuration of a prerun $\rho$ will
be denoted $\rho(i)$.

We define an order $\trianglelefteq$ on preruns as follows: For preruns
$\rho=(e_{0},\mathbf{n}_{0}),\sigma_{1},(e_{1},\mathbf{n}_{1}),\sigma_{2},\ldots$
and
$\rho^{\prime}=(e_{0}^{\prime},\mathbf{n}_{0}^{\prime}),\sigma_{1}^{\prime},(e_{1}^{\prime},\mathbf{n}_{1}^{\prime}),\sigma_{2}^{\prime},\ldots$,
we define $\rho\trianglelefteq\rho^{\prime}$ if $|\rho|=|\rho^{\prime}|$ and
$e_{i}=e_{i}^{\prime},\sigma_{i}=\sigma_{i}^{\prime}$ and
$\mathbf{n}_{i}\preceq\mathbf{n}_{i}^{\prime}$ for each $i\geq 0$. The
_downclosure_ $\mathord{\downarrow}{R}$ of a set $R$ of preruns of
$\mathfrak{P}$ is defined as
$\mathord{\downarrow}{R}=\\{\rho\in\mathsf{Preruns}(\mathfrak{P})\mid\exists\rho^{\prime}\in
R.\;\rho\trianglelefteq\rho^{\prime}\\}$.

A run of an $\mathsf{AP}$
$\mathfrak{P}=(D,\Sigma,(L_{c})_{c\in\mathfrak{C}},d_{0},\mathbf{m}_{0})$ is a
prerun
$\rho=(d_{0},\mathbf{m}_{0}),\sigma_{1},(d_{1},\mathbf{m}_{1}),\sigma_{2},\ldots$
starting with the initial configuration $(d_{0},\mathbf{m}_{0})$, where for
each $i\geq 0$, we have
$(d_{i},\mathbf{m}_{i})\xrightarrow{\sigma_{i+1}}(d_{i+1},\mathbf{m}_{i+1})$.
The set of runs of $\mathfrak{P}$ is denoted $\mathsf{Runs}(\mathfrak{P})$.
Finally, $\mathord{\downarrow}{\mathsf{Runs}(\mathfrak{P})}$ is the downward
closure of $\mathsf{Runs}(\mathfrak{P})$ with respect to $\trianglelefteq$.

An infinite run
$c_{0}\xrightarrow{\sigma_{0}}c_{1}\xrightarrow{\sigma_{1}}\ldots$ is called
_fair_ if for all $i\geq 0$, if $\sigma\in c_{i}.\mathbf{m}$ then there is
some $j\geq i$ such that $c_{j}\xrightarrow{\sigma}c_{j+1}$. That is, whenever
an instance of a handler $\sigma$ is posted, some instance of $\sigma$ is
executed later. Fairness does not guarantee that every specific instance of a
handler is executed eventually. We say that an infinite fair run _starves_ a
handler $\sigma$ if there exists an index $J\geq 0$ such that for each $j\geq
J$, we have (i) $c_{j}.\mathbf{m}(\sigma)\geq 1$ and (ii) whenever
$c_{j}\xrightarrow{\sigma}c_{j+1}$, we have $c_{j}.\mathbf{m}(\sigma)\geq 2$.
In this case, even if the run is fair, a specific instance of $\sigma$ may
never be executed.

Now we give the definitions of the various decision problems.

[Properties of finite runs] The Safety (Global state reachability) problem
asks, given an asynchronous program $\mathfrak{P}$ and a global state
$d_{f}\in D$, is there a reachable configuration $c$ such that $c.d=d_{f}$? If
so, $d_{f}$ is said to be _reachable_ (in $\mathfrak{P}$) and _unreachable_
otherwise. The Boundedness (of the task buffer) problem asks, given an
asynchronous program $\mathfrak{P}$, is there an $N\in\mathbb{N}$ such that
for every reachable configuration $c$, we have $\lvert{c.\mathbf{m}}\rvert\leq
N$? If so, the asynchronous program $\mathfrak{P}$ is _bounded_ ; otherwise it
is _unbounded_. The Configuration reachability problem asks, given an
asynchronous program $\mathfrak{P}$ and a configuration $c$, is $c$ reachable?

[Properties of infinite runs] All the following problems take as input an
asynchronous program $\mathfrak{P}$. The Termination problem asks if all runs
of $\mathfrak{P}$ are finite. The Fair Non-termination problem asks if
$\mathfrak{P}$ has some fair infinite run. The Fair Starvation problem asks if
$\mathfrak{P}$ has some fair run that starves some handler.

Our main result in this section shows that many properties of an asynchronous
program $\mathfrak{P}$ only depend on the downclosure
$\mathord{\downarrow}{\mathsf{Runs}(\mathfrak{P})}$ of the set
$\mathsf{Runs}(\mathfrak{P})$ of runs of the program $\mathfrak{P}$. The proof
is by induction on the length of runs. Please see Appendix B for details. For
any $\mathsf{AP}$
$\mathfrak{P}=(D,\Sigma,(L_{c})_{c\in\mathfrak{C}},d_{0},\mathbf{m}_{0})$, we
define the $\mathsf{AP}$
$\mathord{\downarrow}{\mathfrak{P}}=(D,\Sigma,(\mathord{\downarrow}{L_{c}})_{c\in\mathfrak{C}},d_{0},\mathbf{m}_{0})$,
where $\mathord{\downarrow}{L_{c}}$ is the downclosure of the language $L_{c}$
under the subword order.

######  Proposition 2.

Let $\mathfrak{P}=(D,\Sigma,(L_{c})_{c\in\mathfrak{C}},d_{0},\mathbf{m}_{0})$
be an asynchronous program. Then
$\mathord{\downarrow}{\mathsf{Runs}(\mathord{\downarrow}{\mathfrak{P}})}=\mathord{\downarrow}{\mathsf{Runs}(\mathfrak{P})}$.
In particular, the following holds. (1) For every $d\in D$, $\mathfrak{P}$ can
reach $d$ if and only if $\mathord{\downarrow}{\mathfrak{P}}$ can reach $d$.
(2) $\mathfrak{P}$ is terminating if and only if
$\mathord{\downarrow}{\mathfrak{P}}$ is terminating. (3) $\mathfrak{P}$ is
bounded if and only if $\mathord{\downarrow}{\mathfrak{P}}$ is bounded.

Intuitively, safety, termination, and boundedness is preserved when the
multiset of pending handler instances is “lossy”: posted handlers can get
lost. This corresponds to these handlers never being added to the task buffer.
However, if a run demonstrates reachability of a global state, or non-
termination, or unboundedness, in the lossy version, it corresponds also to a
run in the original problem (and conversely).

In contrast, simple examples show that configuration reachability, fair
termination, and fair non-starvation properties are not preserved under
downclosures.

##  4\. General Decidability Results

In this section, we characterize those full trios $\mathcal{C}$ for which
particular problems for asynchronous programs over $\mathcal{C}$ are
decidable. Our decision procedures will use the following theorem, summarizing
the results from [GM12], as a subprocedure.

[[GM12]] Safety, boundedness, configuration reachability, termination, fair
non-termination, and fair non-starvation are decidable for asynchronous
programs over regular languages.

###  4.1. Safety and termination

Our first main result concerns the problems of safety and termination.

######  Theorem 3.

Let $\mathcal{C}$ be a full trio. The following are equivalent:

  1. (1)

Safety is decidable for asynchronous programs over $\mathcal{C}$.

  2. (2)

Termination is decidable for asynchronous programs over $\mathcal{C}$.

  3. (3)

Emptiness is decidable for $\mathcal{C}$.

######  Proof 4.1.

We begin with “1$\Rightarrow$3”. Let $K\subseteq\Sigma^{*}$ be given. We
construct

$\mathfrak{P}=(D,\Sigma,(L_{c})_{c\in\mathfrak{C}},d_{0},\mathbf{m}_{0})$

such that $\mathbf{m}_{0}={\llbracket\sigma\rrbracket}$,
$D=\\{d_{0},d_{1}\\}$, $L_{d_{0},\sigma,d_{1}}=K$ and $L_{c}=\emptyset$ for
$c\neq(d_{0},\sigma,d_{1})$. We see that $\mathfrak{P}$ can reach $d_{1}$ iff
$K$ is non-empty. Next we show “2$\Rightarrow$3”. Consider the alphabet
$\Gamma=(\Sigma\cup\\{\varepsilon\\})\times\\{0,1\\}$ and the homomorphisms
$g\colon\Gamma^{*}\to\Sigma^{*}$ and $h\colon\Gamma^{*}\to\\{\sigma\\}^{*}$,
where for $x\in\Sigma\cup\\{\varepsilon\\}$, we have $g((x,i))=x$ for
$i\in\\{0,1\\}$, $h((x,1))=\sigma$, and $h((x,0))=\varepsilon$. If
$R\subseteq\Gamma^{*}$ is the regular set of words in which exactly one
position belongs to the subalphabet
$(\Sigma\cup\\{\varepsilon\\})\times\\{1\\}$, then the language
$K^{\prime}:=h(g^{-1}(K)\cap R)$ belongs to $\mathcal{C}$. Note that
$K^{\prime}$ is $\emptyset$ or $\\{\sigma\\}$, depending on whether $K$ is
empty or not. We construct
$\mathfrak{P}=(D,\\{\sigma\\},(L_{c})_{c\in\mathfrak{C}},d_{0},\mathbf{m}_{0})$
with $D=\\{d_{0}\\}$, $\mathbf{m}_{0}={\llbracket\sigma\rrbracket}$,
$L_{d_{0},\sigma,d_{0}}=K^{\prime}$ and all languages $L_{c}=\emptyset$ for
$c\neq(d_{0},\sigma,d_{0})$. Then $\mathfrak{P}$ is terminating iff $K$ is
empty.

To prove “3$\Rightarrow$1”, we design an algorithm deciding safety assuming
decidability of emptiness. Given asynchronous program $\mathfrak{P}$ and state
$d$ as input, the algorithm consists of two semi-decision procedures: one
which searches for a run of $\mathfrak{P}$ reaching the state $d$, and the
second which enumerates regular overapproximations $\mathfrak{P}^{\prime}$ of
$\mathfrak{P}$ and checks the safety of $\mathfrak{P}^{\prime}$ using Section
4. Each $\mathfrak{P}^{\prime}$ consists of a regular language $A_{c}$
overapproximating $L_{c}$ for each context $c$ of $\mathfrak{P}$. We use
decidability of emptiness to check that $L_{c}\cap(\Sigma^{*}\setminus
A_{c})=\emptyset$ to ensure that $\mathfrak{P}^{\prime}$ is indeed an
overapproximation.

Input: Asynchronous program
$\mathfrak{P}=(D,\Sigma,(L_{c})_{c\in\mathfrak{C}},d_{0},\mathbf{m}_{0})$ over
$\mathcal{C}$, state $d\in D$

run concurrently

begin /* find a safe overapproximation */

foreach  _tuple $(A_{c})_{c\in\mathfrak{C}}$ of regular languages
$A_{c}\subseteq\Sigma^{*}$_ do

if  _$L_{c}\cap(\Sigma^{*}\setminus A_{c})=\emptyset$ for each
$c\in\mathfrak{C}$_ then

if
_$\mathfrak{P}^{\prime}=(D,\Sigma,(A_{c})_{c\in\mathfrak{C}},d_{0},\mathbf{m}_{0})$
does not reach $d$_ then

return _$d$ is not reachable._

begin /* find a run reaching $d$ */

foreach  _prerun $\rho$ of $\mathfrak{P}$_ do

if  _$\rho$ is a run that reaches $d$_ then

return _$d$ reachable._

Algorithm 1 Checking Safety

Algorithm 1 clearly gives a correct answer if it terminates. Hence, we only
have to argue that it always does terminate. Of course, if $d$ is reachable,
the first semi-decision procedure will terminate. In the other case,
termination is due to the regularity of downclosures: if $d$ is not reachable
in $\mathfrak{P}$, then Proposition 2 tells us that
$\mathord{\downarrow}{\mathfrak{P}}$ cannot reach $d$ either. But
$\mathord{\downarrow}{\mathfrak{P}}$ is an asynchronous program over regular
languages; this means there exists a safe regular overapproximation and the
second semi-decision procedure terminates.

To prove “3$\Rightarrow$2”, we adopt a similar method as for safety. Algorithm
2 for termination consists of two semi-decision procedures. By standard well-
quasi-ordering arguments, an infinite run of an asynchronous program
$\mathfrak{P}$ is witnessed by a finite self-covering run. The first semi-
decision procedure enumerates finite self-covering runs (trying to show non-
termination). The second procedure enumerates regular asynchronous programs
$\mathfrak{P}^{\prime}$ that overapproximate $\mathfrak{P}$. As before, to
check termination of $\mathfrak{P}^{\prime}$, it applies the procedure from
Theorem 4. Clearly, the algorithm’s answer is always correct. Moreover, it
gives an answer for every input. If $\mathfrak{P}$ does not terminate, it will
find a self-covering sequence. If $\mathfrak{P}$ does terminate, then
Proposition 2 tells us that $\mathord{\downarrow}{\mathfrak{P}}$ is a
terminating finite-state overapproximation. This implies that the second
procedure will terminate in that case.

Input: Asynchronous program
$\mathfrak{P}=(D,\Sigma,(L_{c})_{c\in\mathfrak{C}},d_{0},\mathbf{m}_{0})$ over
$\mathcal{C}$

run concurrently

begin /* find a terminating overapproximation */

foreach  _tuple $(A_{c})_{c\in\mathfrak{C}}$ of regular languages
$A_{c}\subseteq\Sigma^{*}$_ do

if  _$L_{c}\cap(\Sigma^{*}\setminus A_{c})=\emptyset$ for each
$c\in\mathfrak{C}$_ then

if
_$\mathfrak{P}^{\prime}=(D,\Sigma,(A_{c})_{c\in\mathfrak{C}},d_{0},\mathbf{m}_{0})$
terminates_ then

return _$\mathfrak{P}$ terminates._

begin /* find a self-covering run */

foreach  _prerun $\rho$ of $\mathfrak{P}$_ do

if  _$\rho$ is a self-covering run_ then

return _$\mathfrak{P}$ does not terminate._

Algorithm 2 Checking Termination

Let us point out a particular example. The class $\mathcal{L}$ of languages of
lossy channel systems is defined like the class of languages of Well-
Structured Transition Systems (WSTS) with upward-closed sets of accepting
configurations as in [GRB07], except that we only consider lossy channel
systems [ABJ98] instead of arbitrary WSTS. Then $\mathcal{L}$ forms a full
trio with decidable emptiness. Although downclosures of lossy channel
languages are not effectively computable (an easy consequence of [May03]), our
algorithm employs Theorem 3 to decide safety and termination.

###  4.2. Boundedness

######  Theorem 4.

Let $\mathcal{C}$ be a full trio. The following are equivalent:

  1. (1)

Boundedness is decidable for asynchronous programs over $\mathcal{C}$.

  2. (2)

Finiteness is decidable for $\mathcal{C}$.

######  Proof 4.2.

Clearly, the construction for “1$\Rightarrow$3” of Theorem 3 also works for
“1$\Rightarrow$2”: $\mathfrak{P}$ is unbounded iff $K$ is infinite.

For the converse, we first note that if finiteness is decidable for
$\mathcal{C}$ then so is emptiness. Given $L\subseteq\Sigma^{*}$ from
$\mathcal{C}$, consider the homomorphism
$h\colon(\Sigma\cup{\\{\lambda\\}})^{*}\to\Sigma^{*}$ with
$h(\mathtt{a})=\mathtt{a}$ for every $\mathtt{a}\in\Sigma$ and
$h(\lambda)=\varepsilon$. Then $h^{-1}(L)$ belongs to $\mathcal{C}$ and
$h^{-1}(L)$ is finite if and only if $L$ is empty: in the inverse
homomorphism, $\lambda$ can be arbitrarily inserted in any word. By Theorem 3,
this implies that we can also decide safety. As a consequence of considering
only full trios, it is easy to see that the problem of _context reachability_
reduces to safety: a context $c=(d,\sigma,d^{\prime})\in\mathfrak{C}$ is
_reachable in $\mathfrak{P}$_ if there is a reachable configuration
$(d,\mathbf{m})$ in $\mathfrak{P}$ with $\mathbf{m}(\sigma)\geq 1$. This
latter condition can be checked by moving from $d$ to a special state via a
$\sigma$ transition.

Input: Asynchronous program
$\mathfrak{P}=(D,\Sigma,(L_{c})_{c\in\mathfrak{C}},d_{0},\mathbf{m}_{0})$ over
$\mathcal{C}$

$F\leftarrow\emptyset$, $I\leftarrow\emptyset$;

foreach  _context $c=(d,\sigma,d^{\prime})\in\mathfrak{C}$_ do

if  _$L_{c}$ is infinite_ then

if  _$c$ is reachable in $\mathfrak{P}$_ then /* using algorithm for safety */

return _$\mathfrak{P}$ is unbounded._

$I\leftarrow I\cup\\{c\\}$

else

$F\leftarrow F\cup\\{c\\}$

foreach  _context $c\in F$_ do

foreach  _finite set $A\subseteq\Sigma^{*}$_ do /* find a finite $A$ with
$L_{c}=A$ */

if  _$L_{c}\cap(\Sigma^{*}\setminus A)=\emptyset$ and
$L_{c}\cap\\{w\\}\neq\emptyset$ for each $w\in A$_ then

$A_{c}\leftarrow A$;

break __;

/* end inner foreach */

foreach  _context $c\in I$_ do

$A_{c}\leftarrow\emptyset$

if
_$\mathfrak{P}^{\prime}=(D,\Sigma,(A_{c})_{c\in\mathfrak{C}},d_{0},\mathbf{m}_{0})$
is bounded_ then

return _$\mathfrak{P}$ is bounded._

else

return _$\mathfrak{P}$ is unbounded._

Algorithm 3 Checking Boundedness

We now explain Algorithm 3 for deciding boundedness of a given aysnchronous
program
$\mathfrak{P}=(D,\Sigma,(L_{c})_{c\in\mathfrak{C}},d_{0},\mathbf{m}_{0})$. For
every context $c$, we first check if $L_{c}$ is infinite (feasible by
assumption). This paritions the set of contexts of $\mathfrak{P}$ into sets
$I$ and $F$ which are the contexts for which the corresponding language
$L_{c}$ is infinite and finite respectively. If any context in $I$ is
reachable, then $\mathfrak{P}$ is unbounded. Otherwise, all the reachable
contexts have a finite language. For every finite language $L_{c}$ for some
$c\in F$, we explicitly find all the members of $L_{c}$. This is possible
because any finite set $A$ can be checked with $L_{c}$ for equality.
$L_{c}\subseteq A$ can be checked by testing whether
$L_{c}\cap(\Sigma^{*}\setminus A)=\emptyset$ and
$L_{c}\cap(\Sigma^{*}\setminus A)$ effectively belongs to $\mathcal{C}$. On
the other hand, checking $A\subseteq L_{c}$ just means checking whether
$L_{c}\cap\\{w\\}\neq\emptyset$ for each $w\in A$, which can be done the same
way. We can now construct asynchronous program $\mathfrak{P}^{\prime}$ which
replaces all languages for contexts in $I$ by $\emptyset$ and replaces those
corresponding to $F$ by the explicit description. Clearly
$\mathfrak{P}^{\prime}$ is bounded iff $\mathfrak{P}$ is bounded (since no
contexts from $I$ are reachable) and the former can be decided by Section 4.

We observe that boundedness is strictly harder than safety or termination:
There are full trios for which emptiness is decidable, but finiteness is
undecidable, such as the languages of reset vector addition systems [DFS98]
(see [TZ19] for a definition of the language class) and languages of lossy
channel systems.

###  4.3. Configuration reachability and liveness properties

Theorems 3 and 4 completely characterize for which full trios safety,
termination, and boundedness are decidable. We turn to configuration
reachability, fair termination, and fair starvation. We suspect that it is
unlikely that there is a simple characterization of those language classes for
which the latter problems are decidable. However, we show that they are
decidable only for a limited range of infinite-state systems. To this end, we
prove that decidability of any of these problems implies (a) decidability of
the others as well, and also implies (b) the decidability of a simple
combinatorial problem (called the $Z$-intersection problem) that is known to
be undecidable for many expressive classes of languages.

Let $Z\subseteq\\{\mathtt{a},\mathtt{b}\\}^{*}$ be the language
$Z=\\{w\in\\{\mathtt{a},\mathtt{b}\\}^{*}\mid|w|_{\mathtt{a}}=|w|_{\mathtt{b}}\\}$.
The _$Z$ -intersection problem_ for a language class $\mathcal{C}$ asks, given
a language $K\subseteq\\{\mathtt{a},\mathtt{b}\\}^{*}$ from $\mathcal{C}$,
whether $K\cap Z\neq\emptyset$. Informally, $Z$ is the language of all words
with an equal number of $\mathtt{a}$s and $\mathtt{b}$s and the
$Z$-intersection problem asks if there is a word in $K$ with an equal number
of $\mathtt{a}$s and $\mathtt{b}$s.

######  Theorem 5.

Let $\mathcal{C}$ be a full trio. The following statements are equivalent:

  1. (1)

Configuration reachability is decidable for asynchronous programs over
$\mathcal{C}$.

  2. (2)

Fair termination is decidable for asynchronous programs over $\mathcal{C}$.

  3. (3)

Fair starvation is decidable for asynchronous programs over $\mathcal{C}$.

Moreover, if decidability holds, then $Z$-intersection is decidable for
$\mathcal{C}$.

######  Proof 4.3.

We prove Theorem 5 by providing reductions among the three problems and
showing that $Z$-intersection reduces to configuration reachability. We use
diagrams similar to automata to describe asynchronous programs. Here, circles
represent global states of the program and we draw an edge

$d$$d^{\prime}$$\sigma|L$

in case we have $L_{d,\sigma,d^{\prime}}=L$ in our asynchronous program
$\mathfrak{P}$. Furthermore, we have $L_{d,\sigma,d^{\prime}}=\emptyset$
whenever there is no edge that specifies otherwise. To simplify notation, we
draw an edge $d$$d^{\prime}$$w|L$ in an asynchronous program for a word
$w\in\Sigma^{*}$, $w=\sigma_{1}\ldots\sigma_{n}$ with
$\sigma_{1},\ldots,\sigma_{n}\in\Sigma$, to symbolize a sequence of states

$d$$2$$\cdots$$n$$d^{\prime}$$\sigma_{1}|\\{\varepsilon\\}$$\sigma_{2}|\\{\varepsilon\\}$$\sigma_{n-1}|\\{\varepsilon\\}$$\sigma_{n}|L$

which removes ${\llbracket\sigma_{1},\ldots,\sigma_{n}\rrbracket}$ from the
task buffer and posts a multiset of handlers specified by the language $L$.

Proof of “2$\Rightarrow$1” Given an asynchronous program
$\mathfrak{P}=(D,\Sigma,(L_{c})_{c\in\mathfrak{C}},d_{0},\mathbf{m}_{0})$ and
a configuration $(d_{f},\mathbf{m}_{f})\in D\times{\mathbb{M}[\Sigma]}$, we
construct asynchronous program $\mathfrak{P}^{\prime}$ as follows. Let
$\mathtt{z}$ be a fresh letter and let
$\mathbf{m}_{f}={\llbracket\sigma_{1},\ldots,\sigma_{n}\rrbracket}$. We obtain
$\mathfrak{P}^{\prime}$ from $\mathfrak{P}$ by adding a new state
$d^{\prime}_{f}$ and including the following edges:

$d_{f}$$d^{\prime}_{f}$$\mathtt{z}\sigma_{1}\cdots\sigma_{n}|\\{\mathtt{z}\\}$$\mathtt{z}|\\{\mathtt{z}\\}$

Starting from $(d_{0},\mathbf{m}_{0}\oplus{\llbracket\mathtt{z}\rrbracket})$,
the program $\mathfrak{P}^{\prime}$ has a fair infinite run iff
$(d_{f},\mathbf{m}_{f})$ is reachable in $\mathfrak{P}$. The ‘if’ direction is
obvious. Conversely, $\mathtt{z}$ has to be executed in any fair run $\rho$ of
$\mathfrak{P}^{\prime}$ which implies that $d^{\prime}_{f}$ is reached by
$\mathfrak{P}^{\prime}$ in $\rho$. Since only $\mathtt{z}$ can be executed at
$d^{\prime}_{f}$ in $\rho$, this means that the multiset is exactly
$\mathbf{m}_{f}$ when $d_{f}$ is reached during $\rho$. Clearly this initial
segment of $\rho$ corresponds to a run of $\mathfrak{P}$ which reaches the
target configuration.
Proof of “3$\Rightarrow$2” We construct
$\mathfrak{P}^{\prime}=(D,\Sigma^{\prime},(L^{\prime}_{c})_{c\in\mathfrak{C}^{\prime}},d_{0},\mathbf{m}^{\prime}_{0})$
given

$\mathfrak{P}=(D,\Sigma,(L_{c})_{c\in\mathfrak{C}},d_{0},\mathbf{m}_{0})$

over $\mathcal{C}$ as follows. Let
$\Sigma^{\prime}=\Sigma\cup\\{\mathtt{s}\\}$, where $\mathtt{s}$ is a fresh
handler. Replace each edge

$d$$d^{\prime}$$\sigma|L$ by $d$$d^{\prime}$$\sigma|L\cup
L\mathtt{s}$$\mathtt{s}|\varepsilon$

at every state $d\in D$. Moreover, we set
$\mathbf{m}^{\prime}_{0}=\mathbf{m}_{0}\oplus{\llbracket\mathtt{s}\rrbracket}$.
Then $\mathfrak{P}^{\prime}$ has an infinite fair run that starves some
handler if and only if $\mathfrak{P}$ has an infinite fair run. From an
infinite fair run $\rho$ of $\mathfrak{P}$, we obtain an infinite fair run of
$\mathfrak{P}^{\prime}$ which starves $\mathtt{s}$, by producing $\mathtt{s}$
while simulating $\rho$ and consuming it in the loop. Conversely, from an
infinite fair run $\rho^{\prime}$ of $\mathfrak{P}^{\prime}$ which starves
some $\tau$, we obtain an infinite fair run $\rho$ of $\mathfrak{P}$ by
omitting all productions and consumptions of $\mathtt{s}$ and removing two
extra instances of $\mathtt{s}$ from all configurations.
Proof of “1$\Rightarrow$3” From
$\mathfrak{P}=(D,\Sigma,(L_{c})_{c\in\mathfrak{C}},d_{0},\mathbf{m}_{0})$ over
$\mathcal{C}$, for each subset $\Gamma\subseteq\Sigma$ and $\tau\in\Sigma$, we
construct an asynchronous program
$\mathfrak{P}_{\Gamma,\tau}=(D^{\prime},\Sigma^{\prime},(L_{c})_{c\in\mathfrak{C}^{\prime}},d^{\prime}_{0},\mathbf{m}^{\prime}_{0})$
over $\mathcal{C}$ such that a particular configuration is reachable in
$\mathfrak{P}_{\Gamma,\tau}$ if and only if $\mathfrak{P}$ has a fair infinite
run $\rho_{\Gamma,\tau}$, where $\Gamma$ is the set of handlers that is
executed infinitely often in $\rho_{\Gamma,\tau}$ and $\rho_{\Gamma,\tau}$
starves $\tau$. Since there are only finitely many choices for $\Gamma$ and
$\tau$, decidability of configuration reachability implies decidability of
fair starvation. The idea is that a run $\rho_{\Gamma,\tau}$ exists if and
only if there exists a run

$(d_{0},\mathbf{m}_{0})\xrightarrow{\sigma_{1}}\cdots\xrightarrow{\sigma_{n}}(d_{n},\mathbf{m}_{n})=(e_{0},\mathbf{n}_{0})\xrightarrow{\gamma_{1}}(e_{1},\mathbf{n}_{1})\xrightarrow{\gamma_{2}}\cdots\xrightarrow{\gamma_{k}}(e_{k},\mathbf{n}_{k}),$
(1)

where $\bigcup_{i=1}^{k}\\{\gamma_{i}\\}=\Gamma$, for each $1\leq i\leq k$
$\mathbf{n}_{i}\in{\mathbb{M}[\Gamma]}$,
$\mathbf{m}_{n}\preceq\mathbf{n}_{k}$, and for each $i\in\\{1,\ldots,k\\}$
with $\gamma_{i}=\tau$, we have $\mathbf{n}_{i-1}(\tau)\geq 2$. In such a run,
we call
$(d_{0},\mathbf{m}_{0})\xrightarrow{\sigma_{1}}\cdots\xrightarrow{\sigma_{n}}(d_{n},\mathbf{m}_{n})$
its _first phase_ and
$(e_{0},\mathbf{n}_{0})\xrightarrow{\gamma_{1}}\cdots\xrightarrow{\gamma_{k}}(e_{k},\mathbf{n}_{k})$
its _second phase_.

Let us explain how $\mathfrak{P}_{\Gamma,\tau}$ reflects the existence of a
run as in Eq. 1. The set $\Sigma^{\prime}$ of handlers of
$\mathfrak{P}_{\Gamma,\tau}$ includes $\Sigma$, $\bar{\Sigma}$ and
$\hat{\Sigma}$, where $\bar{\Sigma}=\\{\bar{\sigma}\mid\sigma\in\Sigma\\}$ and
$\hat{\Sigma}=\\{\hat{\sigma}\mid\sigma\in\Sigma\\}$ are disjoint copies of
$\Sigma$. This means, a multiset ${\mathbb{M}[\Sigma^{\prime}]}$ contains
multisets
$\mathbf{m}^{\prime}=\mathbf{m}\oplus\bar{\mathbf{m}}\oplus\hat{\mathbf{m}}$
with $\mathbf{m}\in{\mathbb{M}[\Sigma]}$,
$\bar{\mathbf{m}}\in{\mathbb{M}[\bar{\Sigma}]}$, and
$\hat{\mathbf{m}}\in{\mathbb{M}[\hat{\Sigma}]}$. A run of
$\mathfrak{P}_{\Gamma,\tau}$ simulates the two phases of $\rho$. While
simulating the first phase, $\mathfrak{P}_{\Gamma,\tau}$ keeps two copies of
the task buffer, $\mathbf{m}$ and $\bar{\mathbf{m}}$. The copying is easily
accomplished by a homomorphism with $\sigma\mapsto\sigma\bar{\sigma}$ for each
$\sigma\in\Sigma$. At some point, $\mathfrak{P}_{\Gamma,\tau}$ switches into
simulating the second phase. There, $\bar{\mathbf{m}}$ remains unchanged, so
that it stores the value of $\mathbf{m}_{n}$ in Eq. 1 and can be used in the
end to make sure that $\mathbf{m}_{n}\preceq\mathbf{n}_{k}$.

Hence, in the second phase, $\mathfrak{P}_{\Gamma,\tau}$ works, like
$\mathfrak{P}$, only with $\Sigma$. However, whenever a handler
$\sigma\in\Sigma$ is executed, it also produces a task $\hat{\sigma}$. These
handlers are used at the end to make sure that every $\gamma\in\Gamma$ has
been executed at least once in the second phase. Also, whenever $\tau$ is
executed, $\mathfrak{P}_{\Gamma,\tau}$ checks that at least two instances of
$\tau$ are present in the task buffer, thereby ensuring that $\tau$ is
starved.

In the end, a distinguished final state allows $\mathfrak{P}_{\Gamma,\tau}$ to
execute handlers in $\Gamma$ and $\bar{\Gamma}$ simultaneously to make sure
that $\mathbf{m}_{n}\preceq\mathbf{n}_{k}$. In its final state,
$\mathfrak{P}_{\Gamma,\tau}$ can execute handlers
$\hat{\gamma}\in\hat{\Gamma}$ and $\gamma\in\Gamma$ (without creating new
handlers). In the final configuration, there can be no $\hat{\sigma}$ with
$\sigma\in\Sigma\setminus\Gamma$, and there has to be exactly one
$\hat{\gamma}$ for each $\gamma\in\Gamma$. This guarantees that (i) each
handler in $\Gamma$ is executed at least once during the second phase, (ii)
every handler executed in the second phase is from $\Gamma$, and (iii)
$\mathbf{m}_{n}$ contains only handlers from $\Gamma$ (because handlers from
$\bar{\Sigma}$ cannot be executed in the second phase).

Let us now describe $\mathfrak{P}_{\Gamma,\tau}$ in detail. We have
$\Sigma^{\prime}=\Sigma\cup\bar{\Sigma}\cup\hat{\Gamma}\cup\\{\mathtt{z}\\}$,
where $\mathtt{z}$ is a fresh letter. The set of states is
$D^{\prime}=D\cup\tilde{D}\cup\\{d_{f}\\}$, where $\tilde{D}=\\{\tilde{d}\mid
d\in D\\}$ is a disjoint copy of $D$ for simulating the second phase, and
$d_{f}$ is a fresh state. Moreover, we change the languages $L_{c}$ in the
following way:

$\leavevmode\hbox to58.48pt{\vbox
to20.1pt{\pgfpicture\makeatletter\hbox{\hskip 7.9pt\lower-7.9pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@fill{0.9}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@fill{0.9}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{}\pgfsys@moveto{7.5pt}{0.0pt}\pgfsys@curveto{7.5pt}{4.14218pt}{4.14218pt}{7.5pt}{0.0pt}{7.5pt}\pgfsys@curveto{-4.14218pt}{7.5pt}{-7.5pt}{4.14218pt}{-7.5pt}{0.0pt}\pgfsys@curveto{-7.5pt}{-4.14218pt}{-4.14218pt}{-7.5pt}{0.0pt}{-7.5pt}\pgfsys@curveto{4.14218pt}{-7.5pt}{7.5pt}{-4.14218pt}{7.5pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.60243pt}{-3.47221pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$d$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}{}{}}{{{{}{}{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@fill{0.9}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@fill{0.9}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{}\pgfsys@moveto{50.17912pt}{0.0pt}\pgfsys@curveto{50.17912pt}{4.14218pt}{46.8213pt}{7.5pt}{42.67912pt}{7.5pt}\pgfsys@curveto{38.53694pt}{7.5pt}{35.17912pt}{4.14218pt}{35.17912pt}{0.0pt}\pgfsys@curveto{35.17912pt}{-4.14218pt}{38.53694pt}{-7.5pt}{42.67912pt}{-7.5pt}\pgfsys@curveto{46.8213pt}{-7.5pt}{50.17912pt}{-4.14218pt}{50.17912pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{42.67912pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{39.3067pt}{-4.25pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$d^{\prime}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{7.9pt}{0.0pt}\pgfsys@lineto{32.77916pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{32.77916pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{11.46864pt}{3.7pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\sigma|L$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{{{}}{{}}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}~{}~{}\leadsto~{}~{}\leavevmode\hbox
to86.93pt{\vbox to21.18pt{\pgfpicture\makeatletter\hbox{\hskip
7.9pt\lower-7.9pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@fill{0.9}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@fill{0.9}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{}\pgfsys@moveto{7.5pt}{0.0pt}\pgfsys@curveto{7.5pt}{4.14218pt}{4.14218pt}{7.5pt}{0.0pt}{7.5pt}\pgfsys@curveto{-4.14218pt}{7.5pt}{-7.5pt}{4.14218pt}{-7.5pt}{0.0pt}\pgfsys@curveto{-7.5pt}{-4.14218pt}{-4.14218pt}{-7.5pt}{0.0pt}{-7.5pt}\pgfsys@curveto{4.14218pt}{-7.5pt}{7.5pt}{-4.14218pt}{7.5pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.60243pt}{-3.47221pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$d$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}{}{}}{{{{}{}{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@fill{0.9}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@fill{0.9}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{}\pgfsys@moveto{78.6319pt}{0.0pt}\pgfsys@curveto{78.6319pt}{4.14218pt}{75.27408pt}{7.5pt}{71.1319pt}{7.5pt}\pgfsys@curveto{66.98972pt}{7.5pt}{63.6319pt}{4.14218pt}{63.6319pt}{0.0pt}\pgfsys@curveto{63.6319pt}{-4.14218pt}{66.98972pt}{-7.5pt}{71.1319pt}{-7.5pt}\pgfsys@curveto{75.27408pt}{-7.5pt}{78.6319pt}{-4.14218pt}{78.6319pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{71.1319pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{67.75948pt}{-4.25pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$d^{\prime}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{7.9pt}{0.0pt}\pgfsys@lineto{61.23193pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{61.23193pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{15.35864pt}{3.7pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\sigma\bar{\sigma}|h^{\pm}(L)$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{{{}}{{}}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}$

where $h^{\pm}\colon\Sigma^{*}\to(\Sigma\cup\bar{\Sigma})^{*}$ is the
homomorphism with $\sigma\mapsto\sigma\bar{\sigma}$ for every
$\sigma\in\Sigma$. This means, for every context $c=(d,\sigma,d^{\prime})$, we
have $d\xrightarrow{\sigma\bar{\sigma}|h^{\pm}(L)}d^{\prime}$ in
$\mathfrak{P}_{\Gamma,\tau}$. Note that since $\mathcal{C}$ is a full trio, it
is in particular closed under homomorphisms. Hence, $h^{\pm}(L)$ belongs to
$\mathcal{C}$. Moreover, $\mathfrak{P}_{\Gamma,\tau}$ can spontaneously switch
to simulating the second phase: For each $d\in D$, we have

$d$$\tilde{d}$$\mathtt{z}|\\{\mathtt{z}\\}$

Here, the handler $\mathtt{z}$ merely allows us to move to state $\tilde{d}$
without interfering with the other handlers. In the second phase,
$\mathfrak{P}_{\Gamma,\tau}$ simulates $\mathfrak{P}$ slightly differently. We
perform the following replacement:

$\leavevmode\hbox to58.48pt{\vbox
to20.1pt{\pgfpicture\makeatletter\hbox{\hskip 7.9pt\lower-7.9pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@fill{0.9}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@fill{0.9}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{}\pgfsys@moveto{7.5pt}{0.0pt}\pgfsys@curveto{7.5pt}{4.14218pt}{4.14218pt}{7.5pt}{0.0pt}{7.5pt}\pgfsys@curveto{-4.14218pt}{7.5pt}{-7.5pt}{4.14218pt}{-7.5pt}{0.0pt}\pgfsys@curveto{-7.5pt}{-4.14218pt}{-4.14218pt}{-7.5pt}{0.0pt}{-7.5pt}\pgfsys@curveto{4.14218pt}{-7.5pt}{7.5pt}{-4.14218pt}{7.5pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.60243pt}{-3.47221pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$d$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}{}{}}{{{{}{}{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@fill{0.9}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@fill{0.9}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{}\pgfsys@moveto{50.17912pt}{0.0pt}\pgfsys@curveto{50.17912pt}{4.14218pt}{46.8213pt}{7.5pt}{42.67912pt}{7.5pt}\pgfsys@curveto{38.53694pt}{7.5pt}{35.17912pt}{4.14218pt}{35.17912pt}{0.0pt}\pgfsys@curveto{35.17912pt}{-4.14218pt}{38.53694pt}{-7.5pt}{42.67912pt}{-7.5pt}\pgfsys@curveto{46.8213pt}{-7.5pt}{50.17912pt}{-4.14218pt}{50.17912pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{42.67912pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{39.3067pt}{-4.25pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$d^{\prime}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{7.9pt}{0.0pt}\pgfsys@lineto{32.77916pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{32.77916pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{11.46864pt}{3.7pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\sigma|L$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{{{}}{{}}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}~{}~{}\leadsto~{}~{}\begin{cases}\leavevmode\hbox
to86.93pt{\vbox to20.1pt{\pgfpicture\makeatletter\hbox{\hskip
7.9pt\lower-7.9pt\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@fill{0.9}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@fill{0.9}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{}\pgfsys@moveto{7.5pt}{0.0pt}\pgfsys@curveto{7.5pt}{4.14218pt}{4.14218pt}{7.5pt}{0.0pt}{7.5pt}\pgfsys@curveto{-4.14218pt}{7.5pt}{-7.5pt}{4.14218pt}{-7.5pt}{0.0pt}\pgfsys@curveto{-7.5pt}{-4.14218pt}{-4.14218pt}{-7.5pt}{0.0pt}{-7.5pt}\pgfsys@curveto{4.14218pt}{-7.5pt}{7.5pt}{-4.14218pt}{7.5pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.77779pt}{-3.61111pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\tilde{d}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}{}{}}{{{{}{}{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@fill{0.9}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@fill{0.9}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{}\pgfsys@moveto{78.6319pt}{0.0pt}\pgfsys@curveto{78.6319pt}{4.14218pt}{75.27408pt}{7.5pt}{71.1319pt}{7.5pt}\pgfsys@curveto{66.98972pt}{7.5pt}{63.6319pt}{4.14218pt}{63.6319pt}{0.0pt}\pgfsys@curveto{63.6319pt}{-4.14218pt}{66.98972pt}{-7.5pt}{71.1319pt}{-7.5pt}\pgfsys@curveto{75.27408pt}{-7.5pt}{78.6319pt}{-4.14218pt}{78.6319pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{71.1319pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{67.58412pt}{-4.38889pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\tilde{d}^{\prime}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{7.9pt}{0.0pt}\pgfsys@lineto{61.23193pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{61.23193pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{22.91725pt}{3.7pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\sigma|L\hat{\sigma}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{{{}}{{}}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}&\text{if
$\sigma\neq\tau$}\\\ \leavevmode\hbox to86.93pt{\vbox
to20.1pt{\pgfpicture\makeatletter\hbox{\hskip 7.9pt\lower-7.9pt\hbox
to0.0pt{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.4pt}\pgfsys@invoke{
}\nullfont\pgfsys@beginscope\pgfsys@invoke{ }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hbox to0.0pt{\pgfsys@beginscope\pgfsys@invoke{ }{{}}
{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@fill{0.9}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@fill{0.9}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{}\pgfsys@moveto{7.5pt}{0.0pt}\pgfsys@curveto{7.5pt}{4.14218pt}{4.14218pt}{7.5pt}{0.0pt}{7.5pt}\pgfsys@curveto{-4.14218pt}{7.5pt}{-7.5pt}{4.14218pt}{-7.5pt}{0.0pt}\pgfsys@curveto{-7.5pt}{-4.14218pt}{-4.14218pt}{-7.5pt}{0.0pt}{-7.5pt}\pgfsys@curveto{4.14218pt}{-7.5pt}{7.5pt}{-4.14218pt}{7.5pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{0.0pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{-2.77779pt}{-3.61111pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\tilde{d}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}{}{}}{{{{}{}{}}}}{{}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@fill{0.9}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{{}{{{}}}{{}}{}{}{}{}{}{}{}{}{}{\pgfsys@beginscope\pgfsys@invoke{
}\definecolor{pgffillcolor}{rgb}{0.9,0.9,0.9}\pgfsys@color@gray@fill{0.9}\pgfsys@invoke{
}\definecolor{pgfstrokecolor}{rgb}{0.3,0.3,0.3}\pgfsys@color@gray@stroke{0.3}\pgfsys@invoke{
}\pgfsys@setlinewidth{0.8pt}\pgfsys@invoke{
}{}\pgfsys@moveto{78.6319pt}{0.0pt}\pgfsys@curveto{78.6319pt}{4.14218pt}{75.27408pt}{7.5pt}{71.1319pt}{7.5pt}\pgfsys@curveto{66.98972pt}{7.5pt}{63.6319pt}{4.14218pt}{63.6319pt}{0.0pt}\pgfsys@curveto{63.6319pt}{-4.14218pt}{66.98972pt}{-7.5pt}{71.1319pt}{-7.5pt}\pgfsys@curveto{75.27408pt}{-7.5pt}{78.6319pt}{-4.14218pt}{78.6319pt}{0.0pt}\pgfsys@closepath\pgfsys@moveto{71.1319pt}{0.0pt}\pgfsys@fillstroke\pgfsys@invoke{
} \pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{67.58412pt}{-4.38889pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{ }\hbox{{$\tilde{d}^{\prime}$}}
}}\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
{{}}{}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{ }{{}}{}{{}}
{{{{{}}{}{}{}{}{{}}}}}{}{{{{{}}{}{}{}{}{{}}}}}{{}}{}{}{}{}{}{{{}{}}}{}{{}}{}{}{}{{{}{}}}{}{}{}{}{{}}\pgfsys@moveto{7.9pt}{0.0pt}\pgfsys@lineto{61.23193pt}{0.0pt}\pgfsys@stroke\pgfsys@invoke{
}{{}{{}}{}{}{{}}{{{}}{{{}}{\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{61.23193pt}{0.0pt}\pgfsys@invoke{
}\pgfsys@invoke{ \lxSVG@closescope }\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}{{}}}}\hbox{\hbox{{\pgfsys@beginscope\pgfsys@invoke{
}{{}{}{{ {}{}}}{ {}{}} {{}{{}}}{{}{}}{}{{}{}} {
}{{{{}}\pgfsys@beginscope\pgfsys@invoke{
}\pgfsys@transformcm{1.0}{0.0}{0.0}{1.0}{19.21701pt}{3.7pt}\pgfsys@invoke{
}\hbox{{\definecolor{pgfstrokecolor}{rgb}{0,0,0}\pgfsys@color@rgb@stroke{0}{0}{0}\pgfsys@invoke{
}\pgfsys@color@rgb@fill{0}{0}{0}\pgfsys@invoke{
}\hbox{{$\tau\tau|L\tau\hat{\tau}$}} }}\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope}}} \pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope}}}
\pgfsys@invoke{\lxSVG@closescope }\pgfsys@endscope{{
{}{}{}{}{}}{{{}}{{}}}}{}{}\hss}\pgfsys@discardpath\pgfsys@invoke{\lxSVG@closescope
}\pgfsys@endscope\hss}}\lxSVG@closescope\endpgfpicture}}&\text{if
$\sigma=\tau$}\end{cases}$ (2)

Note that since $\mathcal{C}$ is a full trio, the languages $Lv=\\{uv\mid u\in
L\\}$ belong to $\mathcal{C}$ for every word $v$. Finally,
$\mathfrak{P}_{\Gamma,\tau}$ can spontaneously switch to its distinguished
state $d_{f}$, so that we have for every $\tilde{d}\in\tilde{D}$ and every
$\gamma\in\Gamma$:

$\tilde{d}$$d_{f}$$\mathtt{z}|\\{\varepsilon\\}$$\gamma\bar{\gamma}|\\{\varepsilon\\}$$\gamma|\\{\varepsilon\\}$$\hat{\gamma}|\\{\varepsilon\\}$
(3)

The initial configuration of $\mathfrak{P}_{\Gamma,\tau}$ is
$(d_{0},\mathbf{m}^{\prime}_{0})$, where
$\mathbf{m}^{\prime}_{0}=\mathbf{m}_{0}\oplus\bar{\mathbf{m}}_{0}\oplus{\llbracket\mathtt{z}\rrbracket}$,
where $\bar{\mathbf{m}}_{0}$ is obtained from $\mathbf{m}_{0}$ by replacing
every occurrence of $\sigma\in\Sigma$ in $\mathbf{m}_{0}$ with $\bar{\sigma}$.
The final configuration is $(d_{f},\mathbf{m}_{f})$, where
$\mathbf{m}_{f}\in{\mathbb{M}[\hat{\Gamma}]}$ is the multiset with
$\mathbf{m}_{f}(\hat{\gamma})=1$ for every $\gamma\in\Gamma$. It is now
straightforward to check that $(d_{f},\mathbf{m}_{f})$ is reachable in
$\mathfrak{P}_{\Gamma,\tau}$ if and only if $\mathfrak{P}$ has an infinite
fair run that starves $\tau$.

Decidability of $Z$-intersection To complete the proof of Theorem 5, we reduce
$Z$-intersection to configuration reachability. Given
$K\subseteq\\{\mathtt{a},\mathtt{b}\\}^{*}$ from $\mathcal{C}$, we construct
the asynchronous program
$\mathfrak{P}=(D,\Sigma,(L_{c})_{c\in\mathfrak{C}},d_{0},\mathbf{m}_{0})$ over
$\mathcal{C}$ where $D=\\{d_{0},0,1\\}$,
$\Sigma=\\{\mathtt{a},\mathtt{b},\mathtt{c}\\}$, by including the following
edges:

$d_{0}$$0$$1$$\mathtt{c}|K$$\mathtt{a}|\\{\varepsilon\\}$$\mathtt{b}|\\{\varepsilon\\}$

The initial task buffer is $\mathbf{m}_{0}={\llbracket\mathtt{c}\rrbracket}$.
Then clearly, the configuration $(0,{\llbracket\rrbracket})$ is reachable in
$\mathfrak{P}$ if and only if $K\cap Z\neq\emptyset$.

If the construction seems abstract, recall the example from Section 2: the
procedure s1 plays the role of $K$ and generates strings from its language in
${\\{\mathtt{a},\mathtt{b}\\}}^{*}$. The procedures $\mathtt{a}$ and
$\mathtt{b}$ take turns to ensure there is an equal number of them; the states
$0$ and $1$ are values of turn.

Theorem 5 is useful in the contrapositive to show undecidability. For example,
one can show undecidability of $Z$-intersection for languages of lossy channel
systems (see Section 4.1): One expresses reachability in a non-lossy FIFO
system by making sure that the numbers of enqueue- and dequeue-operations
match. Thus, for asynchronous programs over lossy channel systems, the
problems of Theorem 5 are undecidable. We also use Theorem 5 in Section 5 to
conclude undecidability for higher-order asynchronous programs, already at
order $2$.

##  5\. Higher-Order Asynchronous Programs

We apply our general decidability results to asynchronous programs over
(deterministic) higher-order recursion schemes ($\mathsf{HORS}$). Kobayashi
[Kob09] has shown how higher-order functional programs can be modeled using
$\mathsf{HORS}$. In his setting, a program contains instructions that access
certain resources. The path language of the $\mathsf{HORS}$ produced by
Kobayashi is the set of possible sequences of instructions. For us, the input
program contains post instructions (which post handlers i.e. add tasks to the
task buffer) and we translate higher-order programs with post instructions
into a $\mathsf{HORS}$ whose path language is used as the language of
handlers.

We recall some definitions from [Kob09]. The set of types is defined by the
grammar $A\ :=\ \mathtt{o}\mid A\rightarrow A$. The order
$\operatorname{ord}(A)$ of a type $A$ is inductively defined as
$\operatorname{ord}(\mathtt{o})=0$ and $\operatorname{ord}(A\rightarrow
B):=\max(\operatorname{ord}(A)+1,\operatorname{ord}(B))$. The arity of a type
is inductively defined by $\operatorname{arity}(\mathtt{o})=0$ and
$\operatorname{arity}(A\rightarrow B)=\operatorname{arity}(B)+1$. We assume a
countably infinite set $\mathrm{Var}$ of typed variables $x:A$. For a set
$\Theta$ of typed symbols, the set $\tilde{\Theta}$ of terms generated from
$\Theta$ is the least set which contains $\Theta$ such that whenever $s:A\to
B$ and $t:A$ belong to $\tilde{\Theta}$, then also $s\,t:B$ belongs to
$\tilde{\Theta}$. By convention the type
$\mathtt{o}\rightarrow\ldots(\mathtt{o}\rightarrow(\mathtt{o}\rightarrow\mathtt{o}))$
is written
$\mathtt{o}\rightarrow\ldots\rightarrow\mathtt{o}\rightarrow\mathtt{o}$ and
the term $((t_{1}t_{2})t_{3}\cdots)t_{n}$ is written $t_{1}t_{2}\cdots t_{n}$.
We write $\bar{x}$ for a sequence $(x_{1},x_{2},\ldots,x_{n})$ of variables.

A higher-order recursion scheme ($\mathsf{HORS}$) is a tuple
$\mathscr{S}=(\Sigma,\mathcal{N},\mathcal{R},S)$ where $\Sigma$ is a set of
typed terminal symbols of types of order 0 or 1, $\mathcal{N}$ is a set of
typed non-terminal symbols (disjoint from terminal symbols), $S:\mathtt{o}$ is
the start non-terminal symbol and $\mathcal{R}$ is a set of rewrite rules
$Fx_{1}x_{2}\cdots x_{n}\twoheadrightarrow t$ where
$F:A_{1}\rightarrow\cdots\rightarrow A_{n}\rightarrow\mathtt{o}$ is a non-
terminal in $\mathcal{N}$, $x_{i}:A_{i}$ for all $i$ are variables and
$t:\mathtt{o}$ is a term generated from
$\Sigma\cup\mathcal{N}\cup\\{x_{1},x_{2},\ldots,x_{n}\\}$. The order of a
$\mathsf{HORS}$ is the maximum order of a non-terminal symbol. We define a
rewrite relation $\twoheadrightarrow$ on terms over $\Sigma\cup\mathcal{N}$ as
follows: $F\bar{a}\twoheadrightarrow t[\bar{x}/\bar{a}]$ if
$F\bar{x}\twoheadrightarrow t\in\mathcal{R}$, and if $t\twoheadrightarrow
t^{\prime}$ then $ts\twoheadrightarrow t^{\prime}s$ and $st\twoheadrightarrow
st^{\prime}$. The reflexive, transitive closure of $\twoheadrightarrow$ is
denoted $\twoheadrightarrow^{*}$. A sentential form $t$ of $\mathscr{S}$ is a
term over $\Sigma\cup\mathcal{N}$ such that $S\twoheadrightarrow^{*}t$.

If $N$ is the maximum arity of a symbol in $\Sigma$, then a (possibly
infinite) tree over $\Sigma$ is a partial function $tr$ from
$\\{0,1,\ldots,N-1\\}^{*}$ to $\Sigma$ that fulfills the following conditions:
$\varepsilon\in\operatorname{dom}(tr)$, $\operatorname{dom}(tr)$ is closed
under prefixes, and if $tr(w)=a$ and $\operatorname{arity}(a)=k$ then
$\\{j\mid wj\in\operatorname{dom}(tr)\\}=\\{0,1,\ldots,k-1\\}$.

A _deterministic_ $\mathsf{HORS}$ is one where there is exactly one rule of
the form $Fx_{1}x_{2}\cdots x_{n}\rightarrow t$ for every non-terminal $F$.
Following [Kob09], we show how a deterministic $\mathsf{HORS}$ can be used to
represent a higher-order pushdown language arising from a higher-order
functional program. Sentential forms can be seen as trees over
$\Sigma\cup\mathcal{N}$. A sequence $\Pi$ over $\\{0,1,\ldots,N-1\\}$ is a
path of $tr$ if every finite prefix of $\Pi\in\operatorname{dom}(tr)$ and
$\Pi$ is maximal. The set of finite paths in a tree $tr$ will be denoted
$\mathsf{Paths}(tr)$. Unless otherwise specified, a path is finite in our
context. Associated with any path $\Pi=n_{1},n_{2},\ldots,n_{k}$ is the word

$w_{\Pi}=tr(n_{1})tr(n_{1}n_{2})\cdots tr(n_{1}n_{2}\cdots n_{k}).$

We will also write $w_{\Pi}(\bar{m})$ to denote the letter $tr(\bar{m})$ where
$\bar{m}=n_{1}n_{2}\ldots n_{l}$ for some $l\leq k$. We associate a value tree
$\mathcal{T}_{\mathscr{S}}$ associated with a deterministic $\mathsf{HORS}$
$\mathscr{S}$ in the following way. For a sentential form $t$ define the
finite tree $t^{\bot}$ by case analysis: $t^{\bot}=f$ if $f$ is a terminal
symbol and $t^{\bot}=t_{1}^{\bot}t_{2}^{\bot}$ if $t=t_{1}t_{2}$ and
$t_{1}^{\bot}\neq\bot$, and $t^{\bot}=\bot$ otherwise.

Intuitively, the tree $t^{\bot}$ is obtained by replacing any subterm whose
root is a non-terminal by the nullary symbol $\bot$. We define the partial
order $\leq_{t}$ on $\operatorname{dom}(\Sigma)\cup\\{\bot\\}$ by
$\bot\leq_{t}a$ for all $a\in\operatorname{dom}(\Sigma)$, which is extended to
trees by

$t\leq_{t}s\iff\forall\bar{n}\in\operatorname{dom}(t):\bar{n}\in\operatorname{dom}(s)\land
t(\bar{n})\leq_{t}s(\bar{n})$

The value tree generated by a $\mathsf{HORS}$ $\mathscr{S}$ is denoted
$\mathcal{T}_{\mathscr{S}}$ and is obtained by repeated application of the
rewrite rules to the start symbol $S$. To make this formal, we write
$\operatorname{lub}(T)$ for the least upper bound of a collection $T$ of trees
with respect to the order $\leq_{t}$. Then we set
$\mathcal{T}_{\mathscr{S}}:=\operatorname{lub}(\\{t^{\bot}\mid
S\rightarrow^{*}t\\})$. Any $\mathsf{HORS}$ for which the value tree
$\mathcal{T}_{\mathscr{S}}$ does not contain any $\bot$ symbol is called
_productive_. All $\mathsf{HORS}$ dealt with in this paper are assumed to be
productive. Checking if a given $\mathsf{HORS}$ is productive is decidable,
see, e.g., [Gre16].

Let $\Sigma_{1}:=\\{a\in\Sigma\mid\operatorname{arity}(a)=1\\}$. The path
language $\mathcal{L}_{\mathsf{p}}(\mathscr{S})$ of a deterministic
$\mathsf{HORS}$ $\mathscr{S}$ is defined as
$\\{\mathrm{Proj}_{\Sigma_{1}}(w_{\Pi})\mid\Pi\in\mathsf{Paths}(\mathcal{T}_{\mathscr{S}})\\}$.
The tree language $\mathcal{L}_{\mathsf{t}}(\mathscr{S})$ associated with a
(nondeterministic) $\mathsf{HORS}$ is the set of sentential forms of
$\mathscr{S}$ which contain only labels from $\Sigma$.

The deterministic $\mathsf{HORS}$ corresponding to the higher-order function
$\mathtt{s4}$ from Figure 1 is given by
$\mathscr{S}=(\Sigma,\mathcal{N},\mathcal{R},S)$, where

$\displaystyle\Sigma=$
$\displaystyle\\{\mathtt{br}:\mathtt{o}\rightarrow\mathtt{o}\rightarrow\mathtt{o},\mathtt{c},\mathtt{d},\mathtt{f}:\mathtt{o}\rightarrow\mathtt{o},\mathtt{e}:\mathtt{o}\\}$
$\displaystyle\mathcal{N}=$
$\displaystyle\\{S:\mathtt{o},F:(\mathtt{o}\rightarrow\mathtt{o})\rightarrow\mathtt{o}\rightarrow\mathtt{o},H:(\mathtt{o}\rightarrow\mathtt{o})\rightarrow\mathtt{o}\rightarrow\mathtt{o},I:\mathtt{o}\rightarrow\mathtt{o}\\}$
$\displaystyle\mathcal{R}=$ $\displaystyle\\{S\twoheadrightarrow
F\;I\;\mathtt{e},I\;x\twoheadrightarrow
x,F\;G\;x\twoheadrightarrow\mathtt{br}(F\;(H\;G)\;(\mathtt{f}x))\;(G\;x),H\;G\;x\twoheadrightarrow\mathtt{c}(G(\mathtt{d}x))\\}$

The path language
$\mathcal{L}_{\mathsf{p}}(\mathscr{S})={\\{\mathtt{c}^{n}\mathtt{d}^{n}\mathtt{f}^{n}\mid
n\geq 0\\}}$. To see this, apply the reduction rules to get the value tree
$\mathcal{T}_{\mathscr{S}}$ shown on the right:

$\displaystyle S$ $\displaystyle\twoheadrightarrow
F\;I\;\mathtt{e}\twoheadrightarrow\mathtt{br}\;(F\;(HI)\;(\mathtt{fe}))\;(I\mathtt{e})$
$\displaystyle\twoheadrightarrow\mathtt{br}\;(F\;(HI)\;(\mathtt{fe}))\;\mathtt{e}$
$\displaystyle\twoheadrightarrow\mathtt{br}\;(\mathtt{br}\;(F\;(H(HI))\;(\mathtt{f}(\mathtt{fe})))\;(HI(\mathtt{fe})))\;\mathtt{e}$
$\displaystyle\twoheadrightarrow\mathtt{br}\;(\mathtt{br}\;(F\;(H(HI))\;(\mathtt{f}(\mathtt{fe})))\;(\mathtt{c}(I(\mathtt{d(fe)}))))\;\mathtt{e}$
$\displaystyle\twoheadrightarrow\mathtt{br}\;(\mathtt{br}\;(F\;(H(HI))\;(\mathtt{f}(\mathtt{fe})))\;(\mathtt{c(d(fe))}))\;\mathtt{e}$
$\displaystyle\twoheadrightarrow\cdots$

$\mathtt{br}$$\mathtt{e}$$\mathtt{br}$$\mathtt{c}$$\mathtt{br}$$\mathtt{d}$$\mathtt{f}$$\mathtt{e}$$..$$..$

A $\mathsf{HORS}$ $\mathscr{S}$ is called a _word scheme_ if it has exactly
one nullary terminal symbol $\mathsf{e}$ and all other terminal symbols
$\tilde{\Sigma}$ are of arity one. The word language
$\mathcal{L}_{\mathsf{w}}(\mathscr{S})\subseteq\tilde{\Sigma}^{*}$ defined by
$\mathscr{S}$ is $\mathcal{L}_{\mathsf{w}}(\mathscr{S})=\\{a_{1}a_{2}\cdots
a_{n}\mid(a_{1}(a_{2}\cdots(a_{n}(\mathsf{e}))\cdots))\in\mathcal{L}_{\mathsf{t}}(\mathscr{S})\\}$.
We denote by $\mathcal{H}$ the class of languages
$\mathcal{L}_{\mathsf{w}}(\mathscr{S})$ that occur as the word language of a
higher-order recursion scheme $\mathscr{S}$. Note that path languages and
languages of word schemes are both word languages over the set
$\tilde{\Sigma}$ of unary symbols considered as letters. They are connected by
the following proposition, a proof of which is given in Appendix C.222 The
models of $\mathsf{HORS}$ (used in model checking higher-order programs
[Kob09]) and word schemes (used in language-theoretic exploration of
downclosures [HKO16, CPSW16]) are somewhat different. Thus, we show an
explicit reduction between the two formalisms.

######  Proposition 6.

For every order-$n$ $\mathsf{HORS}$
$\mathscr{S}=(\Sigma,\mathcal{N},S,\mathcal{R})$ there exists an order-$n$
word scheme
$\mathscr{S}^{\prime}=(\Sigma^{\prime},\mathcal{N}^{\prime},S^{\prime},\mathcal{R}^{\prime})$
such that
$\mathcal{L}_{\mathsf{p}}(\mathscr{S})=\mathcal{L}_{\mathsf{w}}(\mathscr{S}^{\prime})$.

A consequence of [Kob09] and Prop. 6 is that the “post” language of higher-
order functional programs (i.e. the language corresponding to sequences of
newly spawned tasks) can be modeled as the language of a word scheme. Hence,
we define an _asynchronous program over $\mathsf{HORS}$_ as an asynchronous
program over the language class $\mathcal{H}$ and we can use the following
results on word schemes.

######  Theorem 7.

$\mathsf{HORS}$ and word schemes form effective full trios [CPSW16]. Emptiness
[KO11] and finiteness [Par17] of order-$n$ word schemes are ${(n-1)}\mathchar
45\relax\mathsf{EXPTIME}$-complete.

Now Theorems 3 and 4, together with Proposition 6 imply the decidability
results in Corollary 8. The undecidability result is a consequence of Theorem
5 and the undecidability of the $Z$-intersection problem for indexed languages
or equivalently, order-2 pushdown automata as shown in [Zet15]. Order-2
pushdown automata can be effectively turned into order-2 OI grammars [DG86],
which in turn can be translated into order-2 word schemes [Dam82]. A direct
(and independent) proof of undecidability of the $Z$-intersection problem for
order-2 word schemes has appeared in [Kob19, Theorem 4].

######  Corollary 8.

For asynchronous programs over $\mathsf{HORS}$: (1) Safety, termination, and
boundedness are decidable. (2) Configuration reachability, fair termination,
and fair starvation are undecidable already at order-2.

##  6\. A Direct Algorithm and Complexity Analysis

We say that _downclosures are computable_ for a language class $\mathcal{C}$
if for a given description of a language $L$ in $\mathcal{C}$, one can compute
an automaton for the regular language $\mathord{\downarrow}{L}$. A consequence
of Proposition 2 and Theorem 4 is that if one can compute downclosures for
some language class, then one can avoid the enumerative approaches of Section
4 and get a “direct algorithm.” The direct algorithm replaces each handler by
its downclosure and then invokes the decision procedure summarized in Theorem
4.

###  6.1. Higher-Order Recursion Schemes

The direct algorithm for asynchronous programs over $\mathsf{HORS}$ relies on
the recent breakthrough results on computing downclosures. [[Zet15, HKO16,
CPSW16]] Downclosures are effectively computable for $\mathcal{H}$.

Unfortunately, current techniques do not yet provide a complexity upper bound
based on the above theorem. To understand why, we describe the current
algorithm for computing downclosures. In [Zet15], it was shown that in a full
trio $\mathcal{C}$, downclosures are computable if and only if the _diagonal
problem_ for $\mathcal{C}$ is decidable. The latter asks, given a language
$L\subseteq\Sigma^{*}$, whether for every $k\in{\mathbb{N}}$, there is a word
$w\in L$ with $|w|_{\sigma}\geq k$ for every $\sigma\in\Sigma$. The diagonal
problem was then shown to be decidable for higher-order pushdown automata
[HKO16] and then for word schemes [CPSW16]. However, the algorithm from
[Zet15] to compute downclosures using an oracle for the diagonal problem
employs enumeration to compute a downclosure automaton. Thus, the enumeration
is hidden inside the downclosure computation.

We conjecture that downclosures can in fact be computed in elementary time
(for word schemes of fixed order). This would imply an elementary time
procedure for asynchronous programs over $\mathsf{HORS}$ as well.

###  6.2. Context Free Languages

For handlers over context-free languages, given e.g., as pushdown automata,
Ganty and Majumdar show an ${\mathsf{EXPSPACE}}$ upper bound. Precisely, the
algorithm of [GM12] constructs for each handler a polynomial-size Petri net
with certain guarantees (forming a so-called _adequate family of Petri nets_)
that accepts a Parikh equivalent language. These Petri nets are then used to
construct a larger Petri net, polynomial in the size of the asynchronous
program and the adequate family of Petri nets, in which the respective
property (safety, boundedness, or termination) can be phrased as a query
decidable in $\mathsf{EXPSPACE}$. A natural question is whether there is a
downclosure-based algorithm with the same asymptotic complexity.

Our goal is to replace the Parikh-equivalent Petri nets with Petri nets
recognizing the downclosure of a language. It is an easy consequence of
Proposition 2 that the resulting Petri nets can be used in place of the
adequate families of Petri nets in the procedures for safety, termination, and
boundedness of [GM12]. Thus, if we can ensure these Petri nets are polynomial
in the size of the handler, we get an ${\mathsf{EXPSPACE}}$ upper bound.
Unfortunately, a finite automaton for $\mathord{\downarrow}{L}$ may require
exponentially many states in the pushdown automaton [BLS15]. Thus a naive
approach gives a $\mathsf{2EXPSPACE}$ upper bound.

We show here that for each context-free language $L$, one can construct in
polynomial time a $1$-bounded Petri net accepting $\mathord{\downarrow}{L}$.
(Recall that a Petri net is $1$-bounded if every reachable marking has at most
one token in each place.) This is a language theoretic result of independent
interest. When used in the construction of [GM12], this matches the
${\mathsf{EXPSPACE}}$ upper bound.

As a byproduct, our translation yields a simple direct construction of a
finite automaton for $\mathord{\downarrow}{L}$ when $L$ is given as a pushdown
automaton. This is of independent interest because earlier constructions of
$\mathord{\downarrow}{L}$ always start from a context-free grammar and produce
(of necessity!) exponentially large NFAs [vL78, Cou91, BLS15].

We begin with some preliminary definitions.

#### Pushdown automata

If $\Gamma$ is an alphabet, we write
$\bar{\Gamma}=\\{\bar{\gamma}\mid\gamma\in\Gamma\\}$. Moreover, if
$x=\bar{\gamma}$, then we define $\bar{x}=\gamma$. For a word
$v\in(\Gamma\cup\bar{\Gamma})^{*}$, $v=v_{1}\cdots v_{n}$,
$v_{1},\ldots,v_{n}\in\Gamma\cup\bar{\Gamma}$, we set
$\bar{v}=\bar{v_{n}}\cdots\bar{v_{1}}$. A _pushdown automaton_ is a tuple
$\mathcal{A}=(Q,\Sigma,\Gamma,E,q_{0},q_{f})$, where $Q$ is a finite set of
_states_ , $\Sigma$ is its _input alphabet_ , $\Gamma$ is its _stack alphabet_
, $E$ is a finite set of _edges_ , $q_{0}\in Q$ is its _initial state_ , and
$F\subseteq Q$ is its set of _final states_. An edge is a four-tuple
$(p,R,v,q)$, where $p,q\in Q$, $R\subseteq\Sigma^{*}$ is a regular language,
and $v\in\Gamma\cup\bar{\Gamma}\cup\\{\varepsilon\\}$. We also write

$p\xrightarrow{R|v}q$

to denote an edge $(p,R,v,q)\in E$. Intuitively, it tells us that from state
$q$, we can read any word in $R$ as input and modify the stack as specified by
$v$. Here, $v\in\Gamma$ means we push $v$ onto the stack. Moreover,
$v\in\Gamma$, $v=\bar{\gamma}$, means we pop $\gamma$ from the stack. Finally,
$v=\varepsilon$ means we do not change the stack. Let us make this formal. A
_configuration_ of $\mathcal{A}$ is a pair $(q,w)$ with $q\in Q$ and
$w\in\Gamma^{*}$. For configurations $(q,w)$ and $(q^{\prime},w^{\prime})$, we
write $(q,w)\xrightarrow{u}(q^{\prime},w^{\prime})$ if there is an edge
$(q,R,v,q^{\prime})$ in $\mathcal{A}$ such that $u\in R$ and (i) if
$v=\varepsilon$, then $w^{\prime}=w$, (ii) if $v\in\Gamma$, then
$w^{\prime}=wv$ and (iii) if $v=\bar{\gamma}$ for $\gamma\in\Gamma$, then
$w=w^{\prime}\gamma$.

A _run_ in $\mathcal{A}$ is a sequence $(q_{0},w_{0}),\ldots,(q_{n},w_{n})$ of
configurations and words $u_{1},\ldots,u_{n}\in\Sigma^{*}$ such that
$(q_{i-1},w_{i-1})\xrightarrow{u_{i}}(q_{i},w_{i})$ for $1\leq i\leq n$. Its
_length_ is $n$ and its _initial_ and _final configuration_ are
$(q_{0},w_{0})$ and $(q_{n},w_{n})$, respectively. The run is said to _read_
the word $u_{1}\cdots u_{n}$. The _stack height_ of the run is defined as
$\max\\{|w_{i}|\mid 0\leq i\leq n\\}$. We call the run _positive_ (resp.
_dually positive_) if $|w_{i}|\geq|w_{0}|$ (resp. $|w_{i}|\geq|w_{n}|$) for
every $1\leq i\leq n$, i.e. if the stack never drops below its initial height
(resp. is always above its final height).

We write $(q,w)\xRightarrow{u}(q^{\prime},w^{\prime})$ for configurations
$(q,w),(q^{\prime},w^{\prime})$ if there is a run with initial configuration
$(q,w)$ and final configuration $(q^{\prime},w^{\prime})$ that reads $u$. If
there is such a run with stack height $\leq h$, then we write
$(q,w)\xRightarrow{u}_{h}(q^{\prime},w^{\prime})$. The _language accepted by
$\mathcal{A}$_ is

$\mathsf{L}(\mathcal{A})=\\{u\in\Sigma^{*}\mid(q_{0},\varepsilon)\xRightarrow{u}(q_{f},\varepsilon)\\}.$

There is also a language accepted with bounded stack height. For
$h\in{\mathbb{N}}$, we define

$\mathsf{L}_{h}(\mathcal{A})=\\{u\in\Sigma^{*}\mid(q_{0},\varepsilon)\xRightarrow{u}_{h}(q_{f},\varepsilon)\\}.$

Thus, $\mathsf{L}_{h}(\mathcal{A})$ is the set of words accepted by
$\mathcal{A}$ using runs of stack height at most $h$.

In order to exploit the symmetry between forward and backward computations in
pushdown automata, we will consider dual pushdown automata. The _dual
automaton_ of $\mathcal{A}$, denoted $\bar{\mathcal{A}}$, is obtained from
$\mathcal{A}$ by changing each edge $p\xrightarrow{R|v}q$ into
$q\xrightarrow{R^{\mathsf{rev}}|\bar{v}}p$. Then
$\mathsf{L}(\bar{\mathcal{A}})=\mathsf{L}(\mathcal{A})^{\mathsf{rev}}$. We
will sometimes argue by _duality_ , which is the principle that every
statement that is true for any $\mathcal{A}$ is also true for any
$\bar{\mathcal{A}}$.

#### Petri nets

A _(labeled) Petri net_ is a tuple
$N=(\Sigma,S,T,\partial_{0},\partial_{1},\lambda,\mathbf{m}_{0},\mathbf{m}_{f})$
where $\Sigma$ is its _input alphabet_ , $S$ is a finite set of _places_ , $T$
is a finite set of _transitions_ , $\partial_{0},\partial_{1}\colon
T\to{\mathbb{M}[S]}$ are maps that specify an _input marking_
$\partial_{0}(t)$ and an _output marking_ $\partial_{1}(t)$ for each
transition $t\in T$, $\lambda\colon T\to\Sigma\cup\\{\varepsilon\\}$ assigns
labels to transitions, and $\mathbf{m}_{0},\mathbf{m}_{f}$ are its _initial_
and _final marking_. More generally, multisets $\mathbf{m}\in{\mathbb{M}[S]}$
are called _markings_ of $N$.

For markings $\mathbf{m}_{1},\mathbf{m}_{2}\in{\mathbb{M}[S]}$ and
$a\in\Sigma\cup\\{\varepsilon\\}$, we write
$\mathbf{m}_{1}\xrightarrow{a}\mathbf{m}_{2}$ if there is a transition $t\in
T$ with $\lambda(t)=a$, $\mathbf{m}_{1}\geq\partial_{0}(t)$, and
$\mathbf{m}_{2}=\mathbf{m}_{1}\ominus\partial_{0}(t)\oplus\partial_{1}(t)$.
Moreover, we write $\mathbf{m}_{1}\xRightarrow{w}\mathbf{m}_{2}$ if there are
$n\in{\mathbb{N}}$, $a_{1},\ldots,a_{n}\in\Sigma\cup\\{\varepsilon\\}$, and
markings $\mathbf{m}^{\prime}_{0},\ldots,\mathbf{m}^{\prime}_{n}$ such that
$w=a_{1}\cdots a_{n}$ and
$\mathbf{m}_{1}=\mathbf{m}^{\prime}_{0}\xrightarrow{a_{1}}\mathbf{m}^{\prime}_{1}\xrightarrow{a_{2}}\cdots\xrightarrow{a_{n}}\mathbf{m}^{\prime}_{n}=\mathbf{m}_{2}$.
Furthermore, we write $\mathbf{m}_{1}\xRightarrow{}\mathbf{m}_{2}$ if there
exists a $w\in\Sigma^{*}$ with $\mathbf{m}_{1}\xRightarrow{w}\mathbf{m}_{2}$.
The _language accepted by $N$_ is
$\mathsf{L}(N)=\\{w\in\Sigma^{*}\mid\mathbf{m}_{0}\xRightarrow{w}\mathbf{m}_{f}\\}$.

For $k\in{\mathbb{N}}$, a Petri net $N$ is _$k$ -bounded_ if for every marking
$\mathbf{m}\in{\mathbb{M}[S]}$ with $\mathbf{m}_{0}\xRightarrow{}\mathbf{m}$,
we have $\lvert{\mathbf{m}}\rvert\leq k$.

Our main results are as follows.

######  Theorem 9 (Succinct Downclosures for PDAs).

Given a pushdown automaton $\mathcal{A}$, one can construct in polynomial time
a pushdown automaton $\hat{\mathcal{A}}$ so that
$\mathord{\downarrow}{\mathsf{L}(\hat{\mathcal{A}})}=\mathord{\downarrow}{\mathsf{L}(\mathcal{A})}$.
Moreover, we have
$\mathsf{L}(\hat{\mathcal{A}})=\mathsf{L}_{h}(\hat{\mathcal{A}})$ for some
bound $h$ that is polynomial in the size of $\mathcal{A}$.

As a pushdown automaton with bounded stack can be simulated by a 1-bounded
Petri net (essentially, by keeping places for each position in the stack), we
get the following corollary and also the promised ${\mathsf{EXPSPACE}}$ upper
bound.

######  Corollary 10.

Given a pushdown automaton $\mathcal{A}$, one can construct in polynomial time
a $1$-bounded Petri net $N$ with
$\mathsf{L}(N)=\mathord{\downarrow}{\mathsf{L}(\mathcal{A})}$.

We now prove Theorem 9. The _augmented automaton_
$\hat{\mathcal{A}}=(Q,\Sigma,\hat{\Gamma},\hat{E},q_{0},q_{f})$ is defined as
follows. We first compute for any $p,q\in Q$ the subalphabet
$\Delta_{p,q}(\mathcal{A})\subseteq\Sigma$ with

$\Delta_{p,q}(\mathcal{A})=\\{a\in\Sigma\mid\exists u\in
M_{p,q}(\mathcal{A}),~{}|u|_{a}\geq 1\\},$

where $M_{p,q}(\mathcal{A})=\\{u\in\Sigma^{*}\mid\exists
v\in\Gamma^{*}\colon(p,\varepsilon)\xRightarrow{u}(p,v),~{}(q,v)\xRightarrow{}(q,\varepsilon)\\}$.
Note that it is easy to construct in polynomial time a pushdown automaton
$\mathcal{A}_{p,q}$ for the language $M_{p,q}(\mathcal{A})$:
$\mathcal{A}_{p,q}$ has a set $Q_{p}\cup Q_{q}$ of states consisting of two
disjoint copies of the states of $\mathcal{A}$. The transitions between two
states in $Q_{p}$ are inherited from $\mathcal{A}$ while for two states in
$Q_{q}$ we replace the input on any transition by $\varepsilon$ but retain the
stack operations from $\mathcal{A}$. The start state is $p\in Q_{p}$ and the
final state is $q\in Q_{q}$. There is an $\varepsilon$-transition from $p\in
Q_{p}$ to $q\in Q_{q}$. This concludes the construction of
$\mathcal{A}_{p,q}$.

Since $a\in\Delta_{p,q}(\mathcal{A})$ iff
$M_{p,q}(\mathcal{A})\cap\Sigma^{*}a\Sigma^{*}\neq\emptyset$, we can decide in
polynomial time whether a given $a\in\Sigma$ belongs to
$\Delta_{p,q}(\mathcal{A})$ by checking the PDA for
$M_{p,q}(\mathcal{A})\cap\Sigma^{*}a\Sigma^{*}\neq\emptyset$ obtained by
product construction for emptiness. Thus, we can compute
$\Delta_{p,q}(\mathcal{A})$ in polynomial time. We construct
$\hat{\mathcal{A}}$ as follows. For any $p,q\in Q$, we introduce a fresh stack
symbol $[p,q]$ and then we add edges

$\displaystyle p\xrightarrow{\Delta_{p,q}(\mathcal{A})^{*}|[p,q]}p,$
$\displaystyle
q\xrightarrow{\Delta_{q,p}(\bar{\mathcal{A}})^{*}|\overline{[p,q]}}q.$ (4)

The following Lemma tells us that $\mathsf{L}(\hat{\mathcal{A}})$ has the same
downward closure as ${\mathsf{\mathcal{A}}}$.

######  Lemma 11.

$\mathsf{L}(\mathcal{A})\subseteq\mathsf{L}(\hat{\mathcal{A}})\subseteq\mathord{\downarrow}{\mathsf{L}(\mathcal{A})}$.

######  Proof 6.1.

Since the inclusion
$\mathsf{L}(\mathcal{A})\subseteq\mathsf{L}(\hat{\mathcal{A}})$ is obvious, we
prove
$\mathsf{L}(\hat{\mathcal{A}})\subseteq\mathord{\downarrow}{\mathsf{L}(\mathcal{A})}$.
We proceed by induction on the number $m$ of executions of new edges (i.e.
those from Eq. 4). More specifically, we show that if
$u\in\mathsf{L}(\hat{\mathcal{A}})$ is accepted using $m$ executions of new
edges, then there is a $u^{\prime}\in\mathsf{L}(\hat{\mathcal{A}})$ such that
$u\sqsubseteq u^{\prime}$ and $u^{\prime}$ is accepted using $<m$ executions
of new edges.

Suppose $u$ is accepted using a run $\rho$ with $m>0$ executions of new edges.
Then $\rho$ must apply one edge
$p\xrightarrow{\Delta_{p,q}(\mathcal{A})|[p,q]}p$ and thus also the edge
$q\xrightarrow{\Delta_{q,p}(\bar{\mathcal{A}})|\overline{[p,q]}}q$ to remove
the letter $[p,q]$ from the stack. Thus, $\rho$ decomposes as
$\rho=\rho_{1}\rho_{2}\rho_{3}\rho_{4}\rho_{5}$, where $\rho_{2}$ and
$\rho_{4}$ are the executions of the new edges. Let
$u=u_{1}u_{2}u_{3}u_{4}u_{5}$ be the corresponding decomposition of $u$.

The run $\rho_{1}$ must end in state $p$ and with some stack content
$w\in\Gamma^{*}$. Then, $\rho_{3}$ is a run from $(p,w[p,q])$ to $(q,w[p,q])$
and $\rho_{5}$ is a run from $(q,w)$ to $(q_{f},\varepsilon)$ with $q_{f}\in
F$.

Since $u_{2}$ and $u_{4}$ are read while executing the new edges, we have
$u_{2}\in\Delta_{p,q}(\mathcal{A})^{*}$ and
$u_{4}\in\Delta_{q,p}(\bar{\mathcal{A}})^{*}$. We can therefore write
$u_{2}=r_{1}\cdots r_{k}$ and $u_{4}=s_{1}\cdots s_{\ell}$ with
$r_{1},\ldots,r_{k}\in\Delta_{p,q}(\mathcal{A})$ and
$s_{1},\ldots,s_{\ell}\in\Delta_{q,p}(\bar{\mathcal{A}})$. By definition, this
means for each $1\leq i\leq k$, there is a word $\tilde{r}_{i}\in
M_{p,q}(\mathcal{A})$ that contains the letter $r_{i}$. Likewise, for every
$1\leq i\leq\ell$, there is a $\tilde{s}_{i}\in M_{q,p}(\bar{\mathcal{A}})$
that contains $s_{i}$.

Since $\tilde{r}_{i}\in M_{p,q}(\mathcal{A})$ and $\tilde{s}_{j}\in
M_{q,p}(\bar{\mathcal{A}})$ for $1\leq i\leq k$ and $1\leq j\leq\ell$, there
are words $x_{i}$ and $y_{j}$ in $\Gamma^{*}$ so that

$\displaystyle(p,\varepsilon)\xRightarrow{\tilde{r}_{i}}(p,x_{i})$ and
$\displaystyle(q,x_{i})\xRightarrow{}(q,\varepsilon)$
$\displaystyle(p,\varepsilon)\xRightarrow{}(p,y_{j})$ and
$\displaystyle(q,y_{i})\xRightarrow{\tilde{s}_{j}}(q,\varepsilon)$

We can therefore construct a new run
$\rho^{\prime}=\rho_{1}\rho^{\prime}_{2}\rho^{\prime}_{3}\rho^{\prime}_{4}\rho_{5}$,
where

$\displaystyle\rho^{\prime}_{2}:(p,w)\xRightarrow{\tilde{r}_{1}}\cdots\xRightarrow{\tilde{r}_{k}}(p,wx_{1}\cdots
x_{k})\xRightarrow{}\cdots\xRightarrow{}(p,wx_{1}\cdots x_{k}y_{\ell}\cdots
y_{1})$ $\displaystyle\rho^{\prime}_{4}:(q,wx_{1}\cdots x_{k}y_{\ell}\cdots
y_{1})\xRightarrow{\tilde{s}_{1}}\cdots\xRightarrow{\tilde{s}_{\ell}}(q,wx_{1}\cdots
x_{k})\xRightarrow{}\cdots\xRightarrow{}(q,w).$

Moreover, since $\rho_{3}$ is a positive run from $(p,w)$ to $(q,w)$, we
obtain $\rho^{\prime}_{3}$ from $\rho_{3}$ by replacing the prefix $w$ of
every stack by $wx_{1}\cdots x_{k}y_{1}\cdots y_{\ell}$.

Then $\rho^{\prime}$ reads some word
$u_{1}\tilde{r}_{1}\cdots\tilde{r}_{k}fu_{3}\tilde{s}_{1}\cdots\tilde{s}_{\ell}gu_{5}$
for $f,g\in\Sigma^{*}$. Note that since $r_{i}$ occurs in $\tilde{r}_{i}$ and
$s_{i}$ occurs in $\tilde{s}_{j}$, we have
$u=u_{1}u_{2}u_{3}u_{4}u_{5}\sqsubseteq
u_{1}\tilde{r}_{1}\cdots\tilde{r}_{k}fu_{3}\tilde{s}_{1}\cdots\tilde{s}_{\ell}gu_{5}$.

We now show that every word in $\hat{\mathcal{A}}$ is accepted by a run with
bounded stack height.

######  Lemma 12.

$\mathsf{L}(\hat{\mathcal{A}})=\mathsf{L}_{h}(\hat{\mathcal{A}})$, where
$h=2|Q|^{2}$.

Before we prove Lemma 12, we need another observation. Just like Lemma 11, one
can show that for any $p,q\in Q$, we have $M_{p,q}(\mathcal{A})\subseteq
M_{p,q}(\hat{\mathcal{A}})\subseteq\mathord{\downarrow}{M_{p,q}(\mathcal{A})}$
and in particular

$\displaystyle\Delta_{p,q}(\mathcal{A})=\Delta_{p,q}(\hat{\mathcal{A}})$
$\displaystyle\Delta_{q,p}(\bar{\mathcal{A}})=\Delta_{q,p}(\bar{\hat{\mathcal{A}}}),$
(5)

where the second identity follows from the first: Duality yields
$\Delta_{q,p}(\bar{\mathcal{A}})=\Delta_{q,p}(\hat{\bar{\mathcal{A}}})$ and
since $\hat{\bar{\mathcal{A}}}$ and $\bar{\hat{\mathcal{A}}}$ are isomorphic
(i.e. they are the same up to a renaming of stack symbols), we have
$\Delta_{q,p}(\hat{\bar{\mathcal{A}}})=\Delta_{q,p}(\bar{\hat{\mathcal{A}}})$.

We now prove Lemma 12. Let $u\in\mathsf{L}(\hat{\mathcal{A}})$. We show that
any minimal length accepting run $\rho$ reading $u$ must have stack height
$\leq h$ and hence $u\in\mathsf{L}_{h}(\hat{\mathcal{A}})$.

Suppose the stack height of $\rho$ is larger than $h=2|Q|^{2}$.

#### Claim:

$\rho$ decomposes into runs $\rho_{1},\rho_{2},\rho_{3},\rho_{4},\rho_{5}$
reading $u_{1},u_{2},u_{3},u_{4},u_{5}$, respectively, so that there are
$p,q\in Q$ and $w\in\Gamma^{*}$ with

  * •

$\rho_{2}$ is a positive run from $(p,w)$ to $(p,wv)$ of length $\geq 2$

  * •

$\rho_{3}$ is a positive run from $(p,wv)$ to $(q,wv)$

  * •

$\rho_{4}$ is a dually positive run from $(q,wv)$ to $(q,w)$

Let $c_{h}$ be a configuration along $\rho$ with stack height at least
$2|Q|^{2}+1$. Then there exist $|Q|^{2}$ configurations
$c_{2}\xRightarrow{}c_{4}\xRightarrow{}\cdots\xRightarrow{}c_{2|Q|^{2}}\xRightarrow{}c_{h}$
along $\rho$ such that $c_{2i}$ is the last time that the stack height is $2i$
before visiting $c_{h}$. Symmetrically, we have
$c_{h}\xRightarrow{}c^{\prime}_{2|Q|^{2}}\xRightarrow{}\cdots
c^{\prime}_{4}\xRightarrow{}c^{\prime}_{2}$ where $c^{\prime}_{2i}$ is the
first occurrence of stack height $2i$ after visiting $c_{h}$. Clearly by
definition the run between consecutive $c_{2i}$ (resp. $c^{\prime}_{2i}$)
configurations is positive (resp. dually positive). Additionally, the length
of the run between them must be at least two, because the stack heights differ
by two. Considering the pair of states at each $c_{2i},c^{\prime}_{2i}$, there
are $|Q|^{2}$ possibilities. Hence there must exist indices $2i<2j$ such that
the $c_{2i}$ and $c_{2j}$ have the same state $p$ and $c^{\prime}_{2i}$ and
$c^{\prime}_{2j}$ have the same state $q$. It is now clear that
$\rho_{2}\colon c_{2i}\xRightarrow{}c_{2j}$, $\rho_{3}\colon
c_{2j}\xRightarrow{}c^{\prime}_{2j}$ and $\rho_{4}\colon
c^{\prime}_{2j}\xRightarrow{}c^{\prime}_{2i}$ satisfy the conditions of the
claim.

These conditions imply that $u_{2}\in M_{p,q}(\hat{\mathcal{A}})$ and
$u_{4}\in M_{q,p}(\bar{\hat{\mathcal{A}}})$. Therefore, we have
$u_{2}\in\Delta_{p,q}(\hat{\mathcal{A}})^{*}=\Delta_{p,q}(\mathcal{A})^{*}$
and
$u_{4}\in\Delta_{q,p}(\bar{\hat{\mathcal{A}}})^{*}=\Delta_{q,p}(\bar{\mathcal{A}})^{*}$
by Eq. 5.

We obtain the run $\rho^{\prime}$ from $\rho$ as follows. We replace
$\rho_{2}$ by a single execution of the edge
$p\xrightarrow{\Delta_{p,q}(\mathcal{A})^{*}|[p,q]}p$ reading $u_{2}$.
Moreover, we replace $\rho_{4}$ by a single execution of the edge
$q\xrightarrow{\Delta_{q,p}(\bar{\mathcal{A}})^{*}|\overline{[p,q]}}q$. Then
$\rho^{\prime}$ is clearly a run reading $u=u_{1}u_{2}u_{3}u_{4}u_{5}$.
Furthermore, since $\rho_{2}$ has length $\geq 2$, but the single edge used
instead in $\rho^{\prime}$ only incurs length $1$, $\rho^{\prime}$ is strictly
shorter than $\rho$. This is in contradiction to the minimal length of $\rho$.
This completes the proof of Lemma 12 and thus also Theorem 9.

######  Remark 6.2.

The augmented automaton $\hat{\mathcal{A}}$ yields a very simple construction
of a finite automaton (of exponential size) for
$\mathord{\downarrow}{\mathsf{L}(\mathcal{A})}$. First, it is easy to
construct a finite automaton for $\mathsf{L}_{h}(\hat{\mathcal{A}})$. Then, by
introducing $\varepsilon$-edges, we get a finite automaton for
$\mathord{\downarrow}{\mathsf{L}_{h}(\hat{\mathcal{A}})}$, which, by Lemmas 11
and 12, equals $\mathord{\downarrow}{\mathsf{L}(\mathcal{A})}$.

It is now straightforward to construct a polynomial size $1$-bounded Petri net
$N=(\Sigma,S,T,\partial_{0},\partial_{0},\mathbf{m}_{0},\mathbf{m}_{f})$ with
$\mathsf{L}(N)=\mathsf{L}_{h}(\hat{\mathcal{A}})$, thus proving Corollary 10.
First, by adding states, we turn $\hat{\mathcal{A}}$ into a pushdown automaton
$\mathcal{A}^{\prime}=(Q^{\prime},\Sigma,\hat{\Gamma},E^{\prime},q_{0},q_{f})$,
where every edge reads at most one letter, i.e. every edge
$p\xrightarrow{R|v}q$ in $\mathcal{A}^{\prime}$ has $R=\\{x\\}$ for some
$x\in\Sigma\cup\\{\varepsilon\\}$ (this is done by ‘pasting’ the automaton for
$R$ in place of the edge). Moreover, we add $\varepsilon$-edges, so that for
every edge $p\xrightarrow{\\{x\\}|v}q$, we also have an edge
$p\xrightarrow{\\{\varepsilon\\}|v}q$. Then clearly
$\mathsf{L}_{h}(\mathcal{A}^{\prime})=\mathord{\downarrow}{\mathsf{L}_{h}(\hat{\mathcal{A}})}=\mathord{\downarrow}{\mathsf{L}(\mathcal{A})}$.

The net $N$ has a place $p$ for each state $p$ of $\mathcal{A}^{\prime}$ and
for each $i\in\\{1,\ldots,h\\}$ and $\gamma\in\hat{\Gamma}$, it has a place
$(i,\gamma)$. Moreover, for each $i\in\\{0,\ldots,h\\}$, it has a place
$s_{i}$. Here, the idea is that a configuration
$c=(p,\gamma_{1}\cdots\gamma_{n})$ of $\mathcal{A}^{\prime}$ with
$\gamma_{1},\ldots,\gamma_{n}\in\hat{\Gamma}$ is represented as a marking
$\mathbf{m}_{c}={\llbracket
p,(1,\gamma_{1}),\ldots,(n,\gamma_{n}),s_{n}\rrbracket}$. We call a marking of
this form a _stack marking_ and will argue that every reachable marking in $N$
is a stack marking. The transitions in $N$ correspond to edges in
$\mathcal{A}^{\prime}$. For each edge $p\xrightarrow{\\{x\\}|v}q$ in
$\hat{\mathcal{A}}$, we add the following transitions:

  * •

if $v=\bar{\gamma}$ for some $\gamma\in\hat{\Gamma}$, then we have for every
$1\leq n\leq h$ a transition $t$ with $\partial_{0}(t)={\llbracket
p,(n,\gamma),s_{n}\rrbracket}$, $\partial_{1}(t)={\llbracket
q,s_{n-1}\rrbracket}$, and $\lambda(t)=x$.

  * •

if $v\in\hat{\Gamma}$, then for every $0\leq n<h$, we add a transition $t$
with $\partial_{0}(t)={\llbracket p,s_{n}\rrbracket}$,
$\partial_{1}(t)={\llbracket q,(n+1,v),s_{n+1}\rrbracket}$, and
$\lambda(t)=x$.

  * •

if $v=\varepsilon$, then we add a transition $t$ with
$\partial_{0}(t)={\llbracket p\rrbracket}$, $\partial_{1}(t)={\llbracket
q\rrbracket}$, and $\lambda(t)=x$.

Then clearly every reachable marking is a stack marking and we have
$c\xrightarrow{x}c^{\prime}$ for configurations $c,c^{\prime}$ of
$\mathcal{A}^{\prime}$ of stack height $\leq h$ if and only if
$\mathbf{m}_{c}\xrightarrow{x}\mathbf{m}_{c^{\prime}}$. Therefore, if we set
$\mathbf{m}_{0}={\llbracket q_{0},s_{0}\rrbracket}$ and
$\mathbf{m}_{f}={\llbracket q_{f},s_{0}\rrbracket}$ as initial and final
marking, we have
$\mathsf{L}(N)=\mathsf{L}_{h}(\mathcal{A}^{\prime})=\mathord{\downarrow}{\mathsf{L}(\mathcal{A})}$.
This completes the proof of Corollary 10.

## References

  * [ABJ98] Parosh Aziz Abdulla, Ahmed Bouajjani, and Bengt Jonsson.  On-the-fly analysis of systems with unbounded, lossy FIFO channels.  In Proceedings of the 10th International Conference on Computer Aided Verification (CAV 1998), pages 305–318, 1998.  doi:10.1007/BFb0028754.
  * [ABQ09] Mohamed Faouzi Atig, Ahmed Bouajjani, and Shaz Qadeer.  Context-bounded analysis for concurrent programs with dynamic creation of threads.  In Tools and Algorithms for the Construction and Analysis of Systems, 15th International Conference, TACAS 2009, Held as Part of the Joint European Conferences on Theory and Practice of Software, ETAPS 2009, York, UK, March 22-29, 2009. Proceedings, volume 5505 of Lecture Notes in Computer Science, pages 107–123. Springer, 2009.  doi:10.1007/978-3-642-00768-2\\_11.
  * [Aho68] Alfred V. Aho.  Indexed grammars - an extension of context-free grammars.  J. ACM, 15(4):647–671, 1968.  doi:10.1145/321479.321488.
  * [Ber79] Jean Berstel.  Transductions and context-free languages.  Teubner-Verlag, 1979.
  * [BLS15] Georg Bachmeier, Michael Luttenberger, and Maximilian Schlund.  Finite automata for the sub- and superword closure of cfls: Descriptional and computational complexity.  In Language and Automata Theory and Applications - 9th International Conference, LATA 2015, Nice, France, March 2-6, 2015, Proceedings, volume 8977 of Lecture Notes in Computer Science, pages 473–485. Springer, 2015.  doi:10.1007/978-3-319-15579-1\\_37.
  * [Cou91] Bruno Courcelle.  On constructing obstruction sets of words.  Bulletin of the EATCS, 44:178–186, 1991.
  * [CPSW16] Lorenzo Clemente, Paweł Parys, Sylvain Salvati, and Igor Walukiewicz.  The diagonal problem for higher-order recursion schemes is decidable.  In Proceedings of the 31st Annual ACM/IEEE Symposium on Logic in Computer Science, LICS ’16, New York, NY, USA, July 5-8, 2016, pages 96–105. ACM, 2016.  doi:10.1145/2933575.2934527.
  * [CV07] Rohit Chadha and Mahesh Viswanathan.  Decidability results for well-structured transition systems with auxiliary storage.  In CONCUR 2007 - Concurrency Theory, 18th International Conference, CONCUR 2007, Lisbon, Portugal, September 3-8, 2007, Proceedings, volume 4703 of Lecture Notes in Computer Science, pages 136–150. Springer, 2007.  doi:10.1007/978-3-540-74407-8\\_10.
  * [Dam82] Werner Damm.  The IO-and OI-hierarchies.  Theoretical Computer Science, 20(2):95–207, 1982.
  * [DFS98] Catherine Dufourd, Alain Finkel, and Philippe Schnoebelen.  Reset nets between decidability and undecidability.  In Automata, Languages and Programming, 25th International Colloquium, ICALP’98, Aalborg, Denmark, July 13-17, 1998, Proceedings, volume 1443 of Lecture Notes in Computer Science, pages 103–115. Springer, 1998.  doi:10.1007/BFb0055044.
  * [DG86] Werner Damm and Andreas Goerdt.  An automata-theoretical characterization of the OI-hierarchy.  Information and Control, 71(1):1–32, 1986.
  * [GM12] Pierre Ganty and Rupak Majumdar.  Algorithmic verification of asynchronous programs.  ACM Transactions on Programming Languages and Systems (TOPLAS), 34(1):6, 2012.  doi:10.1145/2160910.2160915.
  * [GRB07] Gilles Geeraerts, Jean-François Raskin, and Laurent Van Begin.  Well-structured languages.  Acta Informatica, 44(3-4):249–288, 2007.  doi:10.1007/s00236-007-0050-3.
  * [Gre78] Sheila A. Greibach.  Remarks on blind and partially blind one-way multicounter machines.  Theoretical Computer Science, 7(3):311 – 324, 1978.  doi:10.1016/0304-3975(78)90020-8.
  * [Gre16] Charles Grellois.  Semantics of linear logic and higher-order model-checking.  PhD thesis, Univeristé Denis Diderot Paris 7, 2016.
  * [Hai69] Leonard H Haines.  On free monoids partially ordered by embedding.  Journal of Combinatorial Theory, 6(1):94–98, 1969.
  * [HKO16] Matthew Hague, Jonathan Kochems, and C.-H. Luke Ong.  Unboundedness and downward closures of higher-order pushdown automata.  In Proceedings of the 43rd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2016, St. Petersburg, FL, USA, January 20 - 22, 2016, pages 151–163. ACM, 2016.  doi:10.1145/2837614.2837627.
  * [HMOS08] Matthew Hague, Andrzej S. Murawski, C.-H. Luke Ong, and Olivier Serre.  Collapsible pushdown automata and recursion schemes.  In Proceedings of the Twenty-Third Annual IEEE Symposium on Logic in Computer Science, LICS 2008, 24-27 June 2008, Pittsburgh, PA, USA, pages 452–461, 2008.  doi:10.1109/LICS.2008.34.
  * [HMU07] John E. Hopcroft, Rajeev Motwani, and Jeffrey D. Ullman.  Introduction to automata theory, languages, and computation, 3rd Edition.  Pearson international edition. Addison-Wesley, 2007.
  * [Jan79] Matthias Jantzen.  On the hierarchy of Petri net languages.  RAIRO - Theoretical Informatics and Applications - Informatique Théorique et Applications, 13(1):19–30, 1979.  URL: http://www.numdam.org/item?id=ITA_1979__13_1_19_0.
  * [JM07] Ranjit Jhala and Rupak Majumdar.  Interprocedural analysis of asynchronous programs.  In Proceedings of the 34th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2007, Nice, France, January 17-19, 2007, pages 339–350. ACM, 2007.  doi:10.1145/1190216.1190266.
  * [KO11] Naoki Kobayashi and C.-H. Luke Ong.  Complexity of model checking recursion schemes for fragments of the modal mu-calculus.  Logical Methods in Computer Science, 7(4), 2011.
  * [Kob09] Naoki Kobayashi.  Types and higher-order recursion schemes for verification of higher-order programs.  In Proceedings of the 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL 2009, Savannah, GA, USA, January 21-23, 2009, pages 416–428, 2009.  doi:10.1145/1480881.1480933.
  * [Kob19] Naoki Kobayashi.  Inclusion between the frontier language of a non-deterministic recursive program scheme and the Dyck language is undecidable.  Theoretical Computer Science, 777:409–416, 2019.
  * [Mas74] AN Maslov.  The hierarchy of indexed languages of an arbitrary level.  Doklady Akademii Nauk, 217(5):1013–1016, 1974.
  * [May03] Richard Mayr.  Undecidable problems in unreliable computations.  Theoretical Computer Science, 297(1-3):337–354, 2003.
  * [Ong15] Luke Ong.  Higher-order model checking: An overview.  In 30th Annual ACM/IEEE Symposium on Logic in Computer Science, LICS 2015, Kyoto, Japan, July 6-10, 2015, pages 1–15, 2015.  doi:10.1109/LICS.2015.9.
  * [Par17] Paweł Parys.  The complexity of the diagonal problem for recursion schemes.  In 37th IARCS Annual Conference on Foundations of Software Technology and Theoretical Computer Science, FSTTCS 2017, December 11-15, 2017, Kanpur, India, volume 93 of LIPIcs, pages 45:1–45:14. Schloss Dagstuhl - Leibniz-Zentrum für Informatik, 2017.  doi:10.4230/LIPIcs.FSTTCS.2017.45.
  * [Sip97] Michael Sipser.  Introduction to the theory of computation.  PWS Publishing Company, 1997.
  * [SV06] Koushik Sen and Mahesh Viswanathan.  Model checking multithreaded programs with asynchronous atomic methods.  In Computer Aided Verification, 18th International Conference, CAV 2006, Seattle, WA, USA, August 17-20, 2006, Proceedings, volume 4144 of Lecture Notes in Computer Science, pages 300–314. Springer, 2006.  doi:10.1007/11817963\\_29.
  * [TZ19] Ramanathan S. Thinniyam and Georg Zetzsche.  Regular separability and intersection emptiness are independent problems.  In Proceedings of FSTTCS 2019, volume 150 of Leibniz International Proceedings in Informatics (LIPIcs), pages 51:1–51:15, Dagstuhl, Germany, 2019. Schloss Dagstuhl–Leibniz-Zentrum fuer Informatik.  doi:10.4230/LIPIcs.FSTTCS.2019.51.
  * [vL78] Jan van Leeuwen.  Effective constructions in well-partially-ordered free monoids.  Discrete Mathematics, 21(3):237–252, 1978.  doi:10.1016/0012-365X(78)90156-5.
  * [Zet15] Georg Zetzsche.  An approach to computing downward closures.  In ICALP 2015, volume 9135, pages 440–451. Springer, 2015.  The undecidability of $Z$ intersection is shown in the full version: http://arxiv.org/abs/1503.01068.

##  Appendix A Compiling away internal actions

We have commented in the examples of Section 2 that internal actions and
internal updates of the global state are useful in modeling asynchronous
programs from their programming language syntax. Indeed, we note that the
definition of asynchronous programs in [GM12] additionally uses a separate
alphabet of _internal actions_ , in addition to the alphabet of handler posts.
We show how a model of asynchronous programs with internal actions can be
reduced to our, simpler, model.

Let $\mathcal{C}$ be a language class over an alphabet $\Sigma$ of handler
names. The definition of asynchronous programs with internal actions, as used
by [SV06, JM07, GM12], is as follows.333 The language class $\mathcal{C}$ in
[GM12] is fixed to be the class of context free languages. Their definition
generalizes to any language class.  An asynchronous program over $\mathcal{C}$
with _internal actions_ (aka $\mathsf{AP}$ over $\mathcal{C}$ with internal
actions) is a tuple
$\mathfrak{P}=(D,\Sigma,\Sigma_{\mathsf{i}},\mathscr{L},R,d_{0},\mathbf{m}_{0}),$
where $D$, $\Sigma$, $d_{0}$, $\mathbf{m}_{0}$ are as in Definition 2,
$\Sigma_{\mathsf{i}}$ is an alphabet of internal actions disjoint from
$\Sigma$, the set $\mathscr{L}=(L_{\sigma})_{\sigma\in\Sigma}$ consists of
languages from $\mathcal{C}$ (one for each handler $\sigma\in\Sigma)$, and
$R=(D,\Sigma\cup\Sigma_{\mathsf{i}},\delta)$ a deterministic finite state
automaton where $D$ is the set of states, $\Sigma\cup\Sigma_{\mathsf{i}}$ the
alphabet and $\delta$ the transition relation specifying the effect of each
internal action on the global state $D$. We will write
$d\overset{w}{\underset{R}{\Rightarrow}^{*}}d^{\prime}$ to mean that there is
a sequence of transitions with labels $w_{1}w_{2}...w_{n}=w$ in the automaton
$R$ using which we can reach $d^{\prime}$ from $d$.

For alphabets $\Sigma,\Sigma^{\prime}$ with $\Sigma\subseteq\Sigma^{\prime}$,
the Parikh map
${\mathsf{Parikh}}\colon\Sigma^{\prime*}\rightarrow{\mathbb{M}[\Sigma]}$ maps
a word $w\in\Sigma^{\prime*}$ to a multiset ${\mathsf{Parikh}}(w)$ such that
${\mathsf{Parikh}}(w)(a)$ is the number of occurrences of $a$ in $w$ for each
$a\in\Sigma$. For example, ${\mathsf{Parikh}}(abbab)(a)=2$,
${\mathsf{Parikh}}(abbab)(b)=3$ and
${\mathsf{Parikh}}(\varepsilon)={\llbracket\rrbracket}$. For a language $L$,
we define ${\mathsf{Parikh}}(L)={\\{{\mathsf{Parikh}}(w)\mid w\in L\\}}$. If
the alphabet $\Sigma$ is not clear from the context, we write
${\mathsf{Parikh}}_{\Sigma}$ (usually $\Sigma^{\prime}=\Sigma$).

The semantics of a $\mathfrak{P}$ is given as a labeled transition system over
the set of configurations, with a transition relation
$\rightarrow\subseteq(D\times{\mathbb{M}[\Sigma]})\times\Sigma\times(D\times{\mathbb{M}[\Sigma]})$
defined as follows: let
$\mathbf{m},\mathbf{m}^{\prime}\in{\mathbb{M}[\Sigma]}$, $d,d^{\prime}\in D$
and $\sigma\in\Sigma$

$\displaystyle(d,\mathbf{m}\oplus{\llbracket\sigma\rrbracket})\underset{\mathfrak{P}}{\overset{\sigma}{\rightarrow}}(d^{\prime},\mathbf{m}\oplus\mathbf{m}^{\prime})$
iff  $\displaystyle\exists w\in(\Sigma\cup\Sigma_{\mathsf{i}})^{*}\colon
d\overset{w}{\underset{R}{\Rightarrow}^{*}}d^{\prime}\land w\in
L_{\sigma}\land\mathbf{m}^{\prime}={\mathsf{Parikh}}_{\Sigma}(w)\enspace.$

We now show that internal actions can be compiled away. Thus, for the
algorithms presented in this paper, we use the more abstract, language-
theoretic version of Definition 2, while we use internal actions as syntactic
sugar in examples.

######  Lemma 13.

Let $\mathcal{C}$ be a full trio. Given an $\mathsf{AP}$
$\mathfrak{P}_{\mathsf{i}}$ with internal actions over $\mathcal{C}$, one can
construct an $\mathsf{AP}$ $\mathfrak{P}$ over $\mathcal{C}$ such that both
have identical sets of runs.

######  Proof A.1.

The proof is along similar lines to that of Lemmas 4.3, 4.5 in [GM12]. Given
$\mathfrak{P}_{\mathsf{i}}=(D,\Sigma,\Sigma_{\mathsf{i}},\mathscr{L},R,d_{0},\mathbf{m}_{0})$
we construct
$\mathfrak{P}=(D,\Sigma,(L_{c})_{c\in\mathfrak{C}},d_{0},\mathbf{m}_{0})$ such
that

$\displaystyle(d,\mathbf{m}\oplus{\llbracket\sigma\rrbracket})\underset{\mathfrak{P}}{\overset{\sigma}{\rightarrow}}(d^{\prime},\mathbf{m}\oplus\mathbf{m}^{\prime})\quad\text{
if{}f
}\quad(d,\mathbf{m}\oplus{\llbracket\sigma\rrbracket})\underset{\mathfrak{P}_{\mathsf{i}}}{\overset{\sigma}{\rightarrow}}(d^{\prime},\mathbf{m}\oplus\mathbf{m}^{\prime})$

Let $L(R_{d,d^{\prime}})$ be the language of the automaton $R$ when $d$ is the
initial state and $d^{\prime}$ is the accepting state. We define $L_{d\sigma
d^{\prime}}$ as:

$L_{d\sigma d^{\prime}}:=\mathrm{Proj}_{\Sigma}(L_{\sigma}\cap
L(R_{d,d^{\prime}}))$