11institutetext: TU Braunschweig, 11email: {e.keskin, roland.meyer, s.van-der-
<EMAIL_ADDRESS>
# Urgency Annotations for Alternating Choices

Eren Keskin  Roland Meyer  Sören van der Wall

###### Abstract

We propose urgency programs, a new programming model with support for
alternation, imperfect information, and recursion. The novelty are urgency
annotations that decorate the (angelic and demonic) choice operators and
control the order in which alternation is resolved. We study standard notions
of contextual equivalence for urgency programs. Our first main result are
fully abstract characterizations of these relations based on sound and
complete axiomatizations. Our second main result settles their computability
via a normal form construction. Notably, we show that the contextual preorder
is ($2\mathsf{h}-1$)-EXPTIME-complete for programs of maximal urgency
$\mathsf{h}$ when the regular observable is given as an input resp. PTIME-
complete when the regular observable is fixed. We designed urgency programs as
a framework in which it is convenient to formulate and study verification and
synthesis problems. We demonstrate this on a number of examples including the
verification of concurrent and recursive programs and hyper model checking.

###### Keywords:

Alternation, Imperfect Information, Contextual Equivalence, Full Abstraction,
Axiomatization, Verification, Complexity.

##  1 Introduction

Algorithmic program verification may seem like a zoo of approaches that do not
have much in common. Refinement is checked by establishing a relation between
the program and a reference implementation [1], the model checking of linear-
time properties [2] is formulated as language inclusion [3], and branching-
time properties are reduced to games [4]. This variety makes it difficult to
choose a verification approach when one is confronted with a new class of
programs. Fortunately, there are master problems that provide guidance. When
the new class of programs is concurrent, there is a good chance that the
verification problem can be cast as coverability in well-structured transition
systems [5, 6, 7]. When it is recursive, one would try to reduce it to higher-
order model checking [8, 9]. The master problem then informs us about how to
implement the verification algorithm [10], from the symbolic representation of
program states [11] to the search strategy [12]. But the master problems are
no silver bullet. Well-structured transition systems are not good at modeling
recursion, and the verification of branching-time properties is undecidable
for them. Higher-order models, in turn, are not good at modeling concurrency.

We propose a new programming construct to capture verification tasks that are
not handled well by the existing master problems. The key insight is that by
_combining alternation[13] with imperfect information [14]_ one can model
concurrency even in a sequential programming model. We combine the two by
adding urgency annotations to the (angelic and demonic) choice operators.
Choices are classically resolved in program order [13]. Urgency annotations
are natural numbers that define when a choice has to be made: the higher the
urgency, the sooner. The lower urgency choices remain unresolved in the
program term until all higher urgency choices have been made. Choices of
different urgency can thus be imagined as belonging to different components in
the verification task, the program threads or the specification that has to
judge the program behavior. To illustrate the order in which choices with
urgency are made, consider the transition sequence

$\displaystyle(a_{l}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}a_{r}).\underline{(b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}}c)}\quad\rightarrow\quad\underline{(a_{l}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}a_{r})}.b\quad\rightarrow\quad
a_{l}.b\ .$

The demonic choice
$\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}$
of urgency $1$ is resolved only after the angelic choice
$\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}}$
of urgency $2$, although the demonic choice is written earlier in the program.

Urgency programs not only serve as a convenient backend to which to reduce
verification tasks. By comparing the reductions, we also understand how the
tasks are related. As a running example, we study the formulation of
simulation and language inclusion as urgency programs. Let the systems of
interest be $\mathcal{A}$ and $\mathcal{B}$ from Figure 1. We examine whether
(_a_) $\mathcal{A}$is simulated by $\mathcal{B}$ and  (_b_) the language of
$\mathcal{A}$ is included in the language of $\mathcal{B}$.  The transitions
$a_{l}$ and $a_{r}$ carry the observation $a$. The programs
$\mathit{p}_{\precsim}$ and $\mathit{p}_{{\subseteq}}$ from Figure 1 encode
the simulation resp. the inclusion problem. For now, just observe that the
difference in these programs is merely a shift in urgency.

$\mathcal{B}$$\mathit{O}_{\mathcal{B}}=\\{a_{l}b,a_{r}c\\}$$a_{l}$$a_{r}$$b$$c$$\mathcal{A}$$\mathit{O}_{\mathcal{A}}=\\{ab,ac\\}$$a$$b$$c$$\mathit{p}_{\precsim}=a.\underline{(a_{l}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}a_{r})}.(b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}}c).(b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}c)$$\mathit{p}_{{\subseteq}}=a.(a_{l}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}a_{r}).\underline{(b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}}c)}.(b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}c)$
Figure 1:  Automata $\mathcal{A}$, $\mathcal{B}$ and programs
$\mathit{p}_{\precsim},\mathit{p}_{{\subseteq}}$ for simulation resp.
inclusion.

Urgency programs can only provide guidance for solving verification tasks if
their verification problem is decidable and the decision procedure is easy to
adapt to the new setting. To develop decision procedures for urgency programs,
we follow a common approach: understand the contextual equivalence [15] of the
programming model, then one understands how to summarize programs, and every
algorithm will be a fixed point over these summaries. The notion of contextual
equivalence depends on the level of detail at which one intends to observe the
program behavior. We consider two standard definitions [16]:

$\displaystyle\mathit{p}\ $ $\displaystyle\simeq\ \mathit{q}\quad$ if
$\displaystyle\quad\forall\mathit{O}.\forall c[{\bullet}].$
$\displaystyle\quad{c[{\mathit{p}}]}\Downarrow{\mathit{O}}\quad$
$\displaystyle\text{iff}\quad{c[{\mathit{q}}]}\Downarrow{\mathit{O}}$
$\displaystyle\mathit{p}\ $ $\displaystyle\simeq_{\mathit{O}}\
\mathit{q}\quad$ if $\displaystyle\quad\phantom{\forall\mathit{O}.}\forall
c[{\bullet}].$
$\displaystyle\quad{c[{\mathit{p}}]}\Downarrow{\mathit{O}}\quad$
$\displaystyle\text{iff}\quad{c[{\mathit{q}}]}\Downarrow{\mathit{O}}\ .$

The former definition quantifies over observables $\mathit{O}$ and contexts
$c[{\bullet}]$ and is our notion of _contextual equivalence_. The latter fixes
an observable, like termination or reaching an error, and we refer to it as
_$\mathit{O}$ -specialized contextual equivalence_. Due to the alternating
choices in urgency programs, making an observation is defined in a game-
theoretic way: ${c[{\mathit{q}}]}\Downarrow{\mathit{O}}$ means Eve has a
winning strategy in the game arena $[[c[{\mathit{q}}]]]$ when
$\mathit{O}\subseteq\Sigma^{*}$ is the objective.

Our first contribution are full abstraction results: contextual equivalence
and its specialized variant coincide with congruence relations that neither
quantify over contexts nor observables. The congruences are defined
axiomatically, and one may say we axiomatize the contextual equivalences. An
important insight is that imperfect information distributes over perfect
information. In the example,

$\displaystyle(a_{l}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}a_{r}).(b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}}c)\
\simeq\
(a_{l}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}a_{r}).b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}}(a_{l}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}a_{r}).c\
\simeq\
(a_{l}.b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}a_{r}.b)\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}}(a_{l}.c\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}a_{r}.c)\
.$

Our second contribution is to settle the complexity of the two contextual
equivalences and their preorder variants. The main finding is that the
specialized contextual preorder is ($2\mathsf{h}-1$)-EXPTIME-complete for
programs of maximal urgency $\mathsf{h}$ when the regular observable is given
as an input resp. PTIME-complete when it is fixed. A consequence is indeed
that the verification problem can be solved with the same complexity. To get
the upper bound right, an important idea is to factorize the set of contexts.
We equate contexts $c[{\bullet}]$ that have the same solution space: the same
set of programs $\mathit{p}$ so that
${c[{\mathit{p}}]}\Downarrow{\mathit{O}}$. The challenge is to handle the
factorization algorithmically. We show how to represent solution spaces using
the novel concept of characteristic terms.

For the lower bound, we reduce context-bounded multi-pushdown games [17] to
the verification of urgency programs. This justifies our claim that urgency
programs can capture concurrency in a rather natural way. To further
demonstrate the usefulness of urgency programs, we show how to encode other
popular verification problems, notably the recent hyper model checking [18,
19].

#### Structure.

After an introduction to urgency programs, we state the full abstraction
results in Section 3, followed by the proofs of soundness, normalization, and
completeness. In Section 7, we give the decidability and complexity results,
followed by the upper and lower bound proofs in Sections 9 and 8.

##  2 Programming Model

Throughout the development, we fix a natural number $\mathsf{h}>0$ for the
maximal urgency in programs, a finite alphabet $\Sigma$ of terminal symbols
with typical elements $a,b,c$, and a finite or infinite set of non-terminals
$N$ with elements $A,B,C$. Each non-terminal has a so-called defining program
term given by $\mathit{E}:N\to\mathbf{T}$.

The set $\mathbf{T}$ of _program terms_ (of urgency up to $\mathsf{h}$ over
$\Sigma,N$) is defined as

$\displaystyle\mathit{p}\quad::=\quad a\ \mid\ \mathsf{skip}\ \mid\
\mathsf{err}\ \mid\ A\ \mid\ \mathit{p}.\mathit{p}\ \mid\
\mathop{\ooalign{\raisebox{4.2pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}\crcr$\bigvee$}}{}{P}\
\mid\
\mathop{\ooalign{\raisebox{-3.5pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}\crcr$\bigwedge$}}{}{P}\
.$

Terminal symbols represent program commands with visible behavior,
$\mathsf{skip}$ is a command without visible effect, and $\mathsf{err}$ aborts
the computation unsuccessfully. Non-terminals model recursive functions, we
have concatenation, and angelic
($\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}}$)
as well as demonic
($\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}}$)
choice of urgency $0<\mathsf{u}\leq\mathsf{h}$. We use
$\mathrel{\mathchoice{\ooalign{$\displaystyle\ovoid$\crcr\raisebox{1.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\textstyle\ovoid$\crcr\raisebox{1.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptstyle\ovoid$\crcr\raisebox{1.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptscriptstyle\ovoid$\crcr\raisebox{1.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}}$
to mean
$\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}}$
or
$\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}}$,
infix notation for binary choices, and
$\mathop{\ooalign{\raisebox{2.4pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}\crcr$\bigovoid$}}{}{\mathit{p}}$
for
$\mathop{\ooalign{\raisebox{2.4pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}\crcr$\bigovoid$}}{}{\\{\mathit{p}\\}}$.
An action is a term $A$ or
$\mathop{\ooalign{\raisebox{2.4pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}\crcr$\bigovoid$}}{}{P}$.
Terms that contain actions are called active. Terms that do not contain
actions are called passive. Passive terms are words over
$\Sigma\cup\\{\mathsf{skip},\mathsf{err}\\}$, and we also call them word terms
$w\in\mathbf{W}$. To avoid brackets, we let concatenation bind stronger than
choices. Choices range over non-empty but possibly infinite sets of terms.
Infinitary syntax requires care to make sure set and game-theoretic concepts
remain sound. We moved the corresponding lemmas to Appendix 0.A and 0.B to
keep the presentation light. The motivation for infinitary syntax will be
given at the end of the section. We lift the notion of urgency from choices to
program terms and define $\mathsf{urg}:\mathbf{T}\to\mathbb{N}$ by

$\displaystyle\mathsf{urg}(\mathsf{skip})$
$\displaystyle=\mathsf{urg}(\mathsf{err})=\mathsf{urg}(a)=0$
$\displaystyle\qquad\mathsf{urg}(A)$ $\displaystyle=\mathsf{h}$
$\displaystyle\mathsf{urg}(\mathit{p}.\mathit{q})$
$\displaystyle=\max\\{\mathsf{urg}(\mathit{p}),\mathsf{urg}(\mathit{q})\\}$
$\displaystyle\qquad\mathsf{urg}(\mathop{\ooalign{\raisebox{2.4pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}\crcr$\bigovoid$}}P)$
$\displaystyle=\mathsf{u}\ .$

A _context_ $c[{\bullet}]$ (of maximal urgency $\mathsf{h}$ over $\Sigma$ and
$N$) is a term that contains at most one occurrence of the fresh non-terminal
$\bullet$. The set of all contexts is denoted by $\mathbf{C}$. The expression
$c[{\mathit{p}}]$ refers to the term obtained from $c[{\bullet}]$ by replacing
$\bullet$ with the term $\mathit{p}$. A term $\mathit{q}$ is a subterm of
$\mathit{p}$ if there is a context $c[{\bullet}]$ with
$\mathit{p}=c[{\mathit{q}}]$. A subterm is called outermost if it is not
enclosed by a choice. For example, $\mathit{p}$ is outermost in
$\mathit{p}.\mathit{q}$ but not in
$(\mathit{p}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}}\mathit{q}).\mathit{r}$.
The _leading subterm_ $\mathsf{lead}(\mathit{p})$ of a term $\mathit{p}$ is
defined as the outermost action with the highest urgency. If several outermost
actions have this urgency, then the leftmost of them is leading. Passive terms
do not have leading subterms. Where helpful, we will underline a subterm that
contains the leading subterm. Note that $\underline{\mathit{p}}.\mathit{q}$
implies $\mathsf{urg}(\mathit{p})\geq\mathsf{urg}(\mathit{q})$ and
$\mathit{p}.\underline{\mathit{q}}$ implies
$\mathsf{urg}(\mathit{q})>\mathsf{urg}(\mathit{p})$. We denote the unique
context enclosing the leading subterm $\mathsf{lead}(\mathit{p})$ in
$\mathit{p}$ by $\mathsf{en}_{\mathit{p}}[\bullet]\in\mathbf{C}$. We have
$\mathit{p}=\mathsf{en}_{\mathit{p}}[\mathsf{lead}(\mathit{p})]$.

######  Example 1.

Consider $\mathit{p}_{{\subseteq}}$ from Figure 1. Its urgency is
$\mathsf{urg}(\mathit{p}_{{\subseteq}})=2$, the leading subterm is
$b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}}c$,
and the enclosing context is
$\mathsf{en}_{\mathit{p}_{{\subseteq}}}[\bullet]=a.(a_{l}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}a_{r}).\bullet.(b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}c)$.
Further,
$a_{l}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}a_{r}$
is an outermost subterm of $\mathit{p}_{{\subseteq}}$ and $a_{l}$ is not.

###  2.1 Semantics

Given that our programming model has alternation, the operational semantics of
a term is not a plain transition system but a _game arena_
$[[\mathit{p}]]=(\mathbf{T},\mathit{p},\mathsf{own},\rightarrow)$ in which
positions are owned by player $\mathit{Eve}$ or player $\mathit{Adam}$. The
set of positions is the set of all terms. The initial position is the given
term. The ownership assignment
$\mathsf{own}:\mathbf{T}\to\\{\mathit{Eve},\mathit{Adam}\\}$ returns the owner
of the leading subterm,
$\mathsf{own}(\mathit{p})=\mathsf{own}(\mathsf{lead}(\mathit{p}))$. Adam owns
the demonic choices,
$\mathsf{own}(\mathop{\ooalign{\raisebox{-3.5pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}\crcr$\bigwedge$}}P)=\mathit{Adam}$,
and Eve owns the angelic choices,
$\mathsf{own}(\mathop{\ooalign{\raisebox{4.2pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}\crcr$\bigvee$}}P)=\mathit{Eve}$.
We also give $\mathsf{skip}$, $\mathsf{err}$, terminals, and non-terminals to
Eve. This has no influence on the semantics as there will be at most one move
from these positions. The set of moves is defined as the smallest relation
satisfying the following rules:

$\displaystyle\prooftree[center=false]\hypo{\mathit{p}\in P}\infer
1[]{\mathop{\ooalign{\raisebox{2.4pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}\crcr$\bigovoid$}}P\rightarrow\mathit{p}}\hskip
36.98866pt\prooftree[center=false]\hypo{}\infer
1[]{A\rightarrow\mathit{E}(A)}\hskip
36.98866pt\prooftree[center=false]\hypo{\mathsf{lead}(\mathit{p})\rightarrow\mathit{q}}\infer
1[]{\mathit{p}\rightarrow\mathsf{en}_{\mathit{p}}[\mathit{q}]}\ $

A move always rewrites the leading subterm as illustrated by Figure 2. For a
choice, it selects one alternative. For a non-terminal, it inserts the
defining term. We define
$\mathsf{succ}(\mathit{p})=\\{\mathit{q}\mid\mathit{p}\rightarrow\mathit{q}\\}$.
It is worth noting that the game arena has perfect information. Imperfect
information is modeled through choices, and they are eventually resolved.

The operational semantics is intensional in that it gives precise information
about the program state at runtime. From a programming perspective, what
matters is the result of a computation or, more generally, the _observable
behavior_ of the program. Due to Adam’s influence, the observable behavior
will rarely be a single word but rather a language
$\mathit{O}\subseteq\Sigma^{*}$. We write ${\mathit{p}}\Downarrow{\mathit{O}}$
to mean that Eve can enforce termination and the result will be a word from
$\mathit{O}$, no matter how Adam plays. We make this precise.

Our notion of observable behavior is based on concepts from game theory. We
refer to a language $\mathit{O}\subseteq\Sigma^{*}$ as a reachability
objective for the game arena $[[\mathit{p}]]$. A play in this arena is a
maximal (finite or infinite) sequence of positions
$\pi=\mathit{p}_{0},\mathit{p}_{1},\ldots$ that starts in the given term,
$\mathit{p}_{0}=\mathit{p}$, and respects the moves of the game arena,
$\mathit{p}_{i}\rightarrow\mathit{p}_{i+1}$ for all $i$. If the play ends, the
result is a word term $w\in\mathbf{W}$. We interpret it as an element of the
monoid with zero
$(\Sigma^{*}\cup\\{\mathsf{err}\\},.\;,\mathsf{skip},\mathsf{err})$. Here,
$\mathsf{skip}$ is the unit, often denoted by $\varepsilon$, and
$\mathsf{err}$ is the zero. We use
$\mathrel{\mathchoice{{\ooalign{$\displaystyle=$\crcr$\displaystyle\raisebox{0.6pt}{*}$}}{}}{{\ooalign{$\textstyle=$\crcr$\textstyle\raisebox{0.6pt}{*}$}}{}}{{\ooalign{$\scriptstyle=$\crcr$\scriptstyle\raisebox{0.6pt}{*}$}}{}}{{\ooalign{$\scriptscriptstyle=$\crcr$\scriptscriptstyle\raisebox{0.6pt}{*}$}}{}}}$
to denote the monoid equality. Eve wins the play when $w$ belongs to
$\mathit{O}$, meaning there is $v\in\mathit{O}$ so that
$w\mathrel{\mathchoice{{\ooalign{$\displaystyle=$\crcr$\displaystyle\raisebox{0.6pt}{*}$}}{}}{{\ooalign{$\textstyle=$\crcr$\textstyle\raisebox{0.6pt}{*}$}}{}}{{\ooalign{$\scriptstyle=$\crcr$\scriptstyle\raisebox{0.6pt}{*}$}}{}}{{\ooalign{$\scriptscriptstyle=$\crcr$\scriptscriptstyle\raisebox{0.6pt}{*}$}}{}}}v$
(write $w\in\mathit{O}$). Otherwise, Adam wins the play. In particular, Adam
wins all infinite plays and all plays exhibiting $\mathsf{err}\notin\Sigma$.

A positional strategy for Eve is a function $\sigma:\mathbf{T}\to\mathbf{T}$
so that $\mathit{q}\rightarrow\sigma(\mathit{q})$ for all terms $\mathit{q}$
owned by Eve that admit further rewriting. Since we are interested in
reachability objectives, we can use positional strategies without loss of
generality [20]. A play $\pi$ is conform to $\sigma$ if for all $i$ with
$\mathsf{own}(\mathit{p}_{i})=\mathit{Eve}$ and
$\mathsf{succ}(\mathit{p}_{i})\neq\emptyset$ we have
$\sigma(\mathit{p}_{i})=\mathit{p}_{i+1}$. Eve wins objective $\mathit{O}$, if
she has a strategy $\sigma$ so as to win all plays that are conform to this
strategy. This is what we denote by ${\mathit{p}}\Downarrow{\mathit{O}}$.

######  Example 2.

We demonstrate how to encode simulation and inclusion between $\mathcal{A}$
and $\mathcal{B}$ from Figure 1. In $\mathit{p}_{\precsim}$, Eve is tasked to
find a violation of the simulation property, while Adam tries to prove it:
whenever Eve takes a transition in $\mathcal{A}$, Adam tries to select a
simulating transition right away in $\mathcal{B}$. The term
$\mathit{p}_{{\subseteq}}$ models inclusion: Eve selects a run in
$\mathcal{A}$ and Adam tries to come up with a run in $\mathcal{B}$ with
matching observations. We define an objective $\mathit{O}$ so that
${\mathit{p}_{\precsim}}\Downarrow{\mathit{O}}$ holds precisely when
$\mathcal{A}$ is simulated by $\mathcal{B}$ and
${\mathit{p}_{{\subseteq}}}\Downarrow{\mathit{O}}$ holds precisely when
$\mathcal{A}$’s language is included in $\mathcal{B}$’s. The objective has to
make sure that the choices of transitions form paths in the automata and that
the letters actually match. The latter is easy to check. The former can be
guaranteed by interleaving $\mathit{O}_{\mathcal{A}}$ and
$\mathit{O}_{\mathcal{B}}$ in an alternating fashion, so $a_{1}.a_{2}$ and
$b_{1}.b_{2}$ yield $a_{1}.b_{1}.a_{2}.b_{2}$. Details are in Section 9.

$f$
$(\underline{a_{l}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}a_{r}}).(b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}}c)$$f$$a_{l}.(\underline{b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}}c})$$f$$a_{l}.b$$f$$a_{l}.c$$f$$a_{r}.(\underline{b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}}c})$$f$$a_{r}.b$$f$$a_{r}.c$

$f$$(a_{l}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}a_{r}).(\underline{b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}}c})$$f$$(\underline{a_{l}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}a_{r}}).b$$f$$a_{l}.b$$f$$a_{r}.b$$f$$(\underline{a_{l}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}a_{r}}).c$$f$$a_{l}.c$$f$$a_{r}.c$

Figure 2: The game arenas
$[[(a_{l}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}}a_{r}).(b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}c)]]$
and
$[[(a_{l}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}}a_{r}).(b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{2}}$}}}}c)]]$.
$\mathit{O}$ is gray.

######  Example 3.

The encodings for simulation and inclusion only differ in the terms
$(a_{l}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}a_{r}).(b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}}c)$
and
$(a_{l}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}a_{r}).(b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}}c)$.
Their semantics is given in Figure 2. Rectangular nodes are owned by Adam,
circular ones by Eve, and for rectangular nodes with rounded corners the
ownership does not matter. The objective is
$\mathit{O}=\\{a_{l}.c,a_{r}.b\\}$. Indeed, $\mathcal{A}$’s language is
included in $\mathcal{B}$’s,
${(a_{l}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}a_{r}).(b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}}c)}\mathrel{\mathchoice{\ooalign{$\displaystyle\Downarrow$\crcr$\displaystyle/$}{}}{\ooalign{$\textstyle\Downarrow$\crcr$\textstyle/$}{}}{\ooalign{$\scriptstyle\Downarrow$\crcr$\scriptstyle/$}{}}{\ooalign{$\scriptscriptstyle\Downarrow$\crcr$\scriptscriptstyle/$}{}}}{\mathit{O}}$,
but $\mathcal{A}$ is not simulated by $\mathcal{B}$,
${(a_{l}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}a_{r}).(b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}}c)}\Downarrow{\mathit{O}}$.

###  2.2 Contextual Preorder

The notion of observable behavior is not compositional: we may have
${\mathit{p}}\Downarrow{\mathit{O}}$ if and only if
${\mathit{q}}\Downarrow{\mathit{O}}$ for all objectives $\mathit{O}$, yet the
two terms behave differently when placed into a context. In our example,
${(b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}}c)}\Downarrow{\mathit{U}}$
if and only if
${(b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}}c)}\Downarrow{\mathit{U}}$
for all objectives $\mathit{U}\subseteq\Sigma^{*}$. When inserting the terms
into the context
$c[{\bullet}]=(a_{l}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}a_{r}).\bullet$,
however, we have the difference discussed above. This is a common problem, and
the way out is to consider the largest congruence that lives inside
observational equivalence. It is more elegant to work with a precongruence and
define the congruence of interest as a derived notion.

######  Definition 1.

The _contextual preorder_ $\preceq\ \subseteq\mathbf{T}\times\mathbf{T}$ is
defined by $\mathit{p}\preceq\mathit{q}$, if

$\displaystyle\forall\mathit{O}\subseteq\Sigma^{*}.\ \forall
c[{\bullet}]\in\mathbf{C}.\ {c[{\mathit{p}}]}\Downarrow{\mathit{O}}\text{
implies }{c[{\mathit{q}}]}\Downarrow{\mathit{O}}\ .$

The _$\mathit{O}$ -specialized contextual preorder_ $\preceq_{\mathit{O}}\
\subseteq\mathbf{T}\times\mathbf{T}$ is defined by fixing $\mathit{O}$ and
dropping the leading universal quantifier. The _contextual equivalence_ is
then $\simeq\ =\ \preceq\cap\succeq$, and the _$\mathit{O}$ -specialized
contextual equivalence_ is $\simeq_{\mathit{O}}\ =\
\preceq_{\mathit{O}}\cap\succeq_{\mathit{O}}$.

In the example,
$(b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}}c)\preceq(b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}}c)$
and so by congruence
$(a_{l}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}a_{r}).(b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}}c)\preceq(a_{l}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}a_{r}).(b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}}c)$.
The reverse does not hold, consider context
$(a_{l}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}a_{r}).\bullet$
and objective $\\{a_{l}.c,a_{r}.b\\}$ from above. Note that
$\mathit{p}\preceq\mathit{q}$ implies
$\mathit{p}\preceq_{\mathit{O}}\mathit{q}$ for all $\mathit{O}$.

With $\mathit{O}_{\mathit{Term}}=\Sigma^{*}$ as the objective, we can use the
specialized contextual equivalence to study the termination behavior of
programs. We can also introduce a letter $\mathsf{loc}$ so that
${\mathit{p}}\Downarrow{\mathit{O}_{\mathit{Reach}}}$ with
$\mathit{O}_{\mathit{Reach}}=\Sigma^{*}.\mathsf{loc}.\Sigma^{*}$ observes
visits to a specific location. (Non-specialized) Contextual equivalence is
more precise and takes into account all objectives. Both notions are also
motivated by verification, where contextual equivalence gives information
about which information can be abstracted away from an urgency term without an
influence on the objective, similar to how bisimilarity preserves
$\text{CTL}^{*}$ properties [21].

The motivation for an infinite set of non-terminals and infinitary terms is to
model parameterized functions in a simple yet general way. The idea is to
introduce a non-terminal for each instantiation of the function’s formal
parameters by actual values, inspired by value passing in process algebra
[22]. Another more technical argument is that our normal form relies on
infinitary syntax.

##  3 Full Abstraction

We define a precongruence $\sqsubseteq\ \subseteq\mathbf{T}\times\mathbf{T}$
on program terms that neither quantifies over contexts nor objectives but
relates terms solely based on their syntactic structure. The relation is
defined through a set of axioms that should be understood as explaining the
interplay between the operators in our programming model. The main finding is
that this axiomatic precongruence coincides with the contextual preorder, and
we say that we axiomatize (in a sound and complete way) the contextual
preorder. This is our main theorem.

######  Theorem 3.1 (Full Abstraction 1).

$\mathit{p}\sqsubseteq\mathit{q}$ if and only if
$\mathit{p}\preceq\mathit{q}$.

We have a corresponding result for the $\mathit{O}$-specialized contextual
preorder. In this setting, a complete axiomatization is considerably more
difficult to obtain because, intuitively, we have to understand the
concatenation behavior of language $\mathit{O}$. Our solution is partial in
that we impose a side condition on the objective to obtain completeness: it
should be right-separating, a notion we will define in a moment. Luckily, the
objectives of interest $\mathit{O}_{\mathit{Term}}$ and
$\mathit{O}_{\mathit{Reach}}$ are right-separating. It is always sound to
reason with the $\mathit{O}$-specialized axiomatic precongruence.

######  Theorem 3.2 (Full Abstraction 2).

$\mathit{p}\sqsubseteq_{\mathit{O}}\mathit{q}$ implies
$\mathit{p}\preceq_{\mathit{O}}\mathit{q}$. If $\mathit{O}$ is right-
separating, then also $\mathit{p}\preceq_{\mathit{O}}\mathit{q}$ implies
$\mathit{p}\sqsubseteq_{\mathit{O}}\mathit{q}$.

We understand the concatenation behavior of an objective with the help of the
syntactic precongruence over the monoid $\Sigma^{*}\cup\\{\mathsf{err}\\}$. It
may relate terminal words to $\mathsf{err}$ in case they cannot be extended to
a word from the objective.

######  Definition 2.

The _syntactic precongruence_ induced by $\mathit{O}$ on
$\Sigma^{*}\cup\\{\mathsf{err}\\}$ is defined by $w\leq^{s}_{\mathit{O}}v$, if
for all $x,y\in\Sigma^{*}$we have $x.w.y\in\mathit{O}$ implies
$x.v.y\in\mathit{O}$.

An objective is then right-separating, if the concatenation from left in the
above definition is not needed to distinguish words. We define
$\leq^{r}_{\mathit{O}}$ on $\Sigma^{*}\cup\\{\mathsf{err}\\}$ by
$w\leq^{r}_{\mathit{O}}v$, if for all $y\in\Sigma^{*}$ we have
$w.y\in\mathit{O}$ implies $v.y\in\mathit{O}$.

######  Definition 3 (and Lemma).

Objective $\mathit{O}$ is _right-separating_ , if $\leq^{s}_{\mathit{O}}\ =\
\leq^{r}_{\mathit{O}}$. The objectives $\mathit{O}_{\mathit{Term}}$ and
$\mathit{O}_{\mathit{Reach}}$ are right-separating.

######  Example 4.

The syntactic congruence
${\cong^{s}_{\mathit{O}}}={\leq^{s}_{\mathit{O}}\cap\geq^{s}_{\mathit{O}}}$
induced by the objective $\mathit{O}=\\{a_{l}.c,a_{r}.b\\}$ has classes
$\Sigma^{*}\cup\\{\mathsf{err}\\}/_{\cong^{s}_{\mathit{O}}}=\\{[{\mathsf{skip}}],[{a_{l}}],[{a_{r}}],[{b}],[{c}],[{a_{l}.c,a_{r}.b}]\\}$
plus a class for the remaining words.

Intuitively, right-separating objectives allow us to evaluate the
$\mathit{O}$-specialized contextual preorder by using contexts
$\bullet.\mathit{r}$ that only append to the right. For arbitrary objectives,
we have to consider contexts $\mathit{s}.\bullet.\mathit{r}$ and it is
difficult to understand the interplay between high urgencies in $\mathit{r}$
and low urgencies in $\mathit{s}$.

We now give the two axiomatizations and explain them on an intuitive level.
Recall that a precongruence is a reflexive and transitive relation that is
preserved when inserting related terms into the same context.

######  Definition 4.

The _axiomatic precongruence_ $\sqsubseteq\
\subseteq\mathbf{T}\times\mathbf{T}$ is the least precongruence satisfying the
axioms in Figure 4 except 4(g). The _$\mathit{O}$ -specialized axiomatic
precongruence_ $\sqsubseteq_{\mathit{O}}$ on terms is the least precongruence
satisfying all axioms in Figure 4. We use $\equiv$ for
$\sqsubseteq\cap\sqsupseteq$ and $\equiv_{\mathit{O}}$ for
$\sqsubseteq_{\mathit{O}}\cap\sqsupseteq_{\mathit{O}}$.

(a) Lattice

[center=false] ∀i∈I. p_i⊑q_i [left label=(L1)]1
$\scriptstyle{\mathsf{\mathsf{u}}}$ {p_i∣i∈I}⊑
$\scriptstyle{\mathsf{\mathsf{u}}}$ {q_i∣i∈I} [center=false] urg(p) [left
label=(L2)]1  $\scriptstyle{\mathsf{\mathsf{u}}}$ $\bigvee$ _i∈I
$\scriptstyle{\mathsf{\mathsf{u}}}$ $\bigwedge$ P_i ≡
$\scriptstyle{\mathsf{\mathsf{u}}}$ $\bigwedge$ _f: I→P_I
$\scriptstyle{\mathsf{\mathsf{u}}}$ $\bigvee$ {f (i)∣i∈I} [center=false]
urg(p)≤u [left label=(L3)]1 p  $\wedge$ $\scriptstyle{\mathsf{\mathsf{u}}}$ (p
$\vee$ $\scriptstyle{\mathsf{\mathsf{u}}}$ q)≡p p  $\vee$
$\scriptstyle{\mathsf{\mathsf{u}}}$ (p  $\wedge$
$\scriptstyle{\mathsf{\mathsf{u}}}$ q)≡p [center=false] [left label=(L4)]1
$\scriptstyle{\mathsf{\mathsf{u}}}$ _i∈I  $\scriptstyle{\mathsf{\mathsf{u}}}$
P_i ≡  $\scriptstyle{\mathsf{\mathsf{u}}}$ ⋃_i∈IP_i [center=false] urg(p)≤u
[left label=(L5)]1 p⊑p  $\vee$ $\scriptstyle{\mathsf{\mathsf{u}}}$ q

(b) Distributivity

[center=false] urg(p)<u [left label=(D1)]1 p.(
$\scriptstyle{\mathsf{\mathsf{u}}}$ Q)≡  $\scriptstyle{\mathsf{\mathsf{u}}}$
{p.q∣q∈Q} [center=false] urg(p)≤u [left label=(D2)]1 (
$\scriptstyle{\mathsf{\mathsf{u}}}$ Q).p≡  $\scriptstyle{\mathsf{\mathsf{u}}}$
{q.p∣q∈Q}

(c) Normalization

[center=false] v<u [left label=(N)]1  $\scriptstyle{\mathsf{\mathsf{v}}}$
$\bigvee$ $\scriptstyle{\mathsf{\mathsf{u}}}$ Q ≡
$\scriptstyle{\mathsf{\mathsf{v}}}$ $\bigvee$
$\scriptstyle{\mathsf{\mathsf{v}}}$ Q

(d) Err

[center=false] [left label=(B1)]1 err⊑p

(e) Monoid

[center=false] w  $\scriptscriptstyle=$ * v [left label=(M)]1 w≡v

(f) Fixed point

[center=false] [left label=(FP)]1 A≡E(A) [center=false] ∀A∈N. E(A){N/p_N}⊑p_A
[left label=(LFP)]1 B⊑p_B

(g) Specialization

[center=false] w≤^s_Ov [left label=(S)]1 w⊑_Ov

Figure 4: Axioms defining $\sqsubseteq$ and $\sqsubseteq_{\mathit{O}}$.

With the axioms given in Figure 4(a), the choice operators span a completely
distributive lattice on each urgency. The monotonicity fig. 4(a) is not
covered by the precongruence but implements an infinite replacement. The axiom
has a side condition that can be found Appendix 0.A. Due to this axiom, nodes
in our proof trees may have an infinite degree. Yet, every path is guaranteed
to be finite. To see the premise in axiom 4(a), consider
$\mathit{p}=(a_{l}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{2}}$}}}}a_{r})$
and context
$\bullet.(b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}}c)$.
Then in
$\mathit{p}.(b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}}c)$
Eve wins while in
$(\mathit{p}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}}\mathit{p}).(b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}}c)$
she loses, similar to Figure 2. For 4(a), the reasoning is similar. As a
consequence of the lattice axioms, one can derive the dual rules of 4(a) and
4(a). Distributivity 4(a) states that the order of choices can be changed by
considering all choice functions $f:I\to\bigcup_{i\in I}P_{i}$ with $f(i)\in
P_{i}$ for all $i\in I$, denoted by $f:I\to P_{I}$.

The distributivity in 4(b) captures the essence of imperfect information:
concatenation to the left distributes over choice, provided the internals of
the term are invisible as the choice has a higher urgency. The distributivity
from the right in 4(b) is similar but takes into account that the leading
subterm for equal urgencies is leftmost. This clean interplay between
imperfect information and choice came as a surprise and we consider these laws
an important contribution.

A string with $\mathsf{err}\not\in\Sigma$ is the most disadvantageous term for
Eve, because it belongs to no objective $\mathit{O}\subseteq\Sigma^{*}$.

The monoid fig. 4(e) refers to word terms $w,v\in\mathbf{W}$. We interpret
them in the monoid $\Sigma^{*}\cup\\{\mathsf{err}\\}$ and inherit the equality
there, denoted by
$\mathrel{\mathchoice{{\ooalign{$\displaystyle=$\crcr$\displaystyle\raisebox{0.6pt}{*}$}}{}}{{\ooalign{$\textstyle=$\crcr$\textstyle\raisebox{0.6pt}{*}$}}{}}{{\ooalign{$\scriptstyle=$\crcr$\scriptstyle\raisebox{0.6pt}{*}$}}{}}{{\ooalign{$\scriptscriptstyle=$\crcr$\scriptscriptstyle\raisebox{0.6pt}{*}$}}{}}}$
above. The equality strips brackets and $\mathsf{skip}$, and interprets
$\mathsf{err}$ as zero.

The normalization fig. 4(c) reflects the fact that only the outermost choice
operator determines the urgency of a term. Towards soundess, note that once
the outer choice with urgency $\mathsf{u}$ is resolved, we are sure that the
context to the left has urgency strictly smaller than $\mathsf{u}$ and the
context to the right has urgency at most $\mathsf{u}$. Hence, the inner choice
is the next to be resolved, independent of whether its urgency is $\mathsf{u}$
or $\mathsf{v}\geq\mathsf{u}$.

The fixed-point fig. 4(f) allows us to rewrite non-terminals to their defining
terms. The fig. 4(f) allows us to rewrite non-terminals to a prefixed point,
using Knaster and Tarski’s characterization of least fixed points [23]. Here,
we let $\mathit{p}_{N}$ denote a vector of terms with one entry
$\mathit{p}_{A}$ per non-terminal $A\in N$, and use $\\{N/\mathit{p}_{N}\\}$
for the substitution of all non-terminals by these terms.

Recall that Figure 4(g) only plays a role in the definition of the specialized
axiomatic precongruence. The axiom depends on the objective $\mathit{O}$ of
interest, meaning it actually is a family of axioms. The axiom relates word
terms $w,v\in\mathbf{W}$ as prescribed by the syntactic precongruence.

######  Example 5.

We show that simulation implies inclusion in Example 2. Remember that Eve
tries to refute the relation. We prove axiomatically

$b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}}c\;\stackrel{{\scriptstyle\lx@cref{refnum}{axiom:lattice-
ord}}}{{\sqsubseteq}}\;(b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}}c)\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}}(b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}}c)\;=\;\mathop{\ooalign{\raisebox{4.2pt}{$\scriptstyle{\mathsf{2}}$}\crcr$\bigvee$}}{}{(b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}}c)}\;\stackrel{{\scriptstyle\lx@cref{refnum}{axiom:lattice-
abs},\;\lx@cref{refnum}{axiom:lattice-
assoc}}}{{\equiv}}\;\mathop{\ooalign{\raisebox{-3.5pt}{$\scriptstyle{\mathsf{2}}$}\crcr$\bigwedge$}}{}\mathop{\ooalign{\raisebox{4.2pt}{$\scriptstyle{\mathsf{2}}$}\crcr$\bigvee$}}{}{(b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}}c)}\;\stackrel{{\scriptstyle\lx@cref{refnum}{axiom:lattice-
abs}}}{{\equiv}}\;b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}}c\
.$

By 4(a), we have $b\sqsubseteq
b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}}c$
and $c\sqsubseteq
b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}}c$,
which we can apply to subterms by congruence. The equality holds because
choices range over sets. We apply 4(a) with
$\mathit{p}=\mathit{q}=\mathord{\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}}}(b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}}c)$,
apply 4(a) to flatten the choices, apply 4(a) once more to remove the choices,
and finally apply congruence. This yields
$\mathit{p}_{{\subseteq}}\sqsubseteq\mathit{p}_{\precsim}$. With soundess of
the axiomatization (Section 4), we obtain the desired
$\mathit{p}_{{\subseteq}}\preceq\mathit{p}_{\precsim}$. With a normal form
result (Section 5), we also show completeness (Section 6).

##  4 Soundness

######  Proposition 1 (Soundness).

$\mathit{p}\sqsubseteq\mathit{q}$ implies $\mathit{p}\preceq\mathit{q}$,
$\mathit{p}\sqsubseteq_{\mathit{O}}\mathit{q}$ implies
$\mathit{p}\preceq_{\mathit{O}}\mathit{q}$.

This section is devoted to proving Proposition 1. Proving soundness is
difficult because it requires us to reason over all contexts. If
$\mathit{p}\sqsubseteq_{\mathit{O}}\mathit{q}$ is an axiom, then we need to
show that ${c[{\mathit{p}}]}\Downarrow{\mathit{O}}$ implies
${c[{\mathit{q}}]}\Downarrow{\mathit{O}}$ for all $c[{\bullet}]\in\mathbf{C}$.

We first develop a proof technique for soundness that allows us to reduce the
set of contexts we have to consider, and in a second step prove the axioms
sound. To define the contexts that have to be considered, we introduce some
terminology. We say that term $\mathit{p}$ is _immediate_ for context
$c[{\bullet}]\in\mathbf{C}$, if $c[{\mathit{p}}]\in\mathbf{W}$ or
$c[{\mathit{p}}]$ is active and $\mathit{p}$ contains the leading subterm in
$c[{\mathit{p}}]$, denoted by $c[{\underline{\mathit{p}}}]$. If this is not
the case, we call $\mathit{p}$ _paused_ for $c[{\bullet}]$. As the names
suggest, immediate terms get rewritten in the next move while paused terms do
not. For example, term
$\mathop{\ooalign{\raisebox{4.2pt}{$\scriptstyle{\mathsf{2}}$}\crcr$\bigvee$}}P$
is immediate for
$\bullet.\mathop{\ooalign{\raisebox{-3.5pt}{$\scriptstyle{\mathsf{1}}$}\crcr$\bigwedge$}}Q$
but paused for
$\bullet.\mathop{\ooalign{\raisebox{-3.5pt}{$\scriptstyle{\mathsf{3}}$}\crcr$\bigwedge$}}Q$
and
$\mathop{\ooalign{\raisebox{4.2pt}{$\scriptstyle{\mathsf{2}}$}\crcr$\bigvee$}}\\{\bullet,\mathit{q}\\}$.
In the last context, $\bullet$ is enclosed by a choice. No term is immediate
for such a context.

######  Lemma 1 (Proof Technique).

If ${c[{\mathit{p}}]}\Downarrow{\mathit{O}}$ implies
${c[{\mathit{q}}]}\Downarrow{\mathit{O}}$ for all contexts
$c[{\bullet}]\in\mathbf{C}$ where at least one of $\mathit{p}$ or $\mathit{q}$
is immediate, then $\mathit{p}\preceq_{\mathit{O}}\mathit{q}$.

Lemma 1 defines precisely the contexts we need to consider when proving the
axioms sound. Its proof relies on the following observation: a paused term
does not change the outcome of a move in the context (cf. Appendix 0.C).

######  Lemma 2.

Consider terms $\mathit{p}$ and $\mathit{q}$ that are paused for context
$c[{\bullet}]$. Then,
$\mathsf{own}(c[{\mathit{p}}])=\mathsf{own}(c[{\mathit{q}}])$ and there is a
set of contexts $D\subseteq\mathbf{C}$ so that
$\mathsf{succ}(c[{\mathit{p}}])=\\{\mathit{d}[\mathit{p}]\mid\mathit{d}[\bullet]\in
D\\}$ and
$\mathsf{succ}(c[{\mathit{q}}])=\\{\mathit{d}[\mathit{q}]\mid\mathit{d}[\bullet]\in
D\\}$.

We are now prepared to prove each axiom sound. Using Lemma 1, all proofs share
a common approach: we fix an objective and pick a context that is immediate
for at least one term in the axiom. Then, we unroll the game arena for a few
moves until it reveals the winning implication we are after. We restrict our
presentation to the soundness of Figure 4(b) and defer details to Appendix
0.D. The proofs make use of two properties of immediate terms.

######  Lemma 3.

Let term $\mathit{p}$ be immediate for context $c[{\bullet}]$. Then we have
$\mathsf{own}(c[{\mathit{p}}])=\mathsf{own}(\mathit{p})$. If
$\mathsf{urg}(\mathit{p})\leq\mathsf{urg}(\mathit{q})$, then also term
$\mathit{q}$ is immediate for $c[{\bullet}]$.

###### Proof of Proposition 1 (Soundness).

Figure 4(b): We consider binary choices owned by Eve, the generalization to
choices over arbitrary sets and also Adam’s case are similar. For
$\mathsf{urg}(\mathit{p})<\mathsf{u}$, the axiom says that
$\mathit{p}.(\mathit{q}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}}\mathit{r})\sqsubseteq\mathit{p}.\mathit{q}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}}\mathit{p}.\mathit{r}$
and vice versa. The goal is thus to show
$\mathit{p}.(\mathit{q}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}}\mathit{r})\simeq\mathit{p}.\mathit{q}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}}\mathit{p}.\mathit{r}$.

Consider an objective $\mathit{O}$ and let $c[{\bullet}]$ be a context for
which at least one of
$\mathit{p}.(\mathit{q}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}}\mathit{r})$
or
$\mathit{p}.\mathit{q}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}}\mathit{p}.\mathit{r}$
is immediate. The urgencies of both terms are $\mathsf{u}$. This means that
not only one but actually both terms are immediate for $c[{\bullet}]$ and,
moreover, the owner of
$c[{\underline{\mathit{p}.(\mathit{q}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}}\mathit{r})}}]$
and
$c[{\underline{\mathit{p}.\mathit{q}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}}\mathit{p}.\mathit{r}}}]$
is Eve. The first moves in the game arenas are thus done by the same player
and have the same result:

$c[{\underline{\mathit{p}.\mathit{q}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}}\mathit{p}.\mathit{r}}}]$$c[{\mathit{p}.\mathit{q}}]$$c[{\mathit{p}.\mathit{r}}]$
$c[{\underline{\mathit{p}.(\mathit{q}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}}\mathit{r})}}]$$c[{\mathit{p}.\mathit{q}}]$$c[{\mathit{p}.\mathit{r}}]$

As a consequence, translating winning strategies becomes straightforward and
the equivalence
${{c[{\mathit{p}.(\mathit{q}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}}\mathit{r})}]}\Downarrow{\mathit{O}}}$
iff
${c[{\mathit{p}.\mathit{q}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}}}}\mathit{p}.\mathit{r}}]}\Downarrow{\mathit{O}}$
holds. ∎

##  5 Normalization

As a first step towards completeness, we show that each term can be brought
into a normal form using our axioms. Normalization is a standard approach in
completeness proofs. The treatment of alternation and urgency is new.

The normal form eliminates non-terminals and orders the interplay between
concatenation and choice: a normal form term is a tree of height $2\mathsf{h}$
(with $\mathsf{h}$ the maximal urgency) that repeatedly alternates between
Eve’s and Adam’s choices while decreasing the urgency. The leaves of the tree
are terminal words, $\mathsf{skip}$, or $\mathsf{err}$. Inductively, we define
$\mathit{NF}_{0}=\Sigma^{*}\cup\\{\mathsf{err}\\}$ and for $\mathsf{u}>0$,

$\displaystyle\mathit{ANF}_{\mathsf{u}}\ =\
\\{\mathop{\ooalign{\raisebox{-3.5pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}\crcr$\bigwedge$}}P\mid\emptyset\neq
P\subseteq\mathit{NF}_{\mathsf{u}-1}\\}\hskip
28.45274pt\mathit{NF}_{\mathsf{u}}\ =\
\\{\mathop{\ooalign{\raisebox{4.2pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}\crcr$\bigvee$}}P\mid\emptyset\neq
P\subseteq\mathit{ANF}_{\mathsf{u}}\\}\,.$

The base case terms are all owned by Eve. In an $\mathit{ANF}_{\mathsf{u}}$
term, Adam chooses over $\mathit{NF}_{\mathsf{u}-1}$ terms. In an
$\mathit{NF}_{\mathsf{u}}$ term, Eve chooses over such
$\mathit{ANF}_{\mathsf{u}}$ terms owned by Adam. The main result of this
section is the following.

######  Proposition 2.

There is a function $\mathsf{nf}:\mathbf{T}\to\mathit{NF}_{\mathsf{h}}$ so
that $\mathsf{nf}(\mathit{p})\equiv\mathit{p}$ for all $\mathit{p}$.

######  Example 6.

We illustrate the normal form computation on our running example. Let
$\mathsf{h}=2$ and consider
$(a_{l}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}a_{r}).(b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}}c)$.

$\displaystyle(a_{l}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}a_{r}).(b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}}c)\
\stackrel{{\scriptstyle\hskip 6.29996pt\lx@cref{refnum}{axiom:dist-left}\hskip
6.29996pt}}{{\equiv}}$
$\displaystyle\quad(a_{l}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}a_{r}).b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}}(a_{l}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}a_{r}).c$
$\displaystyle\stackrel{{\scriptstyle\hskip
6.29996pt\lx@cref{refnum}{axiom:dist-right}\hskip 6.29996pt}}{{\equiv}}$
$\displaystyle\quad(a_{l}.b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}a_{r}.b)\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}}(a_{l}.c\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}a_{r}.c)$
$\displaystyle\stackrel{{\scriptstyle\lx@cref{refnum}{axiom:lattice-
abs},\;\lx@cref{refnum}{axiom:lattice-assoc}}}{{\equiv}}$
$\displaystyle\quad[\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{2}}$}}}}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}}(a_{l}.b\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}a_{r}.b)]\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{2}}$}}}}[\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{2}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{2}}$}}}}\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\vee$}$\crcr\raisebox{4.0pt}{$\scriptstyle{\mathsf{1}}$}}}}(a_{l}.c\mathrel{\mathchoice{\ooalign{$\displaystyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\textstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}{\ooalign{$\scriptscriptstyle\scalebox{1.2}[1.0]{$\wedge$}$\crcr\raisebox{-2.5pt}{$\scriptstyle{\mathsf{1}}$}}}}a_{r}.c)]\
.$

Formally, we prove Proposition 2 in two steps. First, we compute a normal form
term $\mathsf{nf}(A)\equiv A$ for every non-terminal $A\in N$ in a fixed-point
iteration. Then, we replace each non-terminal in $\mathit{p}$ by its normal
form. Finally, we normalize the remaining term to obtain
$\mathsf{nf}(\mathit{p})\equiv\mathit{p}$. The two steps are formalized in the
next lemma, details of the normalization can be found in Appendix 0.E.

######  Lemma 4.

For all $\mathit{p}\in\mathbf{T}$ without non-terminals there is
$\mathsf{nf}(\mathit{p})\in\mathit{NF}_{\mathsf{h}}$ with
$\mathit{p}\equiv\mathsf{nf}(\mathit{p})$. For all non-terminals $A\in N$,
there is a $\mathsf{nf}(A)\in\mathit{NF}_{\mathsf{h}}$ with
$\mathsf{nf}(A)\equiv A$.

##  6 Completeness

######  Proposition 3 (Completeness).

$\mathit{p}\preceq\mathit{q}$ implies $\mathit{p}\sqsubseteq\mathit{q}$. For a
right-separating objective $\mathit{O}\subseteq\Sigma^{*}$,
$\mathit{p}\preceq_{\mathit{O}}\mathit{q}$ implies
$\mathit{p}\sqsubseteq_{\mathit{O}}\mathit{q}$.

Interestingly, the completeness for the axiomatic precongruence follows from
the completeness for the specialized version. To prove this implication, we
consider objectives for which Figure 4(g) does not add relations. Formally, we
call an objective $\mathit{O}$ _domain shattering_ , if $\sqsubseteq\ =\
\sqsubseteq_{\mathit{O}}$.

######  Lemma 5.

The language $w.w^{\mathit{reverse}}$ is domain-shattering and right-
separating.

The argument for completeness is this. Let $\mathit{O}\subseteq\Sigma^{*}$ be
the domain-shattering and right-separating objective from Lemma 5. We have

$\preceq\ \overset{\text{Definition}}{\subseteq}\ \preceq_{\mathit{O}}\
\overset{\text{Prop.~{}\ref{Proposition:Completeness}}}{\subseteq}\
\sqsubseteq_{\mathit{O}}\ \overset{\text{Shattering}}{\vphantom{\subseteq}=}\
\sqsubseteq\ \overset{\text{Soundness,
Prop.~{}\ref{Proposition:Soundness}}}{\subseteq}\ \preceq.$

###  6.1 Completeness Proof, Specialized Case

To show Proposition 3, fix a right-separating $\mathit{O}\subseteq\Sigma^{*}$.
With the normalization in Proposition 2 and soundness of the axiomatic
precongruence in Proposition 1, it is sufficient to show completeness for
terms in normal form. For $\mathit{p},\mathit{q}\in\mathit{NF}_{\mathsf{h}}$,
we want to show that $\mathit{p}\not\sqsubseteq_{\mathit{O}}\mathit{q}$
implies $\mathit{p}\not\preceq_{\mathit{O}}\mathit{q}$ by giving a context
that tells them apart. This, however, is difficult as it requires us to
understand precisely when the axiomatic congruence fails.

Our way out is to define a less flexible preorder that is easier to handle.
The _domination preorder_ $\subseteq_{\mathit{O}}$ only relates normal form
terms of the same urgency and owned by the same player. It is defined by
induction on the urgency. For $w,v\in\mathit{NF}_{0}$, we have
$w\subseteq_{\mathit{O}}v$ if $w\leq^{s}_{\mathit{O}}v$. For $\mathsf{u}>0$:

$\mathop{\ooalign{\raisebox{-3.5pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}\crcr$\bigwedge$}}P\subseteq_{\mathit{O}}\mathop{\ooalign{\raisebox{-3.5pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}\crcr$\bigwedge$}}Q\;\text{
if }\forall\mathit{s}\in Q.\exists\mathit{r}\in
P.\mathit{r}\subseteq_{\mathit{O}}\mathit{s}\quad\mathop{\ooalign{\raisebox{4.2pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}\crcr$\bigvee$}}P\subseteq_{\mathit{O}}\mathop{\ooalign{\raisebox{4.2pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}\crcr$\bigvee$}}Q\;\text{
if }\forall\mathit{r}\in P.\exists\mathit{s}\in
Q.\mathit{r}\subseteq_{\mathit{O}}\mathit{s}$

Proposition 3 holds with the following lemma, which we prove in Appendix 0.F.

######  Lemma 6.

For a right-separating objective $\mathit{O}$,
$\mathit{p}\preceq_{\mathit{O}}\mathit{q}$ implies
$\mathit{p}\subseteq_{\mathit{O}}\mathit{q}$ and
$\mathit{p}\subseteq_{\mathit{O}}\mathit{q}$ implies
$\mathit{p}\sqsubseteq_{\mathit{O}}\mathit{q}$.

##  7 Decidability and Complexity

We study the decidability and complexity of checking the contextual preorder
and its specialized variant. To this end, we leave the setting of infinitary
syntax and call $\mathit{p}$ _finitary_ , if it refers to a finite set of non-
terminals $(N,\mathit{E})$ and all defining terms $\mathit{E}(A)$ and
$\mathit{p}$ itself are finite. We make the decision problem parametric in the
relation $\mathit{R}$ to be checked, and instantiate $\mathit{R}$ with
$\simeq$, $\simeq_{\mathit{O}}$, and $\preceq_{\mathit{O}}$:

> Given: Finitary $\mathit{p},\mathit{q}$ over $\Sigma$, $(N,\mathit{E})$ of
> urgency $\mathsf{h}$. Problem: Does $\mathit{p}\ \mathit{R}\ \mathit{q}$
> hold?

The first finding is that already the contextual equivalence is undecidable.
The proof is by a reduction from the equivalence problem for context-free
languages and the result continues to hold if we fix an alphabet with at least
two letters. A consequence is that the specialized contextual equivalence for
domain-shattering objectives is also undecidable.

######  Proposition 4.

$\mathsf{h}$-DEC-$\simeq$ and $\mathsf{h}$-DEC-$\simeq_{\mathit{O}}$ with
$\mathit{O}$ domain-shattering are undecidable for every $\mathsf{h}$.

Recall that the language $w.w^{\mathit{reverse}}$ is domain-shattering, so
already context-free objectives lead to undecidability.

Our main result in this section is that for regular objectives the specialized
contextual preorder is decidable. We can also give the precise complexity, for
which we measure the size of the input in the expected way as
$|{\mathit{p}}|+|{\mathit{q}}|+|{\Sigma}|+|{\mathit{E}}|$. The size of the
defining equations is $|{\mathit{E}}|=\sum_{A\in N}1+|{\mathit{E}(A)}|$. The
size of a term is $|{\mathsf{skip}}|=|{\mathsf{err}}|=|{a}|=|{A}|=1$,
$|{\mathit{p}.\mathit{q}}|=1+|{\mathit{p}}|+|{\mathit{q}}|$, and
$|{{}^{\mathsf{u}}P}|=1+\sum_{\mathit{p}\in P}|{\mathit{p}}|$.

######  Theorem 7.1.

Let $\mathsf{h}$ be an urgency. For every regular objective
$\mathit{O}\neq\emptyset$, the problem $\mathsf{h}$-DEC-$\preceq_{\mathit{O}}$
is PTIME-complete.

It is worth noting that the result does not expect the objective to be right-
separating. We can indeed decide the specialized contextual preorder
$\preceq_{\mathit{O}}$ for all regular objectives $\mathit{O}$. Moreover, the
lower bound holds no matter the objective.

It is natural to define a variant $\mathsf{h}$-DEC-$\preceq_{*}$ of the
problem in which also the objective is part of the input and given as a
deterministic finite automaton
$(\Sigma,\mathpzc{Q},\mathpzc{i},\delta,\mathpzc{F})$. In this case, we use
$|{\mathit{O}}|$ to refer to $|{\Sigma}|+|{\mathpzc{Q}}|$. The following
result shows the dramatic influence that the objective has on the complexity.

######  Theorem 7.2.

$\mathsf{h}$-DEC-$\preceq_{*}$ is
$(2\mathsf{h}-1)-{\textsf{EXPTIME}}$-complete.

A consequence is that we can also solve the problem of making an observation,
denoted as $\mathsf{h}$-DEC-${}\Downarrow{}$ and defined with almost the same
input as $\mathsf{h}$-DEC-$\preceq_{*}$.

######  Corollary 1.

$\mathsf{h}$-DEC-${}\Downarrow{}$ is
$(2\mathsf{h}-1)-{\textsf{EXPTIME}}$-complete.

##  8 Upper Bound

We prove the upper bounds claimed in Theorems 7.1 and 7.2 as follows.

######  Proposition 5.

Given finitary terms $\mathit{p}$ and $\mathit{q}$ and a regular objective
$\mathit{O}$ as a DFA, deciding $\mathit{p}\preceq_{\mathit{O}}\mathit{q}$ can
be done in time
$(|{\mathit{p}}|+|{\mathit{q}}|+|{\mathit{E}}||{N}|)\cdot\mathrm{exp}_{2\mathsf{h}-1}(\mathcal{O}(|{\mathit{O}}|^{2}))$.

The undecidability result in Proposition 4 shows that the normal form for the
axiomatic congruence from Section 5 is insufficient as a basis for algorithms.
The problem is that the normal form terms are typically infinite, and
therefore difficult to handle computationally. The source of infinity can be
found in the base case: already
$\mathit{NF}_{0}=\Sigma^{*}\cup\\{\mathsf{err}\\}$ is infinite, and this
propagates upwards. We realize that the $\mathit{O}$-specialized axiomatic
congruence admits a more refined normal form that is guaranteed to yield
finite terms (and finitely many of them). The key idea is to factorize
$\mathit{NF}_{0}$ using Figure 4(g).

We define the set of _$\mathit{O}$ -specialized normal form terms_ by
induction on the urgency. The base case
$\mathit{SNF}_{0}^{\mathit{O}}=\Sigma_{\mathsf{err}}^{*}/_{\cong^{s}_{\mathit{O}}}$
are classes of words in the syntactic congruence $\cong^{s}_{\mathit{O}}\ =\
\leq^{s}_{\mathit{O}}\cap\geq^{s}_{\mathit{O}}$ induced by $\mathit{O}$. For
$\mathsf{u}>0$, the definition is

$\displaystyle\mathit{SANF}_{\mathsf{u}}^{\mathit{O}}\ =\
\\{\mathop{\ooalign{\raisebox{-3.5pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}\crcr$\bigwedge$}}P\mid\emptyset\neq
P\subseteq\mathit{SNF}_{\mathsf{u}-1}^{\mathit{O}}\\}\quad\mathit{SNF}_{\mathsf{u}}^{\mathit{O}}\
=\
\\{\mathop{\ooalign{\raisebox{4.2pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}\crcr$\bigvee$}}P\mid\emptyset\neq
P\subseteq\mathit{SANF}_{\mathsf{u}}^{\mathit{O}}\\}\ .$

Note that since $\mathit{O}$ is regular, the set
$\mathit{SNF}_{0}^{\mathit{O}}$ and so all
$\mathit{SANF}_{\mathsf{u}}^{\mathit{O}}$ and
$\mathit{SNF}_{\mathsf{u}}^{\mathit{O}}$ are guaranteed to be finite [24].
Another aspect is that we change the alphabet to having
$\cong^{s}_{\mathit{O}}$-congruence classes as letters. This can be fixed by
working with a representative system: we represent every
$\cong^{s}_{\mathit{O}}$-class by one of its elements.

We adapt the normalization process from Section 5 to compute a term in the
$\mathit{O}$-specialized normal form. Only the base case changes, for the
inductive cases we merely study the complexity. Interestingly, the overall
normalization takes time $2\mathsf{h}$-fold exponential only in the size of
the objective, using the common definition $\mathrm{exp}_{0}(x)=x$ and
$\mathrm{exp}_{\mathsf{u}+1}(x)=2^{\mathrm{exp}_{\mathsf{u}}(x)}$.

######  Lemma 7.

Given a finitary term $\mathit{p}$ and a regular objective
$\mathit{O}\subseteq\Sigma^{*}$ as a DFA, we can compute
$\mathsf{nf}_{\mathit{O}}(\mathit{p})\in\mathit{SNF}_{\mathsf{h}}^{\mathit{O}}$
with $\mathsf{nf}_{\mathit{O}}(\mathit{p})\equiv_{\mathit{O}}\mathit{p}$ in
time
$(|{\mathit{p}}|+|{\mathit{E}}||{N}|)\cdot\mathrm{exp}_{2\mathsf{h}-1}(\mathcal{O}(|{\mathit{SNF}_{0}^{\mathit{O}}}|))$.
We have
$|{\mathit{SNF}_{\mathsf{h}}^{\mathit{O}}}|=\mathrm{exp}_{2\mathsf{h}}(\mathcal{O}(|{\mathit{SNF}_{0}^{\mathit{O}}}|))$.

The result already allows us to decide the $\mathit{O}$-specialized contextual
preorder as follows. Since we cannot assume the objective to be right-
separating, the algorithm cannot rely on a full abstraction result. Instead,
we have to evaluate $\mathit{p}\preceq_{\mathit{O}}\mathit{q}$ directly, by
iterating over contexts. What makes this possible is the combination of our
proof technique for soundness in Lemma 1 and the $\mathit{O}$-specialized
normal form just introduced. With Lemma 1, we do not have to iterate over all
contexts to show $\mathit{p}\preceq_{\mathit{O}}\mathit{q}$, but only over
contexts of the form $\mathit{r}.\bullet.\mathit{s}$. With Lemma 7, the terms
$\mathit{r}$ and $\mathit{s}$ can be normalized.

######  Corollary 2.

Let $\mathit{O}$ be regular and $\mathit{p},\mathit{q}$ finitary. Then
$\mathit{p}\preceq_{\mathit{O}}\mathit{q}$ iff for all
$c[{\bullet}]=\mathit{r}.\bullet.\mathit{s}$ with
$\mathit{r}\in\mathit{SNF}_{\mathsf{h}-1}^{\mathit{O}}$,
$\mathit{s}\in\mathit{SNF}_{\mathsf{h}}^{\mathit{O}}$ we have
${\mathsf{nf}_{\mathit{O}}(c[{\mathit{p}}])}\Downarrow{\mathit{O}}$ implies
${\mathsf{nf}_{\mathit{O}}(c[{\mathit{q}}])}\Downarrow{\mathit{O}}$.

The algorithm formulated in the corollary is slower than the promised upper
bound by two exponents because $\mathit{SNF}_{\mathsf{h}}^{\mathit{O}}$
contains $\mathrm{exp}_{2\mathsf{h}+1}(\mathcal{O}(|{\mathit{O}}|^{2}))$ many
terms. To overcome the problem, the first step is to reduce the number of
contexts that have to be considered. The idea is to factorize the contexts
along their solution spaces. The solution space of a context is the set of
terms $\mathit{p}$ for which ${c[{\mathit{p}}]}\Downarrow{\mathit{O}}$ holds.
When checking for $\mathit{p}\preceq_{\mathit{O}}\mathit{q}$, the job of a
context $c[{\bullet}]$ is to disprove
$\mathit{p}\preceq_{\mathit{O}}\mathit{q}$ by showing
${c[{\mathit{p}}]}\Downarrow{\mathit{O}}$ and
${c[{\mathit{q}}]}\mathrel{\mathchoice{\ooalign{$\displaystyle\Downarrow$\crcr$\displaystyle/$}{}}{\ooalign{$\textstyle\Downarrow$\crcr$\textstyle/$}{}}{\ooalign{$\scriptstyle\Downarrow$\crcr$\scriptstyle/$}{}}{\ooalign{$\scriptscriptstyle\Downarrow$\crcr$\scriptscriptstyle/$}{}}}{\mathit{O}}$.
Hence, when two contexts have the same solution space, it suffices to consider
one of them.

What makes the solution space equivalence algorithmically interesting is that
(i) it is coarse enough to save an exponent and (ii) we can directly compute
with equivalence classes of contexts. The key insight behind both statements
is that the solution space of a context can be represented in a convenient
way: it is the $\sqsubseteq_{\mathit{O}}$-upward closure of a so-called
_characteristic term_.

######  Definition 5.

Term $\mathit{p}$ is _characteristic for $c[{\bullet}]$ wrt.
$\mathit{O}\subseteq\Sigma^{*}$_, if for all $\mathit{q}\in\mathbf{T}$ we have
${c[{\mathit{q}}]}\Downarrow{\mathit{O}}$ if and only if
$\mathit{p}\sqsubseteq_{\mathit{O}}\mathit{q}$.

We will show that there are only
$\mathrm{exp}_{2\mathsf{h}}(\mathcal{O}(|{\mathit{O}}|^{2}))$ many
characteristic terms for contexts of the form $\mathit{r}.\bullet.\mathit{s}$.
Moreover, we can compute the characteristic terms directly, without building
up the corresponding contexts. This saves an exponent in the complexity: we
modify the algorithm in Corollary 2 to iterate through characteristic terms
rather than contexts.

We save another exponent in the runtime of our algorithm by a more compact
representation of the terms in $\mathit{O}$-specialized normal form. One
exponent in the size of $\mathit{SNF}_{\mathsf{h}}^{\mathit{O}}$ is inherited
from the base case, where already
$|{\mathit{SNF}_{0}^{\mathit{O}}}|=\mathrm{exp}_{1}(\mathcal{O}(|{\mathit{O}}|^{2}))$.
We use the fact that each class of the syntactic congruence can be represented
by a function $\mathpzc{Q}\to\mathpzc{Q}$ between the states of the objective
DFA [24]. The key idea is to see these functions as sets of state-pairs. We
simulate a function, say for letter $a$, by letting Eve choose a state change
$(\mathpzc{p},\mathpzc{q})$ with $\delta(\mathpzc{p},a)=\mathpzc{q}$. We thus
represent the congruence class
$[{a}]\in\Sigma_{\mathsf{err}}^{*}/\cong^{s}_{\mathit{O}}$ by an angelic
choice of urgency $1$ over letters from the alphabet
$\mathpzc{Q}\times\mathpzc{Q}$. The modification propagates to the normal form
terms, and requires a simple modification of the objective. The new objective
$\mathsf{tr}(\mathit{O})$ has a syntactic congruence with an exponentially
smaller index, namely
$|{\mathit{SNF}_{0}^{\mathsf{tr}(\mathit{O})}}|=\mathcal{O}(|{\mathit{O}}|^{2})$.

Details on the compact term representation and on how to utilize
characteristic terms are given in Appendix 0.K.

##  9 Lower Bound and Applications

We show how to reduce well-known program verification tasks to the problem of
making an observation. The first reduction justifies our complexity lower
bound.

#### Multi-pushdown systems (MPDS).

MPDS are a model for concurrent programs with recursive threads that
synchronize through a shared, finite memory [25, 26]. MPDS are Turing complete
[27]. For bug hunting, it is therefore common to under-approximate their
behavior by limiting the number of context switches [25]. A context is a
sequence of transitions that operate only on one stack, and a context switch
is the moment when this stack changes. We consider multi-pushdown games
(MPDG), the alternating variant of MPDS. A _$\mathsf{b}$ -context-bounded
2-stack pushdown game ($\mathsf{b}$-2PDG)_ is an MPDG with two stacks.

######  Theorem 9.1.

[17, 26] $\mathsf{b}$-2PDG are $(\mathsf{b}-2)-{\textsf{EXPTIME}}$-complete.

Our lower bound is due to the following result that we prove in Appendix 0.P.

######  Proposition 6.

Given a $(2\mathsf{h}+1)$-2PDG $\mathsf{PD}$, we can compute in polynomial
time an alphabet $\Sigma$, a term $\mathit{p}$ and non-terminals
$(N,\mathit{E})$ over $\Sigma$ all of maximal urgency $\mathsf{h}$, and an
objective DFA $\mathit{O}$ so that Eve wins $\mathsf{PD}$ if and only if
${\mathit{p}}\Downarrow{\mathit{O}}$.

#### Hyper model checking (HMC).

Hyperproperties [18] are program properties that refer to sets of
computations, as opposed to the classical linear-time properties [2] that
refer to single computations. The corresponding logics [19] express
hyperproperties by quantifying over the computations of the program
$\mathcal{K}$, as in

$\displaystyle\mathsf{HP}\quad=\quad\forall w_{1}\in\mathit{L}(\mathcal{K}).\
\exists w_{2}\in\mathit{L}(\mathcal{K})\ \ldots\
\mathsf{Q}w_{n}\in\mathit{L}(\mathcal{K}).\ w_{1}\oplus\ldots\oplus
w_{n}\in\mathit{L}_{\mathsf{HP}}\ .$

We use $\oplus$ to denote the convolution of words. The convolution expects
words of the same length (that is then chosen by the first quantifier) and
forms their letter-by-letter product, meaning $\mathit{L}_{\mathsf{HP}}$ is a
language over an alphabet ${\Sigma^{n}}$. The hyper model checking problem
(HMC) asks whether a given program satisfies a given hyperproperty, denoted by
$\mathcal{K}\vDash\mathsf{HP}$. The standard way of solving HMC is to compose
the program with $\mathit{L}_{\mathsf{HP}}$, and then repeatedly with itself
[28, 29]. We show how to encode HMC into the problem of making an observation
for urgency terms. To be precise, HMC is usually defined over infinite words,
but we consider a finite-word version. The details are in Appendix 0.M.

######  Theorem 9.2.

Given $\mathcal{K}$ and $\mathsf{HP}$, we can compute in polynomial time a
term $\mathit{p}_{\mathcal{K},\mathsf{HP}}$ and an objective $\mathit{O}$ so
that $\mathcal{K}\models\mathsf{HP}$ if and only if
${\mathit{p}_{\mathcal{K},\mathsf{HP}}}\Downarrow{\mathit{O}}$.

Interestingly, our reduction to urgency terms even yields decidability results
for HMC over recursive programs. As HMC generalizes inclusion, which is
undecidable for context-free languages, the recursive case needs a
restriction. We can work with a restriction similarly liberal as in the recent
positive results [30, 31], which form the decidability frontier for HMC.

#### Simulation, Inclusion, and Games with imperfect information.

As explained in the introduction, urgency terms can express inclusion and
simulation problems. We now give the details of the encoding, and also add
imperfect information games to the picture. Let
$\mathcal{A}=(\mathpzc{Q}_{\mathcal{A}},\delta_{\mathcal{A}},\mathpzc{i}_{\mathcal{A}},\mathpzc{F}_{\mathcal{A}})$
and
$\mathcal{B}=(\mathpzc{Q}_{\mathcal{B}},\delta_{\mathcal{B}},\mathpzc{i}_{\mathcal{B}},\mathpzc{F}_{\mathcal{B}})$
be non-deterministic finite automata. Let $\mathpzc{p},\mathpzc{q}$ range over
$\mathpzc{Q}_{\mathcal{A}}$ and $\mathpzc{r},\mathpzc{s},\mathpzc{t}$ over
$\mathpzc{Q}_{\mathcal{B}}$ with $\mathpzc{s}\neq\mathpzc{t}$. Imperfect
information games $(\mathcal{A},\mathsf{hd})$ (for a definition, refer to
[14]) are played on a finite automaton $\mathcal{A}$ and hide the concrete
states $\mathpzc{p}\in\mathpzc{Q}_{\mathcal{A}}$ from Adam and only present
him an abstraction $h$, using a function $\mathsf{hd}:\mathpzc{Q}\to H$. Such
a game is played in rounds in which Adam sees the abstraction $h\in H$ of the
current state $\mathpzc{p}$, chooses an action $a\in\Sigma$, and then Eve
selects a transition from $\mathpzc{p}$ for that action. Eve wins $\mathit{G}$
when she can force the play from the initial state $\mathpzc{i}_{\mathcal{A}}$
into a final state in $\mathpzc{F}_{\mathcal{A}}$.

We give the defining equations for the non-terminals:

$\displaystyle A_{\mathpzc{p}}^{\subseteq}$
$\displaystyle=\mathop{\ooalign{\raisebox{4.2pt}{$\scriptstyle{\mathsf{2}}$}\crcr$\bigvee$}}\\{(\mathop{\ooalign{\raisebox{-3.5pt}{$\scriptstyle{\mathsf{1}}$}\crcr$\bigwedge$}}_{(\mathpzc{r},a,\mathpzc{s})\in\delta_{\mathcal{B}}}(\mathpzc{r},a,\mathpzc{s})).A_{\mathpzc{q}}^{\subseteq}\mid(\mathpzc{p},a,\mathpzc{q})\in\delta_{\mathcal{A}}\\}\cup\\{\mathsf{skip}\mid\mathpzc{p}\in\mathpzc{F}_{\mathcal{A}}\\}$
$\displaystyle A_{\mathpzc{p}}^{\precsim}$
$\displaystyle=\mathop{\ooalign{\raisebox{4.2pt}{$\scriptstyle{\mathsf{1}}$}\crcr$\bigvee$}}\\{(\mathop{\ooalign{\raisebox{-3.5pt}{$\scriptstyle{\mathsf{1}}$}\crcr$\bigwedge$}}_{(\mathpzc{r},a,\mathpzc{s})\in\delta_{\mathcal{B}}}(\mathpzc{r},a,\mathpzc{s})).A_{\mathpzc{q}}^{\precsim}\mid(\mathpzc{p},a,\mathpzc{q})\in\delta_{\mathcal{A}}\\}\cup\\{\mathsf{skip}\mid\mathpzc{p}\in\mathpzc{F}_{\mathcal{A}}\\}$
$\displaystyle A_{h}$
$\displaystyle=\mathop{\ooalign{\raisebox{-3.5pt}{$\scriptstyle{\mathsf{1}}$}\crcr$\bigwedge$}}_{a\in\Sigma}\mathop{\ooalign{\raisebox{4.2pt}{$\scriptstyle{\mathsf{1}}$}\crcr$\bigvee$}}\\{A_{h^{\prime}}.\mathop{\ooalign{\raisebox{4.2pt}{$\scriptstyle{\mathsf{1}}$}\crcr$\bigvee$}}_{{(\mathpzc{p},a,\mathpzc{q})\in\delta_{\mathcal{A}},\mathsf{hd}(\mathpzc{q})=h^{\prime}}}(\mathpzc{p},a,\mathpzc{q})\mid
h^{\prime}\in
H\\}\cup\\{\mathsf{skip}\mid\mathpzc{p}\in\mathpzc{F}_{\mathcal{A}}\\}$

The only difference between the encodings of inclusion and simulation is the
urgency of the angelic choice. In the case of inclusion, Adam only has to make
a demonic choice when Eve has chosen the entire word. For simulation, the
players take turns. For imperfect information games, Adam chooses the letter
and Eve chooses the abstraction of the next state that will be made visible to
Adam and the actual transition that is consistent with the letter and the
abstraction. The point is that Adam should see the abstraction but not see the
transition. We achieve this with a left-linear grammar where Eve’s choice for
the next transition will only be revealed when Adam has made all choices. By
using urgency two, we could have avoided this trick and used a right-linear
model. In all cases, the task of the objective $\mathit{O}$ is to check that
we have successive transitions.

######  Theorem 9.3.

${A_{\mathpzc{i}_{\mathcal{A}}}^{\subseteq}}\Downarrow{\mathit{O}}$ if and
only if $\mathcal{L}(\mathcal{A})\not\subseteq\mathcal{L}(\mathcal{B})$,
${A_{\mathpzc{i}_{\mathcal{A}}}^{\precsim}}\Downarrow{\mathit{O}}$ if and only
if $\mathcal{A}\not\precsim\mathcal{B}$,
${A_{{\mathsf{hd}(\mathpzc{i}_{\mathcal{A}})}}}\Downarrow{\mathit{O}}$ if and
only if Eve wins $(\mathcal{A},\mathsf{hd})$.

It would strengthen the usefulness of urgency terms if the above reductions
gave optimal complexity upper bounds. With what we have, this is true only for
imperfect information games, which are EXPTIME-complete [14]. The inclusion
problem is PSPACE-complete, but Corollary 1 only yields 3-EXPTIME upper bound.
Simulation is PTIME-complete, but Corollary 1 yields an EXPTIME upper bound.
The problem with simulation can be fixed with a different encoding that is
also natural but does not show the similarity to language inclusion. There, we
use the fact that the objective is fixed and a consequence of Theorem 7.1 that
is similar to Corollary 1. In the following, we close the gap for language
inclusion.

We identify natural subclasses of urgency terms and study their verification
problems. In the term constructed for inclusion, for every urgency there is a
single player that makes a choice. This is not true for simulation nor for
imperfect information games. We call this fragment the _weak urgency terms_.
Linear grammars as used in $A_{\mathpzc{i}_{\mathcal{A}}}^{\subseteq}$,
$A_{\mathpzc{i}_{\mathcal{A}}}^{\precsim}$, and
$\mathit{p}_{\mathcal{K},\mathsf{HP}}$ further reduce the complexity. The
definition of weak and linear terms can be found in Appendix 0.O.

######  Theorem 9.4.

$\mathsf{h}$-DEC-${}\Downarrow{}$ for weak, linear terms is in
$(\mathsf{h}-2)$-EXPSPACE.

This yields the desired tight upper bound not only for inclusion checking, but
also for the hyper model checking of non-recursive programs [32].

#### Procedure summaries.

Procedure summaries [33, 34, 35] are a standard technique for the analysis of
recursive programs. We now show how to derive procedure summaries from our
axiomatization. The benefit is that the axiomatization guides the development
of summaries, and thus reduces the moment of ingenuity required to come up
with them.

Summaries are a closed-form representation of the call-return behavior of a
recursive procedure. For functions, such a closed-form representation would
capture the input-output behavior. In the context of linear-time model
checking, the call-return behavior is the state change that the procedure may
induce on the observer automaton. Procedure summaries are typically computed
as a fixed point over a suitable domain. We now rediscover these domains as
the normal forms for urgency terms. Our development covers the game version as
well.

Pushdown games [34, 35] extend recursive programs by alternation. We can
assume reachability as the winning condition because parity can be reduced to
reachability in polynomial time [36]. Let
$\mathcal{P}=(\mathpzc{Q}_{\mathit{E}},\mathpzc{Q}_{\mathit{A}},\Sigma,\Gamma,\delta,\mathpzc{F})$
be a pushdown game with transitions
$\delta=(\delta_{\mathit{int}},\delta_{\mathit{push}},\delta_{\mathit{pop}})$.
For convenience, we assume that final states in $\mathpzc{F}$ do not have
outgoing transitions, but only loops that empty the stack. We solve two
verification tasks:  (a) whether Eve can force the play into a final state
(b) while also producing a trace of observations from $\Sigma$ accepted by a
DFA $\mathcal{A}$.  We model both with the same urgency grammar. The alphabet
are again state changes $(\mathpzc{p},a,\mathpzc{q})$, this time of the
pushdown, and the objective $\mathit{O}$ checks whether they form a path. We
define non-terminals $A_{x}^{\mathpzc{p}}$ that express the fact that the
current procedure is $x$ and the current state is $\mathpzc{p}$. In the
definition, is $\bigvee$ if Eve owns the state, and $\bigwedge$ if Adam owns
the state, $a\in\Sigma$ is a letter, and $x,y\in\Gamma$ are stack symbols:

$\displaystyle A_{x}^{\mathpzc{p}}\ =\
\mathop{\ooalign{\raisebox{2.4pt}{$\scriptstyle{\mathsf{1}}$}\crcr$\bigovoid$}}{}$
$\displaystyle\\{(\mathpzc{p},a,\mathpzc{q}).A_{x}^{\mathpzc{q}}\mid(\mathpzc{p},a,\mathpzc{q})\in\delta_{\mathit{int}}\\}$
$\displaystyle A_{x}\ $ $\displaystyle=\
\mathop{\ooalign{\raisebox{4.2pt}{$\scriptstyle{\mathsf{1}}$}\crcr$\bigvee$}}\\{A_{x}^{\mathpzc{p}}\mid\mathpzc{p}\in\mathpzc{Q}\\}$
$\displaystyle\cup\ $
$\displaystyle\\{(\mathpzc{p},a,\mathpzc{q}).A_{y}^{\mathpzc{q}}.A_{x}\mid{(\mathpzc{p},a,\mathpzc{q},y)\in\delta_{\mathit{push}}}\\}$
$\displaystyle\cup\ $
$\displaystyle\\{(\mathpzc{p},a,\mathpzc{q})\mid{(\mathpzc{p},a,\mathpzc{q},y)\in\delta_{\mathit{pop}}}\\}\
.$

We observe that the normal form
$\mathsf{nf}(A_{x}^{\mathpzc{p}})=\mathop{\ooalign{\raisebox{4.2pt}{$\scriptstyle{\mathsf{1}}$}\crcr$\bigvee$}}_{i\in
I}\mathop{\ooalign{\raisebox{-3.5pt}{$\scriptstyle{\mathsf{1}}$}\crcr$\bigwedge$}}R_{i}$
is an Eve choice over a set $I$ followed by an Adam choice over sets
$R_{i}\subseteq\mathpzc{Q}\times\Sigma_{\mathsf{err}}^{*}/_{\cong^{s}_{\mathcal{L}(\mathcal{A})}}\times\mathpzc{Q}$.
By definition, every element of $R_{i}$ has $\mathpzc{p}$ as the first
component. Each $i\in I$ corresponds to a strategy $\sigma$ that Eve can
follow from state $\mathpzc{p}$ with the top of stack being $x$ until this
symbol is popped. An element $(\mathpzc{p},[{w}],\mathpzc{q})\in R_{i}$ thus
corresponds to a play through the pushdown according to $\sigma$ that ends in
state $\mathpzc{q}$ after $x$ has been popped, and the play produces an
observation $v\in[{w}]$. If $\mathcal{L}(\mathcal{A})=\Sigma^{*}$, the middle
part of our summaries becomes irrelevant. This is (up to parity tracking) the
domain that Walukiewicz uses to solve pushdown games in EXPTIME [34], which
matches our complexity. For other DFA, we obtain the summaries for pushdown
games with inclusion objectives [35]. To be precise, we obtain an EXPTIME
rather than a 2-EXPTIME upper bound because we assume the objective to be
deterministic.

##  10 Related Work

Urgency annotations are related to priorities in process algebra [37]. The key
difference is that priorities preserve the program order while urgencies do
not. This out-of-order execution brings a new form of unbounded memory to the
semantics (the unresolved choices) that our axiomatization explains how to
handle. Also alternation [38] is not common in process algebra. Indeed, we
have not found a study of angelic and demonic choice from the perspective of
contextual equivalence. It is the special case of our work when the urgency is
$\mathsf{h}=1$.

Our axiomatization is related to Salomaa’s work on language equivalence [39]
and Milner’s on bisimilarity [40]. The former reference is particularly close:
our Axioms (D1) and (D2) generalize Salomaa’s Axioms (A4) and (A5) to higher
urgencies. Also our context lemma for proving soundness has relatives in
process algebra [41]. Characteristic objects (here, contexts and terms) have
appeared as early as [42]. Our contribution is to adapt the general idea to
our setting.

We showed that urgency programs can capture hyper model checking over regular
languages. Hyper model checking remains decidable if one language is context-
free and the others are regular [43]. We can model this fragment with urgency
programs as well. Urgency programs combine recursion and imperfect
information. This is interesting as the canonical pushdown games with
imperfect information [44] are known to be undecidable even under strong
restrictions [45].

The goal of effective denotational semantics [46, 47] is to solve verification
problems with tailor-made denotational semantics. Given a specification
$\mathit{O}$, the task is to derive a denotational semantics
$\mathcal{D}_{\mathit{O}}$ such that $\mathcal{D}_{\mathit{O}}(\mathit{p})$
answers the question of whether program $\mathit{p}$ satisfies specification
$\mathit{O}$. Satisfying a specification coincides with our notion of making
an observation, ${\mathit{p}}\Downarrow{\mathit{O}}$. The link is close. In
Appendix 0.Q.1, we show how our axiomatization of the specialized contextual
preorder induces a denotational semantics that is effective for finitary
programs. This shows that the semantic domain can be obtained in a systematic
way. The landmark result in this field is an effective denotational semantics
that captures the higher-order model-checking problem [48]. It would be
interesting to consider it from the axiomatic point of view.

##  11 Conclusion and Future Work

We presented urgency annotations for alternating choices as a new programming
construct and studied the standard notions of contextual equivalence for the
resulting programs. We gave sound and complete axiomatizations and settled the
complexity. Our findings can be used to obtain new algorithms for verification
and synthesis tasks, as we demonstrated on examples.

The next step is to extend urgency programs to infinite words. The challenge
is to find the right semantics. If we define the semantics via infinite
unrollings, then it is unclear how to ever switch to choices with lower
urgency. Instead, it seems appropriate to work with programs that contain an
$\omega$-operator and can be rewritten a finite number of times. This,
however, calls for a different set of algebraic techniques [49].

## References

  * [1] R. Milner, “An algebraic definition of simulation between programs,” in _IJCAI_. Kaufmann, 1971, pp. 481–489.
  * [2] A. Pnueli, “The temporal logic of programs,” in _FOCS_. IEEE, 1977, pp. 46–57.
  * [3] M. Y. Vardi and P. Wolper, “An automata-theoretic approach to automatic program verification,” in _LICS_. IEEE, 1986, pp. 332–344.
  * [4] E. A. Emerson and C. S. Jutla, “Tree automata, mu-calculus and determinacy,” in _FOCS_. IEEE, 1991, pp. 368–377.
  * [5] A. Finkel, “A generalization of the procedure of Karp and Miller to well structured transition systems,” in _ICALP_ , ser. LNCS, vol. 267. Springer, 1987, pp. 499–508.
  * [6] P. A. Abdulla and B. Jonsson, “Verifying programs with unreliable channels,” in _LICS_. IEEE, 1993, pp. 160–170.
  * [7] A. Finkel and P. Schnoebelen, “Well-structured transition systems everywhere!” _TCS_ , vol. 256, no. 1-2, pp. 63–92, 2001.
  * [8] C. L. Ong, “On model-checking trees generated by higher-order recursion schemes,” in _LICS_. IEEE, 2006, pp. 81–90.
  * [9] N. Kobayashi and C. L. Ong, “A type system equivalent to the modal mu-calculus model checking of higher-order recursion schemes,” in _LICS_. IEEE, 2009, pp. 179–188.
  * [10] N. Kobayashi, R. Sato, and H. Unno, “Predicate abstraction and CEGAR for higher-order model checking,” in _PLDI_. ACM, 2011, pp. 222–233.
  * [11] A. Finkel and J. Goubault-Larrecq, “Forward analysis for WSTS, part I: completions,” in _STACS_ , ser. LIPIcs, vol. 3. Dagstuhl, 2009, pp. 433–444.
  * [12] J. Kloos, R. Majumdar, F. Niksic, and R. Piskac, “Incremental, inductive coverability,” in _CAV_ , ser. LNCS, vol. 8044. Springer, 2013, pp. 158–173.
  * [13] A. K. Chandra, D. Kozen, and L. J. Stockmeyer, “Alternation,” _JACM_ , vol. 28, no. 1, pp. 114–133, 1981.
  * [14] J. H. Reif, “The complexity of two-player games of incomplete information,” _JCSS_ , vol. 29, no. 2, pp. 274–301, 1984.
  * [15] R. Milner, “Fully abstract models of typed $\lambda$-calculi,” _TCS_ , vol. 4, no. 1, pp. 1–22, 1977.
  * [16] G. Jaber and A. S. Murawski, “Complete trace models of state and control,” in _ESOP_ , ser. LNCS, vol. 12648. Springer, 2021, pp. 348–374.
  * [17] A. Seth, “Games on multi-stack pushdown systems,” in _LFCS_ , ser. LNCS, vol. 5407. Springer, 2009, pp. 395–408.
  * [18] M. R. Clarkson and F. B. Schneider, “Hyperproperties,” _JCS_ , vol. 18, no. 6, pp. 1157–1210, 2010.
  * [19] M. R. Clarkson, B. Finkbeiner, M. Koleini, K. K. Micinski, M. N. Rabe, and C. Sánchez, “Temporal logics for hyperproperties,” in _POST_ , ser. LNCS, vol. 8414. Springer, 2014, pp. 265–284.
  * [20] D. A. Martin, “Borel determinacy,” _AMATH_ , vol. 102, no. 2, pp. 363–371, 1975.
  * [21] M. Hennessy and R. Milner, “Algebraic laws for nondeterminism and concurrency,” _JACM_ , vol. 32, no. 1, pp. 137–161, 1985.
  * [22] J. A. Bergstra, A. Ponse, and S. A. Smolka, Eds., _Handbook of Process Algebra_. Elsevier, 2001.
  * [23] G. Birkhoff, _Lattice Theory_. AMS, 1967\.
  * [24] M. O. Rabin and D. S. Scott, “Finite automata and their decision problems,” _IBM J. Res. Dev._ , vol. 3, no. 2, pp. 114–125, 1959.
  * [25] S. Qadeer and J. Rehof, “Context-bounded model checking of concurrent software,” in _TACAS_ , ser. LNCS, vol. 3440. Springer, 2005, pp. 93–107.
  * [26] R. Meyer and S. van der Wall, “On the complexity of multi-pushdown games,” in _FSTTCS_ , ser. LIPIcs, vol. 182. Dagstuhl, 2020, pp. 52:1–52:35.
  * [27] G. Ramalingam, “Context-sensitive synchronization-sensitive analysis is undecidable,” _TOPLAS_ , vol. 22, no. 2, pp. 416–430, 2000.
  * [28] G. Barthe, P. R. D’Argenio, and T. Rezk, “Secure information flow by self-composition,” in _CSFW_. IEEE, 2004, pp. 100–114.
  * [29] B. Finkbeiner, M. N. Rabe, and C. Sánchez, “Algorithms for model checking HyperLTL and HyperCTL∗,” in _CAV_ , ser. LNCS, vol. 9206\. Springer, 2015, pp. 30–48.
  * [30] J. O. Gutsfeld, M. Müller-Olm, and C. Ohrem, “Deciding asynchronous hyperproperties for recursive programs,” _CoRR_ , vol. abs/2201.12859, 2022\.
  * [31] A. Bajwa, M. Zhang, R. Chadha, and M. Viswanathan, “Stack-aware hyperproperties,” in _TACAS_ , ser. LNCS, vol. 13993. Springer, 2023, pp. 308–325.
  * [32] M. N. Rabe, “A temporal logic approach to information-flow control,” Ph.D. dissertation, Saarland University, 2016.
  * [33] M. Sharir and A. Pnueli, _Two approaches to interprocedural data flow analysis_. New York, NY: New York Univ. Comput. Sci. Dept., 1978.
  * [34] I. Walukiewicz, “Pushdown processes: Games and model-checking,” _IC_ , vol. 164, no. 2, pp. 234–263, 2001.
  * [35] L. Holík, R. Meyer, and S. Muskalla, “Summaries for context-free games,” in _FSTTCS_ , ser. LIPIcs, vol. 65. Dagstuhl, 2016, pp. 41:1–41:16.
  * [36] M. Hague, R. Meyer, S. Muskalla, and M. Zimmermann, “Parity to safety in polynomial time for pushdown and collapsible pushdown systems,” in _MFCS_ , ser. LIPIcs, vol. 117. Dagstuhl, 2018, pp. 57:1–57:15.
  * [37] R. Cleaveland, G. Lüttgen, and V. Natarajan, “Priority in process algebra,” in _Handbook of Process Algebra_. Elsevier, 2001, pp. 711–765.
  * [38] A. K. Chandra and L. J. Stockmeyer, “Alternation,” in _FOCS_. IEEE, 1976, pp. 98–108.
  * [39] A. Salomaa, “Two complete axiom systems for the algebra of regular events,” _JACM_ , vol. 13, no. 1, pp. 158–169, 1966.
  * [40] R. Milner, “A complete inference system for a class of regular behaviours,” _JCSS_ , vol. 28, no. 3, pp. 439–466, 1984.
  * [41] A. Pitts and I. Stark, “Operational reasoning for functions with local state,” in _Higher Order Operational Techniques in Semantics_. CUP, 1998, pp. 227–273.
  * [42] R. McNaughton and S. A. Papert, _Counter-Free Automata_. MIT Press, 1971.
  * [43] A. Pommellet and T. Touili, “Model-checking HyperLTL for pushdown systems,” in _SPIN_ , ser. LNCS, vol. 10869. Springer, 2018, pp. 133–152.
  * [44] B. Aminof, A. Legay, A. Murano, O. Serre, and M. Y. Vardi, “Pushdown module checking with imperfect information,” _IC_ , vol. 223, pp. 1–17, 2013.
  * [45] L. Bozzelli, “New results on pushdown module checking with imperfect information,” in _GandALF_ , ser. EPTCS, vol. 54, 2011, pp. 162–177.
  * [46] K. Aehlig, “A finite semantics of simply-typed lambda terms for infinite runs of automata,” _LMCS_ , vol. 3, no. 3, 2007.
  * [47] K. Terui, “Semantic evaluation, intersection types and complexity of simply typed lambda calculus,” in _RTA_ , ser. LIPIcs, vol. 15. Dagstuhl, 2012, pp. 323–338.
  * [48] S. Salvati and I. Walukiewicz, “A model for behavioural properties of higher-order programs,” in _CSL_ , ser. LIPIcs, vol. 41. Dagstuhl, 2015, pp. 229–243.
  * [49] T. Wilke, “An algebraic theory for regular languages of finite and infinite words,” _Algebra and Computation_ , vol. 3, no. 4, pp. 447–489, 1993.
  * [50] L. M. Goldschlager, “The monotone and planar circuit value problems are log space complete for P,” _ACM SIGACT News_ , vol. 9, no. 2, pp. 25–29, 1977\.
  * [51] O. M. Committee. Openssl. [Online]. Available: openssl.org
  * [52] P. C. Kocher, “Timing attacks on implementations of Diffie-Hellman, RSA, DSS, and other systems,” in _CRYPTO_ , ser. LNCS, vol. 1109. Springer, 1996, pp. 104–113.
  * [53] D. Brumley and D. Boneh, “Remote timing attacks are practical,” in _USENIX Security_. USENIX Association, 2003.
  * [54] W. J. Savitch, “Relationships between nondeterministic and deterministic tape complexities,” _Journal of Computer and System Sciences_ , vol. 4, no. 2, pp. 177–192, 1970.

##  Appendix 0.A Handling Infinitary Syntax

For the development of the section, we call a term an $\mathsf{h}$-term when
no choice subterm has urgency higher than $\mathsf{h}$ and the expansion of
each non-terminal is an $\mathsf{h}$-term. Infinitary syntax requires care to
make sure that set theoretic concepts remain sound. The problem lies on the
unbounded nature of the choice operator. If we were to allow choices to range
over _arbitrary sets_ of terms, the class of all terms would no longer form a
set. To see this, suppose that the class of terms with unbounded choice were a
set $\mathbf{T}$. Then, we could build the term
${\mathop{\ooalign{\raisebox{4.2pt}{$\scriptstyle{\mathsf{\mathsf{u}}}$}\crcr$\bigvee$}}{\mathbf{T}}\in\mathbf{T}}$,
which contradicts the Axiom of Regularity. But for our development in the
paper, it is a convenience to have $\mathbf{T}$ as a set and not be distracted