# A First-Order Complete Temporal Logic for Structured Context-Free Languages

Michele Chiari0000-0001-7742-9233  DEIB, Politecnico di Milano, Italy
<EMAIL_ADDRESS>,  Dino Mandrioli0000-0002-0945-5947  DEIB,
Politecnico di Milano, Italy<EMAIL_ADDRESS>and  Matteo
Pradella0000-0003-3039-1084  DEIB, Politecnico di Milano, Italy and IEIIT,
Consiglio Nazionale delle Ricerche<EMAIL_ADDRESS>
###### Abstract.

The problem of model checking procedural programs has fostered much research
towards the definition of temporal logics for reasoning on context-free
structures. The most notable of such results are temporal logics on Nested
Words, such as CaRet and NWTL. Recently, the logic OPTL was introduced, based
on the class of Operator Precedence Languages (OPLs), more powerful than
Nested Words. We define the new OPL-based logic POTL and prove its FO-
completeness. POTL improves on NWTL by enabling the formulation of
requirements involving pre/post-conditions, stack inspection, and others in
the presence of exception-like constructs. It improves on OPTL too, which
instead we show not to be FO-complete; it also allows to express more easily
stack inspection and function-local properties. In a companion paper we report
a model checking procedure for POTL and experimental results based on a
prototype tool developed therefor. For completeness a short summary of this
complementary result is provided in this paper too.

###### Key words and phrases:

Linear Temporal Logic, Operator-Precedence Languages, Model Checking, First-
Order Completeness, Visibly Pushdown Languages, Input-Driven Languages

##  1\. Introduction

Linear Temporal Logic (LTL) is one of the most successful languages for the
specification and verification of system requirements. Being defined on a
linearly ordered algebraic structure, it is ideal to express safety and
liveness properties on a linear flow of events. In particular, LTL is
equivalent to First-Order Logic (FOL) on this structure [Kam68] and captures
the first-order definable fragment of ($\omega$-)regular languages. Its
satisfiability and model checking are PSPACE-complete with respect to formula
length but polynomial in model size.

The need for model checking software programs lead to several attempts at
widening the expressive power of specifications beyond LTL. Indeed, procedural
programs are often modeled with operational formalisms such as Boolean
programs [BR00], Pushdown Systems, and Recursive State Machines [ABE+05].
Reachability and LTL model checking have been extensively studied for such
systems [BEM97, EHRS00, ABE+05]. However, they present behaviors typical of
pushdown automata. Thus, many properties thereof cannot be expressed by a
formalism whose expressive power is limited to regular languages. Some early
attempts at extending the expressive power of specifications beyond regular
languages in model checking include equipping LTL with Presburger arithmetic
[BH96], using directly a class of pushdown automata for the specification
[KPV02], and a variant of Propositional Dynamic Logic that can express a
restricted class of Context-Free Languages (CFLs) [HKT02].

A natural way of generalizing LTL is defining temporal logics on more complex
algebraic structures. The introduction of logics based on _Nested Words_
[AM09], such as CaRet [AEM04], has been one of the first attempts in this
direction. Nested Words consist of a discrete, linear order with the addition
of a one-to-one nesting relation. They are equivalent to Visibly Pushdown
Languages (VPLs) [AM04], a.k.a. Input-Driven Languages [Meh80], a strict
subclass of deterministic CFLs. The parenthetical nature of VPLs results in
the nesting relation on words, which naturally models the one-to-one
correspondence between function calls and returns in procedural programs.
CaRet is the first temporal logic that extends LTL through explicit modalities
that refer to the underlying model’s context-free structure. Thus, CaRet can
easily express Hoare-style pre/post-conditions, stack inspection, and more.

The applications of Nested Words in model checking lead to the question of
which theoretical properties of LTL could be extended to them. One of the most
prominent is First-Order (FO) completeness. CaRet was devised with the
specification of procedural programs in mind, but its stance with respect to
FOL remains unknown, although it is conjectured not to be FO-complete
[AAB+08]. FO-completeness on Nested Words is thoroughly studied in [AAB+08],
and is achieved with Nested Words Temporal Logic (NWTL) and other logics. NWTL
satisfiability and model checking are EXPTIME-complete and retain
polinomiality on system size.

One natural further question is whether it is possible to define temporal
logics that capture a fragment of CFLs wider than VPLs. Several practical
applications motivate this question: the nesting relation of Nested Words is
one-to-one [MP18], preventing its ability to model behaviors in which a single
event is related to multiple ones. Such behaviors occur, e.g., in widespread
programming constructs such as exceptions, interrupts and continuations.

OPTL [CMP20] is a recent temporal logic that can express specifications
concerning, e.g., whether a function is terminated by an exception, or throws
one, and pre/post-conditions. OPTL is based on Operator Precedence Languages
(OPLs), which are a subclass of deterministic CFLs initially introduced with
the purpose of efficient parsing [Flo63], a field in which they continue to
offer useful applications [GJ08, BCM+15]. They strictly contain VPLs [CM12]
and retain all complexity, closure and decidability properties that make
regular languages and VPLs well-suited for temporal logics: they are closed
under Boolean operations, concatenation, Kleene *, and language emptiness and
inclusion are decidable [CM12]. They have also been characterized through
Monadic Second-Order Logic (MSO) [LMPP15]. This greater expressive power
results in OPTL being based on a structure called _OP word_ , made of a linear
order plus a nesting relation that can be one-to-many and many-to-one, and
considerably generalizes that of Nested Words. Indeed, OPTL is strictly more
expressive than NWTL, but retains the same satisfiability and model checking
complexity [CMP20]. However, the relationship between OPTL and FOL remained
unknown.

In this paper, we close this gap thanks to the novel temporal logic POTL
(Precedence-Oriented Temporal Logic). POTL too is based on OPLs and is devised
to easily navigate a word’s underlying syntax tree (ST). It is also based on
OP words, enabling reasoning on constructs such as exceptions, but has a
better ability to express properties on the context-free structure of words.
It features new until and since modalities based on _summary_ paths, which can
navigate a word’s ST up or down while skipping subtrees, and _hierarchical_
paths, which move between word positions where the nesting relation is many-
to-one or one-to-many.

The gap in expressive power between OPTL and POTL is both practical and
theoretical. In fact, in POTL it is easier to express stack inspection
properties in the presence of uncaught exceptions, as well as function-frame
local properties. We show that one of such properties is not expressible at
all in OPTL, but it is in POTL, and hence POTL is strictly more expressive
than OPTL.

Moreover, we prove that POTL is equivalent to FOL on both OP finite and
$\omega$-words. We obtain the result on finite words by translating an FO-
complete logic for finite trees [Mar04] to POTL. We then extend the proof to
$\omega$-words by employing a composition argument on trees proved with
Ehrenfeucht-Fraïssé games. This last proof is rather involved, as it needs to
distinguish between two classes of trees that arise from OP $\omega$-words.

As a corollary, we show that FOL has the three-variable property on OP words.
I.e., every FO formula on OP words is equivalent to another FOL formula in
which only three distinct variables appear. This property is related to FO-
completeness in temporal logics [Gab81] and holds both on simple Dedekind-
complete linear orders and Nested Words [AAB+08].

Recently, we also showed [MPC20b, MPC20a] that FO-definable OPLs coincide with
aperiodic or noncounting ones, according to a definition of aperiodic
structured CFLs which naturally extends the classic one for regular languages
[MP71]111Noticeably, this equivalence does not hold for tree-languages and
their FO-logic [Tho84, Heu91].. Whereas various regular languages of practical
usage are counting —e.g., many hardware devices are just counters modulo some
integer— we are not aware of programming languages or other CFLs of practical
interest, such as structured data description languages, that exhibit counting
properties: e.g., no language imposes to write programs with an even number of
nested loops. Thus, the breadth of coverage in terms of practical applications
of model-checking algorithms for an FO-complete logic is even larger for the
class of CFLs than that of classic model checkers for regular languages.

POTL’s expressiveness gains do not come at the cost of higher model checking
complexity, which remains EXPTIME-complete, as we show in [CMP21].

The paper is organized as follows: Section 2 provides some background on OPLs;
Section 3 presents the syntax and semantics of POTL, with some qualitative
demonstration of its expressive power and comparison with similar logics, and
the proof of the expressive _in_ completeness of OPTL; Section 4 proves the
equivalence of POTL to FOL on finite words; Section 5 extends this result to
$\omega$-words; Section 6 summarizes the results of the companion paper
[CMP21] where a model checker for OPLs based on POTL is provided, its
complexity evaluated, and experimental results are also reported; Section 7
concludes and proposes future research lines. Appendices A and B contain
proofs that did not fit into the main text.

We assume familiarity with classic topics of theoretical computer science,
specifically context-free grammars and languages, pushdown automata, parsing,
syntax tree (ST) (cf. [Har78]), $\omega$-languages, i.e., languages with
infinite words, and temporal logic —LTL in particular— [Eme90].

##  2\. Operator Precedence Languages

Operator Precedence Languages (OPLs) were originally defined through their
generating grammars [Flo63]: _operator precedence grammars_ (OPGs) are a
special class of context-free grammars (CFGs) in _operator normal form_ —i.e.,
grammars in which right-hand sides (rhs) of production rules contain no
consecutive non-terminals222Every CFG can be effectively transformed into an
equivalent one in operator form [Har78].—. As a consequence, the syntax trees
generated by such grammars never exhibit two consecutive internal nodes.

The distinguishing feature of OPGs is that they define three _precedence
relations_ (PR) between pairs of input symbols which drive the deterministic
parsing and therefore the construction of a unique ST, if any, associated with
an input string. For this reason we consider OPLs a kind of input-driven
languages, but larger then the original VPLs. The three PRs are denoted by the
symbols $\lessdot,\mathbin{\doteq},\gtrdot$ and are respectively named _yields
precedence, equal in precedence_ , and _takes precedence_. They graphically
resemble the traditional arithmetic relations but do not share their typical
ordering and equivalence properties; we kept them for “historical reasons”,
but we recommend the reader not to be confused by the similarity.

Intuitively, given two input characters $a,b$ belonging to a grammar’s
_terminal alphabet_ separated by at most one non-terminal, $a\lessdot b$ iff
in some grammar derivation $b$ is the first terminal character of a grammar’s
rhs following $a$ whether the grammar’s rule contains a non-terminal character
before $b$ or not (for this reasons we also say that non-terminal characters
are “transparent” in OPL parsing); $a\mathbin{\doteq}b$ iff $a$ and $b$ occur
consecutively in some rhs, possibly separated by one non-terminal; $a\gtrdot
b$ iff $a$ is the last terminal in a rhs —whether followed or not by a non-
terminal—, and $b$ follows that rhs in some derivation. The following example
provides a first intuition of how a set of _unique_ PRs drives the parsing of
a string of terminal characters in a deterministic way; subsequently the above
concepts are formalized.

Consider the alphabet of terminal symbols
$\Sigma=\\{\mathbf{call},\mathbf{ret},\mathbf{han},\mathbf{exc}\\}$: as the
chosen identifiers suggest, $\mathbf{call}$ represents the fact that a
procedure call occurs, $\mathbf{ret}$ represents the fact that a procedure
terminates normally and returns to its caller, $\mathbf{exc}$ that an
exception is raised and $\mathbf{han}$ that an exception handler is installed.
We want to implement a policy such that an exception aborts all the pending
calls up to the point where an appropriate handler is found in the stack, _if
any_ ; after that, execution is resumed normally. Calls and returns, as well
as possible pairing of handlers and exceptions are managed according to the
usual LIFO policy. The alphabet symbols are written in boldface for reasons
that will be explained later but are irrelevant for this example.

The above policy is implemented by the PRs described in Figure 1 which
displays the PRs through a square matrix, called _operator precedence matrix
(OPM)_ , where the element of row $i$ and column $j$ is the PR between the
symbol labeling row $i$ and that of column $j$. We also add the special symbol
$\\#$ which is used as a string delimiter and state the convention that all
symbols of $\Sigma$ yield precedence to, and take precedence over it.

$\begin{array}[]{r | c c c c}&\mathbf{call}&\mathbf{ret}&\mathbf{han}&\mathbf{exc}\\\ \hline\cr\mathbf{call}&\lessdot&\mathbin{\doteq}&\lessdot&\gtrdot\\\ \mathbf{ret}&\gtrdot&\gtrdot&\gtrdot&\gtrdot\\\ \mathbf{han}&\lessdot&\gtrdot&\lessdot&\mathbin{\doteq}\\\ \mathbf{exc}&\gtrdot&\gtrdot&\gtrdot&\gtrdot\\\ \end{array}$ Figure 1. The OPM $M_{\mathbf{call}}$.

Let us now see how the OPM of Figure 1, named $M_{\mathbf{call}}$, drives the
construction of a unique ST associated to a string on the alphabet $\Sigma$
through a typical bottom-up parsing algorithm. We will see that the shape of
the obtained ST depends only on the OPM and not on the particular grammar
exhibiting the OPM. Consider the sample word $w_{\mathit{ex}}=\mathbf{call}\
\allowbreak\mathbf{han}\ \allowbreak\mathbf{call}\ \allowbreak\mathbf{call}\
\allowbreak\mathbf{call}\ \allowbreak\mathbf{exc}\ \allowbreak\mathbf{call}\
\mathbf{ret}\ \mathbf{call}\ \mathbf{ret}\ \mathbf{ret}$. First, add the
delimiter $\\#$ at its boundaries and write all precedence relations between
consecutive characters, according to $M_{\mathbf{call}}$. The result is row
$0$ of Figure 2.

Then, select all innermost patterns of the form $a\lessdot
c_{1}\mathbin{\doteq}\dots\mathbin{\doteq}c_{\ell}\gtrdot b$. In row $0$ of
Figure 2 the only such pattern is the underscored $\mathbf{call}$ enclosed
within the pair ($\mathord{\lessdot},\mathord{\gtrdot}$). This means that the
ST we are going to build, if it exists, must contain an internal node with the
terminal character $\mathbf{call}$ as its only child. We mark this fact by
replacing the pattern $\lessdot\underline{\mathbf{call}}\gtrdot$ with a dummy
non-terminal character, say $N$ —i.e., we _reduce_ $\underline{\mathbf{call}}$
to $N$—. The result is row $1$ of Figure 2.

Next, we apply the same labeling to row $1$ by simply ignoring the presence of
the dummy symbol $N$ and we find a new candidate for reduction, namely the
pattern $\lessdot\underline{\mathbf{call}}\ N\gtrdot$. Notice that there is no
doubt on building the candidate rhs as $\lessdot\underline{\mathbf{call}}\
N\gtrdot$: if we reduced just the $\underline{\mathbf{call}}$ and replaced it
by a new $N$, we would produce two adjacent internal nodes, which is
impossible since the ST must be generated by a grammar in operator normal
form.

By skipping the obvious reduction of row $2$, we come to row $3$. This time
the terminal characters to be reduced, again, underscored, are two, with an
$\mathbin{\doteq}$ and an $N$ in between. This means that they embrace a
subtree of the whole ST whose root is the node represented by the dummy symbol
$N$. By executing the new reduction leading from row $3$ to $4$ we produce a
new $N$ immediately to the left of a $\mathbf{call}$ which is matched by an
equal in precedence $\mathbf{ret}$. Then, the procedure is repeated until the
final row $7$ is obtained, where, by convention we state the
$\mathbin{\doteq}$ relation between the two delimiters.

Given that each reduction applied in Figure 2 corresponds to a derivation step
of a grammar and to the expansion of an internal node of the corresponding ST,
it is immediate to realize that the ST of $w_{\mathit{ex}}$ is the one
depicted in Figure 3, where the terminal symbols have been numbered according
to their occurrence —including the conventional numbering of the delimiters—
for future convenience, and labeling internal nodes has been omitted as
useless.

$\begin{array}[]{l | l}0&\\#\lessdot\mathbf{call}\lessdot\mathbf{han}\lessdot\mathbf{call}\lessdot\mathbf{call}\lessdot\underline{\mathbf{call}}\gtrdot\mathbf{exc}\gtrdot\mathbf{call}\mathbin{\doteq}\mathbf{ret}\gtrdot\mathbf{call}\mathbin{\doteq}\mathbf{ret}\gtrdot\mathbf{ret}\gtrdot\\#\\\ 1&\\#\lessdot\mathbf{call}\lessdot\mathbf{han}\lessdot\mathbf{call}\lessdot\underline{\mathbf{call}}\ N\gtrdot\mathbf{exc}\gtrdot\mathbf{call}\mathbin{\doteq}\mathbf{ret}\gtrdot\mathbf{call}\mathbin{\doteq}\mathbf{ret}\gtrdot\mathbf{ret}\gtrdot\\#\\\ 2&\\#\lessdot\mathbf{call}\lessdot\mathbf{han}\lessdot\underline{\mathbf{call}}\ N\gtrdot\mathbf{exc}\gtrdot\mathbf{call}\mathbin{\doteq}\mathbf{ret}\gtrdot\mathbf{call}\mathbin{\doteq}\mathbf{ret}\gtrdot\mathbf{ret}\gtrdot\\#\\\ 3&\\#\lessdot\mathbf{call}\lessdot\underline{\mathbf{han}}\mathbin{\doteq}N\ \underline{\mathbf{exc}}\gtrdot\mathbf{call}\mathbin{\doteq}\mathbf{ret}\gtrdot\mathbf{call}\mathbin{\doteq}\mathbf{ret}\gtrdot\mathbf{ret}\gtrdot\\#\\\ 4&\\#\lessdot\mathbf{call}\lessdot N\ \underline{\mathbf{call}}\mathbin{\doteq}\underline{\mathbf{ret}}\gtrdot\mathbf{call}\mathbin{\doteq}\mathbf{ret}\gtrdot\mathbf{ret}\gtrdot\\#\\\ 5&\\#\lessdot\mathbf{call}\lessdot N\ \underline{\mathbf{call}}\mathbin{\doteq}\underline{\mathbf{ret}}\gtrdot\mathbf{ret}\gtrdot\\#\\\ 6&\\#\lessdot\underline{\mathbf{call}}\mathbin{\doteq}N\ \underline{\mathbf{ret}}\gtrdot\\#\\\ 7&\\#\mathbin{\doteq}N\\#\\\ \end{array}$ Figure 2. The sequence of bottom-up reductions during the parsing of $w_{\mathit{ex}}$. Figure 3. The ST corresponding to word $w_{\mathit{ex}}$. Dots represent non-terminals.

The tree of Figure 3 emphasizes the main difference between various types of
parenthesis-like languages, such as VPLs, and OPLs: whereas in the former ones
every open parenthesis is consumed by the only corresponding closed one333To
be precise, VPLs allow for unmatched closed parentheses but only at the
beginning of a string and unmatched open ones at the end., in our example a
$\mathbf{call}$ can be matched by the appropriate $\mathbf{ret}$ but can also
be “aborted” by an $\mathbf{exc}$ which in turn aborts all pending
$\mathbf{call}$s until its corresponding $\mathbf{han}$ — _if any_ — is found.

Thus, an OPM defines a _universe_ of strings on the given alphabet that can be
parsed according to it and assigns a unique ST —with unlabeled internal nodes—
to each one of them. Such a universe is the whole $\Sigma^{*}$ iff _the OPM is
complete_ , i.e. it has no empty cells, including those of the implicit row
and column referring to the delimiters. In the early literature about OPLs,
e.g., [Flo63, CMM78] OPGs sharing a given OPM were used to define restricted
languages w.r.t. the universe defined by the OPM and their algebraic
properties have been investigated. Later on the same operation has been
defined by using different formalisms such as pushdown automata, monadic
second order logic, and suitable extensions of regular expressions. In this
paper we refer to the use automata and temporal logic, which are typical of
model checking. As a side remark we mention that, in general, it may happen
that in the same string there are several patterns ready to be reduced; this
could enable the implementation of parallel parsing algorithms (see e.g.,
[BCM+15]) which however is not an issue of interest in this paper.

We now state the basics of OPLs needed for this paper in a formal way. Let
$\Sigma$ be a finite alphabet, and $\varepsilon$ the empty string. We use the
special symbol $\\#\not\in\Sigma$ to mark the beginning and the end of any
string.

An operator precedence matrix (OPM) $M$ over $\Sigma$ is a partial function
$(\Sigma\cup\\{\\#\\})^{2}\to\\{\lessdot,\allowbreak\mathbin{\doteq},\allowbreak\gtrdot\\}$,
that, for each ordered pair $(a,b)$, defines the _precedence relation_
$M(a,b)$ holding between $a$ and $b$. If the function is total we say that $M$
is _complete_. We call the pair $(\Sigma,M)$ an _operator precedence
alphabet_. By convention, the initial $\\#$ can only yield precedence to other
symbols, and other symbols can only take precedence on the ending $\\#$.

If $M(a,b)=\pi$, where $\pi\in\\{\lessdot,\mathbin{\doteq},\gtrdot\\}$, we
write $a\mathrel{\pi}b$. For $u,v\in(\Sigma\cup\\{\\#\\})^{+}$ we write
$u\mathrel{\pi}v$ if $u=xa$ and $v=by$ with $a\mathrel{\pi}b$.

The next concept of _chain_ makes the connection between OP relations and ST
structure explicit, through brackets.

A _simple chain_ ${}^{c_{0}}[c_{1}c_{2}\dots c_{\ell}]{}^{c_{\ell+1}}$, with
$\ell\geq 1$, is a string $c_{0}c_{1}c_{2}\dots c_{\ell}c_{\ell+1}$, such
that: $c_{0},\allowbreak c_{\ell+1}\in\Sigma\cup\\{\\#\\}$, $c_{i}\in\Sigma$
for every $i=1,2,\dots\ell$, and $c_{0}\lessdot
c_{1}\mathbin{\doteq}c_{2}\dots c_{\ell-1}\mathbin{\doteq}c_{\ell}\gtrdot
c_{\ell+1}$.

A _composed chain_ is a string $c_{0}s_{0}c_{1}s_{1}c_{2}\dots
c_{\ell}s_{\ell}c_{\ell+1}$, where ${}^{c_{0}}[c_{1}c_{2}\dots
c_{\ell}]{}^{c_{\ell+1}}$ is a simple chain, and $s_{i}\in\Sigma^{*}$ is
either the empty string or is such that ${}^{c_{i}}[s_{i}]{}^{c_{i+1}}$ is a
chain (simple or composed), for every $i=0,1,\dots,\ell$ ($\ell\geq 1$). Such
a composed chain will be written as ${}^{c_{0}}[s_{0}c_{1}s_{1}c_{2}\dots
c_{\ell}s_{\ell}]{}^{c_{\ell+1}}$.

In a chain, simple or composed, $c_{0}$ (resp. $c_{\ell+1}$) is called its
_left_ (resp.  _right_) _context_ ; all terminals between them are called its
_body_.

A finite word $w$ over $\Sigma$ is _compatible_ with an OPM $M$ iff for each
pair of letters $c,d$, consecutive in $w$, $M(c,d)$ is defined and, for each
substring $x$ of $\\#w\\#$ which is a chain of the form ${}^{a}[y]^{b}$,
$M(a,b)$ is defined. For a given operator precedence alphabet $(\Sigma,M)$ the
set of all words compatible with $M$ is called the _universe_ of the operator
precedence alphabet.

The chain below is the chain defined by the OPM $M_{\mathbf{call}}$ of Figure
1 for the word $w_{\mathit{ex}}$. It shows the natural isomorphism between STs
with unlabeled internal nodes (see Figure 3) and chains.

$\\#[\mathbf{call}[[[\mathbf{han}[\mathbf{call}[\mathbf{call}[\mathbf{call}]]]\mathbf{exc}]\mathbf{call}\;\mathbf{ret}]\mathbf{call}\;\mathbf{ret}]\mathbf{ret}]\\#$

Note that, in composed chains, consecutive inner chains are always separated
by an input symbol: this is due to the fact that OPL strings are generated by
grammars in operator normal form.

Next we introduce operator precedence automata as pushdown machines suitable
to carve specific OPLs within the universe of an operator precedence alphabet.

An _operator precedence automaton (OPA)_ is a tuple
$\mathcal{A}=(\Sigma,\allowbreak M,\allowbreak Q,\allowbreak I,\allowbreak
F,\allowbreak\delta)$ where: $(\Sigma,M)$ is an operator precedence alphabet,
$Q$ is a finite set of states (disjoint from $\Sigma$), $I\subseteq Q$ is the
set of initial states, $F\subseteq Q$ is the set of final states,
$\delta\subseteq Q\times(\Sigma\cup Q)\times Q$ is the transition relation,
which is the union of the three disjoint relations
$\delta_{\mathit{shift}}\subseteq Q\times\Sigma\times Q$,
$\delta_{\mathit{push}}\subseteq Q\times\Sigma\times Q$, and
$\delta_{\mathit{pop}}\subseteq Q\times Q\times Q$. An OPA is deterministic
iff $I$ is a singleton, and all three components of $\delta$ are —possibly
partial— functions.

To define the semantics of OPA, we need some new notations. Letters
$p,q,p_{i},\allowbreak q_{i},\dots$ denote states in $Q$. We use
$q_{0}\stackrel{{\scriptstyle a}}{{\longrightarrow}}{q_{1}}$ for
$(q_{0},a,q_{1})\in\delta_{\mathit{push}}$, $q_{0}\stackrel{{\scriptstyle
a}}{{\dashrightarrow}}{q_{1}}$ for
$(q_{0},a,q_{1})\in\delta_{\mathit{shift}}$, $q_{0}\stackrel{{\scriptstyle
q_{2}}}{{\Longrightarrow}}{q_{1}}$ for
$(q_{0},q_{2},q_{1})\in\delta_{\mathit{pop}}$, and
${q_{0}}\stackrel{{\scriptstyle w}}{{\leadsto}}{q_{1}}$, if the automaton can
read $w\in\Sigma^{*}$ going from $q_{0}$ to $q_{1}$. Let $\Gamma$ be
$\Sigma\times Q$ and $\Gamma^{\prime}=\Gamma\cup\\{\bot\\}$ be the stack
alphabet; we denote symbols in $\Gamma$ as $[a,\ q]$. We set
$\mathop{smb}([a,\ q])=a$, $\mathop{smb}(\bot)=\\#$, and $\mathop{st}([a,\
q])=q$. For a stack content $\gamma=\gamma_{n}\dots\gamma_{1}\bot$, with
$\gamma_{i}\in\Gamma$ , $n\geq 0$, we set
$\mathop{smb}(\gamma)=\mathop{smb}(\gamma_{n})$ if $n\geq 1$, and
$\mathop{smb}(\gamma)=\\#$ if $n=0$.

A _configuration_ of an OPA is a triple $c=\langle w,\ q,\ \gamma\rangle$,
where $w\in\Sigma^{*}\\#$, $q\in Q$, and $\gamma\in\Gamma^{*}\bot$. A
_computation_ or _run_ is a finite sequence
$c_{0}\stackrel{{\scriptstyle{}}}{{\vdash}}c_{1}\stackrel{{\scriptstyle{}}}{{\vdash}}\dots\stackrel{{\scriptstyle{}}}{{\vdash}}c_{n}$
of _moves_ or _transitions_
$c_{i}\stackrel{{\scriptstyle{}}}{{\vdash}}c_{i+1}$. There are three kinds of
moves, depending on the PR between the symbol on top of the stack and the next
input symbol:

push move:

if $\mathop{smb}(\gamma)\lessdot a$ then $\langle ax,\ p,\
\gamma\rangle\stackrel{{\scriptstyle{}}}{{\vdash}}\langle x,\ q,\ [a,\
p]\gamma\rangle$, with $(p,a,q)\in\delta_{\mathit{push}}$;

shift move:

if $a\mathbin{\doteq}b$ then $\langle bx,\ q,\ [a,\
p]\gamma\rangle\stackrel{{\scriptstyle{}}}{{\vdash}}\langle x,\ r,\ [b,\
p]\gamma\rangle$, with $(q,b,r)\in\delta_{\mathit{shift}}$;

pop move:

if $a\gtrdot b$ then $\langle bx,\ q,\ [a,\
p]\gamma\rangle\stackrel{{\scriptstyle{}}}{{\vdash}}\langle bx,\ r,\
\gamma\rangle$, with $(q,p,r)\in\delta_{\mathit{pop}}$.

Shift and pop moves are not performed when the stack contains only $\bot$.
Push moves put a new element on top of the stack consisting of the input
symbol together with the current state of the OPA. Shift moves update the top
element of the stack by changing its input symbol only. Pop moves remove the
element on top of the stack, and update the state of the OPA according to
$\delta_{\mathit{pop}}$ on the basis of the current state and the state in the
removed stack symbol. They do not consume the input symbol, which is used only
as a look-ahead to establish the $\gtrdot$ relation. The OPA accepts the
language $L(\mathcal{A})=\left\\{x\in\Sigma^{*}\mid\langle x\\#,\ q_{I},\
\bot\rangle\vdash^{*}\langle\\#,\ q_{F},\ \bot\rangle,\allowbreak q_{I}\in
I,\allowbreak q_{F}\in F\right\\}.$

Let $\mathcal{A}$ be an OPA. We call a _support_ for the simple chain
${}^{c_{0}}[c_{1}c_{2}\dots c_{\ell}]{}^{c_{\ell+1}}$ any path in
$\mathcal{A}$ of the form $q_{0}\stackrel{{\scriptstyle
c_{1}}}{{\longrightarrow}}{q_{1}}\stackrel{{\scriptstyle}}{{\dashrightarrow}}{}\dots\stackrel{{\scriptstyle}}{{\dashrightarrow}}q_{\ell-1}\stackrel{{\scriptstyle
c_{\ell}}}{{\dashrightarrow}}{q_{\ell}}\stackrel{{\scriptstyle
q_{0}}}{{\Longrightarrow}}{q_{\ell+1}}$. The label of the last (and only) pop
is exactly $q_{0}$, i.e. the first state of the path; this pop is executed
because of relation $c_{\ell}\gtrdot c_{\ell+1}$.

We call a _support for the composed chain_
${}^{c_{0}}[s_{0}c_{1}s_{1}c_{2}\dots c_{\ell}s_{\ell}]{}^{c_{\ell+1}}$ any
path in $\mathcal{A}$ of the form $q_{0}\stackrel{{\scriptstyle
s_{0}}}{{\leadsto}}{q^{\prime}_{0}}\stackrel{{\scriptstyle
c_{1}}}{{\longrightarrow}}{q_{1}}\stackrel{{\scriptstyle
s_{1}}}{{\leadsto}}{q^{\prime}_{1}}\stackrel{{\scriptstyle
c_{2}}}{{\dashrightarrow}}{}\dots\stackrel{{\scriptstyle
c_{\ell}}}{{\dashrightarrow}}{q_{\ell}}\stackrel{{\scriptstyle
s_{\ell}}}{{\leadsto}}{q^{\prime}_{\ell}}\stackrel{{\scriptstyle
q^{\prime}_{0}}}{{\Longrightarrow}}{q_{\ell+1}}$ where, for every
$i=0,1,\dots,\ell$: if $s_{i}\neq\varepsilon$, then
$q_{i}\stackrel{{\scriptstyle s_{i}}}{{\leadsto}}{q^{\prime}_{i}}$ is a
support for the chain ${}^{c_{i}}[s_{i}]{}^{c_{i+1}}$, else
$q^{\prime}_{i}=q_{i}$.

Chains fully determine the parsing structure of any OPA over $(\Sigma,M)$. If
the OPA performs the computation $\langle
sb,q_{i},[a,q_{j}]\gamma\rangle\vdash^{*}\langle b,q_{k},\gamma\rangle$, then
${}^{a}[s]{}^{b}$ is necessarily a chain over $(\Sigma,\allowbreak M)$, and
there exists a support like the one above with $s=s_{0}c_{1}\dots
c_{\ell}s_{\ell}$ and $q_{\ell+1}=q_{k}$. This corresponds to the parsing of
the string $s_{0}c_{1}\dots c_{\ell}s_{\ell}$ within the context $a,b$, which
contains all information needed to build the subtree whose frontier is that
string.

Consider the OPA
$\mathcal{A}(\Sigma,M)=(\Sigma,M,\\{q\\},\\{q\\},\\{q\\},\delta_{max})$ where
$\delta_{max}(q,q)=q$, and $\delta_{max}(q,c)=q$, $\forall c\in\Sigma$. We
call it the _OP Max-Automaton_ over $(\Sigma,M)$. For a max-automaton, each
chain has a support; thus, a max-automaton accepts exactly the universe of the
operator precedence alphabet. If $M$ is complete, the language accepted by
$\mathcal{A}(\Sigma,M)$ is $\Sigma^{*}$. With reference to the OPM
$M_{\mathbf{call}}$ of Figure 1, the string $\mathbf{ret}\ \mathbf{call}\
\mathbf{han}$ is accepted by the max-automaton with structure defined by the
chain $\\#[[\mathbf{ret}]\mathbf{call}[\mathbf{han}]]\\#.$

In conclusion, given an OP alphabet, the OPM $M$ assigns a unique structure to
any compatible string in $\Sigma^{*}$; unlike VPLs, such a structure is not
visible in the string, and must be built by means of a non-trivial parsing
algorithm. An OPA defined on the OP alphabet selects an appropriate subset
within the universe of the OP alphabet. OPAs form a Boolean algebra whose
universal element is the max-automaton. The language classes recognized by
deterministic and non-deterministic OPAs coincide. For a more complete
description of the OPL family and of its relations with other CFLs we refer
the reader to [MP18].

|

        pA() {
    A0:   try {
    A1:     pB();
    A2:   } catch {
    A3:     pErr();
    A4:     pErr();
          }
    Ar: }

|

        pB() {
    B0:   pC();
    Br: }

|

        pC() {
    C0:   if (*) {
    C1:     throw;
    C2:   } else {
    C3:     pC();
          }
    Cr: }

|
---|---|---|---|---
M0A0A1B0C0A2A3ErArAr’MrA4$\mathbf{call}$$\mathrm{p}_{A}$$\mathbf{han}$try$\mathbf{call}$$\mathrm{p}_{B}$$\mathbf{call}$$\mathrm{p}_{C}$$\mathbf{call}\,\mathrm{p}_{C}$A1,
B0,
C0$\mathbf{exc}$A0$\mathbf{call}$$\mathrm{p}_{\mathit{Err}}$$\mathbf{ret}\,\mathrm{p}_{\mathit{Err}}$A3$\mathbf{call}$$\mathrm{p}_{\mathit{Err}}$A4$\mathbf{ret}$$\mathrm{p}_{A}$M0
Figure 4. Example procedural program (top) and the derived OPA (bottom). Push,
shift, pop moves are shown by, resp., solid, dashed and double arrows.

For readers not familiar with OPLs, we show how OPAs can naturally model
programming languages such as Java and C++. Given a set $AP$ of atomic
propositions describing events and states of the program, we use
$({\mathcal{P}(AP)},M_{AP})$ as the OP alphabet. For convenience, we consider
a partitioning of $AP$ into a set of normal propositional labels (in round
font), and _structural labels_ (in bold). Structural labels define the OP
structure of the word: $M_{AP}$ is only defined for subsets of $AP$ containing
exactly one structural label, so that given two structural labels
$\mathbf{l}_{1},\mathbf{l}_{2}$, for any
$a,a^{\prime},b,b^{\prime}\in{\mathcal{P}(AP)}$ s.t. $\mathbf{l}_{1}\in
a,a^{\prime}$ and $\mathbf{l}_{2}\in b,b^{\prime}$ we have
$M_{AP}(a,b)=M_{AP}(a^{\prime},b^{\prime})$. In this way, it is possible to
define an OPM on the entire ${\mathcal{P}(AP)}$ by only giving the relations
between structural labels, as we did for $M_{\mathbf{call}}$. Figure 4 shows
how to model a procedural program with an OPA. The OPA simulates the program’s
behavior with respect to the stack, by expressing its execution traces with
four event kinds: $\mathbf{call}$ (resp. $\mathbf{ret}$) marks a procedure
call (resp. return), $\mathbf{han}$ the installation of an exception handler
by a try statement, and $\mathbf{exc}$ an exception being raised. OPM
$M_{\mathbf{call}}$ defines the context-free structure of the word, which is
strictly linked with the programming language semantics: the $\lessdot$ PR
causes nesting (e.g., $\mathbf{call}$s can be nested into other
$\mathbf{call}$s), and the $\mathbin{\doteq}$ PR implies a one-to-one
relation, e.g. between a $\mathbf{call}$ and the $\mathbf{ret}$ of the same
function, and a $\mathbf{han}$ and the $\mathbf{exc}$ it catches. Each OPA
state represents a line in the source code. First, procedure $\mathrm{p}_{A}$
is called by the program loader (M0), and
$[\\{\mathbf{call},\mathrm{p}_{A}\\},\text{M0}]$ is pushed onto the stack, to
track the program state before the $\mathbf{call}$. Then, the try statement at
line A0 of $\mathrm{p}_{A}$ installs a handler. All subsequent calls to
$\mathrm{p}_{B}$ and $\mathrm{p}_{C}$ push new stack symbols on top of the one
pushed with $\mathbf{han}$. $\mathrm{p}_{C}$ may only call itself recursively,
or throw an exception, but never return normally. This is reflected by
$\mathbf{exc}$ being the only transition leading from state C0 to the
accepting state Mr, and $\mathrm{p}_{B}$ and $\mathrm{p}_{C}$ having no way to
a normal $\mathbf{ret}$. The OPA has a look-ahead of one input symbol, so when
it encounters $\mathbf{exc}$, it must pop all symbols in the stack,
corresponding to active function frames, until it finds the one with
$\mathbf{han}$ in it, which cannot be popped because
$\mathbf{han}\mathbin{\doteq}\mathbf{exc}$. Notice that such behavior cannot
be modeled by Visibly Pushdown Automata or Nested Word Automata, because they
need to read an input symbol for each pop move. Thus, $\mathbf{han}$ protects
the parent function from the exception. Since the state contained in
$\mathbf{han}$’s stack symbol is A0, the execution resumes in the catch clause
of $\mathrm{p}_{A}$. $\mathrm{p}_{A}$ then calls twice the library error-
handling function $\mathrm{p}_{\mathit{Err}}$, which ends regularly both
times, and returns. The string of Figure 1 is accepted by this OPA.

In this example, we only model the stack behavior for simplicity, but other
statements, such as assignments, and other behaviors, such as continuations,
could be modeled by a different choice of the OPM, and other aspects of the
program’s state by appropriate abstractions [JPR18].

###  2.1. Operator Precedence $\omega$-Languages

All definitions regarding OPLs are extended to infinite words in the usual
way, but with a few distinctions [LMPP15]. Given an alphabet $(\Sigma,M)$, an
$\omega$-word $w\in\Sigma^{\omega}$ is compatible with $M$ if every prefix of
$w$ is compatible with $M$. OP $\omega$-words are not terminated by the
delimiter $\\#$. An $\omega$-word may contain never-ending chains of the form
$c_{0}\lessdot c_{1}\mathbin{\doteq}c_{2}\mathbin{\doteq}\cdots$, where the
$\lessdot$ relation between $c_{0}$ and $c_{1}$ is never closed by a
corresponding $\gtrdot$. Such chains are called _open chains_ and may be
simple or composed. A composed open chain may contain both open and closed
subchains. Of course, a closed chain cannot contain an open one. A terminal
symbol $a\in\Sigma$ is _pending_ if it is part of the body of an open chain
and of no closed chains.

OPA classes accepting the whole class of $\omega$OPLs can be defined by
augmenting Definition 2 with Büchi or Muller acceptance conditions. In this
paper, we only consider the former one. The semantics of configurations, moves
and infinite runs are defined as for finite OPAs. For the acceptance
condition, let $\rho$ be a run on an $\omega$-word $w$. Define
$\operatorname{Inf}(\rho)=\\{q\in Q\mid\text{there exist infinitely many
positions $i$ s.t.\ }\langle\beta_{i},q,x_{i}\rangle\in\rho\\}$ as the set of
states that occur infinitely often in $\rho$. $\rho$ is successful iff there
exists a state $q_{f}\in F$ such that $q_{f}\in\operatorname{Inf}(\rho)$. An
$\omega$OPBA $\mathcal{A}$ accepts $w\in\Sigma^{\omega}$ iff there is a
successful run of $\mathcal{A}$ on $w$. The $\omega$-language recognized by
$\mathcal{A}$ is $L(\mathcal{A})=\\{w\in\Sigma^{\omega}\mid\mathcal{A}\text{
accepts }w\\}$. Unlike OPAs, $\omega$OPBAs do not require the stack to be
empty for word acceptance: when reading an open chain, the stack symbol pushed
when the first character of the body of its underlying simple chain is read
remains into the stack forever; it is at most updated by shift moves.

The most important closure properties of OPLs are preserved by $\omega$OPLs,
which form a Boolean algebra and are closed under concatenation of an OPL with
an $\omega$OPL [LMPP15]. The equivalence between deterministic and
nondeterministic automata is lost in the infinite case, which is unsurprising,
since it also happens for regular $\omega$-languages and $\omega$VPLs.

A more complete treatment of OPLs properties and parsing algorithms can be
found in [MP18, GJ08]; $\omega$OPLs are described in some depth in [LMPP15].

###  2.2. OPLs vs other structured language families

The nice closure properties of OPLs come from the fact that a word’s syntactic
structure is determined locally, once an OPM is given. Other language classes
enjoy similar properties. The simplest (and earliest) ones are _Parenthesis
Languages_ [McN67]. In Parenthesis Languages, two terminals disjoint from the
input alphabet are used as open and closed parentheses, and they surround all
grammar rule rhs. Thus, the syntactic structure is directly encoded in words
(just like we did in Figure 1 with chains).

Visibly Pushdown Languages (VPLs) [AM04], first introduced as Input-Driven
Languages [Meh80], extend parenthesis languages; they also lead to
applications in model checking. In VPLs, the input alphabet $\Sigma$ is
partitioned into three disjoint sets $\Sigma_{c}$, $\Sigma_{i}$, and
$\Sigma_{r}$, called respectively the _call_ , _internal_ , and _return_
alphabets. _Visibly Pushdown Automata_ (VPA), the automata class recognizing
VPLs, always perform a push move when reading a call symbol, a pop move when
reading a return symbol, and, when reading an internal symbol, they perform a
move that only updates the current state, leaving the stack untouched. Thus, a
string’s syntactic structure is fully determined by the alphabet partition,
and is clearly _visible_ : a symbol in $\Sigma_{c}$ is an open parenthesis,
and one in $\Sigma_{r}$ is a closed parenthesis. The matching between such
symbols is unambiguous. Once the alphabet partition is fixed, VPLs form a
Boolean algebra, which enabled their success in model checking. VPAs are
_real-time_ , as they read exactly one input symbol with each move. This
limitation distinguishes them from OPAs, whose pop moves are so-called
$\varepsilon$-moves. OPLs strictly contain VPLs [CM12].

_Nested Words_ [AM09], an algebraic characterization of VPLs, were introduced
to foster their logic and data-theoretic applications. They consist of a
linear sequence of positions, plus a _matching relation_ encoding the pairing
of call and return symbols. As a result, the matching relation is a strictly
one-to-one nesting relation that never crosses itself (each “open parenthesis”
is matched to a closed one, with a minor exception). The class of Regular
Languages of Nested Words is recognized by Nested Words Automata, and is
equivalent to VPLs.

The original motivation for VPLs was model checking procedural programs: the
matching between call and return symbols easily models the behavior of a
program’s stack during function calls and returns, while internal symbols
model other statements. However, many programming languages manage the stack
in more complex ways. E.g., when an exception is raised, the stack may be
unwound, as multiple procedures are terminated by the exception. In Example 2,
this is easily modeled by an OPM where the $\mathbf{call}$ symbol takes
precedence from $\mathbf{exc}$. In contrast, a VPA would need to read a
different symbol for each pop move, so a single $\mathbf{exc}$ would not
suffice.

An early attempt at overcoming such limitations was made with Colored Nested
Words [AF16], in which multiple calls can be matched with a return of a
different color, allowing many-to-one relations. Colored Nested Words are
subsumed by OPLs and, as we show in Section 3, the nesting relation of OPLs
can be also one-to-many, besides many-to-one.

##  3\. Precedence-Oriented Temporal Logic

${\\#}$${\lessdot}$${\mathbf{call}}$${\lessdot}$${\mathbf{han}}$${\lessdot}$${\mathbf{call}}$${\lessdot}$${\mathbf{call}}$${\lessdot}$${\mathbf{call}}$${\gtrdot}$${\mathbf{exc}}$${\gtrdot}$${\mathbf{call}}$${\mathbin{\doteq}}$${\mathbf{ret}}$${\gtrdot}$${\mathbf{call}}$${\mathbin{\doteq}}$${\mathbf{ret}}$${\gtrdot}$${\mathbf{ret}}$${\gtrdot}$${\\#}$${\mathrm{p}_{A}}$${\mathrm{p}_{B}}$${\mathrm{p}_{C}}$${\mathrm{p}_{C}}$${\mathrm{p}_{\mathit{Err}}}$${\mathrm{p}_{\mathit{Err}}}$${\mathrm{p}_{\mathit{Err}}}$${\mathrm{p}_{\mathit{Err}}}$${\mathrm{p}_{A}}$${0}$${1}$${2}$${3}$${4}$${5}$${6}$${7}$${8}$${9}$${10}$${11}$${12}$
Figure 5. The example string of Figure 1 as an OP word. Chains are highlighted
by arrows joining their contexts; structural labels are in bold, and other
atomic propositions are shown below them. $\mathrm{p}_{l}$ means a
$\mathbf{call}$ or a $\mathbf{ret}$ is related to procedure $\mathrm{p}_{l}$.
First, procedure $\mathrm{p}_{A}$ is called (pos. 1), and it installs an
exception handler in pos. 2. Then, three nested procedures are called, and the
innermost one ($\mathrm{p}_{C}$) throws an exception, which is caught by the
handler. Two more functions are called and, finally, $\mathrm{p}_{A}$ returns.

POTL is a linear-time temporal logic, which extends the classical LTL. We
recall that the semantics of LTL [Pnu77] is defined on a Dedekind-complete set
of word positions $U$ equipped with a total ordering and monadic relations,
called _atomic propositions_ (AP). In this paper, we consider a discrete
timeline, hence $U=\\{0,1,\dots,n\\}$, with $n\in\mathbb{N}$, or
$U=\mathbb{N}$. Each LTL formula $\varphi$ is evaluated in a word position: we
write $(w,i)\models\varphi$ to state that $\varphi$ holds in position $i$ of
word $w$. Besides operators from propositional logic, LTL features modalities
that enable movement between positions; e.g., the _Next_ modality states that
a formula holds in the subsequent position of the current one:
$(w,i)\models\ocircle\varphi$ iff $(w,i+1)\models\varphi$; the _Until_
modality states that there exists a _linear path_ , made of consecutive
positions and starting from the current one, such that a formula $\psi$ holds
in the last position of such path, and another formula $\varphi$ holds in all
previous positions. Formally, $(w,i)\models\varphi\mathbin{\mathcal{U}}\psi$
iff there exists $j\geq i$ s.t. $(w,j)\models\psi$, and for all $j^{\prime}$,
with $i\leq j^{\prime}<j$, we have $(w,j^{\prime})\models\varphi$.

The linear order, however, is not sufficient to express properties of more
complex structures than the linear ones, typically the tree-shaped ones, which
are the natural domain of context-free languages. The history of logic
formalisms suitable to deal with CFLs somewhat parallels the path that led
from regular languages to tree-languages [Tha67] or their equivalent
counterpart in terms of strings, i.e. parenthesis languages [McN67].

A first logic mechanism aimed at “walking through the structure of a context-
free sentence” was proposed in [LST94] and consists in a _matching condition_
that relates the two extreme terminals of the rhs of a context-free grammar in
so-called _double Greibach normal form_ , i.e. a grammar whose production rhs
exhibit a terminal character at both ends: in a sense such terminal characters
play the role of explicit parentheses. [LST94] provides a logic language for
general CFLs based on such a relation which however fails to extend the
decidability properties of logics for regular languages due to lack of closure
properties of CFLs. The matching condition was then resumed in [AM09] to
define their MSO logic for VPLs and subsequently the temporal logics CaRet
[AEM04] and NWTL [AAB+08].

OPLs are structured but not “visibly structured” as they lack explicit
parentheses (see Section 2). Nevertheless, a more sophisticated notion of
matching relation has been introduced in [LMPP15] for OPLs by exploiting the
fact that OPLs remain input-driven thanks to the OPM. We name the new matching
condition _chain relation_ and define it here below. We fix a finite set of
atomic propositions $AP$, and an OPM $M_{AP}$ on ${\mathcal{P}(AP)}$.

A _word structure_ —also called _OP word_ for short— is the tuple $\langle
U,<,M_{AP},P\rangle$, where $U$, $<$, and $M_{AP}$ are as above, and $P\colon
AP\to{\mathcal{P}(U)}$ is a function associating each atomic proposition with
the set of positions where it holds, with $0,(n+1)\in P(\\#)$. For the time
being, we consider just finite string languages; the necessary extensions
needed to deal with $\omega$-languages will be introduced in Section 3.2.

[Chain relation] The _chain relation_ $\chi(i,j)$ holds between two positions
$i,j\in U$ iff $i<j-1$, and $i$ and $j$ are resp. the left and right contexts
of the same chain (cf. Definition 2), according to $M_{AP}$ and the labeling
induced by $P$.

In the following, given two positions $i,j$ and a PR $\pi$, we write
$i\mathrel{\pi}j$ to say $a\mathrel{\pi}b$, where $a=\\{\mathrm{p}\mid i\in
P(\mathrm{p})\\}$, and $b=\\{\mathrm{p}\mid j\in P(\mathrm{p})\\}$. For
notational convenience, we partition $AP$ into structural labels, written in
bold face, which define a word’s structure, and normal labels, in round face,
defining predicates holding in a position. Thus, an OPM $M$ can be defined on
structural labels only, and $M_{AP}$ is obtained by inverse homomorphism of
$M$ on subsets of $AP$ containing exactly one of them.

The chain relation augments the linear structure of a word with the tree-like
structure of OPLs. Figure 5 shows the word of Figure 3 as an OP word and
emphasizes the distinguishing feature of the relation, i.e. that, for composed
chains, it may not be one-to-one, but also one-to-many or many-to-one. Notice
the correspondence between internal nodes in the ST and pairs of positions in
the $\chi$ relation.

In the ST, we say that the right context $j$ of a chain is at the _same level_
as the left one $i$ when $i\mathbin{\doteq}j$ (e.g., in Figure 3, pos. 1 and
11), at a _lower level_ when $i\lessdot j$ (e.g., pos. 1 with 7, and 9), at a
_higher level_ if $i\gtrdot j$ (e.g., pos. 3 and 4 with 6).

Furthermore, given $i,j\in U$, relation $\chi$ has the following properties:

  1. (1)

It never crosses itself: if $\chi(i,j)$ and $\chi(h,k)$, for any $h,k\in U$,
then we have $i<h<j\implies k\leq j$ and $i<k<j\implies i\leq h$.

  2. (2)

If $\chi(i,j)$, then $i\lessdot i+1$ and $j-1\gtrdot j$.

  3. (3)

Consider all positions (if any) $i_{1}<i_{2}<\dots<i_{n}$ s.t. $\chi(i_{p},j)$
for all $1\leq p\leq n$. We have $i_{1}\lessdot j$ or $i_{1}\mathbin{\doteq}j$
and, if $n>1$, $i_{q}\gtrdot j$ for all $2\leq q\leq n$.

  4. (4)

Consider all positions (if any) $j_{1}<j_{2}<\dots<j_{n}$ s.t. $\chi(i,j_{p})$
for all $1\leq p\leq n$. We have $i\gtrdot j_{n}$ or $i\mathbin{\doteq}j_{n}$
and, if $n>1$, $i\lessdot j_{q}$ for all $1\leq q\leq n-1$.

Property 4 says that when the chain relation is one-to-many, the contexts of
the outermost chain are in the $\mathbin{\doteq}$ or $\gtrdot$ relation, while
the inner ones are in the $\lessdot$ relation. Property 3 says that contexts
of outermost many-to-one chains are in the $\mathbin{\doteq}$ or $\lessdot$
relation, and the inner ones are in the $\gtrdot$ relation. Such properties
are proved in Appendix A for readers unfamiliar with OPLs.

The $\chi$ relation is the core of the MSO logic characterization for OPLs
given in [LMPP15] where it is also shown that the greater generality of OPLs
and corresponding MSO logic, though requiring more technical proofs, produces
results in terms of closure properties, decidability and complexity of the
constructions that are the same as the corresponding ones for VPLs. Similarly,
in this paper we are going to show that the temporal logic POTL replicates the
FO-completeness result of NWTL despite the greater complexity of the $\chi$
relation.444In [CMP21] we produce model checking algorithms with the same
order of complexity as those for NWTL.

While LTL’s linear paths only follow the ordering relation $<$, paths in POTL
may follow the $\chi$ relation too. As a result, a POTL path through a string
can simulate paths through the corresponding ST.

We envisage two basic types of path. The first one is that of _summary paths_.
By following the chain relation, summary paths may skip chain bodies, which
correspond to the fringe of a subtree in the ST. We distinguish between
_downward_ and _upward_ summary paths (resp. DSP and USP). Both kinds can
follow both the $<$ and the $\chi$ relations; DSPs can enter a chain body but
cannot exit it so that they can move only downward in a ST or remain at the
same level; conversely, USPs cannot enter one but can move upward by exiting
the current one. In other words, if a position $k$ is part of a DSP, and there
are two positions $i$ and $j$, with $i<k<j$ and $\chi(i,j)$ holds, the next
position in the DSP cannot be $\geq j$. E.g., two of the DSPs starting from
pos. 1 in Figure 5 are 1-2-3, which enters chain $\chi(2,6)$, and 1-2-6, which
skips its body. USPs are symmetric, and some examples thereof are paths 3-6-7
and 4-6-7.

Since the $\chi$ relation can be many-to-one or one-to-many, it makes sense to
write formulas that consider only left contexts of chains that share their
right context, or vice versa. Thus, the paths of our second type, named
_hierarchical paths_ , are made of such positions, but excluding outermost
chains. E.g., in Figure 5, positions 2, 3 and 4 are all in the $\chi$ relation
with 6, so 3-4 is a hierarchical path ($\chi(2,6)$ is the outermost chain).
Symmetrically, 7-9 is another hierarchical path. The reason for excluding the
outermost chain is that, with most OPMs, such positions have a different
semantic role than internal ones. E.g., positions 3 and 4 are both calls
terminated by the same exception, while 2 is the handler. Positions 7 and 9
are both calls issued by the same function (the one called in position 1),
while 11 is its return. This is a consequence of properties 3 and 4 above.

In the next subsection, we describe in a complete and formal way POTL for
finite string OPLs while in the subsequent subsection we briefly describe the
necessary changes to deal with $\omega$-languages.

###  3.1. POTL Syntax and Semantics

Given a finite set of atomic propositions $AP$, let $\mathrm{a}\in AP$, and
$t\in\\{d,u\\}$. The syntax of POTL is the following:

$\displaystyle\varphi::=$
$\displaystyle\;\mathrm{a}\mid\neg\varphi\mid\varphi\lor\varphi\mid\ocircle^{t}\varphi\mid\circleddash^{t}\varphi\mid\chi_{F}^{t}\varphi\mid\chi_{P}^{t}\varphi\mid\varphi\mathbin{\mathcal{U}^{t}_{\chi}}\varphi\mid\varphi\mathbin{\mathcal{S}^{t}_{\chi}}\varphi$
$\displaystyle\mid\ocircle_{H}^{t}\varphi\mid\circleddash_{H}^{t}\varphi\mid\varphi\mathbin{\mathcal{U}^{t}_{H}}\varphi\mid\varphi\mathbin{\mathcal{S}^{t}_{H}}\varphi$

The truth of POTL formulas is defined w.r.t. a single word position. Let $w$
be an OP word, and $\mathrm{a}\in AP$. Then, for any position $i\in U$ of $w$,
we have $(w,i)\models\mathrm{a}$ iff $i\in P(\mathrm{a})$. Operators such as
$\land$ and $\neg$ have the usual semantics from propositional logic. Next,
while giving the formal semantics of POTL operators, we illustrate it by
showing how it can be used to express properties on program execution traces,
such as the one of Figure 5.

##### Next/back operators

The _downward_ next and back operators $\ocircle^{d}$ and $\circleddash^{d}$
are like their LTL counterparts, except they are true only if the next (resp.
current) position is at a lower or equal ST level than the current (resp.
preceding) one. The _upward_ next and back, $\ocircle^{u}$ and
$\circleddash^{u}$, are symmetric. Formally, $(w,i)\models\ocircle^{d}\varphi$
iff $(w,i+1)\models\varphi$ and $i\lessdot(i+1)$ or $i\mathbin{\doteq}(i+1)$,
and $(w,i)\models\circleddash^{d}\varphi$ iff $(w,i-1)\models\varphi$, and
$(i-1)\lessdot i$ or $(i-1)\mathbin{\doteq}i$. Substitute $\lessdot$ with
$\gtrdot$ to obtain the semantics for $\ocircle^{u}$ and $\circleddash^{u}$.

E.g., we can write $\ocircle^{d}\mathbf{call}$ to say that the next position
is an inner call (it holds in pos. 2, 3, 4 of Figure 5),
$\circleddash^{d}\mathbf{call}$ to say that the previous position is a
$\mathbf{call}$, and the current is the first of the body of a function (pos.
2, 4, 5), or the $\mathbf{ret}$ of an empty one (pos. 8, 10), and
$\circleddash^{u}\mathbf{call}$ to say that the current position terminates an
empty function frame (holds in 6, 8, 10). In pos. 2
$\ocircle^{d}\mathrm{p}_{B}$ holds, but $\ocircle^{u}\mathrm{p}_{B}$ does not.

##### Chain Next/Back

The _chain_ next and back operators $\chi_{F}^{t}$ and $\chi_{P}^{t}$ evaluate
their argument resp. on future and past positions in the chain relation with
the current one. The _downward_ (resp.  _upward_) variant only considers
chains whose right context goes down (resp. up) or remains at the same level
in the ST. Formally, $(w,i)\models\chi_{F}^{d}\varphi$ iff there exists a
position $j>i$ such that $\chi(i,j)$, $i\lessdot j$ or $i\mathbin{\doteq}j$,
and $(w,j)\models\varphi$. $(w,i)\models\chi_{P}^{d}\varphi$ iff there exists
a position $j<i$ such that $\chi(j,i)$, $j\lessdot i$ or $j\mathbin{\doteq}i$,
and $(w,j)\models\varphi$. Replace $\lessdot$ with $\gtrdot$ for the upward
versions.

E.g., in pos. 1 of Figure 5, $\chi_{F}^{d}\mathrm{p}_{\mathit{Err}}$ holds
because $\chi(1,7)$ and $\chi(1,9)$, meaning that $\mathrm{p}_{A}$ calls
$\mathrm{p}_{\mathit{Err}}$ at least once. Also, $\chi_{F}^{u}\mathbf{exc}$ is
true in $\mathbf{call}$ positions whose procedure is terminated by an
exception thrown by an inner procedure (e.g. pos. 3 and 4).
$\chi_{P}^{u}\mathbf{call}$ is true in $\mathbf{exc}$ statements that
terminate at least one procedure other than the one raising it, such as the
one in pos. 6. $\chi_{F}^{d}\mathbf{ret}$ and $\chi_{F}^{u}\mathbf{ret}$ hold
in $\mathbf{call}$s to non-empty procedures that terminate normally, and not
due to an uncaught exception (e.g., pos. 1).

##### (Summary) Until/Since operators

POTL has two kinds of until and since operators. They express properties on
paths, which are sequences of positions obtained by iterating the different
kinds of next or back operators. In general, a _path_ of length
$n\in\mathbb{N}$ between $i,j\in U$ is a sequence of positions
$i=i_{1}<i_{2}<\dots<i_{n}=j$. The _until_ operator on a set of paths $\Gamma$
is defined as follows: for any word $w$ and position $i\in U$, and for any two
POTL formulas $\varphi$ and $\psi$,
$(w,i)\models\varphi\mathbin{\mathcal{U}(\Gamma)}\psi$ iff there exist a
position $j\in U$, $j\geq i$, and a path $i_{1}<i_{2}<\dots<i_{n}$ between $i$
and $j$ in $\Gamma$ such that $(w,i_{k})\models\varphi$ for any $1\leq k<n$,
and $(w,i_{n})\models\psi$. _Since_ operators are defined symmetrically. Note
that, depending on $\Gamma$, a path from $i$ to $j$ may not exist. We define
until/since operators by associating them with different sets of paths.

The _summary_ until $\psi\mathbin{\mathcal{U}^{t}_{\chi}}\theta$ (resp. since
$\psi\mathbin{\mathcal{S}^{t}_{\chi}}\theta$) operator is obtained by
inductively applying the $\ocircle^{t}$ and $\chi_{F}^{t}$ (resp.
$\circleddash^{t}$ and $\chi_{P}^{t}$) operators. It holds in a position in
which either $\theta$ holds, or $\psi$ holds together with
$\ocircle^{t}(\psi\mathbin{\mathcal{U}^{t}_{\chi}}\theta)$ (resp.
$\circleddash^{t}(\psi\mathbin{\mathcal{S}^{t}_{\chi}}\theta)$) or
$\chi_{F}^{t}(\psi\mathbin{\mathcal{U}^{t}_{\chi}}\theta)$ (resp.
$\chi_{P}^{t}(\psi\mathbin{\mathcal{S}^{t}_{\chi}}\theta)$). It is an until
operator on paths that can move not only between consecutive positions, but
also between contexts of a chain, skipping its body. With the OPM of Figure 1,
this means skipping function bodies. The downward variants can move between
positions at the same level in the ST (i.e., in the same simple chain body),
or down in the nested chain structure. The upward ones remain at the same
level, or move to higher levels of the ST.

Formula ${\top}\mathbin{\mathcal{U}_{\chi}^{u}}{\mathbf{exc}}$ is true in
positions contained in the frame of a function that is terminated by an
exception. It is true in pos. 3 of Figure 5 because of path 3-6, and false in
pos. 1, because no upward path can enter the chain whose contexts are pos. 1
and 11. Formula ${\top}\mathbin{\mathcal{U}_{\chi}^{d}}{\mathbf{exc}}$ is true
in call positions whose function frame contains $\mathbf{exc}$s, but that are
not directly terminated by one of them, such as the one in pos. 1 (with path
1-2-6).

We formally define _Downward Summary Paths_ (DSP) as follows. Given an OP word
$w$, and two positions $i\leq j$ in $w$, the DSP between $i$ and $j$, if it
exists, is a sequence of positions $i=i_{1}<i_{2}<\dots<i_{n}=j$ such that,
for each $1\leq p<n$,

$i_{p+1}=\begin{cases}k&\text{if $k=\max\\{h\mid h\leq
j\land\chi(i_{p},h)\land(i_{p}\lessdot h\lor i_{p}\mathbin{\doteq}h)\\}$
exists;}\\\ i_{p}+1&\text{otherwise, if $i_{p}\lessdot(i_{p}+1)$ or
$i_{p}\mathbin{\doteq}(i_{p}+1)$.}\end{cases}$

The Downward Summary (DS) until and since operators
${}\mathbin{\mathcal{U}_{\chi}^{d}}{}$ and
${}\mathbin{\mathcal{S}_{\chi}^{d}}{}$ use as $\Gamma$ the set of DSPs
starting in the position in which they are evaluated. The definition for the
upward counterparts is, again, obtained by substituting $\gtrdot$ for
$\lessdot$. In Figure 5,
${\mathbf{call}}\mathbin{\mathcal{U}_{\chi}^{d}}{(\mathbf{ret}\land\mathrm{p}_{\mathit{Err}})}$
holds in pos. 1 because of path 1-7-8 and 1-9-10,
${(\mathbf{call}\lor\mathbf{exc})}\mathbin{\mathcal{S}_{\chi}^{u}}{\mathrm{p}_{B}}$
in pos. 7 because of path 3-6-7, and
${(\mathbf{call}\lor\mathbf{exc})}\mathbin{\mathcal{U}_{\chi}^{u}}{\mathbf{ret}}$
in 3 because of path 3-6-7-8.

##### Hierarchical operators.

A single position may be the left or right context of multiple chains. The
operators seen so far cannot keep this fact into account, since they “forget”
about a left context when they jump to the right one. Thus, we introduce the
_hierarchical_ next and back operators. The _upward_ hierarchical next (resp.
back), $\ocircle_{H}^{u}\psi$ (resp. $\circleddash_{H}^{u}\psi$), is true iff
the current position $j$ is the right context of a chain whose left context is
$i$, and $\psi$ holds in the next (resp. previous) pos. $j^{\prime}$ that is a
right context of $i$, with $i\lessdot j,j^{\prime}$. So,
$\ocircle_{H}^{u}\mathrm{p}_{\mathit{Err}}$ holds in pos. 7 of Figure 5
because $\mathrm{p}_{\mathit{Err}}$ holds in 9, and
$\circleddash_{H}^{u}\mathrm{p}_{\mathit{Err}}$ in 9 because
$\mathrm{p}_{\mathit{Err}}$ holds in 7. In the ST, $\ocircle_{H}^{u}$ goes
_up_ between $\mathbf{call}$s to $\mathrm{p}_{\mathit{Err}}$, while
$\circleddash_{H}^{u}$ goes down. Their _downward_ counterparts behave
symmetrically, and consider multiple inner chains sharing their right context.
They are formally defined as:

  * •

$(w,i)\models\ocircle_{H}^{u}\varphi$ iff there exist a position $h<i$ s.t.
$\chi(h,i)$ and $h\lessdot i$ and a position $j=\min\\{k\mid
i<k\land\chi(h,k)\land h\lessdot k\\}$ and $(w,j)\models\varphi$;

  * •

$(w,i)\models\circleddash_{H}^{u}\varphi$ iff there exist a position $h<i$
s.t. $\chi(h,i)$ and $h\lessdot i$ and a position $j=\max\\{k\mid
k<i\land\chi(h,k)\land h\lessdot k\\}$ and $(w,j)\models\varphi$;

  * •

$(w,i)\models\ocircle_{H}^{d}\varphi$ iff there exist a position $h>i$ s.t.
$\chi(i,h)$ and $i\gtrdot h$ and a position $j=\min\\{k\mid
i<k\land\chi(k,h)\land k\gtrdot h\\}$ and $(w,j)\models\varphi$;

  * •

$(w,i)\models\circleddash_{H}^{d}\varphi$ iff there exist a position $h>i$
s.t. $\chi(i,h)$ and $i\gtrdot h$ and a position $j=\max\\{k\mid
k<i\land\chi(k,h)\land k\gtrdot h\\}$ and $(w,j)\models\varphi$.

In the ST of Figure 3, $\ocircle_{H}^{d}$ and $\circleddash_{H}^{d}$ go _down_
and up among $\mathbf{call}$s terminated by the same $\mathbf{exc}$. For
example, in pos. 3 $\ocircle_{H}^{d}\mathrm{p}_{C}$ holds, because both pos. 3
and 4 are in the chain relation with 6. Similarly, in pos. 4
$\circleddash_{H}^{d}\mathrm{p}_{B}$ holds. Note that these operators do not
consider leftmost/rightmost contexts, so $\ocircle_{H}^{u}\mathbf{ret}$ is
false in pos. 9, as $\mathbf{call}\mathbin{\doteq}\mathbf{ret}$, and pos. 11
is the rightmost context of pos. 1.

The hierarchical until and since operators are defined by iterating these next
and back operators. The upward hierarchical path (UHP) between $i$ and $j$ is
a sequence of positions $i=i_{1}<i_{2}<\dots<i_{n}=j$ such that there exists a
position $h<i$ such that for each $1\leq p\leq n$ we have $\chi(h,i_{p})$ and
$h\lessdot i_{p}$, and for each $1\leq q<n$ there exists no position $k$ such
that $i_{q}<k<i_{q+1}$ and $\chi(h,k)$. The until and since operators based on
the set of UHPs starting in the position in which they are evaluated are
denoted as ${}\mathbin{\mathcal{U}_{H}^{u}}{}$ and
${}\mathbin{\mathcal{S}_{H}^{u}}{}$. E.g.,
${\mathbf{call}}\mathbin{\mathcal{U}_{H}^{u}}{\mathrm{p}_{\mathit{Err}}}$
holds in pos. 7 because of the singleton path 7 and path 7-9, and
${\mathbf{call}}\mathbin{\mathcal{S}_{H}^{u}}{\mathrm{p}_{\mathit{Err}}}$ in
pos. 9 because of paths 9 and 7-9.

The downward hierarchical path (DHP) between $i$ and $j$ is a sequence of
positions $i=i_{1}<i_{2}<\dots<i_{n}=j$ such that there exists a position
$h>j$ such that for each $1\leq p\leq n$ we have $\chi(i_{p},h)$ and
$i_{p}\gtrdot h$, and for each $1\leq q<n$ there exists no position $k$ such
that $i_{q}<k<i_{q+1}$ and $\chi(k,h)$. The until and since operators based on
the set of DHPs starting in the position in which they are evaluated are
denoted as ${}\mathbin{\mathcal{U}_{H}^{d}}{}$ and
${}\mathbin{\mathcal{S}_{H}^{d}}{}$. In Figure 5,
${\mathbf{call}}\mathbin{\mathcal{U}_{H}^{d}}{\mathrm{p}_{C}}$ holds in pos.
3, and ${\mathbf{call}}\mathbin{\mathcal{S}_{H}^{d}}{\mathrm{p}_{B}}$ in pos.
4, both because of path 3-4.

##### Equivalences

The POTL until and since operators enjoy expansion laws similar to those of
LTL. Here we give those for two until operators, those for their since and
downward counterparts being symmetric. All such laws are proved in Appendix B.

$\displaystyle\varphi\mathbin{\mathcal{U}^{t}_{\chi}}\psi$
$\displaystyle\equiv\psi\lor\Big{(}\varphi\land\big{(}\ocircle^{t}(\varphi\mathbin{\mathcal{U}^{t}_{\chi}}\psi)\lor\chi_{F}^{t}(\varphi\mathbin{\mathcal{U}^{t}_{\chi}}\psi)\big{)}\Big{)}$
$\displaystyle{\varphi}\mathbin{\mathcal{U}_{H}^{u}}{\psi}$
$\displaystyle\equiv(\psi\land\chi_{P}^{d}\top\land\neg\chi_{P}^{u}\top)\lor\big{(}\varphi\land\ocircle_{H}^{u}({\varphi}\mathbin{\mathcal{U}_{H}^{u}}{\psi})\big{)}$

As in LTL, it is worth defining some derived operators. For $t\in\\{d,u\\}$,
we define the downward/upward summary _eventually_ as
$\Diamond^{t}\varphi:=\top\mathbin{\mathcal{U}^{t}_{\chi}}\varphi$, and the
downward/upward summary _globally_ as
$\square^{t}\varphi:=\neg\Diamond^{t}(\neg\varphi)$. $\Diamond^{u}\varphi$ and
$\square^{u}\varphi$ respectively say that $\varphi$ holds in one or all
positions in the path from the current position to the root of the ST. Their
downward counterparts are more interesting: they consider all positions in the
current rhs and its subtrees, starting from the current position.
$\Diamond^{d}\varphi$ says that $\varphi$ holds in at least one of such
positions, and $\square^{d}\varphi$ in all of them. E.g., if
$\square^{d}(\neg\mathrm{p}_{A})$ holds in a $\mathbf{call}$, it means that
$\mathrm{p}_{A}$ never holds in its whole function body, which is the subtree
rooted next to the $\mathbf{call}$.

We anticipate that preventing downward paths from crossing the boundaries of
the current subtrees and conversely imposing upward ones to exit it without
entering any inner one adds, rather than limiting, generality w.r.t. paths
that can cross both such boundaries.

###  3.2. POTL on $\omega$-Words

Since applications in model checking usually require temporal logics on
infinite words, we now extend POTL to $\omega$-words.

To define OP $\omega$-words, it suffices to replace the finite set of
positions $U$ with the set of natural numbers $\mathbb{N}$ in the definition
of OP words. Then, the formal semantics of all POTL operators remains the same
as in Section 3.1. The only difference in the intuitive meaning of operators
occurs in $\omega$-words with open chains. In fact, chain next operators
($\chi_{F}^{d}$ and $\chi_{F}^{u}$) do not hold on the left contexts of open
chains, as the $\chi$ relation is undefined on them. The same can be said for
downward hierarchical operators, when evaluated on left contexts of open
chains.

Also, property 4 of the $\chi$ relation does not hold if a position $i$ is the
left context of an open chain. In this case, there may be positions
$j_{1}<j_{2}<\dots<j_{n}$ s.t. $\chi(i,j_{p})$ and $i\lessdot j_{p}$ for all
$1\leq p\leq n$, but no position $k$ s.t. $\chi(i,k)$ and $i\gtrdot k$ or
$i\mathbin{\doteq}k$.

###  3.3. Motivating Examples

POTL can express many useful requirements of procedural programs. To emphasize
the potential practical applications in automatic verification, we supply a
few examples of typical program properties expressed as POTL formulas.

Let $\square\psi$ be the LTL _globally_ operator, which can be expressed in
POTL as in Section 3.4.1. POTL can express Hoare-style pre/postconditions with
formulas such as
$\square(\mathbf{call}\land\rho\implies\chi_{F}^{d}(\mathbf{ret}\land\theta))$,
where $\rho$ is the precondition, and $\theta$ is the postcondition.

Unlike NWTL, POTL can easily express properties related to exception handling
and interrupt management. E.g., the shortcut
$\mathit{CallThr}(\psi):=\ocircle^{u}(\mathbf{exc}\land\psi)\lor\chi_{F}^{u}(\mathbf{exc}\land\psi)$,
evaluated in a $\mathbf{call}$, states that the procedure currently started is
terminated by an $\mathbf{exc}$ in which $\psi$ holds. So,
$\square(\mathbf{call}\land\rho\land\mathit{CallThr}(\top)\implies\mathit{CallThr}(\theta))$
means that if precondition $\rho$ holds when a procedure is called, then
postcondition $\theta$ must hold if that procedure is terminated by an
exception. In object oriented programming languages, if $\rho\equiv\theta$ is
a class invariant asserting that a class instance’s state is valid, this
formula expresses _weak (or basic) exception safety_ [Abr00], and _strong
exception safety_ if $\rho$ and $\theta$ express particular states of the
class instance. The _no-throw guarantee_ can be stated with
$\square(\mathbf{call}\land\mathrm{p}_{A}\implies\neg\mathit{CallThr}(\top))$,
meaning procedure $\mathrm{p}_{A}$ is never interrupted by an exception.

_Stack inspection_ [EKS03, JLT99], i.e. properties regarding the sequence of
procedures active in the program’s stack at a certain point of its execution,
is an important class of requirements that can be expressed with shortcut
$\mathit{Scall}(\varphi,\psi):={(\mathbf{call}\implies\varphi)}\mathbin{\mathcal{S}_{\chi}^{d}}{(\mathbf{call}\land\psi)}$,
which subsumes the _call since_ of CaRet, and works with exceptions too. E.g.,
$\square\big{(}(\mathbf{call}\land\mathrm{p}_{B}\land\mathit{Scall}(\top,\mathrm{p}_{A}))\implies\mathit{CallThr}(\top)\big{)}$
means that whenever $\mathrm{p}_{B}$ is executed and at least one instance of
$\mathrm{p}_{A}$ is on the stack, $\mathrm{p}_{B}$ is terminated by an
exception. The OPA of Figure 4 satisfies this formula, because
$\mathrm{p}_{B}$ is always called by $\mathrm{p}_{A}$, and $\mathrm{p}_{C}$
always throws. If the OPA was an $\omega$OPBA, it would not satisfy such
formula because of computations where $\mathrm{p}_{C}$ does not terminate.

###  3.4. Comparison with the state of the art

####  3.4.1. Linear Temporal Logic (LTL)

The main limitation of LTL is that the algebraic structure it is defined on
only contains a linear order on word positions. Thus, it fails to model
systems that require an additional binary relation, such as the $\chi$
relation of POTL. LTL is in fact expressively equivalent to the first-order
fragment of regular languages, and it cannot represent context-free languages,
as POTL does. LTL model checking on pushdown formalisms has been investigated
extensively [EHRS00, ABE+05].

On the other hand, POTL can express all LTL operators, so that POTL is
strictly more expressive than LTL. Any LTL Next formula $\ocircle\varphi$ is
in fact equivalent to the POTL formula
$\ocircle^{d}\varphi^{\prime}\lor\ocircle^{u}\varphi^{\prime}$, where
$\varphi^{\prime}$ is the translation of $\varphi$ into POTL, and the LTL Back
can be translated symmetrically.

The _Globally_ operator can be translated as
$\square\psi:=\neg\Diamond^{u}(\Diamond^{d}\neg\psi)$. This formula contains
an upward summary eventually followed by a downward one, and it can be
explained by thinking to a word’s ST. The upward eventually evaluates its
argument on all positions from the current one to the root. Its argument
considers paths from each one of such positions to all the leaves of the
subtrees rooted at their right, in the same rhs. Together, the two eventually
operators consider paths from the current position to all subsequent positions
in the word. Thus, with the initial negation this formula means that
$\neg\psi$ never holds in such positions, which is the meaning of the LTL
Globally operator.

The translation for LTL Until and Since is much more involved. We need to
define some shortcuts, that will be used again in Section 4.2.2. For any
$a\subseteq AP$, $\sigma_{a}:=\bigwedge_{\mathrm{p}\in
a}\mathrm{p}\land\bigwedge_{\mathrm{q}\not\in a}\neg\mathrm{q}$ holds in a
position $i$ iff $a$ is the set of atomic propositions holding in $i$. For any
POTL formula $\gamma$, let $\chi_{F}^{\lessdot}\gamma:=\bigvee_{a,b\subseteq
AP,\,a\lessdot b}(\sigma_{a}\land\chi_{F}^{d}(\sigma_{b}\land\gamma))$ be the
restriction of $\chi_{F}^{d}\gamma$ to chains with contexts in the $\lessdot$
PR; $\chi_{P}^{\gtrdot}\gamma$ is analogous.

The translation for $\varphi\mathbin{\mathcal{U}}\psi$ follows, that for LTL
Since being symmetric:

$\psi^{\prime}\lor{\big{(}\varphi^{\prime}\land\alpha(\varphi^{\prime})\big{)}}\mathbin{\mathcal{U}_{\chi}^{u}}{\big{(}\psi^{\prime}\lor{(\varphi^{\prime}\land\beta(\varphi^{\prime}))}\mathbin{\mathcal{U}_{\chi}^{d}}{(\psi^{\prime}\land\beta(\varphi^{\prime}))}\big{)}}$

where $\varphi^{\prime}$ and $\psi^{\prime}$ are the translations of $\varphi$
and $\psi$ into POTL, and

$\displaystyle\alpha(\varphi^{\prime})$
$\displaystyle:=\chi_{F}^{u}\top\implies\neg\big{(}\ocircle^{d}({\top}\mathbin{\mathcal{U}_{\chi}^{d}}{\neg\varphi^{\prime}})\lor\chi_{F}^{\lessdot}({\top}\mathbin{\mathcal{U}_{\chi}^{d}}{\neg\varphi^{\prime}})\big{)}$
$\displaystyle\beta(\varphi^{\prime})$
$\displaystyle:=\chi_{P}^{d}\top\implies\neg\big{(}\circleddash^{u}({\top}\mathbin{\mathcal{S}_{\chi}^{u}}{\neg\varphi^{\prime}})\lor\chi_{P}^{\gtrdot}({\top}\mathbin{\mathcal{S}_{\chi}^{u}}{\neg\varphi^{\prime}})\big{)}$

The main formula is the concatenation of a US until and a DS until, and it can
be explained similarly to the translation for LTL Globally. Let $i$ be the
word position in which the formula is evaluated, and $j$ the last one of the
linear path, in which $\psi^{\prime}$ holds. The outermost US until is
witnessed by a path from $i$ to a position $i^{\prime}$ which, in the ST, is
part of the rhs which is the closest common ancestor of $i$ and $j$. In all
positions $i<k<i^{\prime}$ in this path, formula $\alpha(\varphi)$ holds. It
means $\varphi^{\prime}$ holds in all positions contained in the subtree
rooted at the non-terminal to the immediate right of $k$ (i.e., in the body of
the chain whose left context is $k$).

Then, the DS until is witnessed by a downward path from $i^{\prime}$ to $j$.
Here $\beta(\varphi)$ has a role symmetric to $\alpha(\varphi)$. It forces
$\varphi^{\prime}$ to hold in all subtrees rooted at the non-terminal to the
left of positions in the DS path.

Thus, formulas $\alpha(\varphi)$ and $\beta(\varphi)$ make sure
$\varphi^{\prime}$ holds in all chain bodies skipped by the summary paths, and
$\psi^{\prime}$ holds in $j$.

####  3.4.2. Logics on Nested Words

The first temporal logics with explicit context-free aware modalities were
based on nested words (cf. Section 2.2).

CaRet [AEM04] was the first temporal logic on nested words to be introduced,
and it focuses on expressing properties on procedural programs, which explains
its choice of modalities. The _Abstract_ Next and Until operators are defined
on paths of positions in the frame of the same function, skipping frames of
nested calls. The _Caller_ Next and Until are actually past modalities, and
they operate on paths made of the calls of function frames containing the
current position. LTL Next and Until are also present. The Caller operators
enable upward movement in the ST of a nested word, and abstract operators
enable movement in the same rhs. However, no CaRet operator allows pure
downward movement in the ST, which is needed to express properties limited to
a single subtree. While the LTL until can go downward, it can also go beyond
the rightmost leaf of a subtree, thus effectively jumping upwards.

This seems to be the main expressive limitation of CaRet, which is conjectured
not to be FO-complete [AAB+08]. In fact, FO-complete temporal logics were
introduced in [AAB+08] by adding various kinds of _Within_ modalities to
CaRet. Such operators limit their operands to span only positions within the
same call-return pair, and hence the same subtree of the ST, at the cost of an
exponential jump in the complexity of model checking.

Another approach to FO-completeness is that of NWTL [AAB+08], which is based
on _Summary_ Until and Since operators. Summary paths are made of either
consecutive positions, or matched call-return pairs. Thus, they can skip
function bodies, and enter or exit them. Summary-up and down paths, and the
respective operators, can be obtained from summary paths, enabling exclusive
upward or downward movement in the ST. In particular, summary-down operators
may express properties limited to a single subtree.

In Corollary 11, we show that CaRet $\subseteq$ NWTL $\subset$ POTL.

####  3.4.3. Logics on OPLs

The only way to overcome the limitations of nested words is to base a temporal
logic on a more general algebraic structure. OPTL [CMP20] was introduced with
this aim, but it shares some of the limitations that CaRet has on nested
words. It features all LTL past and future operators, plus the _Matching_ Next
($\ocircle_{\chi}$) and Back ($\circleddash_{\chi}$) operators, resp.
equivalent to POTL $\chi_{F}^{u}$ and $\chi_{P}^{u}$, OP _Summary_ Until and
Since, and _Hierarchical_ Until and Since. POTL has several advantages over
OPTL in its ease of expressing requirements.

Given a set of PRs $\Pi$, an OPTL Summary Until $\mathbin{\mathcal{U}^{\Pi}}$
evaluated on a position $i$ considers paths $i=i_{1}<i_{2}<\dots<i_{n}=j$,
with $i\leq j$, such that for any $1\leq p<n$,

$i_{p+1}=\begin{cases}h&\text{if there exists $h$ s.t.\ $\chi(i_{p},h)$ and
$(i_{p}\mathbin{\doteq}h$ or $i_{p}\gtrdot h)$, and $h\leq j$;}\\\
i_{p}+1&\text{if $i_{p}\mathrel{\pi}i_{p+1}$ for some $\pi\in\Pi$,
otherwise.}\end{cases}$

The Summary Since $\mathbin{\mathcal{S}^{\Pi}}$ is symmetric: positions in the
$\chi$ relation must be in the $\lessdot$ or $\mathbin{\doteq}$ PRs. Since the
PRs checked on chain contexts are fixed, the user can control whether such
paths go up or down in the ST only partially. OPTL’s
$\varphi\mathbin{\mathcal{U}^{\mathbin{\doteq}\gtrdot}}\psi$ is equivalent to
POTL’s ${\varphi}\mathbin{\mathcal{U}_{\chi}^{u}}{\psi}$, and
$\varphi\mathbin{\mathcal{S}^{\lessdot\mathbin{\doteq}}}\psi$ to
${\varphi}\mathbin{\mathcal{S}_{\chi}^{d}}{\psi}$: both operators only go
upwards in the ST. However, there is no OPTL operator equivalent to POTL’s
${}\mathbin{\mathcal{U}_{\chi}^{d}}{}$ or
${}\mathbin{\mathcal{S}_{\chi}^{u}}{}$, which go downward. This makes it
difficult to express function-local properties limited to a single subtree in
OPTL.

Figure 6. Example OP word on OPM $M_{\mathbf{call}}$.

E.g., consider POTL formula
$\alpha:=\square(\mathbf{exc}\implies\chi_{P}^{d}(\mathbf{han}\land\Diamond^{d}\mathrm{p}_{A}))$,
which means that if an exception is thrown, it is always caught, and procedure
$\mathrm{p}_{A}$ is called at some point inside the
$\mathbf{han}$-$\mathbf{exc}$ block. One could try to translate it into OPTL
with a formula such as
$\beta:=\square(\mathbf{exc}\implies\circleddash_{\chi}(\mathbf{han}\land\top\mathbin{\mathcal{U}^{\lessdot\mathbin{\doteq}}}\mathrm{p}_{A}))$.
Consider the OP word of Figure 6. When the until in $\beta$ is evaluated in
the $\mathbf{han}$ of pos. 3, its paths can only consider positions 4 and 5,
because paths touching such positions cannot pass the $\gtrdot$ relation
between 5 and 6. Its paths, unlike those of its POTL counterpart, cannot jump
between chain contexts in the $\lessdot$ relation, and cannot reach positions
6, 8, and 12 in this way. If $\mathrm{p}_{A}$ held in pos. 6 and 10, $\alpha$
would be true in the word, but $\beta$ would be false. Replacing the until
with
$\top\mathbin{\mathcal{U}^{\lessdot\mathbin{\doteq}\gtrdot}}\mathrm{p}_{A}$
overcomes such issues, but it introduces another one: its paths would go past
pos. 14, going outside of the subtree. Thus, if $\mathrm{p}_{A}$ held only in
pos. 15, $\alpha$ would be false, but this variant of $\beta$ would hold.

OPTL has Hierarchical operators, too. Its yield-precedence Hierarchical Until
($\mathbin{\mathcal{U}^{\uparrow}}$) and since
($\mathbin{\mathcal{S}^{\downarrow}}$) operators, when evaluated on a position
$i$, consider paths $i<j_{1}<j_{2}<\dots<j_{n}$ s.t. $\chi(i,j_{p})$ and
$i\lessdot j_{p}$ for all $1\leq p\leq n$, and there is no $k<j_{1}$ s.t.
$\chi(i,k)$. Their take-precedence counterparts
($\mathbin{\mathcal{U}^{\downarrow}}$ and $\mathbin{\mathcal{S}^{\uparrow}}$)
are symmetric. Thus, such paths do not start in the position where until and
since operators are evaluated, but always in a future position: this is
another limitation of OPTL. In fact, it is not possible to concatenate them to
express complex properties on right (resp. left) contexts of chains sharing
their left (resp. right) context, such as several function calls issued by the
same function, or multiple function calls terminated by the same exception.
POTL has both Hierarchical Next/Back and Until/Since pairs which are
composable, making it expressively complete on such positions. For example,
POTL formula
$\gamma:=\square(\mathbf{call}\land\mathrm{p}_{A}\implies{({\top}\mathbin{\mathcal{S}_{H}^{u}}{(\mathbf{call}\land\mathrm{p}_{B})})}\mathbin{\mathcal{S}_{\chi}^{d}}{(\circleddash^{d}\\#\lor\chi_{P}^{d}\\#)})$
means that whenever procedure $\mathrm{p}_{A}$ is called, all procedures in
the stack have previously invoked $\mathrm{p}_{B}$ (possibly excluding the one
directly calling $\mathrm{p}_{A}$). While
${}\mathbin{\mathcal{S}_{\chi}^{d}}{}$ can be replaced with OPTL’s
$\mathbin{\mathcal{S}^{\lessdot\mathbin{\doteq}}}$, POTL’s
${}\mathbin{\mathcal{S}_{H}^{u}}{}$ cannot be easily translated. In fact,
OPTL’s Hierarchical operators would only allow us to state that
$\mathrm{p}_{B}$ is invoked by the procedures in the stack, but not
necessarily before the call to $\mathrm{p}_{A}$.

The above intuition about OPTL’s weaknesses are made formal in the next
subsection.

####  3.4.4. OPTL is not expressively complete

In this section, we prove that no OPTL formula is equivalent to POTL formula
$\Diamond^{d}\mathrm{p}_{A}$. The proof is quite elaborate, which is
unsurprising, since the analogous problem of the comparison between CaRet and
NWTL is still open.

First, we prove the following

######  Lemma 1 (Pumping Lemma for OPTL).

Let $\varphi$ be an OPTL formula and $L$ an OPL, both defined on a set of
atomic propositions $AP$ and an OPM $M_{AP}$. Then, for some positive integer
$n$, for each $w\in L$, $|w|\geq n$, there exist strings
$u,v,x,y,z\in{\mathcal{P}(AP)}^{*}$ such that $w=uvxyz$, $|vy|>1$, $|vxy|\leq
n$ and for any $k>0$ we have $w^{\prime}=uv^{k}xy^{k}z\in L$; for any $0\leq
j\leq k$ and $0\leq i<|v|$ we have $(w,|u|+i)\models\varphi$ iff
$(w^{\prime},|u|+j|v|+i)\models\varphi$, and for any $0\leq i<|y|$ we have
$(w,|uv^{k}x|+i)\models\varphi$ iff
$(w^{\prime},|uv^{k}x|+j|y|+i)\models\varphi$.

######  Proof 3.1.

Given a word $w\in L$, we define $\lambda(w)$ as the word of length $|w|$ such
that, if position $i$ of $w$ is labeled with $a$, then the same position in
$\lambda(w)$ is labeled with $(a,1)$ if $(w,i)\models\varphi$, and with
$(a,0)$ otherwise. Let $\lambda(L)=\\{\lambda(w)\mid w\in L\\}$, and
$\lambda^{-1}$ is such that $\lambda^{-1}(\lambda(w))=w$. If we prove that
$\lambda(L)$ is context-free, from the classic Pumping Lemma [Har78] follows
that, for some $n>0$, for all $\hat{w}\in\lambda(L)$ there exist strings
$\hat{u},\hat{v},\hat{x},\hat{y},\hat{z}\in({\mathcal{P}(AP)}\times\\{0,1\\})^{*}$
such that $\hat{w}=\hat{u}\hat{v}\hat{x}\hat{y}\hat{z}$, $|\hat{v}\hat{y}|>1$,
$|\hat{v}\hat{x}\hat{y}|\leq n$ and for any $k>0$ we have
$\hat{w}^{\prime}=\hat{u}\hat{v}^{k}\hat{x}\hat{y}^{k}\hat{z}\in\lambda(L)$.
The claim follows by applying $\lambda^{-1}$ to such strings, and the word
positions in which $\varphi$ holds in $\lambda^{-1}(\hat{w})$ are those
labeled with $1$.

To prove that $\lambda(L)$ is context-free, we use the OPTL model checking
construction given in [CMP20], which yields an OPA
$\mathcal{A}_{\varphi}=({\mathcal{P}(AP)},\allowbreak M_{AP},\allowbreak
Q,\allowbreak I,\allowbreak F,\allowbreak\delta)$ accepting models of
$\varphi$. The states of $\mathcal{A}_{\varphi}$ are elements of the set
$\operatorname{Cl}({\varphi})$, which contains $\varphi$ and all its
subformulas. Given a word $w$ compatible with $M_{AP}$, the accepting
computations of $\mathcal{A}_{\varphi}$ are such that, for each $0\leq i<|w|$,
the state of $\mathcal{A}_{\varphi}$ prior to reading position $i$ contains
$\psi\in\operatorname{Cl}({\varphi})$ iff $(w,i)\models\psi$.

Thus, we build OPA
$\mathcal{A}_{\lambda({\mathcal{P}(AP)}^{*})}=({\mathcal{P}(AP)}\times\\{0,1\\},\allowbreak
M_{AP},\allowbreak Q,\allowbreak I^{\prime},\allowbreak
F,\allowbreak\delta^{\prime})$ that reads words on
$({\mathcal{P}(AP)}\times\\{0,1\\})^{*}$ and accepts
$\lambda({\mathcal{P}(AP)}^{*})$ as follows:

  * •

$I^{\prime}$ is the set of all states in $Q$ not containing past operators
(and possibly $\varphi$);

  * •

$\delta^{\prime}_{\mathit{push}}$ is such that if
$(\Phi,a,\Theta)\in\delta_{\mathit{push}}$, then
$(\Phi,(a,1),\Theta)\in\delta_{\mathit{push}}$ if $\varphi\in\Phi$, and
$(\Phi,(a,0),\Theta)\in\delta_{\mathit{push}}$ otherwise;

  * •

$\delta^{\prime}_{\mathit{shift}}$ is derived from $\delta_{\mathit{shift}}$
similarly;

  * •

$\delta^{\prime}_{\mathit{pop}}=\delta_{\mathit{pop}}$.

Since $L$ is an OPL, there exists an OPA $\mathcal{A}_{L}$ accepting it.
$\mathcal{A}_{L}$ can be easily modified to obtain $\mathcal{A}^{\prime}_{L}$,
an OPA accepting all words $\hat{w}\in({\mathcal{P}(AP)}\times\\{0,1\\})^{*}$
such that the underlying word $w\in{\mathcal{P}(AP)}^{*}$ is in $L$. Language
$\lambda(L)$ is the intersection between the language accepted by
$\mathcal{A}^{\prime}_{L}$, and $\lambda({\mathcal{P}(AP)}^{*})$. Since OPLs
are closed under intersection, $\lambda(L)$ is also an OPL.

Let $L_{\mathbf{call}}$ be the max-language generated by OPM
$M_{\mathbf{call}}$, with the addition that $\mathrm{p}_{A}$ may appear in any
word position. We prove the following:

Figure 7. Structure of a word in $L_{\mathbf{call}}$.

######  Theorem 2.

Given the POTL formula $\Diamond^{d}\mathrm{p}_{A}$, for every OPTL formula
$\varphi$ there exist a word $w\in L_{\mathbf{call}}$ and an integer $0\leq
i<|w|$ such that either $(w,i)\models\Diamond^{d}\mathrm{p}_{A}$ and
$(w,i)\not\models\varphi$, or $(w,i)\not\models\Diamond^{d}\mathrm{p}_{A}$ and
$(w,i)\models\varphi$.

######  Proof 3.2.

Figure 7 shows the structure of the syntax trees of words in a subset of
$L_{\mathbf{call}}$. Dots between $\mathbf{han}$–$\mathbf{exc}$ pairs can be
replaced with repetitions of the whole tree structure, and other dots with the
repetition of surrounding tree fragments (e.g., $\mathbf{call}$–$\mathbf{ret}$
or $\mathbf{han}$–$\mathbf{exc}$). $\mathbf{han}_{0}$ is the position in which
$\varphi$ is evaluated, and $\mathbf{exc}_{0}$ is its matched $\mathbf{exc}$.
$\mathbf{call}_{1}$ is the $\mathbf{call}$ right after $\mathbf{han}_{0}$, and
$\mathbf{call}_{0}$ is the one at the highest level of the subtree between
$\mathbf{han}_{0}$ and $\mathbf{exc}_{0}$. $\mathbf{call}$s between
$\mathbf{call}_{0}$ and $\mathbf{exc}_{0}$ do not have a corresponding
$\mathbf{ret}$, and are terminated by $\mathbf{exc}_{0}$. The word delimited
by $\mathbf{han}_{0}$ and $\mathbf{exc}_{0}$ is itself part of a larger tree
with the same structure. For $\varphi$ to be equivalent to
$\Diamond^{d}\mathrm{p}_{A}$, it must be able to

  1. (1)

look for the symbol $\mathrm{p}_{A}$ in all positions between
$\mathbf{han}_{0}$ and $\mathbf{exc}_{0}$; and

  2. (2)

not consider any positions before $\mathbf{han}_{0}$ or after
$\mathbf{exc}_{0}$.

In the following, we show that any OPTL formula $\varphi$ fails to satisfy
both requirements, thus

  1. (1)

one can hide $\mathrm{p}_{A}$ in one of the positions not covered, so that
$\varphi$ is false in $\mathbf{han}_{0}$, but $\Diamond^{d}\mathrm{p}_{A}$ is
true; or

  2. (2)

put $\mathrm{p}_{A}$ in one of the positions outside
$\mathbf{han}_{0}$–$\mathbf{exc}_{0}$ reached by $\varphi$, so that it is true
in $\mathbf{han}_{0}$, but $\Diamond^{d}\mathrm{p}_{A}$ is not.

If $\varphi$ is evaluated on position $\mathbf{han}_{0}$, it must contain some
modal operator based on paths that reach each position between
$\mathbf{han}_{0}$ and $\mathbf{exc}_{0}$. The length of the word between
$\mathbf{han}_{0}$ and $\mathbf{exc}_{0}$ has no limit, so $\varphi$ must
contain at least an until operator, which may be a LTL Until, an OPTL
Hierarchical Until, or an OPTL Summary Until $\mathbin{\mathcal{U}^{\Pi}}$.
For $\mathbin{\mathcal{U}^{\Pi}}$, we must have $\gtrdot\in\Pi$, or the path
would not be able to reach past position $\mathbf{ret}_{1}$ (remember that an
OPTL summary path cannot skip chains with contexts in the $\lessdot$
relation). The presence of $\gtrdot$ allows the Summary Until to reach
positions past $\mathbf{exc}_{0}$: the formula could be true if
$\mathrm{p}_{A}$ appears after $\mathbf{exc}_{0}$, but not between
$\mathbf{han}_{0}$ and $\mathbf{exc}_{0}$, unlike
$\Diamond^{d}\mathrm{p}_{A}$. To avoid this, the path must be stopped earlier,
by embedding an appropriate subformula as the left operand of the until.

Suppose there exists a formula $\psi$ that is true in $\mathbf{exc}_{0}$, and
false in all positions between $\mathbf{han}_{0}$ and $\mathbf{exc}_{0}$. By
Lemma 1, there exists an integer $n$ such that for any $w\in
L_{\mathbf{call}}$ longer than $n$ there is $w^{\prime}=uv^{k}xy^{k}z\in
L_{\mathbf{call}}$, for some $k>0$, such that either (a) $\psi$ never holds in
$v^{k}xy^{k}$, or (b) it holds at least $k$ times in there. We can take $w$
such that $\mathbf{han}_{0}$ and $\mathbf{exc}_{0}$ both appear after position
$n$, and they contain nested $\mathbf{han}$–$\mathbf{exc}$ pairs. In case (a),
$\psi$ cannot distinguish $\mathbf{exc}_{0}$ from nested $\mathbf{exc}$s, so a
$\varphi$ based on $\psi$ is not equivalent to $\Diamond^{d}\mathrm{p}_{A}$ in
$\mathbf{han}_{0}$. The same can be said in case (b), by evaluating $\varphi$
in a $\mathbf{han}$ from $v^{i}$ with $i<k$. In this case, also chaining
multiple untils, each one ending in a position in which $\psi$ holds, does not
work, as $k$ can be increased beyond the finite length of any OPTL formula.

The above argument holds verbatim for LTL Until, and does not change if we
prepend LTL or abstract next operators to the until, because the length of the
branch between $\mathbf{call}_{1}$ and $\mathbf{call}_{0}$ is unlimited. The
argument for using since operators starting from $\mathbf{exc}_{0}$ is
symmetric. If both until and since operators are used, it suffices to apply
the Pumping Lemma twice (one for until and one for since), and take a value of
$k$ large enough that a part of the string cannot be reached by the number of
until and since operators in the formula. If Hierarchical operators are used,
the argument does not change, as they still need nested until or since
operators to cover the whole subtree.

This argument also holds when the formula contains (possibly nested) negated
until operators. This is trivial if their paths cannot reach part of the
subtree between $\mathbf{han}_{0}$ and $\mathbf{exc}_{0}$. If, instead, they
can reach positions past $\mathbf{exc}_{0}$, we can build a word with
$\mathrm{p}_{A}$ in one of such positions, but not between $\mathbf{han}_{0}$
and $\mathbf{exc}_{0}$. To distinguish it from a word with $\mathrm{p}_{A}$
between $\mathbf{han}_{0}$ and $\mathbf{exc}_{0}$, the formula would need a
subformula that can distinguish positions between $\mathbf{han}_{0}$ and
$\mathbf{exc}_{0}$ from those outside, which would contradict Lemma 1.

Until now, we have proved that a formula equivalent to
$\Diamond^{d}\mathrm{p}_{A}$ cannot contain until or since operators that stop
exactly at $\mathbf{exc}_{0}$. However, they could be stopped earlier. In the
following, we show that any such OPTL formula can only work for words of a
limited length. Hence, no OPTL formula is equivalent to
$\Diamond^{d}\mathrm{p}_{A}$ on all words in $L_{\mathbf{call}}$.

Let $w\in L_{\mathbf{call}}$, and $x=\mathbf{han}\,y\,\mathbf{exc}$ a subword
of $w$ with the structure of Figure 7, in which each $\mathbf{han}$ has a
matched $\mathbf{exc}$, and conversely. We define
$\operatorname{h_{\mathbf{exc}}}(x)=0$ if $y$ contains no positions labeled
with $\mathbf{han}$ or $\mathbf{exc}$ (hence, only $\mathbf{call}$s and
$\mathbf{ret}$s). Otherwise, let
$x^{\prime}=\mathbf{han}\,y^{\prime}\,\mathbf{exc}$ be the proper subword of
$y$ with the maximum value of $\operatorname{h_{\mathbf{exc}}}(x^{\prime})$:
we set
$\operatorname{h_{\mathbf{exc}}}(x)=\operatorname{h_{\mathbf{exc}}}(x^{\prime})+1$.

We prove by induction on $\operatorname{h_{\mathbf{exc}}}(x)$ that any OPTL
formula evaluated in the first position of $x$ must contain nested until or
since operators with a nesting depth of at least
$2\cdot\operatorname{h_{\mathbf{exc}}}(x)+1$ to be equivalent to
$\Diamond^{d}\mathrm{p}_{A}$.

If $\operatorname{h_{\mathbf{exc}}}(x)=0$, at least one until or since
operator is needed, as the length of $x$ is not fixed. E.g., OPTL formula
$\neg\mathbf{exc}\mathbin{\mathcal{U}^{\lessdot\mathbin{\doteq}\gtrdot}}\mathrm{p}_{A}$
suffices.

If $\operatorname{h_{\mathbf{exc}}}(x)=n>0$, Figure 7 shows a possible
structure of $x$. Any Summary Until in the formula must be nested into another
operator, or its paths would jump to, and go past, the last position of $x$
($\mathbf{exc}_{0}$). A Summary Until could be, instead, nested into any
number of nested next operators, to be evaluated in one of the positions shown
in Figure 7 between $\mathbf{han}_{0}$ and $\mathbf{call}_{0}$. (The tree
fragments between $\mathbf{call}_{1}$ and $\mathbf{call}_{0}$ can be repeated
enough times so that the next operators alone cannot reach
$\mathbf{call}_{0}$.) As noted earlier, any such summary until must allow for
paths with consecutive positions in the $\gtrdot$ relation. It may also jump
to $\mathbf{exc}_{0}$ by following the chain relation, because
$\mathbf{call}\gtrdot\mathbf{exc}$. Hence, the until must be stopped earlier
by choosing appropriate operands (e.g., $\neg\ocircle_{\chi}\mathbf{exc}$ as
the left operand). However, this leaves the subword between
$\mathbf{call}_{0}$ and $\mathbf{exc}_{0}$ unreached, so any of its positions
containing (or not) $\mathrm{p}_{A}$ would be ignored. This can only be solved
with another until operator, so at least two are needed. If it is a Summary
Until, then it must not allow the $\gtrdot$ relation, or it could, again,
escape $\mathbf{exc}_{0}$ (e.g. by skipping chains between $\mathbf{call}$s
and $\mathbf{exc}_{0}$). The argument can be extended by considering an LTL
Until which stops anywhere before $\mathbf{exc}_{0}$, or since operators
evaluated in $\mathbf{exc}$ (e.g., nested in a $\ocircle_{\chi}$ operator).
The same can be said for Hierarchical operators, which can cover only a part
of the subtree if used alone.

Let $x^{\prime}=\mathbf{han}\,y^{\prime}\,\mathbf{exc}$ be a proper subword of
$y$ with $\operatorname{h_{\mathbf{exc}}}(x^{\prime})=n-1$. Suppose it appears
before $\mathbf{call}_{0}$ (the other case is symmetric). It needs at least an
until or since operator to be covered, which must not escape
$\mathbf{han}_{0}$ or $\mathbf{exc}_{0}$. The Pumping Lemma can be used to
show that no OPTL formula can distinguish positions in $x$ or $x^{\prime}$
from those outside. Thus, a formula with until or since operators that do not
exit $y^{\prime}$ is needed. By the inductive hypothesis, it consists of at
least $2(n-1)+1$ until or since operators, thus $x$ needs $2n+1$ of them.

Note that the argument also holds if the until formulas are negated, because
negation cannot change the type of paths considered by an operator, and cannot
decrease the number of nested untils needed to cover the whole subtree.

##  4\. First-Order Completeness on Finite Words

To show that POTL $\subseteq$ FOL on finite OP words, we give a direct
translation of POTL into FOL. Proving that FOL $\subseteq$ POTL is more
involved: we translate $\mathcal{X}_{\mathit{until}}$ [Mar04], a logic on
trees, into POTL. $\mathcal{X}_{\mathit{until}}$ (defined in Section 4.2.2) is
a logic on trees introduced to prove the expressive completeness of
Conditional XPath, and from its being equivalent to FOL on trees [Mar05, LS10]
we derive a FO-completeness result for POTL.

###  4.1. First-Order Semantics of POTL

We show that POTL can be expressed with FOL equipped with monadic relations
for atomic propositions, a total order on positions, and the chain relation
between pairs of positions. We define below the translation function $\nu$,
such that for any POTL formula $\varphi$, word $w$ and position $i$,
$(w,i)\models\nu_{\varphi}(x)$ iff $(w,i)\models\varphi$. The translation for
propositional operators is trivial.

For temporal operators, we first need to define a few auxiliary formulas. We
define the successor relation as the FO formula

$\operatorname{succ}(x,y):=x<y\land\neg\exists z(x<z\land z<y).$

The PRs between positions can be expressed by means of propositional
combinations of monadic atomic relations only. Given a set of atomic
propositions $a\subseteq AP$, we define formula $\sigma_{a}(x)$, stating that
all and only propositions in $a$ hold in position $x$, as follows:

$\sigma_{a}(x):=\bigwedge_{\mathrm{p}\in
a}\mathrm{p}(x)\land\bigwedge_{\mathrm{p}\in AP\setminus a}\neg\mathrm{p}(x)$
(1)

For any pair of FO variables $x,y$ and
$\pi\in\\{\lessdot,\mathbin{\doteq},\gtrdot\\}$, we can build formula

$x\mathrel{\pi}y:=\bigvee_{a,b\subseteq AP\mid
a\mathrel{\pi}b}(\sigma_{a}(x)\land\sigma_{b}(y)).$

The following translations employ the three FO variables $x,y,z$, only. This,
in addition to the FO-completeness result for POTL, proves that FOL on OP
words retains the three-variable property, which holds in regular words.

####  4.1.1. Next and Back Operators

$\nu_{\ocircle^{d}\varphi}(x):=\exists
y\Big{(}\operatorname{succ}(x,y)\land(x\lessdot y\lor
x\mathbin{\doteq}y)\land\exists
x\big{(}x=y\land\nu_{\varphi}(x)\big{)}\Big{)}$

$\nu_{\circleddash^{d}\varphi}(x)$ is defined similarly, and
$\nu_{\ocircle^{u}\varphi}(x)$ and $\nu_{\circleddash^{u}\varphi}(x)$ by
replacing $\lessdot$ with $\gtrdot$.

$\nu_{\chi_{F}^{d}\varphi}(x):=\exists y\big{(}\chi(x,y)\land(x\lessdot y\lor
x\mathbin{\doteq}y)\land\exists x(x=y\land\nu_{\varphi}(x))\big{)}$

$\nu_{\chi_{P}^{d}\varphi}(x)$, $\nu_{\chi_{F}^{u}\varphi}(x)$ and
$\nu_{\chi_{P}^{u}\varphi}(x)$ are defined similarly.

####  4.1.2. Downward/Upward Summary Until/Since

The translation for the DS until operator can be obtained by noting that,
given two positions $x$ and $y$, the DSP between them, if it exists, is the
one that skips all chain bodies entirely contained between them, among those
with contexts in the $\lessdot$ or $\mathbin{\doteq}$ relations. A position
$z$ being part of such a path can be expressed with formula
$\neg\gamma(x,y,z)$ as follows:

$\displaystyle\gamma(x,y,z)$
$\displaystyle:=\gamma_{L}(x,z)\land\gamma_{R}(y,z)$
$\displaystyle\gamma_{L}(x,z)$ $\displaystyle:=\exists y\Big{(}x\leq y\land
y<z\land\exists x\big{(}z<x\land\chi(y,x)\land(y\lessdot x\lor
y\mathbin{\doteq}x)\big{)}\Big{)}$ $\displaystyle\gamma_{R}(y,z)$
$\displaystyle:=\exists x\Big{(}z<x\land x\leq y\land\exists
y\big{(}y<z\land\chi(y,x)\land(y\lessdot x\lor
y\mathbin{\doteq}x)\big{)}\Big{)}$

$\gamma(x,y,z)$ is true iff $z$ is not part of the DSP between $x$ and $y$,
while $x\leq z\leq y$. In particular, $\gamma_{L}(x,z)$ asserts that $z$ is
part of the body of a chain whose left context is after $x$, and
$\gamma_{R}(y,z)$ states that $z$ is part of the body of a chain whose right
context is before $y$. Since chain bodies cannot cross, either the two chain
bodies are actually the same one, or one of them is a sub-chain nested into
the other. In both cases, $z$ is part of a chain body entirely contained
between $x$ and $y$, and is thus not part of the path.

Moreover, for such a path to exist, each one of its positions must be in one
of the admitted PRs with the next one. Formula

$\delta(y,z):=\exists x\big{(}z<x\land x\leq y\land(z\lessdot x\lor
z\mathbin{\doteq}x)\land\neg\gamma(z,y,x)\land(\operatorname{succ}(z,x)\lor\chi(z,x))\big{)}$

asserts this for position $z$, with the path ending in $y$. (Note that by
exchanging $x$ and $z$ in the definition of $\gamma(x,y,z)$ above, one can
obtain $\gamma(z,y,x)$ without using any additional variable.) Finally,
${\varphi}\mathbin{\mathcal{U}_{\chi}^{d}}{\psi}$ can be translated as
follows:

$\displaystyle\nu_{{\varphi}\mathbin{\mathcal{U}_{\chi}^{d}}{\psi}}(x):=\exists
y\Big{(}$ $\displaystyle x\leq y\land\exists x(x=y\land\nu_{\psi}(x))$
$\displaystyle\land\forall z\big{(}x\leq z\land
z<y\land\neg\gamma(x,y,z)\implies\exists
x(x=z\land\nu_{\varphi}(x))\land\delta(y,z)\big{)}\Big{)}$

The translation for the DS since operator is similar:

$\displaystyle\nu_{{\varphi}\mathbin{\mathcal{S}_{\chi}^{d}}{\psi}}(x):=\exists
y\Big{(}$ $\displaystyle y\leq x\land\exists x(x=y\land\nu_{\psi}(x))$
$\displaystyle\land\forall z\big{(}y<z\land z\leq
x\land\neg\gamma(y,x,z)\implies\exists
x(x=z\land\nu_{\varphi}(x))\land\delta(x,z)\big{)}\Big{)}$

$\nu_{{\varphi}\mathbin{\mathcal{U}_{\chi}^{u}}{\psi}}(x)$ and
$\nu_{{\varphi}\mathbin{\mathcal{S}_{\chi}^{u}}{\psi}}(x)$ are defined as
above, substituting $\gtrdot$ for $\lessdot$.

####  4.1.3. Hierarchical Operators

Finally, below are the translations for two hierarchical operators, the others
being symmetric.

$\displaystyle\nu_{\ocircle_{H}^{u}\varphi}(x):=$ $\displaystyle\exists
y\Bigg{(}y<x\land\chi(y,x)\land y\lessdot x\land$ $\displaystyle\qquad\exists
z\Big{(}x<z\land\chi(y,z)\land y\lessdot z\land\exists
x(x=z\land\nu_{\varphi}(x))$ $\displaystyle\qquad\quad\land\forall
y\big{(}x<y\land y<z\implies\forall z(\chi(z,x)\land z\lessdot
x\implies\neg\chi(z,y))\big{)}\Big{)}\Bigg{)}$
$\displaystyle\nu_{{\varphi}\mathbin{\mathcal{U}_{H}^{u}}{\psi}}(x):=\exists
z\bigg{(}$ $\displaystyle z<x\land z\lessdot x\land\chi(z,x)\land$
$\displaystyle\exists y\Big{(}x\leq y\land\chi(z,y)\land z\lessdot
y\land\exists x(x=y\land\nu_{\psi}(x))\land$ $\displaystyle\quad\forall
z\big{(}x\leq z\land z<y\land\exists y(y<x\land y\lessdot
x\land\chi(y,x)\land\chi(y,z))$ $\displaystyle\qquad\qquad\implies\exists
x(x=z\land\nu_{\varphi}(x)))\big{)}\Big{)}\bigg{)}$

###  4.2. Expressing $\mathcal{X}_{\mathit{until}}$ in POTL

To translate $\mathcal{X}_{\mathit{until}}$ to POTL, we give an isomorphism
between OP words and (a subset of) unranked ordered trees (UOT), the
structures on which $\mathcal{X}_{\mathit{until}}$ is defined. First, we show
how to translate OP words into UOTs, and then the reverse.

####  4.2.1. OPM-compatible Unranked Ordered Trees

[Unranked Ordered Trees] A UOT is a tuple $T=\langle
S,R_{\Downarrow},R_{\Rightarrow},L\rangle$. Each node is a sequence of child
numbers, representing the path from the root to it. $S$ is a finite set of
finite sequences of natural numbers closed under the prefix operation, and for
any sequence $s\in S$, if $s\cdot k\in S$, $k\in\mathbb{N}$, then either $k=0$
or $s\cdot(k-1)\in S$ (by $\cdot$ we denote concatenation). $R_{\Downarrow}$
and $R_{\Rightarrow}$ are two binary relations called the _descendant_ and
_following sibling_ relation, respectively. For $s,t\in S$, $sR_{\Downarrow}t$
iff $t$ is any child of $s$ ($t=s\cdot k$, $k\in\mathbb{N}$, i.e. $t$ is the
$k$-th child of $s$), and $sR_{\Rightarrow}t$ iff $t$ is the immediate sibling
to the right of $s$ ($s=r\cdot h$ and $t=r\cdot(h+1)$, for $r\in S$ and
$h\in\mathbb{N}$). $L\colon AP\rightarrow{\mathcal{P}(S)}$ is a function that
maps each atomic proposition to the set of nodes labeled with it. We denote as
$\mathcal{T}$ the set of all UOTs.

Given an OP word $w=\langle U,<,M_{{\mathcal{P}(AP)}},P\rangle$, it is
possible to build a UOT $T_{w}=\langle S_{w},\allowbreak
R_{\Downarrow},\allowbreak R_{\Rightarrow},\allowbreak
L_{w}\rangle\in\mathcal{T}$ with labels in ${\mathcal{P}(AP)}$ isomorphic to
$w$. To do so, we define a function $\tau\colon U\rightarrow S_{w}$, which
maps positions of $w$ into nodes of $T_{w}$. First, $\tau(0)=0$: position 0 is
the root node, and the last $\\#$ is its rightmost child. Given any position
$i\in U$:

  * •

if $i\mathbin{\doteq}i+1$, then $\tau(i+1)=\tau(i)\cdot 0$ is the only child
of $i$;

  * •

if $i\gtrdot i+1$, then $i$ has no children;

  * •

if $i\lessdot i+1$, then the leftmost child of $i$ is $i+1$
($\tau(i+1)=\tau(i)\cdot 0$). Moreover, if $j_{1}<j_{2}<\dots<j_{n}$ is the
largest set of positions such that $\chi(i,j_{k})$ and either $i\lessdot
j_{k}$ or $i\mathbin{\doteq}j_{k}$ for $1\leq k\leq n$, then
$\tau(j_{k})=\tau(i)\cdot k$.

In general, $i$ is in the $\lessdot$ relation with all of its children, except
possibly the rightmost one, with which $i$ may be in the $\mathbin{\doteq}$
relation (cf. property 4 of the $\chi$ relation).

This way, every position $i$ in $w$ appears in the UOT exactly once. Indeed,
if either $(i-1)\lessdot i$ or $(i-1)\mathbin{\doteq}i$, then $i$ is a child
of $i-1$. Conversely, $(i-1)\gtrdot i$ iff $i$ is the right context of at
least one chain. Thus, consider $j$ s.t. $\chi(j,i)$, and for no
$j^{\prime}<j$ we have $\chi(j^{\prime},i)$: by property 3 of $\chi$, either
$j\mathbin{\doteq}i$ or $j\lessdot i$. So, $i$ is a child of $j$ by the third
rule above, and of no other node, because if $(i-1)\gtrdot i$, then no other
rule applies.

Finally, $\tau(i)\in L_{w}(\mathrm{a})$ iff $i\in P(\mathrm{a})$ for all
$\mathrm{a}\in AP$, so each node in $T_{w}$ is labeled with the set of atomic
propositions that hold in the corresponding word position. We denote as
$T_{w}=\tau(w)$ the UOT obtained by applying $\tau$ to every position of an OP
word $w$. Figure 8 shows the translation of the word of Figure 5 into an UOT.

Figure 8. The UOT corresponding to the word of Figure 5, and the ST of Figure
3. PRs between adjacent nodes are highlighted: $\mathord{\lessdot}$ is blue
and $\mathord{\mathbin{\doteq}}$ is green. A dashed red arrow connects each
node to its $\operatorname{Rc}$, if any.

As for the other way of the isomorphism, notice that we are considering only a
subset of UOTs. In fact, we only consider UOTs whose node labels are
compatible with a given OPM $M_{{\mathcal{P}(AP)}}$. In order to define the
notion of OPM compatibility for UOTs, we need to introduce the _right context_
($\operatorname{Rc}$) of a node. Given a UOT $T$ and a node $s\in T$, the
$\operatorname{Rc}$ of $s$ is denoted $\operatorname{Rc}(s)$. If $s$ has a
child $s^{\prime}$ such that $s\mathbin{\doteq}s^{\prime}$, then
$\operatorname{Rc}(s)$ is undefined. Otherwise, if $r$ is the leftmost right
sibling of $s$, then $\operatorname{Rc}(s)=r$; if $s$ has no right siblings,
then $\operatorname{Rc}(s)=\operatorname{Rc}(p)$, where $p$ is the parent of
$s$. In Figure 8, nodes are linked to their $\operatorname{Rc}$ by a dashed
red arrow.

In the following, for any nodes $s,s^{\prime}$ and
$\pi\in\\{\lessdot,\mathbin{\doteq},\gtrdot\\}$, we write
$s\mathrel{\pi}s^{\prime}$ meaning that $a\mathrel{\pi}b$, where
$a=\\{\mathrm{p}\mid s\in L(\mathrm{p})\\}$, and $b=\\{\mathrm{p}\mid
s^{\prime}\in L(\mathrm{p})\\}$. [OPM-compatible UOTs] We denote the set of
UOTs compatible with an OPM $M$ as $\mathcal{T}_{M}$. A UOT $T$ is in
$\mathcal{T}_{M}$ iff the following properties hold. The root node and its
rightmost child are the only ones labeled with $\\#$. For any node $s\in T$,
its rightmost child $r$, if any, is such that either $s\lessdot r$ or
$s\mathbin{\doteq}r$. For any other child $s^{\prime}\neq r$ of $s$, we have
$s\lessdot s^{\prime}$. If $\operatorname{Rc}(s)$ exists, then
$s\gtrdot\operatorname{Rc}(s)$.

Given a tree $T\in\mathcal{T}_{M}$ with labels on ${\mathcal{P}(AP)}$, it is
possible to build an OP word $w_{T}$ isomorphic to $T$. Indeed,

######  Lemma 3.

Given an OP word $w$ and the UOT $T_{w}=\tau(w)$, function $\tau$ is an
isomorphism between positions of $w$ and nodes of $T_{w}$.

######  Proof 4.1.

We define function $\tau^{-1}_{AP}:S\rightarrow{\mathcal{P}(AP)}^{+}$, which
maps a UOT node to the subword corresponding to the subtree rooted in it. For
any node $s\in T$, let its label $a=\\{\mathrm{p}\mid s\in L(\mathrm{p})\\}$,
and let $c_{0},c_{1}\dots c_{n}$ be its children, if any. $\tau^{-1}_{AP}(s)$
is defined as $\tau^{-1}_{AP}(s)=a$ if $s$ has no children, and
$\tau^{-1}_{AP}(s)=a\cdot\tau^{-1}_{AP}(c_{0})\cdot\tau^{-1}_{AP}(c_{1})\cdots\tau^{-1}_{AP}(c_{n})$
otherwise. We prove $\tau^{-1}_{AP}(s)$ is an OP word.

We need to prove by induction on the tree structure that for any tree node
$s$, $\tau^{-1}_{AP}(s)$ is of the form $a_{0}x_{0}a_{1}x_{1}\dots
a_{n}x_{n}$, with $n\geq 0$, and such that for $0\leq k<n$,
$a_{k}\mathbin{\doteq}a_{k+1}$ and either $x_{k}=\varepsilon$ or
${}^{a_{k}}[x_{k}]{}^{a_{k+1}}$. In the following, we denote as
$\operatorname{first}(x)$ the first position of a string $x$, and as
$\operatorname{last}(x)$ the last one. Indeed, for each $0\leq i<n$ we have
$a\lessdot\operatorname{first}(\tau^{-1}_{AP}(c_{i}))$, and the rightmost leaf
$f_{i}$ of the tree rooted in $c_{i}$ is such that
$\operatorname{Rc}(f_{i})=c_{i+1}$. Since
$f_{i}=\tau(\operatorname{last}(\tau^{-1}_{AP}(c_{i})))$ and
$c_{i+1}=\tau(\operatorname{first}(\tau^{-1}_{AP}(c_{i+1})))$, we have
$\operatorname{last}(\tau^{-1}_{AP}(c_{i}))\gtrdot\operatorname{first}(\tau^{-1}_{AP}(c_{i+1}))$.
So,
${}^{a}[\tau^{-1}_{AP}(c_{i})]{}^{\operatorname{first}(\tau^{-1}_{AP}(c_{i+1}))}$.
As for $\tau^{-1}_{AP}(c_{n})$, if $a\lessdot c_{n}$ then
$\tau^{-1}_{AP}(s)=a_{0}x_{0}$ (and
$a_{0}\lessdot\operatorname{first}(x_{0})$), with $a_{0}=a$ and
$x_{0}=\tau^{-1}_{AP}(c_{0})\cdot\tau^{-1}_{AP}(c_{1})\cdots\tau^{-1}_{AP}(c_{n})$.
If $a\mathbin{\doteq}c_{n}$, consider that, by hypothesis,
$\tau^{-1}_{AP}(c_{n})$ is of the form $a_{1}x_{1}a_{2}\dots a_{n}x_{n}$. So
$\tau^{-1}_{AP}(s)=a_{0}x_{0}a_{1}x_{1}a_{2}\dots a_{n}x_{n}$, with $a_{0}=a$
and
$x_{0}=\tau^{-1}_{AP}(c_{0})\cdot\tau^{-1}_{AP}(c_{1})\cdots\tau^{-1}_{AP}(c_{n-1})$.

The root $0$ of $T$ and its rightmost child $c_{\\#}$ are labeled with $\\#$.
So, $\tau^{-1}_{AP}(c_{\\#})=\\#$, and $\tau^{-1}_{AP}(0)=\\#x_{0}\\#$, with
${}^{\\#}[x_{0}]{}^{\\#}$, which is a finite OP word.

$\tau^{-1}:S\rightarrow U$ can be derived from $\tau^{-1}_{AP}$. By
construction, we have $\tau^{-1}(\tau(i))=i$ for any word $w$ and position
$i$.

From Lemma 3 follows:

######  Proposition 4.

Let $M_{AP}$ be an OPM on ${\mathcal{P}(AP)}$. For any FO formula $\varphi(x)$
on OP words compatible with $M_{AP}$, there exists a FO formula
$\varphi^{\prime}(x)$ on trees in $\mathcal{T}_{M_{AP}}$ such that for any OP
word $w$ and position $i$ in it, $w\models\varphi(i)$ iff
$T_{w}\models\varphi^{\prime}(\tau(i))$, with $T_{w}=\tau(w)$.

####  4.2.2. POTL Translation of $\mathcal{X}_{\mathit{until}}$

We now give the full translation of the logic $\mathcal{X}_{\mathit{until}}$
from [Mar04] into POTL.

The syntax of $\mathcal{X}_{\mathit{until}}$ formulas is
$\varphi::=\mathrm{a}\mid\top\mid\neg\varphi\mid\varphi\land\varphi\mid\rho(\varphi,\varphi),$
with $\mathrm{a}\in AP$ and
$\rho\in\\{\Downarrow,\Uparrow,\Rightarrow,\Leftarrow\\}$. The semantics of
propositional operators is the usual one, while $\rho(\varphi,\varphi)$ is an
until/since operator on the child and sibling relations. Let $T\in\mathcal{T}$
be a UOT with nodes in $S$. For any $r,s\in S$, $R_{\Uparrow}$ and
$R_{\Leftarrow}$ are s.t. $rR_{\Uparrow}s$ iff $sR_{\Downarrow}r$, and
$rR_{\Leftarrow}s$ iff $sR_{\Rightarrow}r$. We denote as $R_{\rho}^{+}$ the
transitive (but not reflexive) closure of relation $R_{\rho}$, and by
$R_{\rho}^{*}$ its transitive _and_ reflexive closure. For $s\in S$,
$(T,s)\models\rho(\varphi,\psi)$ iff there exists a node $t\in S$ s.t.
$sR_{\rho}^{+}t$ and $(T,t)\models\psi$, and for any $r\in S$ s.t.
$sR_{\rho}^{+}r$ and $rR_{\rho}^{+}t$ we have $(T,r)\models\varphi$. Notice
that $t\neq s$ and $r\neq s$, so $s$ is not included in the paths: we call
this semantics _strict_. Conversely, in POTL paths always start from the
position where an until/since operator is evaluated.

[LS10] proved the equivalence of $\mathcal{X}_{\mathit{until}}$ to the logic
Conditional XPath, which was proved equivalent to FOL on finite UOTs in
[Mar05]. This result is valid for any labeling of tree nodes, and so is on
OPM-compatible UOTs.

######  Theorem 5 ([Mar05, LS10]).

Let $M_{AP}$ be an OPM on $AP$. For any FO formula $\varphi(x)$ on trees in
$\mathcal{T}_{M_{AP}}$, there exists a $\mathcal{X}_{\mathit{until}}$ formula
$\varphi^{\prime}$ such that, for any $T\in\mathcal{T}_{M_{AP}}$ and node
$t\in T$, we have $T\models\varphi(t)$ iff $(T,t)\models\varphi^{\prime}$.

We define function $\iota_{\mathcal{X}}$, which translates any
$\mathcal{X}_{\mathit{until}}$ formula $\varphi$ into a POTL formula s.t.
$\varphi$ holds on a UOT $T$ iff $\iota_{\mathcal{X}}(\varphi)$ holds on the
isomorphic word $w_{T}$. $\iota_{\mathcal{X}}$ is defined as the identity for
the propositional operators, and with the equivalences below for the other
$\mathcal{X}_{\mathit{until}}$ operators. Recall from Section 3.4.1 that for
any $a\subseteq AP$, $\sigma_{a}:=\bigwedge_{\mathrm{p}\in
a}\mathrm{p}\land\bigwedge_{\mathrm{q}\not\in a}\neg\mathrm{q}$ holds in a
position $i$ iff $a$ is the set of atomic propositions holding in $i$. For any
POTL formula $\gamma$, let $\chi_{F}^{\lessdot}\gamma:=\bigvee_{a,b\subseteq
AP,\,a\lessdot b}(\sigma_{a}\land\chi_{F}^{d}(\sigma_{b}\land\gamma))$ be the
restriction of $\chi_{F}^{d}\gamma$ to chains with contexts in the $\lessdot$
PR; operators $\chi_{F}^{\mathbin{\doteq}}\gamma$,
$\chi_{P}^{\lessdot}\gamma$, $\chi_{P}^{\mathbin{\doteq}}\gamma$,
$\ocircle^{\lessdot}\gamma$, $\circleddash^{\lessdot}\gamma$ are defined
analogously.

For any $\mathcal{X}_{\mathit{until}}$ formulas $\varphi,\psi$, let
$\varphi^{\prime}=\iota_{\mathcal{X}}(\varphi)$ and
$\psi^{\prime}=\iota_{\mathcal{X}}(\psi)$. We define $\iota_{\mathcal{X}}$ as
follows:

$\displaystyle\iota_{\mathcal{X}}(\Downarrow(\varphi,\psi))$
$\displaystyle:=\ocircle^{d}({\varphi^{\prime}}\mathbin{\mathcal{U}_{\chi}^{d}}{\psi^{\prime}})\lor\chi_{F}^{d}({\varphi^{\prime}}\mathbin{\mathcal{U}_{\chi}^{d}}{\psi^{\prime}})$
(2) $\displaystyle\iota_{\mathcal{X}}(\Uparrow(\varphi,\psi))$
$\displaystyle:=\circleddash^{d}({\varphi^{\prime}}\mathbin{\mathcal{S}_{\chi}^{d}}{\psi^{\prime}})\lor\chi_{P}^{d}({\varphi^{\prime}}\mathbin{\mathcal{S}_{\chi}^{d}}{\psi^{\prime}})$
(3) $\displaystyle\iota_{\mathcal{X}}(\Rightarrow(\varphi,\psi)):=$
$\displaystyle\ocircle_{H}^{u}({\varphi^{\prime}}\mathbin{\mathcal{U}_{H}^{u}}{\psi^{\prime}})$
(4)
$\displaystyle\lor\big{(}\neg\ocircle_{H}^{u}({\top}\mathbin{\mathcal{U}_{H}^{u}}{\neg\varphi^{\prime}})\land\chi_{P}^{\lessdot}(\chi_{F}^{\mathbin{\doteq}}\psi^{\prime})\big{)}$
(5)
$\displaystyle\lor\circleddash^{\lessdot}\Big{(}\chi_{F}^{\lessdot}\big{(}\psi^{\prime}\land\neg\circleddash_{H}^{u}({\top}\mathbin{\mathcal{S}_{H}^{u}}{\neg\varphi^{\prime}})\big{)}\Big{)}$
(6)
$\displaystyle\lor\circleddash^{\lessdot}(\chi_{F}^{\mathbin{\doteq}}\psi^{\prime}\land\neg\chi_{F}^{\lessdot}\neg\varphi^{\prime})$
(7) $\displaystyle\iota_{\mathcal{X}}(\Leftarrow(\varphi,\psi)):=$
$\displaystyle\circleddash_{H}^{u}({\varphi^{\prime}}\mathbin{\mathcal{S}_{H}^{u}}{\psi^{\prime}})$
(8)
$\displaystyle\lor\chi_{P}^{\mathbin{\doteq}}\big{(}\chi_{F}^{\lessdot}(\neg\ocircle_{H}^{u}\top\land{\varphi^{\prime}}\mathbin{\mathcal{S}_{H}^{u}}{\psi^{\prime}})\big{)}$
(9)
$\displaystyle\lor\big{(}\chi_{P}^{\lessdot}(\ocircle^{\lessdot}\psi^{\prime})\land\neg\circleddash_{H}^{u}({\top}\mathbin{\mathcal{S}_{H}^{u}}{\neg\varphi^{\prime}})\big{)}$
(10)
$\displaystyle\lor\chi_{P}^{\mathbin{\doteq}}(\ocircle^{\lessdot}\psi^{\prime}\land\neg\chi_{F}^{\lessdot}\neg\varphi^{\prime})$
(11)

We prove the correctness of this translation in the following lemmas.

######  Lemma 6.

Given an OP alphabet $(AP,M_{AP})$, for every $\mathcal{X}_{\mathit{until}}$
formula $\Downarrow(\varphi,\psi)$, and for any OP word $w$ and position $i$
in $w$, we have

$(T_{w},\tau(i))\models\Downarrow(\varphi,\psi)\text{ iff
}(w,i)\models\iota_{\mathcal{X}}(\Downarrow(\varphi,\psi)).$

$T_{w}\in\mathcal{T}_{M_{AP}}$ is the UOT obtained by applying function $\tau$
to every position in $w$, such that for any position $i^{\prime}$ in $w$
$(T_{w},\tau(i^{\prime}))\models\varphi\text{ iff
}(w,i^{\prime})\models\iota_{\mathcal{X}}(\varphi)$, and likewise for $\psi$.

######  Proof 4.2.

Let $\varphi^{\prime}=\iota_{\mathcal{X}}(\varphi)$ and
$\psi^{\prime}=\iota_{\mathcal{X}}(\psi)$.

[Only if] Suppose $(T_{w},\tau(i))\models\Downarrow(\varphi,\psi)$. Let
$r=\tau(i)$, and $s=\tau(j)$ s.t. $rR_{\Downarrow}s$ and $s$ is the first tree
node of the path witnessing $\Downarrow(\varphi,\psi)$.

We inductively prove that
${\varphi^{\prime}}\mathbin{\mathcal{U}_{\chi}^{d}}{\psi^{\prime}}$ holds in
$j$. If $s$ is the last node of the path, then $\psi^{\prime}$ holds in $j$
and so does, trivially,
${\varphi^{\prime}}\mathbin{\mathcal{U}_{\chi}^{d}}{\psi^{\prime}}$.
Otherwise, consider any node $t=\tau(k)$ in the path, except the last one, and
suppose ${\varphi^{\prime}}\mathbin{\mathcal{U}_{\chi}^{d}}{\psi^{\prime}}$
holds in $k^{\prime}$ s.t. $t^{\prime}=\tau(k^{\prime})$ is the next node in
the path. If $t^{\prime}$ is the leftmost child of $t$, then $k^{\prime}=k+1$
and either $k\lessdot k^{\prime}$ or $k\mathbin{\doteq}k^{\prime}$: in both
cases
$\ocircle^{d}({\varphi^{\prime}}\mathbin{\mathcal{U}_{\chi}^{d}}{\psi^{\prime}})$
holds in $k$. If $t^{\prime}$ is not the leftmost child, then
$\chi(k,k^{\prime})$ and $k\lessdot k^{\prime}$ or
$k\mathbin{\doteq}k^{\prime}$: so
$\chi_{F}^{d}({\varphi^{\prime}}\mathbin{\mathcal{U}_{\chi}^{d}}{\psi^{\prime}})$
holds in $k$. Thus, by expansion law
${\varphi^{\prime}}\mathbin{\mathcal{U}_{\chi}^{d}}{\psi^{\prime}}\equiv\psi^{\prime}\lor(\varphi^{\prime}\land(\ocircle^{d}({\varphi^{\prime}}\mathbin{\mathcal{U}_{\chi}^{d}}{\psi^{\prime}})\lor\chi_{F}^{d}({\varphi^{\prime}}\mathbin{\mathcal{U}_{\chi}^{d}}{\psi^{\prime}})))$,
${\varphi^{\prime}}\mathbin{\mathcal{U}_{\chi}^{d}}{\psi^{\prime}}$ holds in
$k$ and, by induction, also in $j$.

Suppose $s$ is the leftmost child of $r$: $j=i+1$, and either $i\lessdot j$ or
$i\mathbin{\doteq}j$, so
$\ocircle^{d}({\varphi^{\prime}}\mathbin{\mathcal{U}_{\chi}^{d}}{\psi^{\prime}})$
holds in $i$. Otherwise, $\chi(i,j)$ and either $i\lessdot j$ or
$i\mathbin{\doteq}j$. In both cases,
$\chi_{F}^{d}({\varphi^{\prime}}\mathbin{\mathcal{U}_{\chi}^{d}}{\psi^{\prime}})$
holds in $i$.

[If] Suppose (2) holds in $i$. If
$\ocircle^{d}({\varphi^{\prime}}\mathbin{\mathcal{U}_{\chi}^{d}}{\psi^{\prime}})$
holds in $i$, then
${\varphi^{\prime}}\mathbin{\mathcal{U}_{\chi}^{d}}{\psi^{\prime}}$ holds in
$j=i+1$, and either $i\lessdot j$ or $i\mathbin{\doteq}j$: then $s=\tau(j)$ is
the leftmost child of $\tau(i)$. If
$\chi_{F}^{d}({\varphi^{\prime}}\mathbin{\mathcal{U}_{\chi}^{d}}{\psi^{\prime}})$
holds in $i$, then
${\varphi^{\prime}}\mathbin{\mathcal{U}_{\chi}^{d}}{\psi^{\prime}}$ holds in
$j$ s.t. $\chi(i,j)$ and $i\lessdot j$ or $i\mathbin{\doteq}j$: $s=\tau(j)$ is
a child of $\tau(i)$ in this case as well.

We prove that if
${\varphi^{\prime}}\mathbin{\mathcal{U}_{\chi}^{d}}{\psi^{\prime}}$ holds in a
position $j$ s.t. $\tau(i)R_{\Downarrow}\tau(j)$, then
$\Downarrow(\varphi,\psi)$ holds in $\tau(i)$. If
${\varphi^{\prime}}\mathbin{\mathcal{U}_{\chi}^{d}}{\psi^{\prime}}$ holds in
$j$, then there exists a DSP of minimal length from $j$ to $h>j$ s.t.
$(w,h)\models\psi^{\prime}$ and $\varphi^{\prime}$ holds in all positions
$j\leq k<h$ of the path, and $(T_{w},\tau(k))\models\varphi$. In any such $k$,
${\varphi^{\prime}}\mathbin{\mathcal{U}_{\chi}^{d}}{\psi^{\prime}}\equiv\psi^{\prime}\lor(\varphi^{\prime}\land(\ocircle^{d}({\varphi^{\prime}}\mathbin{\mathcal{U}_{\chi}^{d}}{\psi^{\prime}})\lor\chi_{F}^{d}({\varphi^{\prime}}\mathbin{\mathcal{U}_{\chi}^{d}}{\psi^{\prime}})))$
holds. Since this DSP is the minimal one, $\psi^{\prime}$ does not hold in
$k$. Either
$\ocircle^{d}({\varphi^{\prime}}\mathbin{\mathcal{U}_{\chi}^{d}}{\psi^{\prime}})$
or
$\chi_{F}^{d}({\varphi^{\prime}}\mathbin{\mathcal{U}_{\chi}^{d}}{\psi^{\prime}})$
hold in it. Therefore, the next position in the path is $k^{\prime}$ s.t.
either $k^{\prime}=k+1$ or $\chi(k,k^{\prime})$, and either $k\lessdot
k^{\prime}$ or $k\mathbin{\doteq}k^{\prime}$, and
$(w,k^{\prime})\models{\varphi^{\prime}}\mathbin{\mathcal{U}_{\chi}^{d}}{\psi^{\prime}}$.
Therefore, $\tau(k^{\prime})$ is a child of $\tau(k)$. So, there is a sequence
of nodes $s_{0},s_{1},\dots,s_{n}$ in $T_{w}$ s.t.
$\tau(i)R_{\Downarrow}s_{0}$, and $s_{i}R_{\Downarrow}s_{i+1}$ and
$(T_{w},s_{i})\models\varphi$ for $0\leq i<n$, and $(T_{w},s_{n})\models\psi$.
This is a path making $\Downarrow(\varphi,\psi)$ true in $\tau(i)$.

The proof for $\iota_{\mathcal{X}}(\Uparrow(\varphi,\psi))$ (3) is analogous
to Lemma 6, and is therefore omitted.

######  Lemma 7.

Given an OP alphabet $(AP,M_{AP})$, for every $\mathcal{X}_{\mathit{until}}$
formula $\Rightarrow(\varphi,\psi)$, and for any OP word $w$ and position $i$
in $w$, we have

$(T_{w},\tau(i))\models\Rightarrow(\varphi,\psi)\text{ iff
}(w,i)\models\iota_{\mathcal{X}}(\Rightarrow(\varphi,\psi)).$

$T_{w}\in\mathcal{T}_{M_{AP}}$ is the UOT obtained by applying function $\tau$
to every position in $w$, such that for any position $i^{\prime}$ in $w$
$(T_{w},\tau(i^{\prime}))\models\varphi\text{ iff
}(w,i^{\prime})\models\iota_{\mathcal{X}}(\varphi)$, and likewise for $\psi$.

######  Proof 4.3.

Let $\varphi^{\prime}=\iota_{\mathcal{X}}(\varphi)$ and
$\psi^{\prime}=\iota_{\mathcal{X}}(\psi)$.

[Only if] Suppose $\Rightarrow(\varphi,\psi)$ holds in $s=\tau(i)$. Then, node
$r=\tau(h)$ s.t. $rR_{\Downarrow}s$ has at least two children, and
$\Rightarrow(\varphi,\psi)$ is witnessed by a path starting in $t=\tau(j)$
s.t. $sR_{\Rightarrow}t$, and ending in $v=\tau(k)$. We have the following
cases:

  1. (1)

_$s$ is not the leftmost child of $r$._

    1. (a)

_$h\lessdot k$._ By the construction of $T_{w}$, for any node $t^{\prime}$ in
the path, there exists a position $j^{\prime}\in w$ s.t.
$t^{\prime}=\tau(j^{\prime})$, $\chi(h,j^{\prime})$ and $h\lessdot
j^{\prime}$. The path made by such positions is a UHP, and
${\varphi^{\prime}}\mathbin{\mathcal{U}_{H}^{u}}{\psi^{\prime}}$ is true in
$j$. Since $s$ is not the leftmost child of $r$, we have $\chi(h,i)$, and
$h\lessdot i$, so (4) holds in $i$.

    2. (b)

_$h\mathbin{\doteq}k$ , so $v$ is the rightmost child of $r$._ $\varphi$ holds
in all siblings between $s$ and $v$ (excluded), and $\varphi^{\prime}$ holds
in the corresponding positions of $w$. All such positions $j$, if any, are
s.t. $\chi(h,j)$ and $h\lessdot j$, and they form a UHP, so
$\ocircle_{H}^{u}({\top}\mathbin{\mathcal{U}_{H}^{u}}{\neg\varphi^{\prime}})$
never holds in $i$. Moreover, since $\psi$ holds in $v$, $\psi^{\prime}$ holds
in $k$. Note that $\chi_{P}^{\lessdot}$ in $i$ uniquely identifies position
$h$, and $\chi_{F}^{\mathbin{\doteq}}$ evaluated in $h$ identifies $k$. So,
(5) holds in $i$.

  2. (2)

_$s$ is the leftmost child of $r$._ In this case, we have $i=h+1$ and
$h\lessdot i$ (if $h\mathbin{\doteq}i$, then $r$ would have only one child).

    1. (a)

_$h\lessdot k$._ $\circleddash^{\lessdot}$ evaluated in $i$ identifies
position $h$. $\psi^{\prime}$ holds in $k$, and
$\circleddash_{H}^{u}({\top}\mathbin{\mathcal{S}_{H}^{u}}{\neg\varphi^{\prime}})$
does not, because in all positions between $i$ and $k$ (excluded)
corresponding to children of $r$, $\varphi^{\prime}$ holds. Note that all such
positions form a UHP, but $i$ is not part of it ($i=h+1$, so $\neg\chi(h,i)$),
and is not considered by
${\top}\mathbin{\mathcal{S}_{H}^{u}}{\neg\varphi^{\prime}}$. So, (6) holds in
$i$.

    2. (b)

_$h\mathbin{\doteq}k$ , so $v$ is the rightmost child of $r$._ $\psi$ holds in
$v$, and $\varphi$ holds in all children of $r$, except possibly the first
($s$) and the last one ($v$). These are exactly all positions s.t. $\chi(h,j)$
and $h\lessdot j$. Since $\varphi^{\prime}$ holds in all of them by
hypothesis, $\neg\chi_{F}^{\lessdot}\neg\varphi^{\prime}$ holds in $h$. Since
$\psi$ holds in $v$, $\psi^{\prime}$ holds in $k$, and
$\chi_{F}^{\mathbin{\doteq}}\psi^{\prime}$ in $h$. So, (7) holds in $i$.

[If] We separately consider cases (4)–(7).

(4):
$\ocircle_{H}^{u}({\varphi^{\prime}}\mathbin{\mathcal{U}_{H}^{u}}{\psi^{\prime}})$
holds in a position $i$ in $w$. Then, there exists a position $h$ s.t.
$\chi(h,i)$ and $h\lessdot i$, and a position $j$ s.t. $\chi(h,j)$ and
$h\lessdot j$ that is the hierarchical successor of $i$, and
${\varphi^{\prime}}\mathbin{\mathcal{U}_{H}^{u}}{\psi^{\prime}}$ holds in $j$.
So, $i$ and $j$ are consecutive children of $r=\tau(h)$. Moreover, there
exists a UHP between $j$ and a position $k\geq j$. The tree nodes
corresponding to all positions in the path are consecutive children of $r$, so
we fall in case 1a of the _only if_ part of the proof. In $T_{w}$, a path
between $t=\tau(j)$ and $v=\tau(k)$ witnesses the truth of
$\Rightarrow(\varphi,\psi)$ in $s$.

(5):
$\neg\ocircle_{H}^{u}({\top}\mathbin{\mathcal{U}_{H}^{u}}{\neg\varphi^{\prime}}\land\chi_{P}^{\lessdot}(\chi_{F}^{\mathbin{\doteq}}\psi^{\prime})$)
holds in position $i\in w$ (this corresponds to case 1b). If
$\chi_{P}^{\lessdot}(\chi_{F}^{\mathbin{\doteq}}\psi^{\prime})$ holds in $i$,
then there exists a position $h$ s.t. $\chi(h,i)$ and $h\lessdot i$, and a
position $k$ s.t. $\chi(h,k)$ and $h\mathbin{\doteq}k$, and $\psi^{\prime}$
holds in $k$. $v=\tau(k)$ is the rightmost child of $r=\tau(h)$, parent of
$s=\tau(i)$. Moreover, if
$\neg\ocircle_{H}^{u}({\top}\mathbin{\mathcal{U}_{H}^{u}}{\neg\varphi^{\prime}})$
holds in $i$, then either:

  * •

$\neg\ocircle_{H}^{u}\top$ holds, i.e. there is no position $j>i$ s.t.
$\chi(h,j)$ and $h\lessdot j$, so $v$ is the immediate right sibling of $s$.
In this case $\Rightarrow(\varphi,\psi)$ holds in $s$ because $\psi$ holds in
$v$.

  * •

$\neg({\top}\mathbin{\mathcal{U}_{H}^{u}}{\neg\varphi^{\prime}})$ holds in
$j>i$, the first position after $i$ s.t. $\chi(h,j)$ and $h\lessdot j$. This
means $\varphi^{\prime}$ holds in all positions $j^{\prime}\geq j$ s.t.
$\chi(h,j^{\prime})$ and $h\lessdot j^{\prime}$. Consequently, the tree nodes
corresponding to these positions plus $v=\tau(k)$ form a path witnessing
$\Rightarrow(\varphi,\psi)$, which holds in $s=\tau(i)$.

(6):
$\circleddash^{\lessdot}\Big{(}\chi_{F}^{\lessdot}\big{(}\psi^{\prime}\land\neg\circleddash_{H}^{u}({\top}\mathbin{\mathcal{S}_{H}^{u}}{\neg\varphi^{\prime}})\big{)}\Big{)}$
holds in $i$. Let $h=i-1$, with $h\lessdot i$ (it exists because
$\circleddash^{\lessdot}$ is true). There exists a position $k$, $\chi(h,k)$
and $h\lessdot k$, in which $\psi^{\prime}$ holds, so $\psi$ does in
$v=\tau(k)$, and
$\circleddash_{H}^{u}({\top}\mathbin{\mathcal{S}_{H}^{u}}{\neg\varphi^{\prime}})$
is false in it. If it is false because $\neg\circleddash_{H}^{u}\top$ holds,
there is no position $j<k$ s.t. $\chi(h,j)$ and $h\lessdot j$, so $v$ is the
second child of $r=\tau(h)$, $s=\tau(i)$ being the first one. So,
$\Rightarrow(\varphi,\psi)$ trivially holds in $s$ because $\psi$ holds in the
next sibling. Otherwise, let $j<k$ be the rightmost position lower than $k$
s.t. $\chi(h,j)$ and $h\lessdot j$.
$\neg({\top}\mathbin{\mathcal{S}_{H}^{u}}{\neg\varphi^{\prime}})$ holds in it,
so $\varphi^{\prime}$ holds in all positions $j^{\prime}$ between $i$ and $k$
that are part of the hierarchical path, i.e. s.t. $\chi(h,j^{\prime})$ and
$h\lessdot j^{\prime}$. The corresponding tree nodes form a path ending in
$v=\tau(k)$ that witnesses the truth of $\Rightarrow(\varphi,\psi)$ in $s$
(case 2a).

(7):
$\circleddash^{\lessdot}(\chi_{F}^{\mathbin{\doteq}}\psi^{\prime}\land\neg\chi_{F}^{\lessdot}\neg\varphi^{\prime})$
holds in $i$. Then let $h=i-1$, $h\lessdot i$, and $s=\tau(i)$ is the leftmost
child of $r=\tau(h)$. Since $\chi_{F}^{\mathbin{\doteq}}\psi^{\prime}$ holds
in $h$, there exists a position $k$, s.t. $\chi(h,k)$ and
$h\mathbin{\doteq}k$, in which $\psi^{\prime}$ holds. So, $\psi$ holds in
$v=\tau(k)$, which is the rightmost child of $r$, by construction. Moreover,
$\varphi^{\prime}$ holds in all positions s.t. $\chi(h,j)$ and $h\lessdot j$.
Hence, $\varphi$ holds in all corresponding nodes $t=\tau(j)$, which are all
nodes between $s$ and $v$, excluded. This, together with $\psi$ holding in
$v$, makes a path that verifies $\Rightarrow(\varphi,\psi)$ in $s$ (case 2b).

######  Lemma 8.