11institutetext: Politecnico di Milano, P.zza L. Da Vinci, 32, 20133 Milano,
Italy 11email<EMAIL_ADDRESS>22institutetext: IEIIT, Consiglio
Nazionale delle Ricerche

# POTL: A First-Order Complete Temporal Logic for Operator Precedence
Languages

Michele Chiari 11 Dino Mandrioli 11 Matteo Pradella 1122

###### 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, we introduced OPTL, based on the
class of Operator Precedence Languages (OPL), more powerful than Nested Words.
In this paper, we introduce the new OPL-based logic POTL, prove its FO-
completeness over finite words, and provide a model checking procedure for it.
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 by being FO-complete, and by
expressing more easily stack inspection and function-local properties.

###### Keywords:

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

##  1 Introduction

Model checking is one of the most successful techniques for the verification
of software programs. It consists in the exhaustive verification of the
mathematical model of a program against a specification of its desired
behavior. The kind of properties that can be proved in this way depends both
on the formalism employed to model the program, and on the one used to express
the specification. The initial and most classical frameworks consist in the
use of Finite State Automata (generally Büchi automata) for the model, and
temporal logics such as LTL, CTL and CTL* for the specification. The success
of such logics is due to their ease in reasoning about linear or branching
sequences of events over time, by expressing liveness and safety properties,
their conciseness with respect to automata, and the complexity of their model
checking.

From the point of view of formal language theory, these kinds of temporal
logics limit their set of expressible properties to the First-Order Logic
(FOL) definable fragment of regular languages. This is quite restrictive when
compared with the most popular abstract models of procedural programs, such as
Pushdown Systems, Boolean Programs [8], and Recursive State Machines [6]. All
such stack-based formalisms show behaviors which are expressible by means of
context-free languages, rather than regular. To expand the expressive power of
specification languages in the same direction, temporal logics based on
Visibly Pushdown Languages (VPL) [4] –a.k.a. Input-Driven Languages [28]– were
introduced. Such logics, namely CaRet [7] and the FO-complete NWTL, model the
execution trace of a procedural program as a Nested Word [5], consisting in a
linear ordering augmented with a one-to-one matching relation between function
calls and returns. This enables requirement specifications to include Hoare-
style pre/post-conditions, stack-inspection properties, and more.

VPL too have their limitations. In particular, they are a language class
slightly more general than Parenthesis Languages [27], which constrains the
matching relation they introduce to be exclusively one-to-one. This hinders
their suitability to model processes in which a single event must be put in
relation with multiple ones. Unfortunately, computer programs often present
such behaviors: exceptions, continuations, and context-switches in real-time
operating systems are single events that cause the termination (or re-
instantiation) of multiple functions on the stack. To be able to reason about
such behaviors, we propose the development of temporal logics based on
Operator Precedence Languages (OPL). OPL were initially introduced with the
purpose of efficient parsing [18], a field in which they continue to offer
useful applications [9]. They are capable of expressing arithmetic
expressions, and other constructs whose context-free structure is not
immediately visible. Indeed, the generality of the structure of their abstract
syntax trees is much greater than that of VPL, which are strictly included in
OPL [15]. Nevertheless, they retain the same closure properties that make
regular languages and VPL suitable for automata-theoretic model checking: OPL
are closed under Boolean operations, concatenation, Kleene *, and language
emptiness and inclusion are decidable [23]. Moreover, they have been
characterized by means of Monadic Second Order Logic.

The first step in this direction was the introduction of OPTL [14]. This
linear-time temporal logic, for which a model checking procedure has been
given on both finite and $\omega$-words, enables reasoning on procedural
programs with exceptions, expressing properties regarding the possibility of a
function to be terminated by and exception, or to throw one, under certain
conditions, or such as pre/post-conditions, which in the presence of
exceptions can be seen as Exception Safety [1], and also function-local
properties. In general, since NWTL can be translated into OPTL linearly, the
latter is capable of expressing all properties of NWTL, and many more.

One of the characterizing features of linear-time temporal logics is their
equivalence to FOL on their respective algebraic structure. This was the
reason for introducing NWTL, since it was not possible to deduce the position
of CaRet in this respect [2]. This is also our motivation for presenting
Precedence Oriented Temporal Logic (POTL). POTL redefines the semantics of
OPTL to be much closer to the “essence” of OPL, i.e. precedence relations. In
this paper, we prove the FO-completeness of POTL over finite Operator
Precedence (OP) words, and we conjecture the extensibility of this proof to
$\omega$-OP words by means of compositional arguments. The greater theoretical
expressive power benefits POTL also in practice: with it, it is easier to
express stack inspection properties in the presence of uncaught exceptions, as
well as certain kinds of function-frame local properties. We conjecture some
of such properties are not expressible at all in OPTL, although proving the
“strict containment” of OPTL in POTL seems to be arduous, as was that of CaRet
in NWTL. Nevertheless, the FO-completeness of POTL and the expressibility of
OPTL in FOL allow us to conclude that POTL is at least as expressive as OPTL.
We also give a tableaux-construction procedure for model checking POTL, which
yields automata of size at most singly exponential in formula length, and is
thus not asymptotically greater that that of LTL and NWTL.

Related Work. Model checking of regular properties against context-free
program models has been thoroughly studied [19, 16, 21, 17, 6, 11]. After some
early attempts at achieving higher expressive power [10, 22], a breakthrough
came with the introduction of VPL [4] and Nested Words [5], and the logics
based on them: CaRet [7], NWTL and others [2]. A $\mu$-calculus based on VPL
extends model checking to branching-time semantics in [3], while [13]
introduces a temporal logic capturing the whole class of VPL. Timed extensions
of CaRet are given in [12].

Organization. Background on OPL is given in Section 2. In Section 3 we present
the syntax and semantics of POTL, and show its use for expressing program
specifications by means of examples. In Section 4 we prove the FO-completeness
of POTL, and we describe its model checking procedure in Section 5. In Section
6 we conclude by delineating research steps subsequent to this work. Most
technical details and proofs are postponed to several appropriately referred
appendices.

##  2 Operator Precedence Languages

Operator Precedence Languages (OPL) are usually defined through their
generating grammars [18]; in this paper, however, we characterize them through
their accepting automata [23] which are the natural way to state equivalence
properties with logic characterization. We assume some familiarity with
classical language theory concepts such as context-free grammar, parsing,
shift-reduce algorithm, syntax tree [20].

Let $\Sigma=\\{a_{1},\dots,a_{n}\\}$ be an alphabet. The empty string is
denoted $\varepsilon$. We use a special symbol # not in $\Sigma$ to mark the
beginning and the end of any string. An operator precedence matrix (OPM) $M$
over an alphabet $\Sigma$ is a partial function
$(\Sigma\cup\\{\\#\\})^{2}\to\\{\lessdot,\allowbreak\doteq,\allowbreak\gtrdot\\}$,
that, for each ordered pair $(a,b)$, defines the _precedence relation_ (PR)
$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_. Relations $\lessdot,\doteq,\gtrdot$, are respectively named _yields
precedence, equal in precedence_ , and _takes precedence_. By convention, the
initial # can only yield precedence, and other symbols can only take
precedence on the ending #. If $M_{a,b}=\pi$, where
$\pi\in\\{\lessdot,\doteq,\gtrdot\\}$, we write $a\mathrel{\pi}b$. For
$u,v\in\Sigma^{+}$ we write $u\mathrel{\pi}v$ if $u=xa$ and $v=by$ with
$a\mathrel{\pi}b$.

###### Definition 1

An _operator precedence automaton (OPA)_ is a tuple
$\mathcal{A}=(\Sigma,M,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 three disjoint
relations:

$\delta_{\text{shift}}\subseteq Q\times\Sigma\times
Q,\quad\delta_{\text{push}}\subseteq Q\times\Sigma\times
Q,\quad\delta_{\text{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 the automaton, we need some new notations. We use
letters $p,q,p_{i},q_{i},\dots$ to denote states in $Q$. We will sometimes use
$q_{0}\stackrel{{\scriptstyle a}}{{\longrightarrow}}{q_{1}}$ for
$(q_{0},a,q_{1})\in\delta_{\text{shift}}\cup\delta_{\text{push}}$,
$q_{0}\stackrel{{\scriptstyle q_{2}}}{{\Longrightarrow}}{q_{1}}$ for
$(q_{0},q_{2},q_{1})\in\delta_{\text{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 let $\Gamma^{\prime}=\Gamma\cup\\{\bot\\}$ be the stack
alphabet; we denote symbols in $\Gamma^{\prime}$ as $[a,\ q]$ or $\bot$. We
set $\mathop{smb}([a,\ q])=a$, $\mathop{smb}(\bot)=\\#$, and $\mathop{st}([a,\
q])=q$. Given a stack content
$\gamma=\gamma_{n}\dots\gamma_{2}\gamma_{1}\bot$, with $\gamma_{i}\in\gamma$ ,
$n\geq 0$, we set $\mathop{smb}(\gamma)=\mathop{smb}(\gamma_{n})$ if $n\geq
1$, $\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_ of the automaton 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
symbol to read:

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_{\text{push}}$;

shift move: if $a\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_{\text{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_{\text{pop}}$.

Shift and pop moves are never performed when the stack contains only $\bot$.
Push and shift moves update the current state of the automaton according to
the transition relations $\delta_{\text{push}}$ and $\delta_{\text{shift}}$,
respectively: push moves put a new element on top of the stack consisting of
the input symbol together with the current state of the automaton, whereas
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 automaton according to $\delta_{\text{pop}}$ on the basis of the pair
of states consisting of the current state of the automaton and the state of
the removed stack symbol. They do not consume the input symbol, which is used
only to establish the $\gtrdot$ relation, remaining available for the next
move. The automaton 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\\}.$

###### Definition 2

A _simple chain_ is a string $c_{0}c_{1}c_{2}\dots c_{\ell}c_{\ell+1}$,
written as ${}^{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$ ($\ell\geq 1$), and $c_{0}\lessdot c_{1}\doteq
c_{2}\dots c_{\ell-1}\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 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}}$. The
pair made of the first and the last symbols of a chain is called its context.

$\begin{array}[]{r | c c c c}&\mathit{call}&\mathit{ret}&\mathit{han}&\mathit{thr}\\\ \hline\cr\mathit{call}&\lessdot&\doteq&\lessdot&\gtrdot\\\ \mathit{ret}&\gtrdot&\gtrdot&\lessdot&\gtrdot\\\ \mathit{han}&\lessdot&\gtrdot&\lessdot&\lessdot\\\ \mathit{thr}&\gtrdot&\gtrdot&\gtrdot&\gtrdot\\\ \end{array}$ |  $\\#[\mathit{call}[\mathit{han}[[[[\mathit{call}[\mathit{call}[\mathit{call}]]]\mathit{thr}]\mathit{thr}]\mathit{thr}]]\mathit{ret}]\\#$
---|---
Figure 1: OPM $M_{\mathit{call}}$ (left) and an example string with chains
shown by brackets (right).

A finite word $w$ over $\Sigma$ is _compatible_ with an OPM $M$ iff for each
pair of letters $c,d$, consecutive in $w$, $M_{cd}$ is defined and, for each
substring $x$ of $\\#w\\#$ which is a chain of the form ${}^{a}[y]^{b}$,
$M_{ab}$ is defined. E.g., the word $\mathit{call}\ \mathit{han}\
\mathit{call}\ \mathit{call}\ \mathit{call}\ \mathit{thr}\ \mathit{thr}\
\mathit{thr}\ \mathit{ret}$ of Fig. 1 is compatible with $M_{\mathit{call}}$.
In the same figure all the resulting chains are reported, e.g.
${}^{\mathit{call}}[\mathit{call}]{}^{\mathit{thr}}$,
${}^{\mathit{han}}[\mathit{thr}]{}^{\mathit{ret}}$ are simple chains, while
${}^{\mathit{han}}[[[[\mathit{call}[\mathit{call}[\mathit{call}]]]\mathit{thr}]\mathit{thr}]\mathit{thr}]{}^{\mathit{ret}}$,
${}^{\mathit{call}}[\mathit{call}[\mathit{call}]]{}^{\mathit{thr}}$ are
composed chains.

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}}{{\longrightarrow}}{}\dots\stackrel{{\scriptstyle}}{{\longrightarrow}}q_{\ell-1}\stackrel{{\scriptstyle
c_{\ell}}}{{\longrightarrow}}{q_{\ell}}\stackrel{{\scriptstyle
q_{0}}}{{\Longrightarrow}}{q_{\ell+1}}$, where the arrow labeled $c_{1}$
corresponds to a push move whereas the remaining ones denote shift moves. 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}}}{{\longrightarrow}}{}\dots\stackrel{{\scriptstyle
c_{\ell}}}{{\longrightarrow}}{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\epsilon$, 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 automaton over
$(\Sigma,M)$. If the automaton 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)$ $=$ $\langle\Sigma,M,$
$\\{q\\},\\{q\\},\\{q\\},\delta_{max}\rangle$ 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. Since there is
a chain ${}^{\\#}[s]{}^{\\#}$ for any string $s$ compatible with $M$, a string
is accepted by $\mathcal{A}(\Sigma,M)$ iff it is compatible with $M$. If $M$
is complete, each string is accepted by $A(\Sigma,M)$, which defines the
universal language $\Sigma^{*}$ by assigning to any string the (unique)
structure compatible with the OPM. With $M_{\mathit{call}}$ of Fig. 1, if we
take e.g. the string $\mathit{ret}\ \mathit{call}\ \mathit{han}$, it is
accepted by the max-automaton with structure
$\\#[[\mathit{ret}]\mathit{call}[\mathit{han}]]\\#.$

In conclusion, given an OP alphabet, the OPM $M$ assigns a structure to any
compatible string in $\Sigma^{*}$; unlike parentheses languages 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 strings compatible with $M$. For a
more complete description of the OPL family and of its relations with other
CFL we refer the reader to [24].

##  3 POTL: Syntax and Semantics

${\\#}$${\lessdot}$${\mathit{call}}$${\lessdot}$${\mathit{han}}$${\lessdot}$${\mathit{call}}$${\lessdot}$${\mathit{call}}$${\lessdot}$${\mathit{call}}$${\gtrdot}$${\mathit{thr}}$${\gtrdot}$${\mathit{thr}}$${\gtrdot}$${\mathit{thr}}$${\gtrdot}$${\mathit{ret}}$${\gtrdot}$${\\#}$${\mathrm{p}_{a}}$${\mathrm{p}_{b}}$${\mathrm{p}_{c}}$${\mathrm{p}_{d}}$${\mathrm{t}_{1}}$${\mathrm{t}_{2}}$${\mathrm{t}_{3}}$${\mathrm{p}_{a}}$${0}$${1}$${2}$${3}$${4}$${5}$${6}$${7}$${8}$${9}$${10}$
Figure 2: An example of execution trace, according to $M_{\mathit{call}}$
(Fig. 1). Chains are highlighted by arrows joining their context; structural
labels are typeset in bold, while other atomic propositions are shown below
them. 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}_{d}$) throws a sequence of exceptions, which are
all caught by the handler. Finally, $\mathrm{p}_{a}$ returns, uninstalling the
handler.

Given a finite set of atomic propositions $AP$, the syntax of POTL is defined
as follows:

$\displaystyle\varphi\equiv$
$\displaystyle\;\mathrm{a}\mid\neg\varphi\mid\varphi\lor\varphi\mid\ocircle^{\Pi}\varphi\mid\circleddash^{\Pi}\varphi\mid\chi_{F}^{\Pi}\varphi\mid\chi_{P}^{\Pi}\varphi\mid\varphi\mathbin{\mathcal{U}^{\Pi}}\varphi\mid\varphi\mathbin{\mathcal{S}^{\Pi}}\varphi$
$\displaystyle\mid\ocircle^{\mu}_{H}\varphi\mid\circleddash^{\mu}_{H}\varphi\mid\varphi\mathbin{\mathcal{U}^{\mu}_{H}}\varphi\mid\varphi\mathbin{\mathcal{S}^{\mu}_{H}}\varphi$

where $\mathrm{a}\in AP$, $\Pi$ is a non-empty subset of
$\\{\lessdot,\doteq,\gtrdot\\}$, and $\mu\in\\{\lessdot,\gtrdot\\}$.

We now informally illustrate its semantics by showing how it can be used to
express properties on program execution traces, such as the one of Fig. 2. In
the following, given two word positions $i$ and $j$ and a PR $\pi$, we write
$i\mathrel{\pi}j$ to say that the respective terminal symbols are in the $\pi$
relation. The _precedence_ next and back operators $\ocircle^{\Pi}$ and
$\circleddash^{\Pi}$ behave like their LTL counterparts, except they are true
only if the current (resp. preceding) position is in one of the PR in $\Pi$
with the next (resp. current) one. For example, with the OPM of Fig. 1, we can
write $\ocircle^{\lessdot\gtrdot}\mathit{call}$ to say that the next position
must be a call, and $\circleddash^{\doteq}\mathit{call}$ to say that the
current position is a return of an empty function frame. In Fig. 2, in pos. 2
$\ocircle^{\lessdot}\mathrm{p}_{b}$ holds, but
$\ocircle^{\doteq\gtrdot}\mathrm{p}_{b}$ does not.

The _chain_ next and back operators $\chi_{F}^{\Pi}$ and $\chi_{P}^{\Pi}$, are
similar to their precedence counterparts, except they jump between contexts of
the same chain, instead of moving along the linear successor relation.
$\chi_{F}^{\Pi}\psi$ is only true in left chain contexts, if $\psi$ holds in
one of the corresponding right contexts. There can be more than one of the
latter, but only those such that a relation in $\Pi$ holds among them are
considered. $\chi_{F}^{\doteq\gtrdot}\psi$ is true in a position $i$ if it is
the left context of a chain such that $\psi$ holds in its right context $j$,
and $i$ and $j$ are in the $\doteq$ or $\gtrdot$ relation. By the definition
of a composed chain ${}^{a}[x^{0}_{0}c^{0}_{0}x^{0}_{1}c^{0}_{1}\dots
c^{0}_{n}x^{0}_{n+1}]{}^{b}$, this only happens if $j$ is the right context of
the outermost chain starting in $i$, i.e. if $i$ is $c^{0}_{k}$ and $j$ is
$c^{0}_{k+1}$, for $0\leq k\leq n-1$, or $i$ is $c^{0}_{n}$ and $j$ is $b$.
Conversely, $\chi_{F}^{\lessdot}\psi$ considers the right contexts of the
inner chains starting in $i$. For example, if we have
${}^{a}[x^{0}_{0}=x^{1}_{0}c^{1}_{0}\dots]{}^{c^{0}_{0}}$,
${}^{a}[x^{1}_{0}=x^{2}_{0}c^{2}_{0}\dots]{}^{c^{1}_{0}}$, and so on,
$\chi_{F}^{\lessdot}\psi$ holds in $a$ iff $\psi$ holds in either of
$c^{0}_{0}$, $c^{1}_{0}$, $c^{2}_{0}$, and so on. So, in pos. 2 of Fig. 2,
$\chi_{F}^{\gtrdot}\mathrm{p}_{a}$ holds, meaning that the handler is
uninstalled by the return statement of procedure $\mathrm{p}_{a}$, and
$\chi_{F}^{\lessdot}\mathrm{t}_{1}$, meaning that it catches an exception of
type $\mathrm{t}_{1}$. Note that if $\Pi\subseteq\\{\doteq,\gtrdot\\}$, the
position considered by $\chi_{F}^{\Pi}$ is uniquely identified, while
$\chi_{F}^{\lessdot}$ existentially quantifies over (possibly) multiple
positions. The past operator $\chi_{P}^{\Pi}$ behaves symmetrically in this
respect, i.e. $\lessdot$ takes the part of $\gtrdot$ in uniquely identifying a
past position, the latter ranging over multiple ones.

The _summary_ until $\psi\mathbin{\mathcal{U}^{\Pi}}\theta$ (resp. since
$\psi\mathbin{\mathcal{S}^{\Pi}}\theta$) operator is obtained by inductively
applying the precedence and chain next (resp. back) operators. It holds in a
position in which either $\theta$ holds, or $\psi$ holds together with
$\ocircle^{\Pi}(\psi\mathbin{\mathcal{U}^{\Pi}}\theta)$ (resp.
$\circleddash^{\Pi}(\psi\mathbin{\mathcal{S}^{\Pi}}\theta)$) or
$\chi_{F}^{\Pi}(\psi\mathbin{\mathcal{U}^{\Pi}}\theta)$ (resp.
$\chi_{P}^{\Pi}(\psi\mathbin{\mathcal{S}^{\Pi}}\theta)$). In practice, it is
an until operator that considers paths that can move not only between
consecutive positions, but also between positions that are the contexts of a
chain, skipping the chain body between them. With the OPM of Fig. 1, this
means skipping function bodies. The relations in $\Pi$ constrain the movement
of such paths. With $\doteq$, they can move between positions in the same
simple chain body, i.e. between $c^{j}_{i}$, $c^{j}_{i+1}$, and so on. With
$\lessdot$, they go down in the nested chain structure, so they can move, for
example, from $a$ to $c^{0}_{0}$, $c^{1}_{0}$, and so on. With $\gtrdot$, they
go upwards, e.g. from $c^{0}_{n}$ to $b$. Formula
$\top\mathbin{\mathcal{U}^{\doteq\gtrdot}}\mathit{thr}$ is true in positions
contained in the frame of a function that is terminated by an exception. It is
true in pos. 3 of Fig. 2 because of path 3-6, and false in pos. 2, because no
path can enter the chain whose context are positions 2 and 9. Formula
$\top\mathbin{\mathcal{U}^{\lessdot\doteq}}\mathit{thr}$ is true in call
positions whose function frame contains throw statements, but that are not
directly terminated by one of them, such as the one in pos. 1.

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 _yield-precedence_ hierarchical
next (resp. back), $\ocircle^{\lessdot}_{H}\psi$ (resp.
$\circleddash^{\lessdot}_{H}\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 the right context of $i$,
with $i\lessdot j,j^{\prime}$. Thus, if $a$ is in pos. $i$, $j$ and
$j^{\prime}$ can be any $c^{k}_{0}$, $c^{k-1}_{0}$. So,
$\ocircle^{\lessdot}_{H}\mathrm{t}_{2}$ holds in pos. 6 of Fig. 2, and
$\circleddash^{\lessdot}_{H}\mathrm{t}_{1}$ in 7. The hierarchical until and
since operators are defined by iterating these next and back operators. Their
_take-precedence_ counterparts behave symmetrically, i.e. considering multiple
positions that are the left context of chains sharing their right context.

POTL’s formal semantics is based on the word structure $\langle
U,M_{\mathcal{P}(AP)},P\rangle$, where

  * •

$U=\\{0,1,\dots,n,n+1\\}$, with $n\in\mathbb{N}$ is a set of word positions;

  * •

$M_{\mathcal{P}(AP)}$ is an operator precedence matrix on ${\mathcal{P}(AP)}$;

  * •

$P\colon U\to{\mathcal{P}(AP)}$ is a function associating each word position
in $U$ with the set of atomic propositions that hold in that position, with
$P(0)=P(n+1)=\\{\\#\\}$.

For convenience, we consider a partitioning of AP into a set of normal
propositional labels (in round font), and _structural labels_ (SL, in
italics). The latter define the OP structure of the word:
$M_{\mathcal{P}(AP)}$ is only defined for subsets of $AP$ containing exactly
one SL, so that given two structural labels $\mathit{l}_{1},\mathit{l}_{2}$,
for any $a,a^{\prime},b,b^{\prime}\in{\mathcal{P}(AP)}$ s.t.
$\mathit{l}_{1}\in a,a^{\prime}$ and $\mathit{l}_{2}\in b,b^{\prime}$ we have
$M_{\mathcal{P}(AP)}(a,b)=M_{\mathcal{P}(AP)}(a^{\prime},b^{\prime})$. This
way, it is possible to define an OPM on the entire ${\mathcal{P}(AP)}$ by only
giving the relations between SL, as we did for $M_{\mathit{call}}$.

We define the chain relation $\chi\subseteq U\times U$ so that $\chi(i,j)$
holds between two positions $i<j-1$ if $i$ and $j$ form the context of a
chain. In case of composed chains, this relation is not one-to-one: there may
be positions where multiple chains start or end. Given $i,j\in U$, the chain
relation 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.

There exists at most one single position $h$ s.t. $\chi(h,j)$ and $h\lessdot
j$ or $h\doteq j$; for any $k$ s.t. $\chi(k,j)$ and $k\gtrdot j$ we have
$k>h$.

  4. 4.

There exists at most one single position $h$ s.t. $\chi(i,h)$ and $i\gtrdot h$
or $i\doteq h$; for any $k$ s.t. $\chi(i,k)$ and $i\lessdot k$ we have $k<h$.

The truth of POTL formulas is defined with respect to 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}$ if $\mathrm{a}\in P(i)$. Operators
such as $\land$ and $\neg$ have the usual semantics from propositional logic.

For the _precedence_ next and back operators, we have
$(w,i)\models\ocircle^{\Pi}\varphi$ iff $i\mathrel{\pi}(i+1)$ for some
$\pi\in\Pi$, and $(w,i+1)\models\varphi$.
$(w,i)\models\circleddash^{\Pi}\varphi$ iff $(i-1)\mathrel{\pi}i$ for some
$\pi\in\Pi$, and $(w,i-1)\models\varphi$.

For the _chain_ next and back operators, we have
$(w,i)\models\chi_{F}^{\Pi}\varphi$ iff there exists a position $j>i$ such
that $\chi(i,j)$, $i\mathrel{\pi}j$ for some $\pi\in\Pi$, and
$(w,j)\models\varphi$. $(w,i)\models\chi_{P}^{\Pi}\varphi$ iff there exists a
position $j<i$ such that $\chi(j,i)$, $j\mathrel{\pi}i$ for some $\pi\in\Pi$,
and $(w,j)\models\varphi$. In Fig. 2, $\chi_{F}^{\gtrdot}\mathit{thr}$ is true
in $\mathit{call}$ positions whose procedure is terminated by an exception
thrown by an inner procedure (e.g. pos. 3 and 4).
$\chi_{P}^{\gtrdot}\mathit{call}$ is true in $\mathit{thr}$ statements that
terminate at least one procedure, such as the one in pos. 6.
$\chi_{F}^{\doteq}\mathit{ret}$ is true in $\mathit{call}$ positions whose
procedure terminates normally, and not because of an uncaught exception.

The _hierarchical_ next/ back operators $\ocircle^{\mu}_{H}$ and
$\circleddash^{\mu}_{H}$, with $\mu\in\\{\lessdot,\gtrdot\\}$, move back and
forth between positions in the chain relation with the same one. They are
defined as:

  * •

$(w,i)\models\ocircle^{\lessdot}_{H}\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 j\\}$ and $(w,j)\models\varphi$;

  * •

$(w,i)\models\circleddash^{\lessdot}_{H}\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^{\gtrdot}_{H}\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^{\gtrdot}_{H}\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$.

For example, in pos. 3 $\ocircle^{\gtrdot}_{H}\mathrm{p}_{c}$ holds, because
both pos. 3 and 4 are in the chain relation with 6. Similarly, in pos. 4
$\circleddash^{\gtrdot}_{H}\mathrm{p}_{b}$ holds. In pos. 7, both
$\circleddash^{\lessdot}_{H}\mathrm{t}_{1}$ and
$\ocircle^{\lessdot}_{H}\mathrm{t}_{3}$ hold.

POTL has different kinds of until and since operators. They express properties
on paths, which are sequences of positions obtained by iterating the different
kinds of next and 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$. The _since_ operator is defined symmetrically.
Note that, depending on the set $\Gamma$, a path from $i$ to $j$ may not
exist. We define all kinds of until/since operators by associating them with
different sets of paths.

Summary Operators. We define _Operator Precedence Summary Paths_ (OPSP) as
follows. Given an OP word $w$, a non-empty set
$\Pi\subseteq\\{\lessdot,\doteq,\gtrdot\\}$, and two positions $i\leq j$ in
$w$, the OPSP 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{iff $k=\max\\{h\mid h\leq
j\land\chi(i_{p},h)\land\bigvee_{\pi\in\Pi}i\mathrel{\pi}k\\}$;}\\\
i_{p}+1&\text{if
$\bigvee_{\pi\in\Pi}i_{p}\mathrel{\pi}(i_{p}+1)$.}\end{cases}$

The Operator Precedence Summary (OPS) until and since operators
$\mathbin{\mathcal{U}^{\Pi}}$ and $\mathbin{\mathcal{S}^{\Pi}}$ are based on
the set of OPSP starting in the position in which they are evaluated. In Fig.
2,
$(\mathit{han}\lor\mathit{thr})\mathbin{\mathcal{U}^{\lessdot}}\mathrm{t}_{2}$
holds in pos. 2 because of path 2-7.
$\mathit{thr}\mathbin{\mathcal{S}^{\gtrdot}}\mathrm{p}_{c}$ holds in pos. 7
because of path 4-6-7. Moreover, we define two kinds of _hierarchical_ paths.

Yield-Precedence. The yield-precedence hierarchical path (YPHP) 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 $i\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 yield-precedence hierarchical paths
starting in the position in which they are evaluated are denoted as
$\mathbin{\mathcal{U}^{\lessdot}_{H}}$ and
$\mathbin{\mathcal{S}^{\lessdot}_{H}}$. E.g.,
$\mathit{thr}\mathbin{\mathcal{U}^{\lessdot}_{H}}\mathrm{t}_{3}$ holds in pos.
6 because of path 6-7-8. Similarly,
$\mathit{thr}\mathbin{\mathcal{S}^{\lessdot}_{H}}\mathrm{t}_{1}$ holds in pos.
8 and is witnessed by the same path.

Take-Precedence. The take-precedence hierarchical path (TPHP) 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 take-precedence hierarchical paths starting in
the position in which they are evaluated are denoted as
$\mathbin{\mathcal{U}^{\gtrdot}_{H}}$ and
$\mathbin{\mathcal{S}^{\gtrdot}_{H}}$. In Fig. 2,
$\mathit{call}\mathbin{\mathcal{U}^{\gtrdot}_{H}}\mathrm{p}_{c}$ holds in pos.
3, and $\mathit{call}\mathbin{\mathcal{S}^{\gtrdot}_{H}}\mathrm{p}_{b}$ in
pos. 4, both because of path 3-4.

The above operators enjoy the following expansion laws, proved in Appendix
0.A.

$\displaystyle\varphi\mathbin{\mathcal{U}^{\Pi}}\psi$
$\displaystyle\equiv\psi\lor\Big{(}\varphi\land\big{(}\ocircle^{\Pi}(\varphi\mathbin{\mathcal{U}^{\Pi}}\psi)\lor\chi_{F}^{\Pi}(\varphi\mathbin{\mathcal{U}^{\Pi}}\psi)\big{)}\Big{)}$
(1) $\displaystyle\varphi\mathbin{\mathcal{S}^{\Pi}}\psi$
$\displaystyle\equiv\psi\lor\Big{(}\varphi\land\big{(}\circleddash^{\Pi}(\varphi\mathbin{\mathcal{S}^{\Pi}}\psi)\lor\chi_{P}^{\Pi}(\varphi\mathbin{\mathcal{S}^{\Pi}}\psi)\big{)}\Big{)}$
(2) $\displaystyle\varphi\mathbin{\mathcal{U}^{\lessdot}_{H}}\psi$
$\displaystyle\equiv(\psi\land\chi_{P}^{\lessdot}\top)\lor\big{(}\varphi\land\ocircle^{\lessdot}_{H}(\varphi\mathbin{\mathcal{U}^{\lessdot}_{H}}\psi)\big{)}$
(3) $\displaystyle\varphi\mathbin{\mathcal{S}^{\lessdot}_{H}}\psi$
$\displaystyle\equiv(\psi\land\chi_{P}^{\lessdot}\top)\lor\big{(}\varphi\land\circleddash^{\lessdot}_{H}(\varphi\mathbin{\mathcal{S}^{\lessdot}_{H}}\psi)\big{)}$
(4) $\displaystyle\varphi\mathbin{\mathcal{U}^{\gtrdot}_{H}}\psi$
$\displaystyle\equiv(\psi\land\chi_{F}^{\gtrdot}\top)\lor\big{(}\varphi\land\ocircle^{\gtrdot}_{H}(\varphi\mathbin{\mathcal{U}^{\gtrdot}_{H}}\psi)\big{)}$
(5) $\displaystyle\varphi\mathbin{\mathcal{S}^{\gtrdot}_{H}}\psi$
$\displaystyle\equiv(\psi\land\chi_{F}^{\gtrdot}\top)\lor\big{(}\varphi\land\circleddash^{\gtrdot}_{H}(\varphi\mathbin{\mathcal{S}^{\gtrdot}_{H}}\psi)\big{)}$
(6)

POTL can express all stack-trace related properties of OPTL. As we mentioned
in the introduction, and formalize in Corollary 2 and Appendix 0.C.3, OPTL
$\subseteq$ POTL. E.g.,
$\square[\mathit{han}\Rightarrow\chi_{F}^{\gtrdot}\mathit{ret}]$, where
$\square\psi$ is a shortcut for
$\neg(\top\mathbin{\mathcal{U}^{\lessdot\doteq\gtrdot}}\neg\psi)$, holds if
all exception handlers are properly uninstalled by a return statement. Formula
$\square[\mathit{thr}\Rightarrow\neg\chi_{P}^{\gtrdot}\mathrm{p}_{b}]$ is
false if $\mathrm{p}_{b}$ is terminated by an exception. Formula
$\neg\chi_{F}^{\lessdot}(\mathit{thr}\land\chi_{P}^{\gtrdot}\mathit{call})$ is
true in $\mathit{handles}$ that do not catch any $\mathit{thr}$ statement that
terminates a procedure. We give a few more examples:

$\displaystyle\square[\mathit{call}\land\mathrm{p}_{A}\implies\neg\ocircle^{\gtrdot}\mathit{thr}\land\neg\chi_{F}^{\gtrdot}\mathit{thr}]$
(7)
$\displaystyle\square[\mathit{call}\land\rho\land(\ocircle^{\gtrdot}\mathit{thr}\lor\chi_{F}^{\gtrdot}\mathit{thr})\implies\ocircle^{\gtrdot}\theta\lor\chi_{F}^{\gtrdot}\theta]$
(8)
$\displaystyle\square[\mathit{call}\land\mathrm{p}_{A}\land(\neg\mathit{ret}\mathbin{\mathcal{U}^{\lessdot\doteq}}\mathrm{wr}_{x})\implies\chi_{F}^{\gtrdot}\mathit{thr}]$
(9)
$\displaystyle\square\big{[}\big{(}\mathrm{p}_{C}\land(\ocircle^{\gtrdot}\mathit{thr}\lor\chi_{F}^{\gtrdot}\mathit{thr})\big{)}\implies\neg\mathrm{p}_{A}\mathbin{\mathcal{S}^{\gtrdot}_{H}}\mathrm{p}_{B}\big{]}$
(10)
$\displaystyle\square\Big{[}\Big{(}\mathit{call}\land\mathrm{p}_{B}\land\neg\big{(}\top\mathbin{\mathcal{S}^{\lessdot}}(\mathrm{p}_{A}\land\mathit{call})\big{)}\Big{)}\implies\top\mathbin{\mathcal{U}^{\lessdot}}(\ocircle^{\gtrdot}\mathit{thr}\lor\chi_{F}^{\gtrdot}\mathit{thr})\Big{]}$
(11)

(7) means procedure $\mathrm{p}_{A}$ is never interrupted by an uncaught
exception. (8) means that if precondition $\rho$ holds when a procedure is
called, then postcondition $\theta$ must hold if that procedure is terminated
by an exception. If $\theta$ is a class invariant asserting that a class
instance is in a valid state, this formula expresses _weak_ exception safety
[1]. If $\rho\equiv\theta$ is a formula expressing a particular state of the
class instance, this formula expresses _strong_ exception safety. (9) means if
a procedure $\mathrm{p}_{A}$ or its subprocedures write to a variable $x$,
they are terminated by an exception. It can be used to check enforcement of
data access permissions. (10) means that whenever the stack frame of a
procedure $\mathrm{p}_{C}$ is unwinded by an uncaught exception,
$\mathrm{p}_{B}$ is present in the backtrace, and it is also unwinded.
Moreover, the frame of $\mathrm{p}_{A}$ cannot be unwinded before the one of
$\mathrm{p}_{B}$. Unlike previous properties, we conjecture this one cannot be
expressed in OPTL. (11) means whenever $\mathrm{p}_{B}$ is executed, at least
one instance of $\mathrm{p}_{A}$ must be on stack, otherwise $\mathrm{p}_{B}$
or a subfunction throw an exception.

##  4 First-Order Completeness

To obtain FO-completeness for POTL, we give a translation of Conditional XPath
(CXPath) [25], a logic on trees, into POTL on OP words. A translation into FOL
is given in Appendix 0.B. From CXPath being equivalent to FOL on trees [26],
we derive a FO-completeness result for POTL. To do so, we give an isomorphism
between OP words and (a subset of) unranked ordered trees, the algebraic
structures on which CXPath is based. First, we show how to translate OP words
into trees, and then the reverse.

An unranked ordered tree 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}$). Finally, $L:S\rightarrow{\mathcal{P}(AP)}$ is a function
that maps each node to its label, i.e. the set of atomic propositions holding
in it. We denote as $\mathcal{T}$ the set of all unranked ordered trees.

|
---|---
Figure 3: The unranked ordered tree corresponding to the word of Fig. 2 (left)
and the corresponding abstract syntax tree (right). PR are highlighted. Dashed
arrows point to the Rcc of each node, decorated with $\lessdot$ when they
represent actual right contexts.

Given an OP word $w=\langle U,M_{{\mathcal{P}(AP)}},P\rangle$, it is possible
to build an unranked ordered tree $T_{w}=\langle
S_{w},R_{\Downarrow},R_{\Rightarrow},L_{w}\rangle\in\mathcal{T}$ with labels
in ${\mathcal{P}(AP)}$ isomorphic to $w$. To do so, we define a translation
function $\tau:U\rightarrow S_{w}$, which maps positions of $w$ into nodes of
$T_{w}$.

  * •

$\tau(0)=0$: position 0 is the root node.

  * •

Given any position $i\in U$, if $i\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$).

  * •

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\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 $\doteq$ relation.
Note that this way, every position $i$ in $w$ appears in the tree exactly
once. Indeed, if the position preceding $i$ is in the $\doteq$ or $\lessdot$
relation with it, then $i$ is one of its children. If $(i-1)\gtrdot i$, then
at least a chain ends in $i$. In particular, consider position $j$ s.t.
$\chi(j,i)$, and for no $j^{\prime}<j$ we have $\chi(j^{\prime},i)$:
necessarily either $j\doteq i$ or $j\lessdot i$, or $i$ would be the right
context of another chain whose body contains $j$. So, $i$ is a child of $j$.
Finally, $L_{w}(\tau(i))=P(i)$, 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 tree obtained by applying $\tau$ to every
position of an OP word $w$. Fig. 3 shows the translation of the word of Fig. 2
into an unranked ordered tree.

As for the other way of the isomorphism, notice that we are considering only a
subset of unranked ordered trees. In fact, we only consider trees whose node
labels are compatible with a given OPM $M_{{\mathcal{P}(AP)}}$. In order to
define the notion of OPM compatibility for trees, we need to introduce the
_right context candidate_ (Rcc) of a node. Given a tree $T$ and a node $s\in
T$, the Rcc of $s$ is denoted $\operatorname{Rcc}(s)$. If $r$ is the leftmost
right sibling of $s$, then $\operatorname{Rcc}(s)=r$. Otherwise,
$\operatorname{Rcc}(s)=\operatorname{Rcc}(p)$, where $p$ is the parent of $s$.

We denote the set of trees compatible with an OPM $M$ as $\mathcal{T}_{M}$. A
tree $T$ is in $\mathcal{T}_{M}$ iff the following properties hold. The root
node is labeled with $\\#$, and it has at most two children, the rightmost one
being labeled with $\\#$. No other node is labeled with $\\#$. In the
following we write $s\mathrel{\pi}s^{\prime}$ meaning that
$L(s)\mathrel{\pi}L(s^{\prime})$, for any $s,s^{\prime}\in S$ and
$\pi\in\\{\lessdot,\doteq,\gtrdot\\}$. For any node $s\in T$, let $r\in T$ be
the rightmost child of $s$. Then either $s\lessdot r$ or $s\doteq r$. For any
child $s^{\prime}\in T$ of $s$ s.t. $s^{\prime}$ is a (left) sibling of $r$,
we have $s\lessdot s^{\prime}$. If $s$ has no child $s^{\prime}$ such that
$s\doteq s^{\prime}$, then $s\gtrdot\operatorname{Rcc}(s)$, if the latter
exists. Note that $\operatorname{Rcc}(s)$ always exists for all nodes not
labeled with $\\#$, because the root always has a second child.

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$. We define function
$\tau^{-1}_{AP}:S\rightarrow{\mathcal{P}(AP)}^{+}$, which maps a tree node to
the substring corresponding to the subtree rooted in it. For any node $s\in
T$, let $a=L(s)$ be its label, and let $c_{0},c_{1}\dots c_{n}$ be its
children, if any. Then $\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.

The string obtained in this way is a valid OP word. To show this, we need to
prove by induction 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}\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{Rcc}(f_{i})=c_{i+1}$, and
$\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\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 of $T$ is labeled with $\\#$, and its first child has the form
$a_{0}x_{0}a_{1}x_{1}\dots a_{n}x_{n}$ as described above. The second child
$c_{\\#}$ of the root is labeled with $\\#$. Consider the tree node
corresponding to $\operatorname{first}(x_{n})$: its rightmost leaf $f$ is such
that $\operatorname{Rcc}(f)=c_{\\#}$, and
$\operatorname{last}(x_{n})\gtrdot\\#$. So $\\#a_{0}x_{0}a_{1}x_{1}\dots
a_{n}x_{n}\\#$ is a finite OP word.

Function $\tau^{-1}:S\rightarrow U$ can be derived from $\tau^{-1}_{AP}$. From
the existence of $\tau^{-1}$ follows

###### Lemma 1

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

Consequently,

###### Proposition 1

Let $M_{\mathcal{P}(AP)}$ be an OPM on ${\mathcal{P}(AP)}$. For any FO formula
$\varphi(x)$ on OP words compatible with $M_{\mathcal{P}(AP)}$, there exists a
FO formula $\varphi^{\prime}(x)$ on trees in
$\mathcal{T}_{M_{\mathcal{P}(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)$.

We now give the full translation of the logic $\mathcal{X}_{\mathit{until}}$
from [25] into POTL. The syntax of $\mathcal{X}_{\mathit{until}}$ formulas is

$\varphi\equiv\mathrm{p}\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 a
strict until/since operator on the child and sibling relations. Let
$T\in\mathcal{T}$ be a tree with nodes in $S$. For any $r,s\in S$, let
$R_{\Uparrow},R_{\Leftarrow}$ be 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}$. 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$.
$\mathcal{X}_{\mathit{until}}$ was proved to be equivalent to FOL on finite
unranked ordered trees in [26]. This result is valid for any labeling of tree
nodes, and so is on OPM-compatible trees as well.

###### Theorem 4.1

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

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 tree $T$ iff $\iota_{\mathcal{X}}(\varphi)$ holds on the
isomorphic word $w_{T}$. For the purely propositional operators,
$\iota_{\mathcal{X}}$ is defined as the identity. Otherwise,
$\iota_{\mathcal{X}}$ is defined by means of the following equivalences.

$\displaystyle\iota_{\mathcal{X}}(\Downarrow(\varphi,\psi))$
$\displaystyle\equiv\ocircle^{\lessdot\doteq}(\varphi^{\prime}\mathbin{\mathcal{U}^{\lessdot\doteq}}\psi^{\prime})\lor\chi_{F}^{\lessdot\doteq}(\varphi^{\prime}\mathbin{\mathcal{U}^{\lessdot\doteq}}\psi^{\prime})$
(12) $\displaystyle\iota_{\mathcal{X}}(\Uparrow(\varphi,\psi))$
$\displaystyle\equiv\circleddash^{\lessdot\doteq}(\varphi^{\prime}\mathbin{\mathcal{S}^{\lessdot\doteq}}\psi^{\prime})\lor\chi_{P}^{\lessdot\doteq}(\varphi^{\prime}\mathbin{\mathcal{S}^{\lessdot\doteq}}\psi^{\prime})$
(13) $\displaystyle\iota_{\mathcal{X}}(\Rightarrow(\varphi,\psi))\equiv$
$\displaystyle\ocircle^{\lessdot}_{H}(\varphi^{\prime}\mathbin{\mathcal{U}^{\lessdot}_{H}}\psi^{\prime})$
(14)
$\displaystyle\lor\big{(}\neg\ocircle^{\lessdot}_{H}(\top\mathbin{\mathcal{U}^{\lessdot}_{H}}\neg\varphi^{\prime})\land\chi_{P}^{\lessdot}(\chi_{F}^{\doteq}\psi^{\prime})\big{)}$
(15)
$\displaystyle\lor\circleddash^{\lessdot}\Big{(}\chi_{F}^{\lessdot}\big{(}\psi^{\prime}\land\neg\circleddash^{\lessdot}_{H}(\top\mathbin{\mathcal{S}^{\lessdot}_{H}}\neg\varphi^{\prime})\big{)}\Big{)}$
(16)
$\displaystyle\lor\circleddash^{\lessdot}(\chi_{F}^{\doteq}\psi^{\prime}\land\neg\chi_{F}^{\lessdot}\neg\varphi^{\prime})$
(17) $\displaystyle\iota_{\mathcal{X}}(\Leftarrow(\varphi,\psi))\equiv$
$\displaystyle\circleddash^{\lessdot}_{H}(\varphi^{\prime}\mathbin{\mathcal{S}^{\lessdot}_{H}}\psi^{\prime})$
(18)
$\displaystyle\lor\chi_{P}^{\doteq}\big{(}\chi_{F}^{\lessdot}(\neg\ocircle^{\lessdot}_{H}\top\land\varphi^{\prime}\mathbin{\mathcal{S}^{\lessdot}_{H}}\psi^{\prime})\big{)}$
(19)
$\displaystyle\lor\big{(}\chi_{P}^{\lessdot}(\ocircle^{\lessdot}\psi^{\prime})\land\neg\circleddash^{\lessdot}_{H}(\top\mathbin{\mathcal{S}^{\lessdot}_{H}}\neg\varphi^{\prime})\big{)}$
(20)
$\displaystyle\lor\chi_{P}^{\doteq}(\ocircle^{\lessdot}\psi^{\prime}\land\neg\chi_{F}^{\lessdot}\neg\varphi^{\prime})$
(21)

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

###### Lemma 2

Given a set of atomic propositions $AP$, and OPM $M_{\mathcal{P}(AP)}$, let
$\varphi$ be a $\mathcal{X}_{\mathit{until}}$ formula, $s$ be a node of
$T\in\mathcal{T}_{M_{\mathcal{P}(AP)}}$, an OPM-compatible tree, and $w_{T}$
be the OP word obtained by applying function $\tau^{-1}$ to every node of $T$.
Then we have

$(T,s)\models\varphi\iff(w_{T},\tau^{-1}(s))\models\iota_{\mathcal{X}}(\varphi).$

###### Proof

_(Sketch)_ We sketch the proof of equivalences (12) and (14)-(17), the others
being analogous. The full proofs are in Appendix 0.C.2. For
$\Downarrow(\varphi,\psi)$, we need an until operator spanning paths in which
two consecutive nodes are resp. parent and child. Two nodes $r,s$ are s.t.
$rR_{\Downarrow}s$ in a tree $T_{w}$ iff, in the corresponding word $w$,
$h=\tau^{-1}(r)$ and $k=\tau^{-1}(s)$ are s.t. either $k=h+1$ or $\chi(h,k)$
and $h\lessdot k$ or $h\doteq k$. So,
$\varphi^{\prime}\mathbin{\mathcal{U}^{\lessdot\doteq}}\psi^{\prime}$ is the
appropriate translation. It must be preceded by $\ocircle^{\lessdot\doteq}$
and $\chi_{F}^{\lessdot\doteq}$ due to the strict semantics of
$\mathcal{X}_{\mathit{until}}$, in which paths do not start from the current
node, but from its immediate children.

$\Rightarrow(\varphi,\psi)$ is an until on children of a node. It holds on a
tree node $s=\tau(i)$ iff it is satisfied by a path starting in the first
sibling after $s$ and ending in $t=\tau(j)$ s.t. $sR_{\Rightarrow}^{+}t$. This
is captured by the disjunction of four cases in the corresponding word $w$.
Let $r=\tau(h)$ be the parent of $s$, and $p=\tau(m)$ and $q=\tau(n)$ be the
left- and rightmost children of $r$.

  * •

(14): $s\neq p$ and $r\lessdot t$. Then, all positions $j^{\prime}$ in $w$
corresponding to nodes in the path are s.t. $\chi(h,j^{\prime})$ and
$h\lessdot j^{\prime}$, so formula (14) is a valid translation.

  * •

(15): $s\neq p$, $t=q$ and $s\doteq q$. In $w$, $\varphi^{\prime}$ must hold
in all positions $j^{\prime}>i$ s.t. $\chi(h,j^{\prime})$ and $h\lessdot
j^{\prime}$, and this is captured by
$\neg\ocircle^{\lessdot}_{H}(\top\mathbin{\mathcal{U}^{\lessdot}_{H}}\neg\varphi^{\prime})$.
Moreover, $\psi^{\prime}$ holds in $n$, the only position s.t. $\chi(h,n)$ and
$h\doteq n$, which is equivalent to
$\chi_{P}^{\lessdot}(\chi_{F}^{\doteq}\psi^{\prime})$ holding in $i$.

  * •

(16): $s=p$ and $r\lessdot t$. In $w$, $i=h+1$, so if
$\circleddash^{\lessdot}$ is evaluated in $i$, its argument holds in $h$. The
first sibling node after $s$ corresponds in $w$ to $m^{\prime}$, the leftmost
position s.t. $\chi(h,m^{\prime})$ and $h\lessdot m^{\prime}$. If $n$ is s.t.
$\chi(h,n)$ and $h\doteq n$, the path starting from $m^{\prime}$ ends before
$n$. So, there exists a position $j^{\prime}$ s.t. $\chi(h,j^{\prime})$,
$h\lessdot j^{\prime}$ in which $\psi^{\prime}$ holds, while
$\varphi^{\prime}$ holds in all positions $j^{\prime\prime}$ s.t.
$m^{\prime}\leq j^{\prime\prime}<j^{\prime}$, $\chi(h,j^{\prime\prime})$ and
$h\lessdot j^{\prime\prime}$. So
$\chi_{F}^{\lessdot}\big{(}\psi^{\prime}\land\neg\circleddash^{\lessdot}_{H}(\top\mathbin{\mathcal{S}^{\lessdot}_{H}}\neg\varphi^{\prime})\big{)}$
must hold in $h$.

  * •

(17): $s=p$, $t=q$ and $s\doteq q$. In this case, $\varphi^{\prime}$ holds in
all positions $j^{\prime}$ s.t. $\chi(h,j^{\prime})$ and $h\lessdot
j^{\prime}$, while $\psi^{\prime}$ holds in position $n$ s.t. $\chi(h,n)$ and
$h\doteq n$. This is equivalent to
$\chi_{F}^{\doteq}\psi^{\prime}\land\neg\chi_{F}^{\lessdot}\neg\varphi^{\prime}$
holding in $h$.

It is possible to express all POTL operators in FOL, by following the
semantics described in Section 3. The translation of OPS until/since operators
is similar to the one employed for NWTL in [2]. The full translation can be
found in Appendix 0.B. From this, and Lemma 2 together with Theorem 4.1, we
derive

###### Theorem 4.2

POTL is equivalent to FO with one free variable on finite OP words.

From the results above follows that

###### Corollary 1

The set of operators
$\ocircle^{\Pi},\circleddash^{\Pi},\chi_{F}^{\Pi},\chi_{P}^{\Pi},\mathbin{\mathcal{U}^{\lessdot\doteq}},\mathbin{\mathcal{S}^{\lessdot\doteq}},\ocircle^{\lessdot}_{H},\allowbreak\circleddash^{\lessdot}_{H},\allowbreak\mathbin{\mathcal{U}^{\lessdot}_{H}},\allowbreak\mathbin{\mathcal{S}^{\lessdot}_{H}}$,
where $\Pi\subseteq\\{\mathord{\lessdot},\mathord{\doteq}\\}$, is expressively
complete on OP words.

The semantics of OPTL can be expressed in FOL similarly to POTL, hence

###### Corollary 2

OPTL $\subseteq$ POTL over finite OP words.

##  5 Model Checking

We present an automata-theoretic model checking procedure for POTL based on
OPA. Its correctness is proved in Appendix 0.D. Given an OP alphabet
$({\mathcal{P}(AP)},M_{\mathcal{P}(AP)})$, where $AP$ is a finite set of
atomic propositions, and a formula $\varphi$, let
$\mathcal{A}_{\varphi}=\langle{\mathcal{P}(AP)},\allowbreak
M_{\mathcal{P}(AP)},\allowbreak Q,\allowbreak I,\allowbreak
F,\allowbreak\delta\rangle$ be an OPA. The construction of
$\mathcal{A}_{\varphi}$ resembles the classical one for LTL and the ones for
NWTL and OPTL, diverging from them significantly when dealing with temporal
obligations that involve positions in the chain relation. We first introduce
$\operatorname{Cl}({\varphi})$, the _closure_ of $\varphi$, containing all
subformulas of $\varphi$, plus a few auxiliary operators. Initially,
$\operatorname{Cl}({\varphi})$ is the smallest set such that

  1. 1.

$\varphi\in\operatorname{Cl}({\varphi})$,

  2. 2.

$AP\subseteq\operatorname{Cl}({\varphi})$,

  3. 3.

if $\psi\in\operatorname{Cl}({\varphi})$ and $\psi\neq\neg\theta$, then
$\neg\psi\in\operatorname{Cl}({\varphi})$;

  4. 4.

if $\neg\psi\in\operatorname{Cl}({\varphi})$, then
$\psi\in\operatorname{Cl}({\varphi})$;

  5. 5.

if any of $\psi\land\theta$ or $\psi\lor\theta$ is in
$\operatorname{Cl}({\varphi})$, then $\psi\in\operatorname{Cl}({\varphi})$ and
$\theta\in\operatorname{Cl}({\varphi})$;

  6. 6.

if any of the unary temporal operators (such as $\ocircle^{\Pi}$,
$\chi_{F}^{\Pi}$, …) is in $\operatorname{Cl}({\varphi})$, and $\psi$ is its
argument, then $\psi\in\operatorname{Cl}({\varphi})$;

  7. 7.

if any of the until- and since-like operators is in
$\operatorname{Cl}({\varphi})$, and $\psi$ and $\theta$ are its operands, then
$\psi,\theta\in\operatorname{Cl}({\varphi})$.

The set $\operatorname{Atoms}({\varphi})$ contains all consistent subsets of
$\operatorname{Cl}({\varphi})$, i.e. all
$\Phi\subseteq\operatorname{Cl}({\varphi})$ such that

  1. 1.

for every $\psi\in\operatorname{Cl}({\varphi})$, $\psi\in\Phi$ iff
$\neg\psi\notin\Phi$;

  2. 2.

if $\psi\land\theta\in\Phi$, then $\psi\in\Phi$ and $\theta\in\Phi$;

  3. 3.

if $\psi\lor\theta\in\Phi$, then $\psi\in\Phi$ or $\theta\in\Phi$, or both.

The consistency constraints on $\operatorname{Atoms}({\varphi})$ will be
augmented incrementally in the following sections, for each operator.

The set of states of $\mathcal{A}_{\varphi}$ is
$Q=\operatorname{Atoms}({\varphi})^{2}$, and its elements, which we denote
with Greek capital letters, are of the form $\Phi=(\Phi_{c},\Phi_{p})$, where
$\Phi_{c}$ is the set of formulas that hold in the current position, and
$\Phi_{p}$ is the set of temporal obligations. The latter keep track of
arguments of temporal operators that must be satisfied after a chain body,
skipping it. The way they do so depends on the transition relation $\delta$,
which we also define incrementally in the next sections. Each word position is
associated to an automaton state. So, for
$(\Phi,a,\Psi)\in\delta_{\mathit{push/shift}}$, with
$\Phi\in\operatorname{Atoms}({\varphi})^{2}$ and $a\in{\mathcal{P}(AP)}$, we
have $\Phi_{c}\cap AP=a$ (by $\Phi_{c}\cap AP$ we mean the set of atomic
propositions in $\Phi_{c}$). _Pop_ moves do not read input symbols, and the
automaton remains stuck at the same time instant when performing them: for any
$(\Phi,\Theta,\Psi)\in\delta_{\mathit{pop}}$ we impose
$\Phi_{c}\subseteq\Psi_{c}$, and $\Phi_{c}\cap AP=\Psi_{c}\cap AP$. The
initial set $I$ only contains states of the form $(\Phi_{c},\emptyset)$, with
$\varphi\in\Phi_{c}$, and the final set $F$ only states of the form
$(\Psi_{c},\emptyset)$, s.t. $\Psi_{c}\cap AP=\\{\\#\\}$ and $\Psi_{c}$
contains no future operators.

Precedence Next/Back Operators. Let
$\ocircle^{\Pi}\psi\in\operatorname{Cl}({\varphi})$, with
$\Pi\subseteq\\{\lessdot,\doteq,\gtrdot\\}$: then
$\psi\in\operatorname{Cl}({\varphi})$. Moreover, let
$(\Phi,a,\Psi)\in\delta_{\mathit{shift}}\cup\delta_{\mathit{push}}$, with
$\Phi,\Psi\in\operatorname{Atoms}({\varphi})^{2}$, $a\in{\mathcal{P}(AP)}$,
and let $b=\Psi_{c}\cap AP$: we have $\ocircle^{\Pi}\psi\in\Phi_{c}$ iff
$\psi\in\Psi_{c}$ and there exists a PR $\pi\in\Pi$ such that
$a\mathrel{\pi}b$. The constraints introduced for the $\circleddash^{\Pi}$
operator are symmetric.

Chain Next/Back Operators. The semantics of $\chi_{F}^{\Pi}\psi$, with
$\Pi\in\\{\lessdot,\doteq,\gtrdot\\}$, depends on the PR in $\Pi$. We describe
the automaton construction for singleton values of $\Pi$ only. If $\Pi$ is not
a singleton, then for each $\pi\in\Pi$ we add
$\chi_{F}^{\pi}\in\operatorname{Cl}({\varphi})$, and for each
$\Phi\in\operatorname{Atoms}({\varphi})^{2}$ we impose that if
$\chi_{F}^{\Pi}\psi\in\Phi_{c}$, then $\chi_{F}^{\pi^{\prime}}\psi\in\Phi_{c}$
for some $\pi^{\prime}\in\Pi$.

First, we need to add into $\operatorname{Cl}({\varphi})$ the auxiliary symbol
$\chi_{L}$, which forces the previous position to be the left context of a
chain, by imposing the current one to be the first position of a chain body.
If the current state of the OPA is
$\Phi\in\operatorname{Atoms}({\varphi})^{2}$, and $\chi_{L}\in\Phi_{p}$, then
the next transition (i.e. the one reading the current position) must be a
push. This is formalized by the following rules: if
$(\Phi,a,\Psi)\in\delta_{\mathit{shift}}$ or
$(\Phi,\Theta,\Psi)\in\delta_{\mathit{pop}}$, for any $\Phi,\Theta,\Psi$ and
$a$, then $\chi_{L}\not\in\Phi_{p}$. If
$(\Phi,a,\Psi)\in\delta_{\mathit{push}}$, we may have $\chi_{L}\in\Phi_{c}$
and possibly $\chi_{L}\not\in\Psi$.

The satisfaction of $\chi_{F}^{\doteq}\psi$ is ensured by the following
constraints on $\delta$.

  1. 1.

Let $(\Phi,a,\Psi)\in\delta_{\mathit{push/shift}}$: then
$\chi_{F}^{\doteq}\psi\in\Phi_{c}$ iff
$\chi_{F}^{\doteq}\psi,\chi_{L}\in\Psi_{p}$;

  2. 2.

let $(\Phi,\Theta,\Psi)\in\delta_{\mathit{pop}}$: then
$\chi_{F}^{\doteq}\psi\not\in\Phi_{p}$, and
$\chi_{F}^{\doteq}\psi\in\Theta_{p}$ iff $\chi_{F}^{\doteq}\psi\in\Psi_{p}$;

  3. 3.

let $(\Phi,a,\Psi)\in\delta_{\mathit{shift}}$: then
$\chi_{F}^{\doteq}\psi\in\Phi_{p}$ iff $\psi\in\Phi_{c}$.

The rules for $\chi_{F}^{\gtrdot}\psi$ only differ in $\psi$ being enforced by
a pop transition, triggered by the $\gtrdot$ relation between the left and
right contexts of the chain on which $\chi_{F}^{\gtrdot}\psi$ holds.

  1. 1.

Let $(\Phi,a,\Psi)\in\delta_{\mathit{push/shift}}$: then
$\chi_{F}^{\gtrdot}\psi\in\Phi_{c}$ iff
$\chi_{F}^{\gtrdot}\psi,\chi_{L}\in\Psi_{p}$;

  2. 2.

let $(\Phi,\Theta,\Psi)\in\delta_{pop}$: $\chi_{F}^{\gtrdot}\psi\in\Theta_{p}$
iff $\chi_{F}^{\gtrdot}\psi\in\Psi_{p}$, and
$\chi_{F}^{\gtrdot}\psi\in\Phi_{p}$ iff $\psi\in\Phi_{c}$;

  3. 3.

let $(\Phi,a,\Psi)\in\delta_{\mathit{shift}}$: then
$\chi_{F}^{\gtrdot}\psi\not\in\Phi_{p}$.

The constraints for $\chi_{F}^{\lessdot}\psi$ are the following.

  1. 1.

Let $(\Phi,a,\Psi)\in\delta_{\mathit{push/shift}}$: then
$\chi_{F}^{\lessdot}\psi\in\Phi_{c}$ iff
$\chi_{F}^{\lessdot}\psi,\chi_{L}\in\Psi_{p}$;

  2. 2.

let $(\Phi,\Theta,\Psi)\in\delta_{\mathit{pop}}$: then
$\chi_{F}^{\lessdot}\psi\in\Theta_{p}$ iff $\chi_{L}\in\Psi_{p}$, and either
(a) $\chi_{F}^{\gtrdot}\psi\in\Psi_{p}$or  (b) $\psi\in\Phi_{c}$.

We illustrate how the construction works for $\chi_{F}^{\doteq}$ with the
example of Fig. 4. The OPA starts in state $\Phi^{0}$, with
$\chi_{F}^{\doteq}\mathit{ret}\in\Phi^{0}_{c}$. Since
$\\#\lessdot\mathit{call}$, $\mathit{call}$ is read by a push move, resulting
in state $\Phi^{1}$. By rule 1, we have
$\chi_{F}^{\doteq}\mathit{ret},\chi_{L}\in\Phi^{1}_{p}$. Since
$\mathit{call}\lessdot\mathit{han}$, the next move is a push (step 2-3),
consistently with the presence of $\chi_{L}$ in $\Phi^{1}_{p}$. Thus, the
pending obligation for $\chi_{F}^{\doteq}\mathit{ret}$ is stored onto the
stack in $\Phi^{1}$. The OPA, then, reads the body of the chain between
$\mathit{call}$ and $\mathit{ret}$ normally, until the stack symbol containing
$\Phi^{1}$ is popped, in step 7-8. By rule 2, the temporal obligation is
resumed in the next state $\Phi^{4}$, so
$\chi_{F}^{\doteq}\mathit{ret}\in\Phi^{4}_{p}$. Finally, $\mathit{ret}$ is
read by a shift which, by rule 3, may occur only if
$\mathit{ret}\in\Phi^{4}_{c}$, ensuring the satisfaction of
$\chi_{F}^{\doteq}\mathit{ret}$, and bringing the OPA to the final state
$\Phi^{5}$. Rule 3 fulfills the temporal obligation contained in
$\Phi^{4}_{p}$, by preventing computations in which
$\mathit{ret}\not\in\Phi^{4}_{c}$ from continuing. Note that, had the next
transition been a pop (e.g. because there was no $\mathit{ret}$ and
$\mathit{call}\gtrdot\\#$), the run would have been blocked by rule 2,
preventing the OPA from reaching an accepting state, and from emptying the
stack. The constructions for past operators, given in Appendix 0.D, and for
$\chi_{F}^{\lessdot}$ and $\chi_{F}^{\gtrdot}$ work similarly.

step | input | state | stack
---|---|---|---
1 | $\mathit{call}\lessdot\mathit{han}\lessdot\mathit{thr}\gtrdot\mathit{thr}\gtrdot\mathit{ret}\gtrdot\\#$ | $\Phi^{0}=(\\{\mathit{call},\chi_{F}^{\doteq}\mathit{ret}\\},\emptyset)$ | $\bot$
2 | $\mathit{han}\lessdot\mathit{thr}\gtrdot\mathit{thr}\gtrdot\mathit{ret}\gtrdot\\#$ | $\Phi^{1}=(\\{\mathit{han}\\},\\{\chi_{F}^{\doteq}\mathit{ret},\chi_{L}\\})$ | $[\mathit{call},\Phi^{0}]\bot$
3 | $\mathit{thr}\gtrdot\mathit{thr}\gtrdot\mathit{ret}\gtrdot\\#$ | $\Phi^{2}=(\\{\mathit{thr}\\},\emptyset)$ | $[\mathit{han},\Phi^{1}][\mathit{call},\Phi^{0}]\bot$
4 | $\mathit{thr}\gtrdot\mathit{ret}\gtrdot\\#$ | $\Phi^{2}=(\\{\mathit{thr}\\},\emptyset)$ | $[\mathit{thr},\Phi^{2}][\mathit{han},\Phi^{1}][\mathit{call},\Phi^{0}]\bot$
5 | $\mathit{thr}\gtrdot\mathit{ret}\gtrdot\\#$ | $\Phi^{2}=(\\{\mathit{thr}\\},\emptyset)$ | $[\mathit{han},\Phi^{1}][\mathit{call},\Phi^{0}]\bot$
6 | $\mathit{ret}\gtrdot\\#$ | $\Phi^{3}=(\\{\mathit{ret}\\},\emptyset)$ | $[\mathit{thr},\Phi^{2}][\mathit{han},\Phi^{1}][\mathit{call},\Phi^{0}]\bot$
7 | $\mathit{ret}\gtrdot\\#$ | $\Phi^{3}=(\\{\mathit{ret}\\},\emptyset)$ | $[\mathit{han},\Phi^{1}][\mathit{call},\Phi^{0}]\bot$
8 | $\mathit{ret}\gtrdot\\#$ | $\Phi^{4}=(\\{\mathit{ret}\\},\\{\chi_{F}^{\doteq}\mathit{ret}\\})$ | $[\mathit{call},\Phi^{0}]\bot$
9 | $\\#$ | $\Phi^{5}=(\\{\\#\\},\emptyset)$ | $[\mathit{ret},\Phi^{0}]\bot$
10 | $\\#$ | $\Phi^{5}=(\\{\\#\\},\emptyset)$ | $\bot$
Figure 4: Example accepting run of the automaton for
$\chi_{F}^{\doteq}\mathit{ret}$.

Summary Until and Since. The construction procedure for these operators is
based on the expansion laws (1) and (2). The rules for until follow, those of
since being symmetric. For any $\Phi\in\operatorname{Atoms}({\varphi})^{2}$,
we have $\psi\mathbin{\mathcal{U}^{\Pi}}\theta\in\Phi_{c}$, with $\Pi$ being a
set of PR, iff either:  1. $\theta\in\Phi_{c}$,  2.
$\ocircle^{\Pi}(\psi\mathbin{\mathcal{U}^{\Pi}}\theta),\psi\in\Phi_{c}$, or
3. $\chi_{F}^{\Pi}(\psi\mathbin{\mathcal{U}^{\Pi}}\theta),\psi\in\Phi_{c}$.

Hierarchical Operators. For the hierarchical operators, we do not give an
explicit OPA construction, but we rely on a translation into other POTL
operands. For each hierarchical operator $\eta$ in $\varphi$, we add a
propositional symbol $\mathrm{q}_{(\eta)}$. The $\lessdot$-hierarchical
operators consider the right contexts of chains sharing the same left context.
To distinguish such positions, the following formula, evaluated in one of the
right contexts, asserts that $\mathrm{q}_{(\eta)}$ holds in the unique left
context of the same chain, only.

$\gamma_{L,\eta}\equiv\chi_{P}^{\lessdot}\big{(}\mathrm{q}_{(\eta)}\land\ocircle^{\lessdot\doteq\gtrdot}(\square\neg\mathrm{q}_{(\eta)})\land\circleddash^{\lessdot\doteq\gtrdot}(\boxminus\neg\mathrm{q}_{(\eta)})\big{)}$

where
$\square\psi\equiv\neg(\top\mathbin{\mathcal{U}^{\lessdot\doteq\gtrdot}}\neg\psi)$,
and $\boxminus$ is symmetric. This allows us to define the following
equivalences for $\lessdot$ operators, and symmetric ones for their $\gtrdot$
counterparts.

$\displaystyle\ocircle^{\lessdot}_{H}\psi$
$\displaystyle\equiv\gamma_{L,\ocircle^{\lessdot}_{H}\psi}\land\ocircle^{\lessdot\doteq\gtrdot}\big{(}(\neg\chi_{P}^{\lessdot}\mathrm{q}_{(\ocircle^{\lessdot}_{H}\psi)})\mathbin{\mathcal{U}^{\doteq\gtrdot}}(\chi_{P}^{\lessdot}\mathrm{q}_{(\ocircle^{\lessdot}_{H}\psi)}\land\psi)\big{)}$
(22) $\displaystyle\circleddash^{\lessdot}_{H}\psi$
$\displaystyle\equiv\gamma_{L,\circleddash^{\lessdot}_{H}\psi}\land\circleddash^{\lessdot\doteq\gtrdot}\big{(}(\neg\chi_{P}^{\lessdot}\mathrm{q}_{(\circleddash^{\lessdot}_{H}\psi)})\mathbin{\mathcal{S}^{\doteq\gtrdot}}(\chi_{P}^{\lessdot}\mathrm{q}_{(\circleddash^{\lessdot}_{H}\psi)}\land\psi)\big{)}$
(23) $\displaystyle\psi\mathbin{\mathcal{U}^{\lessdot}_{H}}\theta$
$\displaystyle\equiv\gamma_{L,\psi\mathbin{\mathcal{U}^{\lessdot}_{H}}\theta}\land(\chi_{P}^{\lessdot}\mathrm{q}_{(\psi\mathbin{\mathcal{U}^{\lessdot}_{H}}\theta)}\implies\psi)\mathbin{\mathcal{U}^{\doteq\gtrdot}}(\chi_{P}^{\lessdot}\mathrm{q}_{(\psi\mathbin{\mathcal{U}^{\lessdot}_{H}}\theta)}\land\theta)$
(24) $\displaystyle\psi\mathbin{\mathcal{S}^{\lessdot}_{H}}\theta$
$\displaystyle\equiv\gamma_{L,\psi\mathbin{\mathcal{S}^{\lessdot}_{H}}\theta}\land(\chi_{P}^{\lessdot}\mathrm{q}_{(\psi\mathbin{\mathcal{S}^{\lessdot}_{H}}\theta)}\implies\psi)\mathbin{\mathcal{S}^{\doteq\gtrdot}}(\chi_{P}^{\lessdot}\mathrm{q}_{(\psi\mathbin{\mathcal{S}^{\lessdot}_{H}}\theta)}\land\theta)$
(25)

Complexity. The set $\operatorname{Cl}({\varphi})$ is linear in $|\varphi|$,
the length of $\varphi$. $\operatorname{Atoms}({\varphi})$ has size at most
$2^{|\operatorname{Cl}({\varphi})|}=2^{O(|\varphi|)}$, and the size of the set
of states is the square of that. Moreover, the use of the equivalences for the
hierarchical operators causes only a linear increase in the length of
$\varphi$. Therefore,

###### Theorem 5.1

Given a POTL formula $\varphi$, it is possible to build an OPA accepting the
language denoted by $\varphi$ with at most $2^{O(|\varphi|)}$ states.

##  6 Conclusions

We introduced the temporal logic POTL by extensively redefining the semantics
of OPTL. We proved its FO-completeness on finite OP words, and we gave an
automata-theoretic model checking procedure for it. The next natural research
step is the extension of such results to $\omega$-words, which, for model
checking, may follow the approach sketched in [14] for OPTL. Whether POTL is
strictly more expressive than OPTL also remains an open problem, although we
conjecture OPTL is not FO-complete. A direct explanation of the completeness
result of Corollary 1 also remains to be given. An important future step is
the implementation of a model checker for POTL, to prove that OP languages and
logics are suitable in practice to program verification.

## References

  * [1] Abrahams, D.: Exception-Safety in Generic Components. In: Generic Programming. pp. 69–79. Springer (2000). https://doi.org/10.1007/3-540-39953-4_6
  * [2] Alur, R., Arenas, M., Barceló, P., Etessami, K., Immerman, N., Libkin, L.: First-order and temporal logics for nested words. LMCS 4(4) (2008). https://doi.org/10.2168/LMCS-4(4:11)2008
  * [3] Alur, R., Chaudhuri, S., Madhusudan, P.: Software model checking using languages of nested trees. ACM Trans. Program. Lang. Syst. 33(5), 15:1–15:45 (2011). https://doi.org/10.1145/2039346.2039347
  * [4] Alur, R., Madhusudan, P.: Visibly Pushdown Languages. In: ACM STOC (2004)
  * [5] Alur, R., Madhusudan, P.: Adding nesting structure to words. JACM 56(3) (2009). https://doi.org/10.1145/1516512.1516518
  * [6] Alur, R., Benedikt, M., Etessami, K., Godefroid, P., Reps, T., Yannakakis, M.: Analysis of recursive state machines. ACM Trans. Program. Lang. Syst. 27(4), 786–818 (2005). https://doi.org/10.1145/1075382.1075387
  * [7] Alur, R., Etessami, K., Madhusudan, P.: A temporal logic of nested calls and returns. In: TACAS 2004. pp. 467–481. Springer (2004). https://doi.org/10.1007/978-3-540-24730-2_35
  * [8] Ball, T., Rajamani, S.K.: Bebop: A symbolic model checker for boolean programs. In: SPIN Model Checking and Software Verification. pp. 113–130. Springer (2000). https://doi.org/10.1007/10722468_7
  * [9] Barenghi, A., Crespi Reghizzi, S., Mandrioli, D., Panella, F., Pradella, M.: Parallel parsing made practical. Sci. Comput. Program. 112, 195–226 (2015). https://doi.org/10.1016/j.scico.2015.09.002
  * [10] Bouajjani, A., Echahed, R., Habermehl, P.: On the verification problem of nonregular properties for nonregular processes. In: LICS 95. pp. 123–133 (1995). https://doi.org/10.1109/LICS.1995.523250
  * [11] Bouajjani, A., Esparza, J., Maler, O.: Reachability analysis of pushdown automata: Application to model-checking. In: CONCUR ’97. pp. 135–150. Springer (1997). https://doi.org/10.1007/3-540-63141-0_10
  * [12] Bozzelli, L., Murano, A., Peron, A.: Timed context-free temporal logics. In: GandALF 2018. EPTCS, vol. 277, pp. 235–249. Open Publishing Association (2018). https://doi.org/10.4204/EPTCS.277.17
  * [13] Bozzelli, L., Sánchez, C.: Visibly linear temporal logic. In: Automated Reasoning. pp. 418–433. Springer (2014). https://doi.org/10.1007/978-3-319-08587-6_33
  * [14] Chiari, M., Mandrioli, D., Pradella, M.: Temporal logic and model checking for operator precedence languages. In: GandALF 2018. EPTCS, vol. 277, pp. 161–175. Open Publishing Association (2018). https://doi.org/10.4204/EPTCS.277.12
  * [15] Crespi Reghizzi, S., Mandrioli, D.: Operator Precedence and the Visibly Pushdown Property. JCSS 78(6), 1837–1867 (2012). https://doi.org/10.1016/j.jcss.2011.12.006
  * [16] Esparza, J., Hansel, D., Rossmanith, P., Schwoon, S.: Efficient algorithms for model checking pushdown systems. In: CAV 2000. LNCS, vol. 1855, pp. 232–247. Springer (2000)
  * [17] Esparza, J., Kučera, A., Schwoon, S.: Model checking LTL with regular valuations for pushdown systems. Information and Computation 186(2), 355–376 (2003). https://doi.org/10.1016/S0890-5401(03)00139-1
  * [18] Floyd, R.W.: Syntactic Analysis and Operator Precedence. JACM 10(3), 316–333 (1963). https://doi.org/10.1145/321172.321179
  * [19] Godefroid, P., Yannakakis, M.: Analysis of boolean programs. In: TACAS 2013. pp. 214–229. Springer (2013). https://doi.org/10.1007/978-3-642-36742-7_16
  * [20] Grune, D., Jacobs, C.J.: Parsing techniques: a practical guide. Springer, New York (2008). https://doi.org/10.1007/978-0-387-68954-8
  * [21] Kupferman, O., Piterman, N., Vardi, M.Y.: Model Checking Linear Properties of Prefix-Recognizable Systems. In: CAV 2002. LNCS, vol. 2404, pp. 371–385. Springer (2002). https://doi.org/10.1007/3-540-45657-0_31
  * [22] Kupferman, O., Piterman, N., Vardi, M.Y.: Pushdown Specifications. In: LPAR 2002\. LNCS, vol. 2514, pp. 262–277. Springer (2002). https://doi.org/10.1007/3-540-36078-6_18
  * [23] Lonati, V., Mandrioli, D., Panella, F., Pradella, M.: Operator precedence languages: Their automata-theoretic and logic characterization. SIAM J. Comput. 44(4), 1026–1088 (2015). https://doi.org/10.1137/140978818
  * [24] Mandrioli, D., Pradella, M.: Generalizing input-driven languages: Theoretical and practical benefits. Computer Science Review 27, 61–87 (2018). https://doi.org/10.1016/j.cosrev.2017.12.001
  * [25] Marx, M.: Conditional XPath, the first order complete XPath dialect. In: PODS ’04. p. 13. ACM Press, New York, USA (2004). https://doi.org/10.1145/1055558.1055562
  * [26] Marx, M.: Conditional XPath. ACM Transactions on Database Systems 30(4), 929–959 (dec 2005). https://doi.org/10.1145/1114244.1114247
  * [27] McNaughton, R.: Parenthesis Grammars. JACM 14(3), 490–500 (1967). https://doi.org/10.1145/321406.321411
  * [28] Mehlhorn, K.: Pebbling mountain ranges and its application of DCFL-recognition. In: ICALP ’80. LNCS, vol. 85, pp. 422–435 (1980)

##  Appendix 0.A Omitted Proofs: Semantics of POTL

In the following Lemma, we prove a few properties of the chain relation.

######  Lemma 3 (Properties of the $\chi$ relation.)

Given an OP word $w$ and positions $i,j,h,k$ in it, the following properties
hold.

  1. 1.

If $\chi(i,j)$ and $\chi(h,k)$, 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.

Given $j$, there exists at most one single position $i$ s.t. $\chi(i,j)$ and
$i\lessdot j$ or $i\doteq j$; for any $i^{\prime}$ s.t. $\chi(i^{\prime},j)$
and $i^{\prime}\gtrdot j$ we have $i^{\prime}>i$.

  4. 4.

Given $j$, there exists at most one single position $j$ s.t. $\chi(i,j)$ and
$i\gtrdot j$ or $i\doteq j$; for any $j^{\prime}$ s.t. $\chi(i,j^{\prime})$
and $i\lessdot j^{\prime}$ we have $j^{\prime}<j$.

###### Proof

In the following, we denote by $c_{p}$ the character labeling word position
$p$, and by writing ${}^{c_{-1}}[x_{0}c_{0}x_{1}\dots
x_{n}c_{n}x_{n+1}]{}^{c_{n+1}}$ we imply $c_{-1}$ and $c_{n+1}$ are the
context of a simple or composed chain, in which either $x_{p}=\varepsilon$, or
${}^{c_{p-1}}[x_{p}]{}^{c_{p}}$ is a chain, for each $p$.

  1. 1.

Suppose, by contradiction, that $\chi(i,j)$, $\chi(h,k)$, and $i<h<j$, but
$k>j$. Consider the case in which $\chi(i,j)$ is the innermost chain whose
body contains $h$, so it is of the form ${}^{c_{i}}[x_{0}c_{0}\dots
c_{h}x_{p}c_{p}\dots c_{n}x_{n+1}]{}^{c_{j}}$ or ${}^{c_{i}}[x_{0}c_{0}\dots
c_{h}x_{n+1}]{}^{c_{j}}$. By the definition of chain, we have either
$c_{h}\doteq c_{p}$ or $c_{h}\gtrdot c_{j}$, respectively.

Since $\chi(h,k)$, this chain must be of the form
${}^{c_{h}}[x_{p}c_{p}\dots]{}^{c_{k}}$ or
${}^{c_{h}}[x_{n+1}c_{j}\dots]{}^{c_{k}}$, implying $c_{h}\lessdot c_{p}$ or
$c_{h}\lessdot c_{j}$, respectively. This means there is a conflict in the
OPM, contradicting the hypothesis that $w$ is an OP word.

In case $\chi(i,j)$ is not the innermost chain whose body contains $h$, we can
reach the same contradiction by inductively considering the chain between $i$
and $j$ containing $h$ in its body. Moreover, it is possible to reach a
symmetric contradiction with the hypothesis $\chi(i,j)$, $\chi(h,k)$, and
$i<k<j$, but $i>h$.

  2. 2.

Trivially follows from the definition of chain.

  3. 3.

Suppose, by contradiction, there exists a position $h\neq i$, and w.l.o.g.,
$h<i$, s.t. $\chi(h,j)$ and $h\lessdot j$. Since $i\lessdot j$, by the
definition of chain, $j$ must be part of the body of another composed chain
whose left context is $i$. So, $w$ contains a structure of the form
${}^{c_{i}}[x_{0}c_{j}\dots]{}^{c_{k}}$ where $|x_{0}|\geq 1$,
${}^{c_{i}}[x_{0}]{}^{c_{j}}$, and $k>j$ is such that $\chi(i,k)$. This
contradicts the hypothesis that $\chi(h,j)$ and $h<i$, because such a chain
would cross $\chi(i,k)$, contradicting property (1).

Similarly, if $\chi(h,j)$, $\chi(i,j)$, $h\doteq j$, and $h<i$, then $w$
contains a structure ${}^{c_{h}}[\dots c_{i}x_{i}]{}^{c_{j}}$, with
$|x_{i}|\geq 1$ and ${}^{c_{i}}[x_{i}]{}^{c_{j}}$. By the definition of chain,
we have $i\gtrdot j$, which contradicts the hypothesis that either $i\lessdot
j$ or $i\doteq j$. This proves that $i$ is unique.

For the second part of the property, suppose there exists a position
$i^{\prime}$ s.t. $\chi(i^{\prime},j)$ and $i^{\prime}\gtrdot j$, but
$i^{\prime}<i$ (the case $i^{\prime}=i$ is trivial). The only way of having
both $\chi(i^{\prime},j)$ and $\chi(i,j)$ in this case is
${}^{c_{i^{\prime}}}[\dots c_{i}x_{i}]{}^{c_{j}}$, with $|x_{i}|\geq 1$ and
${}^{c_{i}}[x_{i}]{}^{c_{j}}$. From the definition of chain follows that
$i\gtrdot j$, which contradicts the hypothesis that $i\lessdot j$ or $i\doteq
j$.

  4. 4.

The proof is symmetric to the previous one.

In the rest of this section, we prove the expansion laws of the until and
since operators.

###### Lemma 4

Given a word $w$ on an OP alphabet $({\mathcal{P}(AP)},M_{\mathcal{P}(AP)})$,
two POTL formulas $\varphi$ and $\psi$, and a non-empty set
$\Pi\subseteq\\{\lessdot,\doteq,\gtrdot\\}$, for any position $i\in w$ the
following equivalence holds:

$\varphi\mathbin{\mathcal{U}^{\Pi}}\psi\equiv\psi\lor\Big{(}\varphi\land\big{(}\ocircle^{\Pi}(\varphi\mathbin{\mathcal{U}^{\Pi}}\psi)\lor\chi_{F}^{\Pi}(\varphi\mathbin{\mathcal{U}^{\Pi}}\psi)\big{)}\Big{)}.$

###### Proof

$[\Rightarrow]$ Suppose $\varphi\mathbin{\mathcal{U}^{\Pi}}\psi$ holds in $i$.
If $\psi$ holds in $i$, the equivalence is trivially verified. Otherwise,
$\varphi\mathbin{\mathcal{U}^{\Pi}}\psi$ is verified by an OPSP
$i=i_{0}<i_{1}<\dots<i_{n}=j$ with $n\geq 1$, s.t. $(w,i_{p})\models\varphi$
for $0\leq p<n$ and $(w,i_{n})\models\psi$. Note that, by the definition of
OPSP, any suffix of such a path is also an OPSP ending in $j$. Consider
position $i_{1}$: $\varphi$ holds in it, and it can be either

  * •

$i_{1}=i+1$. Then there exists $\pi\in\Pi$ s.t. $i\mathrel{\pi}(i+1)$, and
path $i_{1}<i_{2}<\dots<i_{n}=j$ is the OPSP between $i_{1}$ and $j$, and
$\varphi$ holds in all $i_{p}$ with $1\leq p<n$, and $\psi$ in $j_{n}$. So,
$\varphi\mathbin{\mathcal{U}^{\Pi}}\psi$ holds in $i_{1}$, and
$\ocircle^{\Pi}(\varphi\mathbin{\mathcal{U}^{\Pi}}\psi)$ holds in $i$.

  * •

$i_{1}>i+1$. Then, $\chi(i,i_{1})$, and there exists $\pi\in\Pi$ s.t.
$i\mathrel{\pi}i_{1}$. Since $i_{1}<i_{2}<\dots<i_{n}=j$ is the OPSP from
$i_{1}$ to $j$, $\varphi\mathbin{\mathcal{U}^{\Pi}}\psi$ holds in $i_{1}$, and
so does $\chi_{F}^{\Pi}(\varphi\mathbin{\mathcal{U}^{\Pi}}\psi)$ in $i$.

$[\Leftarrow]$ Suppose
$\psi\lor\Big{(}\varphi\land\big{(}\ocircle^{\Pi}(\varphi\mathbin{\mathcal{U}^{\Pi}}\psi)\lor\chi_{F}^{\Pi}(\varphi\mathbin{\mathcal{U}^{\Pi}}\psi)\big{)}\Big{)}$
holds in $i$. The case $(w,i)\models\psi$ is trivial. Suppose $\psi$ does not
hold in $i$. Then $\varphi$ holds in $i$, and either:

  * •

$\ocircle^{\Pi}(\varphi\mathbin{\mathcal{U}^{\Pi}}\psi)$ holds in $i$. Then,
we have $i\mathrel{\pi}(i+1)$, $\pi\in\Pi$, and there is an OPSP
$i+1=i_{1}<i_{2}<\dots<i_{n}=j$, with $\varphi$ holding in all $i_{p}$ with
$1\leq i_{p}<n$, and $\psi$ in $i_{n}$. If $i$ is not the left context of any
chain, then $i=i_{0}<i_{1}<i_{2}<\dots<i_{n}$ is an OPSP satisfying
$\varphi\mathbin{\mathcal{U}^{\Pi}}\psi$ in $i$. Otherwise, let
$k=\min\\{h\mid\chi(i,h)\\}$. Since $i$ is the left context of a chain,
$\mathord{\lessdot}\in\Pi$, or
$\ocircle^{\Pi}(\varphi\mathbin{\mathcal{U}^{\Pi}}\psi)$ would not be true in
$i$.

Suppose $k>j$. This is always the case if $\mathord{\gtrdot}\not\in\Pi$,
because then there is no position $h\leq i$ s.t. $\chi(h,i_{p})$ for any
$1\leq p\leq n$. So, adding $i$ to the OPSP generates another OPSP, because
there is no position $h$ s.t. $\chi(i,h)$ with $h\leq j$, and the successor of
$i$ in the path can only be $i_{1}=i+1$.

Suppose $k\leq j$. Let $k^{\prime}=\max\\{h\mid h\leq
j\land\chi(i,h)\land\bigvee_{\pi\in\Pi}i\mathrel{\pi}k\\}$. Since $i_{1}>i$,
and chains cannot cross each other, there exists a value $q$, $1\leq q\leq n$,
s.t. $i_{q}=k^{\prime}$. The path $i=i_{0}<i_{q}<\dots<i_{n}=j$ is an OPSP by
definition, and $\varphi$ holds both in $i$ and $i_{q}$. So, this path makes
$\varphi\mathbin{\mathcal{U}^{\Pi}}\psi$ true in $i$.

  * •

$\chi_{F}^{\Pi}(\varphi\mathbin{\mathcal{U}^{\Pi}}\psi)$ holds in $i$. Then,
there exists a position $k$ s.t. $\chi(i,k)$ and $i\mathrel{\pi}k$ with
$\pi\in\Pi$, and $\varphi\mathbin{\mathcal{U}^{\Pi}}\psi$ holds in $k$,
because of an OPSP $k=i_{1}<i_{2}<\dots<i_{n}=j$. If $k=\max\\{h\mid h\leq
j\land\chi(i,h)\land\bigvee_{\pi\in\Pi}i\mathrel{\pi}k\\}$, then
$i=i_{0}<i_{1}<i_{2}<\dots<i_{n}$ is an OPSP by definition, and since
$\varphi$ holds in $i$, $\varphi\mathbin{\mathcal{U}^{\Pi}}\psi$ is satisfied
in it. Otherwise, let $k^{\prime}=\max\\{h\mid h\leq
j\land\chi(i,h)\land\bigvee_{\pi\in\Pi}i\mathrel{\pi}k\\}$. Since $i_{1}>i$
and chains cannot cross, there exists a value $q$, $1<q\leq n$, s.t.
$i_{q}=k^{\prime}$. $i_{q}<i_{q+1}<\dots<i_{n}=j$ is an OPSP, so
$\varphi\mathbin{\mathcal{U}^{\Pi}}\psi$ holds in $i_{q}$ as well. The path
$i<i_{q}<\dots<i_{n}$ is an OPSP, and $\varphi\mathbin{\mathcal{U}^{\Pi}}\psi$
holds in $i$.

The proof for the OPS since operator is analogous.

###### Lemma 5

Given a word $w$ on an OP alphabet $({\mathcal{P}(AP)},M_{\mathcal{P}(AP)})$,
and two POTL formulas $\varphi$ and $\psi$, for any position $i\in w$ the
following equivalence holds:

$\varphi\mathbin{\mathcal{U}^{\lessdot}_{H}}\psi\equiv(\psi\land\chi_{P}^{\lessdot}\top)\lor\big{(}\varphi\land\ocircle^{\lessdot}_{H}(\varphi\mathbin{\mathcal{U}^{\lessdot}_{H}}\psi)\big{)}.$

###### Proof

$[\Rightarrow]$ Suppose $\varphi\mathbin{\mathcal{U}^{\lessdot}_{H}}\psi$
holds in $i$. Then, there exists a path $i=i_{0}<i_{1}<\dots<i_{n}$, $n\geq
0$, and a position $h<i$ s.t. $\chi(h,i_{p})$ and $h\lessdot i_{p}$ for each
$0\leq p\leq n$, $\varphi$ holds in all $i_{q}$ for $0\leq q<n$, and $\psi$
holds in $i_{n}$. If $n=0$, $\psi$ holds in $i=i_{0}$, and so does
$\chi_{P}^{\lessdot}\top$. Otherwise, the path $i_{1}<\dots<i_{n}$ is also a
YPHP, so $\varphi\mathbin{\mathcal{U}^{\lessdot}_{H}}\psi$ is true in $i_{1}$.
Therefore,
$\ocircle^{\lessdot}_{H}(\varphi\mathbin{\mathcal{U}^{\lessdot}_{H}}\psi)$
holds in $i$, and so does $\varphi$.

$[\Leftarrow]$ If $\chi_{P}^{\lessdot}\top$ holds in $i$, then there exists a
position $h<i$ s.t. $\chi(h,i)$ and $h\lessdot i$. If $\psi$ also holds in
$i$, then $\varphi\mathbin{\mathcal{U}^{\lessdot}_{H}}\psi$ is trivially
satisfied in $i$ by the path made of only $i$ itself. Otherwise, if
$\ocircle^{\lessdot}_{H}(\varphi\mathbin{\mathcal{U}^{\lessdot}_{H}}\psi)$
holds in $i$, then there exist a position $h<i$ s.t. $\chi(h,i)$ and
$h\lessdot i$, and a position $i_{1}$ which is the minimum one s.t. $i_{1}>i$,
$\chi(h,i_{1})$ and $h\lessdot i_{1}$. In $i_{1}$,
$\varphi\mathbin{\mathcal{U}^{\lessdot}_{H}}\psi$ holds, so it is the first
position of a YPHP $i_{1}<i_{2}<\dots<i_{n}$. Since $\varphi$ also holds in
$i$, the path $i=i_{0}<i_{1}<\dots<i_{n}$ is also a YPHP, satisfying
$\varphi\mathbin{\mathcal{U}^{\lessdot}_{H}}\psi$ in $i$.

The proofs for the other hierarchical operators are analogous.

##  Appendix 0.B First Order Semantics

We now show that POTL can be expressed with First Order logic 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 $x$, $(w,x)\models\nu_{\varphi}(x)$ iff $(w,x)\models\varphi$. The
translation for propositional operators is trivial.
For temporal operators, we first need to define a few auxiliary formulae. We
define the successor relation as the FO formula

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

In the following, $\mathrel{\pi}\in\\{\lessdot,\doteq\gtrdot\\}$ and
$\Pi\subseteq\\{\lessdot,\doteq\gtrdot\\}$. The PR 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)\equiv\bigwedge_{\mathrm{p}\in
a}\mathrm{p}(x)\land\bigwedge_{\mathrm{p}\in AP\setminus a}\neg\mathrm{p}(x)$

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

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

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

###  0.B.1 Precedence and Chain Next/Back

$\nu_{\ocircle^{\Pi}\varphi}(x)\equiv\exists
y\Big{(}\operatorname{succ}(x,y)\land\bigvee_{\mathrel{\pi}\in\Pi}(x\mathrel{\pi}y)\land\exists
x\big{(}x=y\land\nu_{\varphi}(x)\big{)}\Big{)}$
$\nu_{\circleddash^{\Pi}\varphi}(x)\equiv\exists
y\Big{(}\operatorname{succ}(y,x)\land\bigvee_{\mathrel{\pi}\in\Pi}(y\mathrel{\pi}x)\land\exists
x\big{(}x=y\land\nu_{\varphi}(x)\big{)}\Big{)}$

Note that $\operatorname{succ}(y,x)$ can be obtained by exchanging $x$ and $y$
in the definition of $\operatorname{succ}(x,y)$ above.

$\nu_{\chi_{F}^{\Pi}\varphi}(x)\equiv\exists
y\big{(}x<y\land\chi(x,y)\land\bigvee_{\mathrel{\pi}\in\Pi}(x\mathrel{\pi}y)\land\exists
x(x=y\land\nu_{\varphi}(x))\big{)}$
$\nu_{\chi_{P}^{\Pi}\varphi}(x)\equiv\exists
y\big{(}y<x\land\chi(y,x)\land\bigvee_{\mathrel{\pi}\in\Pi}(y\mathrel{\pi}x)\land\exists
x(x=y\land\nu_{\varphi}(x))\big{)}$

###  0.B.2 Operator Precedence Summary Until/Since

The translation for the OPS until operator can be obtained by noting that,
given two positions $x$ and $y$, the OPS path between them, if it exists, is
the one that skips all chain bodies entirely contained between them, among
those whose contexts are in a relation in $\Pi$. The fact that a position $z$
is part of such path can be expressed with formula $\neg\gamma(x,y,z)$ as
follows:

$\displaystyle\gamma(x,y,z)$
$\displaystyle\equiv\gamma_{L}(x,z)\land\gamma_{R}(y,z)$
$\displaystyle\gamma_{L}(x,z)$ $\displaystyle\equiv\exists y\Big{(}x\leq
y\land y<z\land\exists
x\big{(}z<x\land\chi(y,x)\land\bigvee_{\mathrel{\pi}\in\Pi}(y\mathrel{\pi}x)\big{)}\Big{)}$
$\displaystyle\gamma_{R}(y,z)$ $\displaystyle\equiv\exists x\Big{(}z<x\land
x\leq y\land\exists
y\big{(}y<z\land\chi(y,x)\land\bigvee_{\mathrel{\pi}\in\Pi}(y\mathrel{\pi}x)\big{)}\Big{)}$

$\gamma(x,y,z)$ is true iff $z$ is not part of the OPS path 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$. Only chains whose contexts are in a relation in $\Pi$
are considered. 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 PR with the next one. Formula

$\delta(y,z)\equiv\exists x\big{(}z<x\land x\leq
y\land\bigvee_{\mathrel{\pi}\in\Pi}(z\mathrel{\pi}x)\land\neg\gamma(z,y,x)\land(\operatorname{succ}(z,x)\lor\chi(z,x))\big{)}$

asserts this for each 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}^{\Pi}}\psi$ can be translated as follows:

$\displaystyle\nu_{\varphi\mathbin{\mathcal{U}^{\Pi}}\psi}(x)\equiv\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 OPS since operator is similar:

$\displaystyle\nu_{\varphi\mathbin{\mathcal{S}^{\Pi}}\psi}(x)\equiv\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{)}$

###  0.B.3 Hierarchical Next/Back

Finally, the translations for hierarchical operators.

$\displaystyle\nu_{\ocircle^{\lessdot}_{H}\varphi}(x)\equiv$
$\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_{\circleddash^{\lessdot}_{H}\varphi}(x)\equiv$
$\displaystyle\exists y\Bigg{(}y<x\land\chi(y,x)\land y\lessdot x\land$
$\displaystyle\qquad\exists z\Big{(}z<x\land\chi(y,z)\land y\lessdot
z\land\exists x(x=z\land\nu_{\varphi}(x))$
$\displaystyle\qquad\quad\land\forall y\big{(}z<y\land y<x\implies\forall
z(\chi(z,x)\land z\lessdot x\implies\neg\chi(z,y))\big{)}\Big{)}\Bigg{)}$
$\displaystyle\nu_{\ocircle^{\gtrdot}_{H}\varphi}(x)\equiv$
$\displaystyle\exists y\Bigg{(}x<y\land\chi(x,y)\land x\gtrdot y\land$
$\displaystyle\qquad\exists z\Big{(}x<z\land\chi(z,y)\land z\gtrdot
y\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(x,z)\land x\gtrdot z\implies\neg\chi(y,z))\big{)}\Big{)}\Bigg{)}$
$\displaystyle\nu_{\circleddash^{\gtrdot}_{H}\varphi}(x)\equiv$
$\displaystyle\exists y\Bigg{(}x<y\land\chi(x,y)\land x\gtrdot y\land$
$\displaystyle\qquad\exists z\Big{(}z<x\land\chi(z,y)\land z\gtrdot
y\land\exists x(x=z\land\nu_{\varphi}(x))$
$\displaystyle\qquad\quad\land\forall y\big{(}z<y\land y<x\implies\forall
z(\chi(x,z)\land x\gtrdot z\implies\neg\chi(y,z))\big{)}\Big{)}\Bigg{)}$

###  0.B.4 Hierarchical Until/Since

$\displaystyle\nu_{\varphi\mathbin{\mathcal{U}^{\lessdot}_{H}}\psi}(x)\equiv\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{)}$
$\displaystyle\nu_{\varphi\mathbin{\mathcal{S}^{\lessdot}_{H}}\psi}(x)\equiv\exists
z\bigg{(}$ $\displaystyle z<x\land z\lessdot x\land\chi(z,x)\land$
$\displaystyle\exists y\Big{(}y\leq x\land\chi(z,y)\land z\lessdot
y\land\exists x(x=y\land\nu_{\psi}(x))\land$ $\displaystyle\quad\forall
z\big{(}y<z\land z\leq x\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{)}$
$\displaystyle\nu_{\varphi\mathbin{\mathcal{U}^{\gtrdot}_{H}}\psi}(x)\equiv\exists
z\bigg{(}$ $\displaystyle x<z\land x\gtrdot z\land\chi(x,z)\land$
$\displaystyle\exists y\Big{(}x\leq y\land\chi(y,z)\land y\gtrdot
z\land\exists x(x=y\land\nu_{\psi}(x))\land$ $\displaystyle\quad\forall
z\big{(}x\leq z\land z<y\land\exists y(x<y\land x\gtrdot
y\land\chi(x,y)\land\chi(z,y))$ $\displaystyle\qquad\qquad\implies\exists
x(x=z\land\nu_{\varphi}(x)))\big{)}\Big{)}\bigg{)}$
$\displaystyle\nu_{\varphi\mathbin{\mathcal{S}^{\gtrdot}_{H}}\psi}(x)\equiv\exists
z\bigg{(}$ $\displaystyle x<z\land x\gtrdot z\land\chi(x,z)\land$
$\displaystyle\exists y\Big{(}y\leq x\land\chi(y,z)\land y\gtrdot
z\land\exists x(x=y\land\nu_{\psi}(x))\land$ $\displaystyle\quad\forall
z\big{(}y<z\land z\leq x\land\exists y(x<y\land x\gtrdot
y\land\chi(x,y)\land\chi(z,y))$ $\displaystyle\qquad\qquad\implies\exists
x(x=z\land\nu_{\varphi}(x))\big{)}\Big{)}\bigg{)}$

##  Appendix 0.C Omitted Proofs: Conditional XPath Translation

###  0.C.1 Completeness of CXPath on OPM-compatible trees

First, we give an argument for Theorem 4.1, by proving a more general result.

###### Lemma 6

Let $\mathcal{M}$ be the set of algebraic structures with common signature
$\sigma$, let $\mathcal{L}$ be a logic formalism that is FO-complete on
$\mathcal{M}$, and let $\mathcal{N}$ be FO-definable subset of $\mathcal{M}$.
Then, $\mathcal{L}$ is also FO-complete on $\mathcal{N}$.

###### Proof

Since $\mathcal{N}$ is FO-definable, there exists a FO formula
$\varphi_{\mathcal{N}}$ such that, for any $M\in\mathcal{M}$, we have
$M\models\varphi_{\mathcal{N}}$ iff $M\in\mathcal{N}$. Thus, any FO formula
$\psi$ on $\mathcal{N}$ is equivalent to $\psi\land\varphi_{\mathcal{N}}$ on
$\mathcal{M}$.

Since $\mathcal{L}$ is FO-complete, there exists an $\mathcal{L}$-formula
$\Phi$ such that, for any $M\in\mathcal{M}$, $M\models\Phi$ iff
$M\models\psi\land\varphi_{\mathcal{N}}$. Therefore, since
$\mathcal{N}\subseteq\mathcal{M}$, we also have $N\models\Phi$ iff
$N\models\psi\land\varphi_{\mathcal{N}}$ for any $N\in\mathcal{N}$. By
construction, $\varphi_{\mathcal{N}}\equiv\top$ on any $N\in\mathcal{N}$, and
thus $N\models\Phi$ iff $N\models\psi$.

In our case, $\mathcal{M}$ is the set of all unranked ordered trees
$\mathcal{T}$, while $\mathcal{N}$ is $\mathcal{T}_{M_{\mathcal{P}(AP)}}$, for
a given OPM $M_{\mathcal{P}(AP)}$. $\mathcal{L}$ is the logic CXPath, proved
to be FO-complete in [26]. We only need to show that the set
$\mathcal{T}_{M_{\mathcal{P}(AP)}}$ is FO-definable.

Note that the actual signature of $\mathcal{T}$ differs from the one reported
in Section 4 in the fact that the transitive and reflexive closures of the
$R_{\Downarrow}$ and $R_{\Rightarrow}$ relations are used (denoted resp.
$R_{\Downarrow}^{*}$ and $R_{\Rightarrow}^{*}$). We also use
$R_{\Downarrow}^{+}$ to denote the transitive closure of $R_{\Downarrow}$.
Moreover, the signature contains monadic predicates for propositional symbols,
instead of the labeling function $L$. First, we define the following FO
formula on $\mathcal{T}$, which is true iff a node $y$ is the _right context
candidate_ of another node $x$:

$\displaystyle\operatorname{Rcc}(x,y)\equiv xR_{\Rightarrow}y\lor\big{(}$
$\displaystyle\neg\exists z(xR_{\Rightarrow}z)$ $\displaystyle\land\exists
z(zR_{\Downarrow}^{*}x\land zR_{\Rightarrow}y$
$\displaystyle\qquad\land\forall y(zR_{\Downarrow}^{+}y\land
yR_{\Downarrow}^{*}x\implies\neg\exists x(yR_{\Rightarrow}x))))\big{)}$

We also express sets of atomic propositions and PR as detailed at the
beginning of Section 0.B, and we define the following shortcuts:

$\displaystyle\operatorname{leftmost}(x)$ $\displaystyle\equiv\neg\exists
y(yR_{\Rightarrow}x)$ $\displaystyle\operatorname{rightmost}(x)$
$\displaystyle\equiv\neg\exists y(xR_{\Rightarrow}y)$

The following formula $\varphi_{\mathcal{T}_{M_{\mathcal{P}(AP)}}}$ defines
the set $\mathcal{T}_{M_{\mathcal{P}(AP)}}$.

$\displaystyle\varphi_{\mathcal{T}_{M_{\mathcal{P}(AP)}}}\equiv\forall
x\Big{[}$ $\displaystyle\Big{(}\neg\exists
y(yR_{\Downarrow}x)\implies\big{(}\sigma_{\\#}(x)\land\exists
y(xR_{\Downarrow}y\land\operatorname{rightmost}(y)\land\sigma_{\\#}(y)$
$\displaystyle\qquad\qquad\land(\operatorname{leftmost}(y)\lor\exists
z(zR_{\Rightarrow}y\land\operatorname{leftmost}(z)\land\neg\\#(z))))\big{)}\Big{)}$
$\displaystyle\land(\exists y(yR_{\Downarrow}x)\implies\neg\\#(x))$
$\displaystyle\land\big{(}\forall
y(xR_{\Downarrow}y\land\operatorname{rightmost}(y)\implies x\lessdot y\lor
x\doteq y)$ $\displaystyle\qquad\land\forall
y(xR_{\Downarrow}y\land\neg\operatorname{rightmost}(y)\implies x\lessdot y)$
$\displaystyle\qquad\land\neg\exists y(xR_{\Downarrow}y\land x\doteq
y)\implies\forall y(\operatorname{Rcc}(x,y)\implies x\gtrdot y)\big{)}\Big{]}$

The first two lines say that the root is labeled with $\\#$ and it has at most
two children, the rightmost one labeled with $\\#$. The third line states that
no other position is labeled with $\\#$. The remaining lines describe the PR
among sets of labels of each node, as described in Section 4.

###  0.C.2 POTL Translation of CXPath

We now proceed with the proof of the translation of CXPath into POTL, with one
lemma for each translated operator.

###### Lemma 7

Given a set of atomic propositions $AP$, and OPM $M_{\mathcal{P}(AP)}$, for
every $\mathcal{X}_{\mathit{until}}$ formula $\Downarrow(\varphi,\psi)$, and
for any OP word $w$ based on $M_{\mathcal{P}(AP)}$ and position $i$ in $w$, we
have

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

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

###### Proof

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

We shall now inductively prove that
$\varphi^{\prime}\mathbin{\mathcal{U}^{\lessdot\doteq}}\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}^{\lessdot\doteq}}\psi^{\prime}$.
Otherwise, consider any node $t=\tau(k)$ of the path, except the last one, and
suppose $\varphi^{\prime}\mathbin{\mathcal{U}^{\lessdot\doteq}}\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 ether $k\lessdot k^{\prime}$ or $k\doteq k^{\prime}$. In both cases,
$\ocircle^{\lessdot\doteq}(\varphi^{\prime}\mathbin{\mathcal{U}^{\lessdot\doteq}}\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\doteq k^{\prime}$. In
both cases,
$\chi_{F}^{\lessdot\doteq}(\varphi^{\prime}\mathbin{\mathcal{U}^{\lessdot\doteq}}\psi^{\prime})$
holds in $k$. So, by expansion formula
$\varphi^{\prime}\mathbin{\mathcal{U}^{\lessdot\doteq}}\psi^{\prime}\equiv\psi^{\prime}\lor\Big{(}\varphi^{\prime}\land\big{(}\ocircle^{\lessdot\doteq}(\varphi^{\prime}\mathbin{\mathcal{U}^{\lessdot\doteq}}\psi^{\prime})\lor\chi_{F}^{\lessdot\doteq}(\varphi^{\prime}\mathbin{\mathcal{U}^{\lessdot\doteq}}\psi^{\prime})\big{)}\Big{)}$,
$\varphi^{\prime}\mathbin{\mathcal{U}^{\lessdot\doteq}}\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\doteq j$, so
$\ocircle^{\lessdot\doteq}(\varphi^{\prime}\mathbin{\mathcal{U}^{\lessdot\doteq}}\psi^{\prime})$
holds in $i$. Otherwise, $\chi(i,j)$ and either $i\lessdot j$ or $i\doteq j$.
In both cases,
$\chi_{F}^{\lessdot\doteq}(\varphi^{\prime}\mathbin{\mathcal{U}^{\lessdot\doteq}}\psi^{\prime})$
holds in $i$.

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

We shall now prove that if
$\varphi^{\prime}\mathbin{\mathcal{U}^{\lessdot\doteq}}\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}^{\lessdot\doteq}}\psi^{\prime}$ holds in
$j$, then there exists an OPSP from $j$ to $h>j$ s.t.
$(w,h)\models\psi^{\prime}$ and $\varphi^{\prime}$ holds in all positions
$j\leq k<k$ of the path, and $(T_{w},\tau(k))\models\varphi$. In any such $k$,
$\varphi^{\prime}\mathbin{\mathcal{U}^{\lessdot\doteq}}\psi^{\prime}\equiv\psi^{\prime}\lor\Big{(}\varphi^{\prime}\land\big{(}\ocircle^{\lessdot\doteq}(\varphi^{\prime}\mathbin{\mathcal{U}^{\lessdot\doteq}}\psi^{\prime})\lor\chi_{F}^{\lessdot\doteq}(\varphi^{\prime}\mathbin{\mathcal{U}^{\lessdot\doteq}}\psi^{\prime})\big{)}\Big{)}$
holds. Since $\psi^{\prime}$ does not hold in $k$, either
$\ocircle^{\lessdot\doteq}(\varphi^{\prime}\mathbin{\mathcal{U}^{\lessdot\doteq}}\psi^{\prime})$
or
$\chi_{F}^{\lessdot\doteq}(\varphi^{\prime}\mathbin{\mathcal{U}^{\lessdot\doteq}}\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\doteq k^{\prime}$, and
$(w,k^{\prime})\models\varphi^{\prime}\mathbin{\mathcal{U}^{\lessdot\doteq}}\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)$.

###### Lemma 8

Given a set of atomic propositions $AP$, and OPM $M_{\mathcal{P}(AP)}$, for
every $\mathcal{X}_{\mathit{until}}$ formula $\Uparrow(\varphi,\psi)$, and for
any OP word $w$ based on $M_{\mathcal{P}(AP)}$ and position $i$ in $w$, we
have

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

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

###### Proof

The proof of this lemma is analogous to the one of Lemma 7, and is therefore
omitted.

###### Lemma 9

Given a set of atomic propositions $AP$, and OPM $M_{\mathcal{P}(AP)}$, for
every $\mathcal{X}_{\mathit{until}}$ formula $\Rightarrow(\varphi,\psi)$, and
for any OP word $w$ based on $M_{\mathcal{P}(AP)}$ and position $i$ in $w$, we
have

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

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

###### Proof

$[\Rightarrow]$ 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
t^{\prime}$. The path made by such positions is a YPHP, and
$\varphi^{\prime}\mathbin{\mathcal{U}^{\lessdot}_{H}}\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 (14)
($\ocircle^{\lessdot}_{H}(\varphi^{\prime}\mathbin{\mathcal{U}^{\lessdot}_{H}}\psi^{\prime})$)
holds in $i$.

    2. (b)

_$h\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, if any, are s.t.
$\chi(h,j)$ and $h\lessdot j$, and they form a YPHP, so
$\ocircle^{\lessdot}_{H}(\top\mathbin{\mathcal{U}^{\lessdot}_{H}}\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}^{\doteq}$ evaluated in $h$ identifies $k$. So, (15) 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\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^{\lessdot}_{H}(\top\mathbin{\mathcal{S}^{\lessdot}_{H}}\neg\varphi^{\prime})$
does not, because in all positions between $i$ and $k$ (excluded)
corresponding to children of $r$, $\psi^{\prime}$ holds. Note that all such
positions form a YPHP, but $i$ is not part of it ($i=h+1$, so
$\neg\chi(h,i)$), and is not considered by
$\top\mathbin{\mathcal{S}^{\lessdot}_{H}}\neg\varphi^{\prime}$. So, (16) holds
in $i$.

    2. (b)

_$h\doteq k$ , so $v$ is the rightmost child of $r$._ $\psi^{\prime}$ holds in
$k$, and $\varphi$ holds in all children of $r$, except possibly the first
($i$) 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}^{\doteq}\psi^{\prime}$ in $h$. So, (17) holds in $i$.

$[\Leftarrow]$ Suppose (14)
($\ocircle^{\lessdot}_{H}(\varphi^{\prime}\mathbin{\mathcal{U}^{\lessdot}_{H}}\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}^{\lessdot}_{H}}\psi^{\prime}$ holds in
$j$. So, $i$ and $j$ are consecutive children of $r=\tau(h)$. Moreover, there
exists a YPHP between $j$ and a position $k>j$. The tree nodes corresponding
to all positions in the path are consecutive children of $r$, so we fall in
case 1a of the proof of the other side of the implication. In $T_{w}$, a path
between $t=\tau(j)$ and $v=\tau(k)$ witnesses the truth of
$\Rightarrow(\varphi,\psi)$ in $s$.

Suppose (15)
($\neg\ocircle^{\lessdot}_{H}(\top\mathbin{\mathcal{U}^{\lessdot}_{H}}\neg\varphi^{\prime})\land\chi_{P}^{\lessdot}(\chi_{F}^{\doteq}\psi^{\prime})$)
holds in position $i\in w$. If
$\chi_{P}^{\lessdot}(\chi_{F}^{\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\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^{\lessdot}_{H}(\top\mathbin{\mathcal{U}^{\lessdot}_{H}}\neg\varphi^{\prime})$
holds in $i$, then either:

  * •

$\neg\ocircle^{\lessdot}_{H}\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}^{\lessdot}_{H}}\neg\varphi^{\prime})$ holds in
$j$, the first position after $i$ s.t. $chain(h,j)$ and $h\lessdot j$. This
means $\varphi^{\prime}$ holds in all positions $j^{\prime}$ s.t.
$chain(h,j^{\prime})$ and $h\lessdot j^{\prime}$ greater or equal to $j$.
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)$.

This corresponds to case 1b.

Suppose (16)
($\circleddash^{\lessdot}\Big{(}\chi_{F}^{\lessdot}\big{(}\psi^{\prime}\land\neg\circleddash^{\lessdot}_{H}(\top\mathbin{\mathcal{S}^{\lessdot}_{H}}\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$ in which
$\psi^{\prime}$ holds, so $\psi$ does in $v=\tau(k)$, and
$\circleddash^{\lessdot}_{H}(\top\mathbin{\mathcal{S}^{\lessdot}_{H}}\neg\varphi^{\prime})$
is false in it. If it is false because $\neg\circleddash^{\lessdot}_{H}\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$ be the rightmost position lower than $k$ s.t.
$\chi(h,j)$ and $h\lessdot j$.
$\neg(\top\mathbin{\mathcal{S}^{\lessdot}_{H}}\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).

If (17)
($\circleddash^{\lessdot}(\chi_{F}^{\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}^{\doteq}\psi^{\prime}$ holds in $h$,
there exists a position $k$, s.t. $\chi(h,k)$ and $h\doteq k$, in which
$\psi^{\prime}$ holds. So, $\psi$ holds in $v=\tau(k)$, which is the rightmost
child of $r$, by construction. Moreover, in all positions s.t. $\chi(h,j)$ and
$h\lessdot j$, $\psi^{\prime}$ holds. 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 10

Given a set of atomic propositions $AP$, and OPM $M_{\mathcal{P}(AP)}$, for
every $\mathcal{X}_{\mathit{until}}$ formula $\Leftarrow(\varphi,\psi)$, and
for any OP word $w$ based on $M_{\mathcal{P}(AP)}$ and position $i$ in $w$, we
have

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

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

###### Proof

$[\Rightarrow]$ Suppose $\Leftarrow(\varphi,\psi)$ holds in $s=\tau(i)$. Then
node $r$ s.t. $rR_{\Downarrow}s$ has at least two children, and
$\Leftarrow(\varphi,\psi)$ is true because of a path starting in $t=\tau(j)$
s.t. $tR_{\Rightarrow}s$ and ending in $v=\tau(k)$, s.t. $rR_{\Downarrow}v$
and $(T_{w},v)\models\psi$. We must distinguish between the following cases:

  1. 1.

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

    1. (a)

_$h\lessdot i$._ By construction, all nodes in the path correspond to
positions $j^{\prime}\in w$ s.t. $\chi(h,j^{\prime})$ and $h\lessdot
j^{\prime}$, so they form a YPHP. Hence,
$\varphi^{\prime}\mathbin{\mathcal{S}^{\lessdot}_{H}}\psi^{\prime}$ holds in
$j$, and (18)
($\circleddash^{\lessdot}_{H}(\varphi^{\prime}\mathbin{\mathcal{S}^{\lessdot}_{H}}\psi^{\prime})$)
holds in $i$.

    2. (b)

_$h\doteq i$._ In this case, $s$ is the rightmost child of $r$, and
$\chi(h,i)$. The path made of positions between $k$ and $j$ corresponding to
nodes between $v$ and $t$ (included) form a YPHP. So
$\varphi^{\prime}\mathbin{\mathcal{S}^{\lessdot}_{H}}\psi^{\prime}$ holds in
$j$, which is the rightmost position of any possible such YPHP: so
$\neg\ocircle^{\lessdot}_{H}\top$ also holds in $j$. Hence, (19)
($\chi_{P}^{\doteq}\big{(}\chi_{F}^{\lessdot}(\neg\ocircle^{\lessdot}_{H}\top\land\varphi^{\prime}\mathbin{\mathcal{S}^{\lessdot}_{H}}\psi^{\prime})\big{)}$)
holds in $i$.

  2. 2.

_$v$ is the leftmost child of $r$._

    1. (a)

_$h\lessdot i$._ In this case, $k=h+1$ and $\psi^{\prime}$ holds in $k$. So,
$\ocircle^{\lessdot}\psi^{\prime}$ holds in $h$, and
$\chi_{P}^{\lessdot}(\ocircle^{\lessdot}\psi^{\prime})$ holds in $i$.
Moreover, in all positions $j^{\prime}\in w$, $k<j^{\prime}<j$, corresponding
to tree nodes, $\varphi^{\prime}$ holds. Such positions form a YPHP. So
$\neg\circleddash^{\lessdot}_{H}(\top\mathbin{\mathcal{S}^{\lessdot}_{H}}\neg\varphi^{\prime})$
holds in $i$. Note that this is also true if $s$ is the first right sibling of
$v$. In conclusion, (20) holds in $i$.

    2. (b)

_$h\doteq i$._ $\psi^{\prime}$ holds in $k=h+1$, so
$\ocircle^{\lessdot}\psi^{\prime}$ holds in $h$. Since $\chi(h,i)$ and
$h\doteq i$, $\chi_{P}^{\doteq}(\ocircle^{\lessdot}\psi^{\prime})$ holds in
$i$. Moreover, $\varphi$ holds in all children of $r$ except the first and
last one, i.e. $\varphi^{\prime}$ holds in all positions $j^{\prime}$ s.t.
$\chi(h,j^{\prime})$ and $h\lessdot j^{\prime}$. So
$\neg\chi_{F}^{\lessdot}\neg\varphi^{\prime}$ holds in $h$, and (21)
($\chi_{P}^{\doteq}(\ocircle^{\lessdot}\psi^{\prime}\land\neg\chi_{F}^{\lessdot}\neg\varphi^{\prime})$)
in $i$.

$[\Leftarrow]$ Suppose (18)
($\circleddash^{\lessdot}_{H}(\varphi^{\prime}\mathbin{\mathcal{S}^{\lessdot}_{H}}\psi^{\prime})$)
holds in $i$. Then, there exists a position $h$ s.t. $\chi(h,i)$ and
$h\lessdot i$, and a position $j<i$ s.t. $\chi(h,j)$ and $h\lessdot j$. Since
$j\neq h+1$ and $h\lessdot i$, the corresponding tree nodes are not the
leftmost nor the rightmost one. So, this is case 1a, and
$\Leftarrow(\varphi,\psi)$ holds in $s=\tau(i)$.

Suppose (19)
($\chi_{P}^{\doteq}\big{(}\chi_{F}^{\lessdot}(\neg\ocircle^{\lessdot}_{H}\top\land\varphi^{\prime}\mathbin{\mathcal{S}^{\lessdot}_{H}}\psi^{\prime})\big{)}$)
holds in $i$. Then, there exists a position $h$ s.t. $\chi(h,i)$ and $h\doteq
i$. Moreover, at least a position $j^{\prime}$ s.t. $\chi(h,j^{\prime})$ and
$h\lessdot j^{\prime}$ exists. Let $j$ be the rightmost one, i.e. the only one
in which $\neg\ocircle^{\lessdot}_{H}\top$ holds. The corresponding tree node
$t=\tau(j)$ is s.t. $tR_{\Rightarrow}s$, with $s=\tau(i)$. Since
$\varphi^{\prime}\mathbin{\mathcal{S}^{\lessdot}_{H}}\psi^{\prime}$ holds in
$j$, a YPHP starts from it, and $\psi$ and $\varphi$ hold in the tree nodes
corresponding to, respectively, the first and all other positions in the path.
This is case 1b, and $\Leftarrow(\varphi,\psi)$ holds in $s$.

Suppose (20)
($\chi_{P}^{\lessdot}(\ocircle^{\lessdot}\psi^{\prime})\land\neg\circleddash^{\lessdot}_{H}(\top\mathbin{\mathcal{S}^{\lessdot}_{H}}\neg\varphi^{\prime})$)
holds in $i$. Then, there exists a position $h$ s.t. $\chi(h,i)$ and
$h\lessdot i$. $\psi^{\prime}$ holds in $k=h+1$, so $\psi$ holds in the
leftmost child of $r=\tau(h)$. Moreover, $\varphi^{\prime}$ holds in all
positions $j^{\prime}<i$ s.t. $\chi(h,j^{\prime})$ and $h\lessdot j^{\prime}$,
so $\varphi$ holds in all children of $r$ between $v=\tau(k)$ and $s=\tau(i)$,
excluded. This corresponds to case 2a, and $\Leftarrow(\varphi,\psi)$ holds in
$s$.

Finally, suppose (21)
($\chi_{P}^{\doteq}(\ocircle^{\lessdot}\psi^{\prime}\land\neg\chi_{F}^{\lessdot}\neg\varphi^{\prime})$)
holds in $i$. Then, there exists a position $h$ s.t. $\chi(h,i)$ and $h\doteq
i$. $\ocircle^{\lessdot}\psi^{\prime}$ holds in $h$, so $\psi$ holds in node
$v=\tau(h+1)$, which is the leftmost child of $r=\tau(h)$. Since
$\neg\chi_{F}^{\lessdot}\neg\varphi^{\prime}$ holds in $h$, $\psi^{\prime}$
holds in all positions $j^{\prime}$ s.t. $\chi(h,j^{\prime})$ and $h\lessdot
j$. So, $\psi$ holds in all children of $r$ except (possibly) the leftmost
($v$) and the rightmost ($s=\tau(i)$) ones. This is case 2b, and
$\Leftarrow(\varphi,\psi)$ holds in $s$.

###  0.C.3 POTL Translation of OPTL

As an alternative proof of Corollary 2, we provide a direct translation of
OPTL into POTL. We define function $\nu$, which given an OPTL formula
$\varphi$, yields a POTL formula $\nu(\varphi)$ such that, for any OP word $w$
and position $i$, we have $(w,i)\models\varphi$ iff
$(w,i)\models\nu(\varphi)$. $\nu$ is defined as the identity for propositional
operators. In the following, we use the abbreviations
$\varphi^{\prime}\equiv\nu(\varphi)$ and $\psi^{\prime}\equiv\nu(\psi)$.

$\displaystyle\nu(\ocircle\varphi)$
$\displaystyle\equiv\ocircle^{\lessdot\doteq\gtrdot}\varphi^{\prime}$
$\displaystyle\nu(\circleddash\varphi)$
$\displaystyle\equiv\circleddash^{\lessdot\doteq\gtrdot}\varphi^{\prime}$
$\displaystyle\nu(\ocircle_{\chi}\varphi)$
$\displaystyle\equiv\chi_{F}^{\doteq\gtrdot}\varphi^{\prime}$
$\displaystyle\nu(\circleddash_{\chi}\varphi)$
$\displaystyle\equiv\chi_{P}^{\lessdot\doteq}\varphi^{\prime}$

The translation for LTL until and since is much more involved:

$\nu(\varphi\mathbin{\mathcal{U}}\psi)\equiv\psi^{\prime}\lor\big{(}\varphi^{\prime}\land\alpha(\varphi^{\prime})\big{)}\mathbin{\mathcal{U}^{\doteq\gtrdot}}\big{(}\psi^{\prime}\lor(\varphi^{\prime}\land\beta(\varphi^{\prime}))\mathbin{\mathcal{U}^{\lessdot\doteq}}(\psi^{\prime}\land\beta(\varphi^{\prime}))\big{)}$

where

$\displaystyle\alpha(\varphi^{\prime})$
$\displaystyle\equiv\chi_{F}^{\doteq\gtrdot}\top\implies\neg\big{(}\ocircle^{\lessdot}(\top\mathbin{\mathcal{U}^{\lessdot\doteq}}\neg\varphi^{\prime})\lor\chi_{F}^{\lessdot}(\top\mathbin{\mathcal{U}^{\lessdot\doteq}}\neg\varphi^{\prime})\big{)}$
$\displaystyle\beta(\varphi^{\prime})$
$\displaystyle\equiv\chi_{P}^{\lessdot\doteq}\top\implies\neg\big{(}\circleddash^{\gtrdot}(\top\mathbin{\mathcal{S}^{\doteq\gtrdot}}\neg\varphi^{\prime})\lor\chi_{P}^{\gtrdot}(\top\mathbin{\mathcal{S}^{\doteq\gtrdot}}\neg\varphi^{\prime})\big{)}$

The main formula is the concatenation of two OP summary until operators. The
first one only admits the $\doteq$ and $\gtrdot$ PR: it can only go upwards in
the chain structure. Whenever one of its paths contains the left context of a
chain, either the path ends there or it continues with the right context of
that chain. The second until only admits $\doteq$ and $\lessdot$. It can
therefore go downwards in the chain structure, and whenever one of its paths
contains a right chain context, it must contain the left context too.

When evaluated in the left context of a chain, subformula $\alpha(\varphi)$
makes sure $\varphi^{\prime}$ holds in all positions of the body of the
outermost (forward maximal) chain starting in that position (i.e. the one
whose left and right contexts are in the $\doteq$ or $\gtrdot$ relation).
Therefore, including it in the left side of the first until makes sure
$\varphi^{\prime}$ holds in all chain bodies skipped by its paths.

Symmetrically, when evaluated in the right context of a chain,
$\beta(\varphi)$ makes sure $\varphi^{\prime}$ holds in all positions in the
body of the outermost (backward-maximal) chain ending there. It is included in
both sides of the second until, so that $\varphi^{\prime}$ holds in all chain
bodies skipped by its paths.

The translation for the since operator is symmetric.

The translations of the summary operators changes depending on the allowed PR.
The main difference between the semantics of OPS until in OPTL and POTL is
that, in the former, PR are checked only on consecutive positions, and the
path can follow all “maximal” chains, whose contexts are in the $\doteq$ or
$\gtrdot$ relations. In POTL, the allowed PR must holds between all positions
consecutive in the path, including contexts of the same chain, and the
$\lessdot$ relation is also allowed in this case. Since maximal chains have
their contexts in the $\doteq$ or $\gtrdot$ relations, we have

$\nu(\varphi\mathbin{\mathcal{U}^{\doteq\gtrdot}}\psi)\equiv\varphi^{\prime}\mathbin{\mathcal{U}^{\doteq\gtrdot}}\psi^{\prime}.$

When only one of such relation is allowed, we must prevent the path from
spanning consecutive positions in the wrong relation.

$\displaystyle\nu(\varphi\mathbin{\mathcal{U}^{\doteq}}\psi)$
$\displaystyle\equiv(\varphi^{\prime}\land\neg\ocircle^{\gtrdot}\top)\mathbin{\mathcal{U}^{\doteq\gtrdot}}\psi^{\prime}$
$\displaystyle\nu(\varphi\mathbin{\mathcal{U}^{\gtrdot}}\psi)$
$\displaystyle\equiv(\varphi^{\prime}\land\neg\ocircle^{\doteq}\top)\mathbin{\mathcal{U}^{\doteq\gtrdot}}\psi^{\prime}$

Things become more complicated when the $\lessdot$ relation is also allowed.

$\displaystyle\nu(\varphi\mathbin{\mathcal{U}^{\lessdot\doteq\gtrdot}}\psi)$
$\displaystyle\equiv\varphi^{\prime}\mathbin{\mathcal{U}^{\doteq\gtrdot}}[\psi^{\prime}\lor(\varphi^{\prime}\land\gamma(\varphi^{\prime}))\mathbin{\mathcal{U}^{\lessdot\doteq\gtrdot}}(\psi\land\gamma(\varphi^{\prime}))]$
$\displaystyle\gamma(\varphi^{\prime})$
$\displaystyle\equiv\chi_{P}^{\lessdot}\top\implies[\circleddash^{\lessdot}_{H}(\boxminus^{\lessdot}_{H}(\varphi^{\prime}\land\square^{\doteq}\varphi^{\prime}))\land\chi_{P}^{\lessdot}\ocircle^{\lessdot}\square^{\doteq}\varphi^{\prime}]$

where
$\boxminus^{\lessdot}_{H}\theta\equiv\neg[\top\mathbin{\mathcal{S}^{\lessdot}_{H}}(\neg\theta)]$,
and
$\square^{\doteq}\theta\equiv\neg[\top\mathbin{\mathcal{U}^{\doteq}}(\neg\theta)]$.

In this case, we must make up for the fact that OPSP in POTL can skip bodies
of chain whose contexts are in the $\lessdot$ relation, while OPTL cannot. In
such cases, OPSP in OPTL continue by following the successor edge. So, we
split an OPSP in a path that goes only upwards in the abstract syntax tree
(the first until with $\doteq\gtrdot$), followed by one that can go downwards.
In the latter, $\gamma(\varphi^{\prime})$ must also hold. Let $i$ be a
position in an OPSP, and let $j_{p}$, $1\leq p\leq n$, be all positions such
that $\chi(i,j_{p})$ and $i\lessdot j_{p}$. Suppose $j_{q}$, $1\leq q\leq n$,
is also part of the OPSP. Formula $\gamma(\varphi^{\prime})$, if evaluated in
$i_{q}$, enforces $\varphi^{\prime}$ to hold in all positions that the OPTL
OPSP would span between $i$ and $j_{q}$.
$\circleddash^{\lessdot}_{H}(\boxminus^{\lessdot}_{H}(\varphi^{\prime}\land\square^{\doteq}\varphi^{\prime}))$
enforces $\varphi^{\prime}$ to hold in all right hand sides (rhs) starting
with $j_{k}$, $1\leq k<q$ (note that $\square^{\doteq}$ only considers the
rhs, without entering inner chains).
$\chi_{P}^{\lessdot}\ocircle^{\lessdot}\square^{\doteq}\varphi^{\prime}$
enforces $\varphi^{\prime}$ in the rhs starting in $i+1$.

For other PR combinations containing $\lessdot$, it suffices to forbid
consecutive positions in the wrong relation. For
$\nu(\varphi\mathbin{\mathcal{U}^{\lessdot\doteq}}\psi)$ and
$\nu(\varphi\mathbin{\mathcal{U}^{\lessdot\gtrdot}}\psi)$, just substitute
$\varphi^{\prime}$ with, respectively,
$\varphi^{\prime}\land\neg\ocircle^{\gtrdot}\top$ and
$\varphi^{\prime}\land\neg\ocircle^{\doteq}\top$ in
$\nu(\varphi\mathbin{\mathcal{U}^{\lessdot\doteq\gtrdot}}\psi)$.

The translations for hierarchical operators just need to take into account
that, in OPTL, they are evaluated in the opposite chain context.

$\displaystyle\nu(\varphi\mathbin{\mathcal{U}^{\uparrow}}\psi)$
$\displaystyle\equiv\chi_{F}^{\lessdot}[\neg\circleddash^{\lessdot}_{H}\top\land\varphi^{\prime}\mathbin{\mathcal{U}^{\lessdot}_{H}}\psi^{\prime}]$
$\displaystyle\nu(\varphi\mathbin{\mathcal{S}^{\downarrow}}\psi)$
$\displaystyle\equiv\chi_{F}^{\lessdot}[\neg\ocircle^{\lessdot}_{H}\top\land\varphi^{\prime}\mathbin{\mathcal{S}^{\lessdot}_{H}}\psi^{\prime}]$

The translations for the take precedence hierarchical until and since are
symmetric.

##  Appendix 0.D Omitted Proofs: Model Checking

In this section, we prove the correctness of the model checking OPA
construction of Section 5, and we give the construction for operators omitted
in the main text.

######  Theorem 0.D.1 (Correctness of Finite Model Checking.)

Given a finite set of atomic propositions $AP$, an OP alphabet
$({\mathcal{P}(AP)},\allowbreak M_{\mathcal{P}(AP)})$, a word $w$ on it, and
an POTL formula $\varphi$, the automaton built according to the procedure in
this section is such that we have

$(w,1)\models\varphi$

if and only if it performs at least one accepting computation on a word
$w^{\prime}$ equal to $w$, except for the presence of one more propositional
symbol for each hierarchical operator in $\varphi$.

###### Proof

In the following, we prove that all chain next/back operators hold in a