Prophecies All the Way: Game-Based Model-Checking for HyperQPTL Beyond ∀*∃*

Winter, Sarah; Zimmermann, Martin

doi:10.4230/LIPIcs.CONCUR.2025.37

Prophecies All the Way: Game-Based
Model-Checking for HyperQPTL Beyond ${\forall^{}\exists^{}}$

Sarah Winter

IRIF, Université Paris Cité, Paris, France Martin Zimmermann

Aalborg University, Denmark

Abstract

Model-checking HyperLTL, a temporal logic expressing properties of sets of traces with applications to information-flow based security and privacy, has a decidable, but TOWER-complete, model-checking problem. While the classical model-checking algorithm for full HyperLTL is automata-theoretic, more recently, a game-based alternative for the $\forall^{*}\exists^{*}$ -fragment has been presented.

Here, we employ imperfect information-games to extend the game-based approach to full HyperQPTL, which features arbitrary quantifier prefixes and quantification over propositions and can express every $\omega$ -regular hyperproperty. As a byproduct of our game-based algorithm, we obtain finite-state implementations of Skolem functions via transducers with lookahead that explain satisfaction or violation of HyperQPTL properties.

Keywords and phrases:

HyperLTL, HyperQPTL, model-checking games, prophecies

Funding:

Martin Zimmermann: Supported by DIREC - Digital Research Centre Denmark.

Copyright and License:

2012 ACM Subject Classification:

Theory of computation

\rightarrow

Logic and verification ; Theory of computation

\rightarrow

Modal and temporal logics ; Theory of computation

\rightarrow

Verification by model checking

Editors:

Patricia Bouyer and Jaco van de Pol

Series and Publisher:

Leibniz International Proceedings in Informatics, Schloss Dagstuhl – Leibniz-Zentrum für Informatik

1 Introduction

Hyperlogics like HyperLTL and HyperCTL^∗ [6] extend their classical counterparts LTL [20] and CTL^∗ [10] by trace quantification and are thereby able to express so-called hyperproperties [7], properties which relate multiple execution traces of a system. These are crucial for expressing information-flow properties capturing security and privacy requirements [6]. For example, generalized noninterference [19] is captured by the HyperLTL formula

\varphi_{\mathrm{GNI}}=\forall\pi.\ \forall\pi^{\prime}.\ \exists\pi^{\prime% \prime}.\ \mathop{\mathbf{G}\vphantom{a}}\nolimits\left(\bigwedge\nolimits_{% \texttt{p}\in L_{\mathrm{in}}\cup L_{\mathrm{out}}}\texttt{p}_{\pi}% \leftrightarrow\texttt{p}_{\pi^{\prime\prime}}\right)\wedge\mathop{\mathbf{G}% \vphantom{a}}\nolimits\left(\bigwedge\nolimits_{\texttt{p}\in H_{\mathrm{in}}}% \texttt{p}_{\pi^{\prime}}\leftrightarrow\texttt{p}_{\pi^{\prime\prime}}\right)

expressing that for all traces $\pi$ and $\pi^{\prime}$ there exists a trace $\pi^{\prime\prime}$ that agrees with the low-security inputs (propositions in $L_{\mathrm{in}}$ ) and low-security outputs (propositions in $L_{\mathrm{out}}$ ) of $\pi$ and the high-security inputs (propositions in $H_{\mathrm{in}}$ ) of $\pi^{\prime}$ . Intuitively, it is satisfied if every input-output behavior observable by a low-security user of a system is compatible with any sequence of high-security inputs, i.e., the low security input-output behavior does not leak information about the high-security inputs, which should indeed be unobservable (directly and indirectly) by a low-security user.

These expressive logics offer a uniform approach to the specification, analysis, and verification of hyperproperties with intuitive syntax and semantics, and a decidable [6], albeit Tower-complete [22, 18], model-checking problem. The classical model-checking algorithm [6] is automata-based and even the case of $\forall^{*}\exists^{*}$ -formulas like $\varphi_{\mathrm{GNI}}$ requires the complementation of $\omega$ -automata, a famously challenging construction to implement.

As an alternative, it is beneficial to draw upon the deep connections between logic and games. Consider a HyperLTL formula of the form $\forall\pi.\ \exists\pi^{\prime}.\psi$ with quantifier-free $\psi$ . It is straightforward to capture the semantics of HyperLTL by a model-checking game between two players called Verifier (trying to prove $\mathfrak{T}\models\varphi$ ) and Falsifier (trying to prove $\mathfrak{T}\not\models\varphi$ ). In the model-checking game, Falsifier picks a trace of $\mathfrak{T}$ to interpret $\pi$ and then Verifier picks a trace of $\mathfrak{T}$ to interpret $\pi^{\prime}$ . Verifier wins if these two traces satisfy the formula $\psi$ , otherwise Falsifier wins. The game can easily be shown sound (if Verifier wins, then $\mathfrak{T}\models\varphi$ ) and complete (if $\mathfrak{T}\models\varphi$ then Verifier wins), as winning strategies for Verifier are Skolem functions for $\pi^{\prime}$ and vice versa. But the game has one major drawback: both players have in general uncountably many possible moves as they are picking traces.

To obtain a game that can be handled algorithmically, Coenen et al. introduced the following variation of the model-checking game [8] (which we will call the alternating game): Instead of picking the traces of $\mathfrak{T}$ in one move, the players construct them alternatingly one vertex at a time. Together with a deterministic $\omega$ -automaton that is equivalent to $\psi$ , this yields a finite game with $\omega$ -regular winning condition that is sound, but possibly incomplete ( $\mathfrak{T}\models\varphi$ does not always imply that Verifier wins the alternating game).

The problem boils down to the informedness of Verifier: In the model-checking game, she has knowledge about the full trace assigned to $\pi$ when picking $\pi^{\prime}$ . On the other hand, in the alternating game, Verifier only has access to the first vertex of the trace assigned to $\pi$ when picking the first vertex of the trace assigned to $\pi^{\prime}$ , which puts her at a disadvantage. That the alternating game can be incomplete is witnessed by the formula

\varphi_{\mathrm{inc}}=\forall\pi.\ \exists\pi^{\prime}.\ \texttt{p}_{\pi^{% \prime}}\leftrightarrow\mathop{\mathbf{F}\vphantom{a}}\nolimits\texttt{p}_{\pi}

expressing that for every trace $\pi$ in $\mathfrak{T}$ there is a trace $\pi^{\prime}$ in $\mathfrak{T}$ such that p holds at the first position of $\pi^{\prime}$ if and only if there is a p somewhere in $\pi$ , i.e., the first letter of $\pi^{\prime}$ depends (possibly) on every letter of $\pi$ . So, by not picking a p in the first round, Falsifier forces Verifier to make a prediction about whether Falsifier will ever pick a p or not in the future. However, Falsifier can easily contradict that prediction and thereby win, e.g., for a transition system $\mathfrak{T}_{\mathrm{all}}$ having all traces over p. Thus, we indeed have $\mathfrak{T}_{\mathrm{all}}\models\varphi$ , but Verifier does not win the alternating game.

However, a single bit of lookahead allows Verifier to win the alternating game induced by $\mathfrak{T}_{\mathrm{all}}$ and $\varphi_{\mathrm{inc}}$ , i.e., the answer to the query “will the trace picked by Falsifier contain a p”. If Falsifier has to provide this information with his first move, then Verifier can make her first move accordingly. For correctness, we additionally have to adapt the rules of the alternating game so that Falsifier loses when contradicting his answer made during the first round, e.g., if he commits to there being no p’s in his trace, but then picking one.

In general, it is not sufficient to ask a single query at the beginning of a play, but one needs to ask queries at every move of Falsifier. To see this, let us consider another example, this time with the formula

\varphi_{\mathrm{inc}}^{\prime}=\forall\pi.\ \exists\pi^{\prime}.\ \mathop{% \mathbf{G}\vphantom{a}}\nolimits(\texttt{p}_{\pi^{\prime}}\leftrightarrow% \mathop{\mathbf{X}\vphantom{a}}\nolimits\texttt{p}_{\pi}).

Here, Verifier has to always pick a p in her move if and only if Falsifier will pick a p in his next move (which Verifier does not have yet access to). Thus, Verifier wins if she gets the (truthful) answer to the query “does the next move by Falsifier contain a p”, but loses without the ability to query Falsifier. Note that in both cases, the queries are used to obtain a (binding) commitment about the future moves that Falsifier will make.

Coenen et al. [8] and Beutner and Finkbeiner [5] showed how to formalize this intuition using so-called prophecies [1]. A single prophecy is a language $P$ of traces and is associated with a (Boolean) prophecy variable. Now, in addition to picking, vertex by vertex, a trace of $\mathfrak{T}$ , Falsifier also picks a truth value for the prophecy variable with the interpretation that a value of $1$ corresponds to the suffix of the trace picked by him from now on being in $P$ and that a value of of $0$ corresponds to the suffix of the trace picked by him from now on not being in $P$ . If the language $P$ is $\omega$ -regular, then one can employ an $\omega$ -automaton to check whether the predictions made by Falsifier are actually truthful (and make him lose if they are not truthful). We call the resulting game the alternating game with prophecies. Intuitively, it constitutes a middle-ground between the naive game where both players pick traces and the alternating game (without prophecies). The former is sound and complete, but not finite-state while the latter is sound and finite-state, but not complete.

The alternating game with (finitely many) $\omega$ -regular prophecies is sound and finite-state and Beutner and Finkbeiner showed that for every $\forall^{*}\exists^{*}$ -formula there is a finite and effectively computable set of $\omega$ -regular prophecies such that Verifier wins the alternating game with these prophecies if and only if $\mathfrak{T}\models\varphi$ , i.e., there are always prophecies that make the alternating game-based approach to model-checking also complete. Furthermore, the resulting game with prophecies has a $\omega$ -regular winning condition, and can therefore be solved effectively. Note that this construction is still automata-based, as the prophecies are derived from a (deterministic) $\omega$ -automaton for the quantifier-free part of $\varphi$ . Beutner and Finkbeiner implemented their prophecy-based model-checking algorithm and presented encouraging results on small instances, e.g., their prototype implementation is in some cases the first tool that can prove $\mathfrak{T}\not\models\varphi$ , a result that was out of reach for existing model-checking tools [5]. These results shows the potential of the game-based approach to HyperLTL model-checking.

However, one question remains open: can the alternating game-based approach be extended to full HyperLTL, i.e., beyond a single quantifier alternation. There is precedent for such a game-based analysis of full HyperLTL: Recently, Winter and Zimmermann showed that the existence of (Turing) computable Skolem functions for existentially quantified variables can be characterized by a game [24]. For example, $\mathfrak{T}_{\mathrm{all}}\models\varphi_{\mathrm{inc}}^{\prime}$ is witnessed by computable Skolem functions, as reading a prefix of length $n$ of $\pi$ allows to compute the prefix of length $n-1$ of $\pi^{\prime}$ so that for every $\pi$ , $\pi$ and the resulting $\pi^{\prime}$ satisfy $\mathop{\mathbf{G}\vphantom{a}}\nolimits(\texttt{p}_{\pi^{\prime}}% \leftrightarrow\mathop{\mathbf{X}\vphantom{a}}\nolimits\texttt{p}_{\pi})$ . On the other hand, $\mathfrak{T}_{\mathrm{all}}\models\varphi_{\mathrm{inc}}$ is not witnessed by computable Skolem functions, as the choice of the first letter of $\pi^{\prime}$ depends, as explained above, on all letters of $\pi^{\prime}$ . Such a Skolem function is not computable by a Turing machine, as it is not continuous.

The game characterizing the existence of computable Skolem functions, say for a formula

\varphi=\forall\pi_{0}.\ \exists\pi_{1}.\ \ldots\forall\pi_{k-2}.\ \exists\pi_% {k-1}.\ \psi

with quantifier-free $\psi$ , is a multi-player game played between a player in charge of selecting, vertex by vertex, a trace for each universally quantified variable (i.e., he has the role that Falsifier has in the previous games), and a coalition of players, one for each existentially quantified variable (i.e., the coalition has the role that Verifier has in the previous games). Furthermore, the game must be of imperfect information in order to capture the semantics of HyperLTL, where the choice of $\pi_{i}$ may only depend on the choice of the $\pi_{j}$ with $j<i$ . Thus, in the game, the player in charge of an existentially quantified $\pi_{i}$ only has access to the choices made so far for the $\pi_{j}$ for $j<i$ . Furthermore, the game needs to incorporate a delay [16, 17, 12] between the moves of the different players to capture the fact that a choice by one of the existential players may depend on future moves by the universal player (see, e.g., the formula $\varphi_{\mathrm{inc}}^{\prime}$ above). The main insight then is that a bounded delay is always sufficient, if there are computable Skolem functions at all (see, again, the difference between $\varphi_{\mathrm{inc}}$ (which has no computable Skolem functions over $\mathfrak{T}_{\mathrm{all}}$ ) and $\varphi_{\mathrm{inc}}^{\prime}$ (which has computable Skolem functions over $\mathfrak{T}_{\mathrm{all}}$ )).

Our Contribution.

We present the first effective game-based characterization of model-checking for full HyperLTL (and even HyperQPTL, which allows to express all $\omega$ -regular hyperproperties [22, 13]), yielding a sound and complete imperfect information finite-state game with $\omega$ -regular winning condition. This result generalizes both the alternating game with prophecies from $\forall^{*}\exists^{*}$ -formulas to formulas with arbitrary quantifier prefixes and the game of Winter and Zimmermann from characterizing the existence of computable Skolem functions witnessing $\mathfrak{T}\models\varphi$ to characterizing $\mathfrak{T}\models\varphi$ .

However, since $\mathfrak{T}\models\varphi_{\mathrm{inc}}$ holds, but does not have computable Skolem functions, the games of Winter and Zimmermann are not a special case of the games we construct here: Our games here are still multi-player games of imperfect information (to capture the semantics of quantification) and use prophecies (for completeness), but do not require delayed moves, as prophecies can be seen as a (restricted) form of infinite lookahead. And while the existence of computable Skolem functions is concerned with bounded lookahead, here we do indeed need infinite lookahead as witnessed by the formula $\varphi_{\mathrm{inc}}$ .

Our main result shows that there is again a finite and effectively computable set of $\omega$ -regular prophecies so that the coalition of players in charge of the existentially quantified variables has a winning strategy in the game with these prophecies if and only if $\mathfrak{T}\models\varphi$ . One challenge to overcome here is a careful definition of the prophecies, so that they are not leaking any information about choices for variables $\pi_{j}$ that a player in charge of $\pi_{i}$ with $i<j$ must not have access to.

Our result can also be framed in terms of Skolem function implementable by letter-to-letter transducers with ( $\omega$ -regular) lookahead: such a transducer computes a Skolem function for an existentially quantified variable $\pi$ while reading values for the variables universally quantified before $\pi$ while also being able to get a regular lookahead on the trace for those universally quantified variable (much like prophecies). The use of regular lookahead is well-studied in automata theory, see e.g., [9, 11, 3].

All proofs omitted due to space restrictions can be found in the full version [25].

2 Preliminaries

For convenience, technical terms and notations in the electronic version of this manuscript are hyper-linked to their definitions (cf. https://ctan.org/pkg/knowledge).

Hereafter, we denote the set of nonnegative integers by $\mathbbm{N}$ .

Traces, Transition Systems, and Automata.

An alphabet is a nonempty finite set. The sets of finite and infinite words over an alphabet $\Sigma$ are denoted by $\Sigma^{*}$ and $\Sigma^{\omega}$ , respectively. The length of finite or infinite word $w$ is denoted by $|w|\in\mathbbm{N}\cup\{\infty\}$ . For a word $w$ of length at least $n$ , we write $w[0,n)$ for the prefix of $w$ of length $n$ . Given $n$ infinite words $w_{0},\ldots,w_{n-1}$ , let their merge (also known as zip), which is an infinite word over $\Sigma^{n}$ , be defined as

{\immediate\immediate\immediate{\color[rgb]{0,0,1}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,1}\mathrm{mrg}}(w_{0},\ldots,w_{n-1})}=(w_{0}(0),% \ldots,w_{n-1}(0))(w_{0}(1),\ldots,w_{n-1}(1))(w_{0}(2),\ldots,w_{n-1}(2))\cdots.

We define ${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathrm{mrg% }}(w_{0},\ldots,w_{n-1})}$ for finite words $w_{0},\ldots,w_{n-1}$ of the same length analogously.

Let $\mathrm{AP}$ be a nonempty finite set of atomic propositions. A trace over $\mathrm{AP}$ is an infinite word over the alphabet $2^{\mathrm{AP}}$ . Given a subset $\mathrm{AP}^{\prime}\subseteq\mathrm{AP}$ , the $\mathrm{AP}^{\prime}$ -projection of a trace $t(0)t(1)t(2)\cdots$ over $\mathrm{AP}$ is the trace $(t(0)\cap\mathrm{AP}^{\prime})(t(1)\cap\mathrm{AP}^{\prime})(t(2)\cap\mathrm{% AP}^{\prime})\cdots\in(2^{\mathrm{AP}^{\prime}})^{\omega}$ . Now, let $\mathrm{AP}$ and $\mathrm{AP}^{\prime}$ be two disjoint sets, let $t$ be a trace over $\mathrm{AP}$ , and let $t^{\prime}$ be a trace over $\mathrm{AP}^{\prime}$ . Then, we define $t^{\smallfrown}t^{\prime}$ as the pointwise union of $t$ and $t^{\prime}$ , i.e., $t^{\smallfrown}t^{\prime}$ is the trace over $\mathrm{AP}\cup\mathrm{AP}^{\prime}$ defined as $(t(0)\cup t^{\prime}(0))(t(1)\cup t^{\prime}(1))(t(2)\cup t^{\prime}(2))\cdots$ .

A transition system $\mathfrak{T}=(V,E,V_{I},\lambda)$ consists of a finite set $V$ of vertices, a set $E\subseteq V\times V$ of (directed) edges, a nonempty set $V_{I}\subseteq V$ of initial vertices, and a labelling $\lambda\colon V\rightarrow 2^{\mathrm{AP}}$ of the vertices by sets of atomic propositions. We assume that every vertex has at least one outgoing edge. For $v\in V$ , we denote by $\mathrm{S}(v)$ the set of its successors. A path $\rho$ through $\mathfrak{T}$ is an infinite sequence $\rho=v_{0}v_{1}v_{2}\cdots$ of vertices with $v_{0}\in V_{I}$ and $(v_{n},v_{n+1})\in E$ for every $n\geq 0$ . The trace of $\rho$ is defined as $\lambda(\rho)=\lambda(v_{0})\lambda(v_{1})\lambda(v_{2})\cdots\in(2^{\mathrm{% AP}})^{\omega}$ . The set of traces of $\mathfrak{T}$ is ${\immediate{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}% \mathrm{Tr}}(\mathfrak{T})}=\{\lambda(\rho)\mid\rho\text{ is a {\color[rgb]{% 0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}path} of $\mathfrak{T% }$}\}$ . For $V^{\prime}\subseteq V$ , we write $\mathfrak{T}_{V^{\prime}}$ to denote the transition system $(V,E,V^{\prime},\lambda)$ obtained from $\mathfrak{T}$ by making $V^{\prime}$ the set of initial states, and use $\mathfrak{T}_{v}$ as shorthand for $\mathfrak{T}_{\{v\}}$ for $v\in V$ .

A (deterministic) parity automaton¹¹1Note that we use parity acceptance, as we need deterministic automata for our proofs. $\mathcal{A}=(Q,\Sigma,q_{I},\delta,\Omega)$ consists of a finite set $Q$ of states containing the initial state $q_{I}\in Q$ , an alphabet $\Sigma$ , a transition function $\delta\colon Q\times\Sigma\rightarrow Q$ , and a coloring $\Omega\colon Q\rightarrow\mathbbm{N}$ of its states by natural numbers. Let $w=w(0)w(1)w(2)\cdots\in\Sigma^{\omega}$ . The run of $\mathcal{A}$ on $w$ is the sequence $q_{0}q_{1}q_{2}\cdots$ with $q_{0}=q_{I}$ and $q_{n+1}=\delta(q_{n},w(n))$ for all $n\geq 0$ . A run $q_{0}q_{1}q_{2}\cdots$ is (parity) accepting if the maximal color appearing infinitely often in the sequence $\Omega(q_{0})\Omega(q_{1})\Omega(q_{2})\cdots$ is even. The language (parity) recognized by $\mathcal{A}$ , denoted by $L(\mathcal{A})$ , is the set of infinite words over $\Sigma$ such that the run of $\mathcal{A}$ on $w$ is accepting.

$\blacktriangleright$ Remark 1.

Deterministic parity automata accept exactly the $\omega$ -regular languages (see, e.g., [15] for definitions).

HyperQPTL, HyperLTL and QPTL.

Let ${\immediate\immediate\immediate{\color[rgb]{0,0,1}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,1}\mathcal{V}}}$ be a countable set of trace variables. The formulas of HyperQPTL are given by the grammar

\displaystyle\varphi\mathop{::=}{}\exists\pi.\ \varphi\mid\forall\pi.\ \varphi% \mid\psi\qquad\psi\mathop{::=}{}\tilde{\exists}\texttt{q}.\ \psi\mid\tilde{% \forall}\texttt{q}.\ \psi\mid\psi\mid\texttt{p}_{\pi}\mid\texttt{q}\mid\lnot% \psi\mid\psi\lor\psi\mid\mathop{\mathbf{X}\vphantom{a}}\nolimits\psi\mid\psi% \operatorname{\mathbf{U}}\psi

where p and q range over $\mathrm{AP}$ and where $\pi$ ranges over ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {V}}$ . Here, we use a tilde to decorate propositional quantifiers to distinguish them from trace quantifiers.

Note that there are two types of atomic formulas, i.e., propositions labeled by trace variables on which they are evaluated ( $\texttt{p}_{\pi}$ with $\texttt{p}\in\mathrm{AP}$ and $\pi\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathcal{V}}$ ) and unlabeled propositions ( $\texttt{q}\in\mathrm{AP}$ ).²²2We use different letters in these cases, but let us stress again that both p and q are propositions in $\mathrm{AP}$ . A formula is a sentence, if every occurrence of an atomic formula $\texttt{p}_{\pi}$ is in the scope of a quantifier binding $\pi$ (otherwise $\pi$ is said to be a free trace variable) and every occurrence of an atomic formula q is in the scope of a quantifier binding q (otherwise q is said to be a free propositional variable). Note that the proposition p in an atomic formula $\texttt{p}_{\pi}$ is not considered free. Finally, we use the usual syntactic sugar like conjunction ( $\wedge$ ), implication ( $\rightarrow$ ), equivalence ( $\leftrightarrow$ ), eventually ( $\mathop{\mathbf{F}\vphantom{a}}\nolimits$ ), and always ( $\mathop{\mathbf{G}\vphantom{a}}\nolimits$ ).

A (trace) variable assignment is a partial mapping $\Pi\colon{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7% }\mathcal{V}}\rightarrow(2^{\mathrm{AP}})^{\omega}$ . Given a variable $\pi\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathcal{V}}$ , and a trace $t$ , we denote by $\Pi[\pi\mapsto t]$ the assignment that coincides with $\Pi$ on all variables but $\pi$ , which is mapped to $t$ . Let $\texttt{q}\in\mathrm{AP}$ , let $t\in(2^{\mathrm{AP}})^{\omega}$ be a trace over $\mathrm{AP}$ , and let $t_{\texttt{q}}\in(2^{\{\texttt{q}\}})^{\omega}$ be a trace over $\{\texttt{q}\}$ . We define the trace $t[\texttt{q}\mapsto t_{\texttt{q}}]=t^{\prime}{}^{\smallfrown}t_{\texttt{q}}$ , where $t^{\prime}$ is the $(\mathrm{AP}\setminus\{\texttt{q}\})$ -projection of $t$ : Intuitively, the occurrences of q in $t$ are replaced according to $t_{\texttt{q}}$ . We lift this to sets $T$ of traces by defining $T[\texttt{q}\mapsto t_{\texttt{q}}]=\{t[\texttt{q}\mapsto t_{\texttt{q}}]\mid t% \in T\}$ . Note that all traces in $T[\texttt{q}\mapsto t_{\texttt{q}}]$ have the same $\{\texttt{q}\}$ -projection, which is $t_{\texttt{q}}$ .

Now, for a trace assignment $\Pi$ , a position $i\in\mathbbm{N}$ , and a nonempty set $T$ of traces, i.e., we disregard the empty set of traces as model, we define

$\blacksquare$

$T,\Pi,i\models\texttt{p}_{\pi}$ if $\texttt{p}\in\Pi(\pi)(i)$ ,
$\blacksquare$

$T,\Pi,i\models\texttt{q}$ if for all $t\in T$ we have $\texttt{q}\in t(i)$ ,
$\blacksquare$

$T,\Pi,i\models\lnot\psi$ if $T,\Pi,i\not\models\psi$ ,
$\blacksquare$

$T,\Pi,i\models\psi_{1}\lor\psi_{2}$ if $T,\Pi,i\models\psi_{1}$ or $T,\Pi,i\models\psi_{2}$ ,
$\blacksquare$

$T,\Pi,i\models\mathop{\mathbf{X}\vphantom{a}}\nolimits\psi$ if $T,\Pi,i+1\models\psi$ ,
$\blacksquare$

$T,\Pi,i\models\psi_{1}\operatorname{\mathbf{U}}\psi_{2}$ if there is a $j\geq i$ such that $T,\Pi,j\models\psi_{2}$ and $T,\Pi,j^{\prime}\models\psi_{1}$ for all $i\leq j^{\prime}<j$ ,
$\blacksquare$

$T,\Pi,i\models\tilde{\exists}\texttt{q}.\ \psi$ if there exists a trace $t_{\texttt{q}}\in(2^{\{\texttt{q}\}})^{\omega}$ such that $T[\texttt{q}\mapsto t_{\texttt{q}}],\Pi,i\models\psi$ ,
$\blacksquare$

$T,\Pi,i\models\tilde{\forall}\texttt{q}.\ \psi$ if for all traces $t_{\texttt{q}}\in(2^{\{\texttt{q}\}})^{\omega}$ we have $T[\texttt{q}\mapsto t_{\texttt{q}}],\Pi,i\models\psi$ ,
$\blacksquare$

$T,\Pi,i\models\exists\pi.\,\varphi$ if there exists a trace $t\in T$ such that $T,\Pi[\pi\mapsto t],i\models\varphi$ , and
$\blacksquare$

$T,\Pi,i\models\forall\pi.\ \varphi$ if for all traces $t\in T$ we have $T,\Pi[\pi\mapsto t],i\models\varphi$ .

We say that an (again nonempty) set $T$ of traces satisfies a sentence $\varphi$ , written $T\models\varphi$ , if $T,\Pi_{\emptyset},0\models\varphi$ where $\Pi_{\emptyset}$ is the variable assignment with empty domain. We then also say that $T$ is a model of $\varphi$ . A transition system $\mathfrak{T}$ satisfies $\varphi$ , written $\mathfrak{T}\models\varphi$ , if ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{% Tr}}(\mathfrak{T})\models\varphi$ . Let $\psi$ be a trace quantifier-free formula that has no free (unlabeled) propositions. A labeled proposition of the form $\texttt{p}_{\pi}$ in $\psi$ is evaluated on the traces assigned to $\pi$ and an unlabeled proposition of the form q is evaluated on a trace “selected” by the quantifier binding q. Hence, $T,\Pi,i\models\psi$ is independent of $T$ and we often write $\Pi\models\psi$ instead of $T,\Pi,0\models\psi$ .

Some comments on the definition of HyperQPTL are due.

$\blacktriangleright$ Remark 2.

We have, for technical reasons, defined HyperQPTL so that every formula has a prefix of trace quantifiers followed by a formula (possibly) containing propositional quantifiers, but no more trace quantifiers. On the other hand, Finkbeiner et al. [13] require formulas to be in prenex normal form, but allow to mix trace and propositional quantification in the quantifier prefix. We refrained from doing so, as one can duplicate the vertices of the transition system one is interested in, so that it has enough paths to simulate propositional quantification by trace quantification, and can adapt the formula correspondingly. This construction has a linear blowup.

$\blacktriangleright$ Remark 3.

HyperLTL is the fragment of HyperQPTL sentences that do not use the propositional quantifiers $\tilde{\exists}$ and $\tilde{\forall}$ (and thus also not use unlabeled propositions).

We say that a HyperQPTL formula $\varphi$ is a QPTL sentence if it has no trace quantifiers and no free propositional variables, i.e., all unlabeled propositional variables are in the scope of a propositional quantifier. But a QPTL sentence may have free trace variables, say $\pi_{0},\ldots,\pi_{k-1}$ for some $k\geq 0$ . Typically, QPTL is defined without trace variables labelling propositions and QPTL formulas define languages over the alphabet $2^{\mathrm{AP}}$ [23]. For technical necessity, we allow such labels, which implies that our formulas define languages over the alphabet $(2^{\mathrm{AP}})^{k}$ , where $k$ is the number of trace variables occurring in the formula. More formally, a QPTL sentence with trace variables $\pi_{0},\pi_{1},\ldots,\pi_{k-1}$ defines the language

L(\varphi)=\{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0,0.7}\mathrm{mrg}}(t_{0},\ldots,t_{k-1})\mid t_{0},\ldots,t_{k-1}\in(2^{% \mathrm{AP}})^{\omega}:\Pi_{\emptyset}[\pi_{0}\mapsto t_{0},\ldots,\pi_{k-1}% \mapsto t_{k-1}]\models\varphi\}.

Now, let $\varphi=Q_{0}\pi_{0}Q_{1}\pi_{1}\cdots Q_{k-1}\pi_{k-1}.\ \psi$ with $Q_{i}\in\{\exists,\forall\}$ and trace quantifier-free $\psi$ be a HyperQPTL sentence and define $\varphi_{i}=Q_{i+1}\pi_{i+1}Q_{i+2}\pi_{i+2}\cdots Q_{k-1}\pi_{k-1}.\ \psi$ for $i\in\{0,1,\ldots,k-1\}$ and $\varphi_{-1}=\varphi$ . Note that $\varphi_{k-1}=\psi$ and that the free trace variables of each $\varphi_{i}$ with $i\in\{-1,0,\ldots,k-1\}$ are exactly $\pi_{0},\ldots,\pi_{i}$ . The following results follows by combining and adapting automata constructions for classical QPTL and HyperLTL [6, 14, 23].

Proposition 4.

1.

Let $\mathfrak{T}$ be a transition system. For every $i\in\{-1,0,\ldots,k-1\}$ there is an (effectively constructible) parity automaton $\mathcal{A}_{i}^{\mathfrak{T}}$ such that

$L(\mathcal{A}_{i}^{\mathfrak{T}})=\{{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{mrg}}(\Pi(\pi_{0}),\ldots,\Pi(\pi_{i}))% \mid\Pi(\pi_{j})\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0,0.7}\mathrm{Tr}}(\mathfrak{T})\text{ for $0\leq j\leq i$ and }{\color% [rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{Tr}}(% \mathfrak{T}),\Pi,0\models\varphi_{i}\}.$
2.

A language over $(2^{\mathrm{AP}})^{k}$ is $\omega$ -regular if and only if it is of the form $L(\varphi)$ for a QPTL-sentence $\varphi$ over some $\mathrm{AP}^{\prime}\supseteq\mathrm{AP}$ with $k$ free trace variables.³³3For the sake of readability, in the following, we do not distinguish between $\mathrm{AP}$ and $\mathrm{AP}^{\prime}$ , i.e., we assume that $\mathrm{AP}$ always contains enough propositions not used in our languages to quantify over.

3 Gamed-based Model-Checking for HyperQPTL

In this section, we present our game-based characterization of $\mathfrak{T}\models\varphi$ for finite transition systems $\mathfrak{T}$ and HyperQPTL sentences $\varphi$ . To this end, we introduce multi-player games with hierarchical information in Section 3.1 and then present the construction of our game in Section 3.2, while we introduce prophecies and prove their soundness in Section 3.3. Then, in Section 4, we show how to construct complete prophecies for the special case of safety formulas (to be defined formally there). Finally, in Section 5, we show how to construct complete prophecies for arbitrary formulas. This allows us to first explain how to generalize the prophecy definition from $\forall^{*}\exists^{*}$ to arbitrary quantifier prefixes and then, in a second step, move from safety to $\omega$ -regular languages.

3.1 Multi-player Graph Games with Hierarchical Information

We develop a game-based characterization of model-checking for HyperQPTL via (multi-player) graph games with hierarchical information, using the notations of Berwanger et al. [4]. First, we introduce the necessary definitions and then present our game in Section 3.2. The games considered by Berwanger et al. are concurrent games (i.e., the players make their moves simultaneously), while for our purpose turn-based games (i.e., the players make their moves one after the other) are sufficient. Turn-based games are simpler versions of concurrent games. To avoid cumbersome notation, we introduce a turn-based variant of these games.

Fix some finite set $C$ of players forming a coalition playing against a distinguished agent called Nature (which is not in $C$ ). For each player $i\in C$ we fix a finite set $B^{i}$ of observations. A game graph $G=(V,E,v_{I},(\beta^{i})_{i\in C})$ consists of a finite set $V=\biguplus_{i\in C}V_{i}\uplus V_{\text{Nat}}$ of positions partitioned into sets controlled by some player resp. Nature, an edge relation $E\subseteq V\times V$ representing moves, an initial position $v_{I}\in V$ , and a collection $(\beta^{i})_{i\in C}$ of observation functions $\beta^{i}\colon V\rightarrow B^{i}$ that label, for each player, the positions with observations. We require that $E$ has no dead-ends, i.e., for every $v\in V$ there is a $v^{\prime}\in V$ with $(v,v^{\prime})\in E$ .

A game graph $(V,E,v_{I},(\beta^{i})_{i\in C})$ yields hierarchical information if there exists a total order $\preceq$ over $C$ such that if $i\preceq j$ then for all $v,v^{\prime}\in V$ , $\beta^{i}(v)=\beta^{i}(v^{\prime})$ implies $\beta^{j}(v)=\beta^{j}(v^{\prime})$ , i.e., if Player $i$ cannot distinguish $v$ and $v^{\prime}$ , then neither can Player $j$ for $i\preceq j$ .

Intuitively, a play starts at position $v_{I}\in V$ . At position $v$ , the player that controls this position chooses a successor position $v^{\prime}$ such that $(v,v^{\prime})\in E$ . Now, each player $i\in C$ receives the observation $\beta^{i}(v^{\prime})$ and the play continues from position $v^{\prime}$ . Thus, a play of $G$ is an infinite sequence $v_{0}v_{1}v_{2}\cdots$ of vertices such that $v_{0}=v_{I}$ and for all $r\geq 0$ we have $(v_{r},v_{r+1})\in E$ .

A history is a prefix $v_{0}v_{1}\cdots v_{r}$ of a play. We denote the set of all histories by $\mathrm{Hist}(G)$ and extend $\beta^{i}\colon V\rightarrow B^{i}$ to plays and histories by defining $\beta^{i}(v_{0}v_{1}v_{2}\cdots)=\beta^{i}(v_{1})\beta^{i}(v_{2})\beta^{i}(v_{% 3})\cdots$ . Note that the observation of the initial position is discarded for technical reasons [4]. We say two histories $h$ and $h^{\prime}$ are indistinguishable to Player $i\in C$ , denoted by $h\sim_{i}h^{\prime}$ , if $\beta^{i}(h)=\beta^{i}(h^{\prime})$ .

A strategy for Player $i\in C$ is a mapping $s^{i}\colon V^{*}\rightarrow V$ that satisfies $s^{i}(h)=s^{i}(h^{\prime})$ for all histories $h,h^{\prime}$ with $h\sim_{i}h^{\prime}$ (i.e., the move selected by the strategy only depends on the observations of the history). A play $v_{0}v_{1}v_{2}\cdots$ is consistent with $s^{i}$ if for every $r\geq 0$ , we have $v_{r+1}=s^{i}(v_{0}v_{1}\cdots v_{r})$ . A play is consistent with a collection of strategies $(s^{i})_{i\in C}$ if it is consistent with each $s^{i}$ . The set of possible outcomes of a collection of strategies is the set of all plays that are consistent with it. As usual, a strategy is finite-state, if it is implemented by some Moore machine.

Lastly, a game $\mathcal{G}$ consists of a game graph $G$ and a winning condition $W\subseteq V^{\omega}$ , where $V$ is the set of positions of $G$ . A play is winning if it is in $W$ and a collection of strategies is winning if all its outcomes are winning.

Proposition 5 ([21, 4]).

1.

It is decidable, given a game with hierarchical information with $\omega$ -regular winning condition, whether it has a winning collection of strategies.
2.

A game with hierarchical information with $\omega$ -regular winning condition has a winning collection of strategies if and only if it has a winning collection of finite-state strategies.

3.2 The Model-checking Game

For the remainder of this paper, we fix a HyperQPTL sentence ${\immediate\immediate\immediate{\color[rgb]{0,0,1}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,1}\varphi}}$ and a transition system ${\immediate{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}% \mathfrak{T}}}$ . We assume (w.l.o.g.)⁴⁴4The following reasoning can easily be extended to general sentences with arbitrary quantifier prefixes, albeit at the cost of more complex notation. We substantiate this claim in Remark 20 on Remark 20.

{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\varphi}={% \color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\forall\pi_{0% }\exists\pi_{1}\cdots\forall\pi_{k-2}\exists\pi_{k-1}.\ \psi}

such that ${\immediate\immediate\immediate{\color[rgb]{0,0,1}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,1}\psi}}$ is trace quantifier-free, define

{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\varphi_{i}}% ={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}Q_{i+1}\pi_% {i+1}Q_{i+2}\pi_{i+2}\cdots\forall\pi_{k-2}\exists\pi_{k-1}.\ \psi}

for $i\in\{-1,0,\ldots,\mathmbox{k-1}\}$ and use the automata ${\immediate\immediate\immediate{\color[rgb]{0,0,1}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,1}\mathcal{A}^{\mathfrak{T}}_{i}}}$ constructed in Proposition 4 satisfying

L({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathcal{A}^{\mathfrak{T}}_{i}})=\{{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{mrg}}(\Pi(\pi_{0}),\ldots,\Pi(\pi_{i}))% \mid\Pi(\pi_{j})\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0,0.7}\mathrm{Tr}}({\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\mathfrak{T}})\text{ for all $0\leq j\leq i$ and % }{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathrm% {Tr}}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}),\Pi,0\models{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\varphi}_{i}\}.

We use the notation ${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}(\mathcal{A% }_{i}^{\mathfrak{T}})_{q}}}$ to denote the parity automaton obtained from ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{i}}$ by making its state $q$ the initial state. Finally, let ${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\mathcal{A}% ^{\mathfrak{T}}_{k-1}}}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}% {rgb}{0,0,1}(Q,\Sigma,q_{I},\delta,\Omega)}$ . Note that ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{k-1}}$ accepts the trace assignments coming from paths trough ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}$ that satisfy ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\psi}$ . We say that ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{k-1}}$ checks ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\psi}$ .

We define a multi-player game ${\immediate\immediate\immediate{\color[rgb]{0,0,1}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,1}\mathcal{G}}({\color[rgb]{0,0,0.7}\definecolor[% named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathfrak{T}},{\color[rgb]{0,0,0.7}% \definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\varphi})}$ with hierarchical information induced by the transition system ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}$ and the HyperQPTL sentence ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\varphi}$ . This game is played between Falsifier (who takes on the role of Nature, cf. Section 3.1), who is in charge of providing traces (from paths trough the transition system) for the universally quantified variables, and a coalition of Verifier-players $\{1,3,\ldots,k-1\}$ (Verifier $i$ for short), who are in charge of providing traces (also from paths trough the transition system) for the existentially quantified variables. The goal of Falsifier is to prove ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}\not\models{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\varphi}$ and the goal of the coalition of Verifier-players is to prove ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}\models{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0,0.7}\varphi}$ . Therefore, the $k$ traces built during a play are read synchronously by the parity automaton ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{k-1}}$ accepting the trace assignments that satisfy ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\psi}$ (recall that ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\psi}$ is the trace quantifier-free part of ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\varphi}$ ).

The game has two phases, an initialization phase where initial vertices for all paths through the transition system are picked, and a second phase (of infinite duration) where the paths (which induce the trace assignment) are built. Formally, in the initialization phase, a position of the game is of the form $((v_{0},\ldots,v_{i-1},\underbrace{\bullet,\ldots,\bullet}_{k-i\text{ times}})% ,q_{I},i)$ where $v_{0},\ldots,v_{i-1}\in V_{I}$ are initial vertices in the transition system ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}$ , $\bullet$ is a fresh (placeholder) symbol, $q_{I}\in Q$ is the initial state of ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{k-1}}$ , and $i\in\{0,1,\cdots,\mathmbox{k-1}\}$ . In the second phase, a position of the game is of the form $((v_{0},\ldots,v_{k-1}),q,i)$ where $v_{0},v_{1},\ldots,v_{k-1}\in V$ , $q\in Q$ , and $i\in\{0,1,\ldots,\mathmbox{k-1}\}$ . A vertex whose last component is an odd $i$ is controlled by Verifier $i$ and a vertex whose last component is even is controlled by Falsifier.

The edges (also called moves) of the game graph are defined as follows, where the first two items are the moves in the initialization phase:

$\blacksquare$

$\bigl{(}((v_{0},\ldots,v_{i-1},\bullet,\ldots,\bullet),q_{I},i),((v_{0},\ldots% ,v_{i-1},v_{i},\bullet,\ldots,\bullet),q_{I},i+1)\bigr{)}$ for all $v_{i}\in V_{I}$ and all $i\in\{0,1,\ldots,\mathmbox{k-2}\}$ : An initial vertex in ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}$ for the $i$ -th path is picked.
$\blacksquare$

$\bigl{(}((v_{0},\ldots,v_{k-2},\bullet),q_{I},k-1),((v_{0},\ldots,v_{k-2},v_{k% -1}),q,0)\bigr{)}$ for all $v_{k-1}\in V_{I}$ where $q=\delta(q_{I},{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0,0.7}\mathrm{mrg}}(\lambda(v_{0}),\ldots,\lambda(v_{k-1})))$ : An initial vertex in ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}$ for the last path is picked. With this move, the initialization phase is over and the state of ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{k-1}}$ checking ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\psi}$ is updated for the first time.
$\blacksquare$

$\bigl{(}((v^{\prime}_{0},\ldots,v^{\prime}_{i-1},v_{i},v_{i+1},\ldots,v_{k-1})% ,q,i),((v^{\prime}_{0},\ldots,v^{\prime}_{i-1},v^{\prime}_{i},v_{i+1},\ldots,v% _{k-1}),q,i+1)\bigr{)}$ for all $(v_{i},v^{\prime}_{i})\in E$ and all $i\in\{0,1,\ldots,\mathmbox{k-2}\}$ : The $i$ -th path is updated by moving to a successor vertex in ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}$ .
$\blacksquare$

$\bigl{(}((v^{\prime}_{0},\ldots,v^{\prime}_{k-2},v_{k-1}),q,k-1),((v^{\prime}_% {0},\ldots,,v^{\prime}_{k-2},v^{\prime}_{k-1}),q^{\prime},0)\bigr{)}$ for all $(v_{k-1},v^{\prime}_{k-1})\in E$ where $q^{\prime}=\delta(q,{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0,0.7}\mathrm{mrg}}(\lambda(v^{\prime}_{0}),\lambda(v^{\prime}_{1}),% \ldots,\lambda(v^{\prime}_{k-1})))$ : The last path is updated by moving to a successor vertex in ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}$ . Simultaneously, the state of ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{k-1}}$ checking ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\psi}$ is updated.

The initial position is $((\bullet,\ldots,\bullet),q_{I},0)$ . We use a parity winning condition. The color of all positions of the initialization phase is $0$ (the color is of no consequence as these vertices are seen only once during the course of a play). The color of positions of the form $((v_{0},\ldots,v_{k-1}),q,i)$ is the color that $q$ has in ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{k-1}}$ , i.e., a play is winning for the Verifier-players if and only if the trace assignment picked by them and Falsifier satisfies $\psi$ .

The game described must be a game of hierarchical information to capture the fact that the Skolem function for an existentially quantified $\pi_{i}$ depends only on the universally quantified variables $\pi_{j}$ with $j\in\{0,2,\ldots,i-1\}$ . To capture that, we define an equivalence relation ${\immediate\immediate\immediate{\color[rgb]{0,0,1}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,1}\equiv_{i}}}$ between positions of the game for $i\in\{1,3,\ldots,\mathmbox{k-1}\}$ which ensures that for Verifier $i$ , two positions are indistinguishable if they coincide on their first $i+1$ components and additionally belong to the same player. Formally, regarding positions from the initialization phase, let $((v_{0},\ldots,v_{m-1},\bullet,\ldots,\bullet),q_{I},m)$ and $((v^{\prime}_{0},\ldots,v^{\prime}_{n-1},\bullet,\ldots,\bullet),q_{I},n)$ be ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\equiv_{% i}}$ -equivalent if $v_{j}=v^{\prime}_{j}$ for all $j\leq i$ and $m=n$ . Regarding all other positions, let $((v_{0},\ldots,v_{k-1}),p,m)$ and $((v^{\prime}_{0},\ldots,v^{\prime}_{k-1}),q,n)$ be ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\equiv_{% i}}$ -equivalent if $v_{j}=v^{\prime}_{j}$ for all $j\leq i$ and $m=n$ . Now, we define the observation functions: For Verifier $i$ , it maps positions to their ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\equiv_{% i}}$ -equivalence classes.

3.3 The Model-Checking Game with Prophecies

The game ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {G}}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}},{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0,0.7}\varphi})$ as introduced in Section 3.2 does not capture ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}\models{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0,0.7}\varphi}$ . While it is sound (see Lemma 8 for the empty set of prophecies), i.e., the coalition of Verifier-players having a winning collection of strategies for ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {G}}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}},{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0,0.7}\varphi})$ implies that ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}\models{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0,0.7}\varphi}$ , but the converse is not necessarily true. This is witnessed, e.g., by a transition system $\mathfrak{T}$ with ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{% Tr}}(\mathfrak{T})=(2^{\{\texttt{p}\}})^{\omega}$ and the sentence $\forall\pi.\ \exists\pi^{\prime}.\ \texttt{p}_{\pi^{\prime}}\leftrightarrow% \mathop{\mathbf{F}\vphantom{a}}\nolimits\texttt{p}_{\pi}$ . As explained in the introduction, the Verifier-player does not have a strategy to select, step-by-step, a trace $t^{\prime}$ for $\pi^{\prime}$ while given, again step-by-step, a trace $t$ for $\pi$ , as the choice of the first letter of $t^{\prime}$ depends on all positions of $t$ . Hence, the coalition does not win ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {G}}(\mathfrak{T},\varphi)$ , even though $\mathfrak{T}\models\varphi$ .

In the following, we show how prophecies, binding commitments about future moves by Falsifier, make the game-based approach to model-checking complete. In our example, Falsifier has to make, with his first move, a commitment about whether he will ever play a p or not. This allows the Verifier-player to pick the “right” first letter of $t^{\prime}$ and thereby win the game, if Falsifier honors the commitment. If not, the rules of the game make him loose. To add prophecies to ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {G}}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}},{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0,0.7}\varphi})$ , we do not change the rules of the game, but instead modify the transition system the game is played on (to allow Falsifier to select truth values for the prophecy variables⁵⁵5Note that prophecy variables are Boolean variables that are set by Falsifier during each move of a play and should not be confused with trace variables or with propositional variables., which is the mechanism he uses to make the commitments) and modify the formula (to ensure that Falsifier loses if he breaks a commitment). Hence, given ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}$ and ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\varphi}$ , we construct ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}^{\mathcal{P}}}$ and ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\varphi^% {\mathcal{P},\Xi}}$ such that the following two properties are satisfied:

$\blacksquare$

Soundness: If the coalition of Verifier-players has a winning collection of strategies for ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {G}}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}^{\mathcal{P}}},{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\varphi^{\mathcal{P},\Xi}})$ , then ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}\models{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0,0.7}\varphi}$ .
$\blacksquare$

Completeness: If ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}\models{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0,0.7}\varphi}$ , then the coalition of Verifier-players has a winning collection of strategies for ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {G}}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}^{\mathcal{P}}},{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\varphi^{\mathcal{P},\Xi}})$ .

The challenge here is to construct the “right” prophecies that allow us to prove completeness, as soundness is independent of the prophecies chosen.

Recall that $\pi_{0},\pi_{2},\ldots,\pi_{k-2}$ resp. $\pi_{1},\pi_{3},\ldots,\pi_{k-1}$ are the universally resp. existentially quantified variables in our fixed formula ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\varphi}$ . We frequently need to refer to their indices. Hence, we define ${\immediate\immediate\immediate{\color[rgb]{0,0,1}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,1}I_{\forall}}}={\color[rgb]{0,0,1}\definecolor[named% ]{pgfstrokecolor}{rgb}{0,0,1}\{0,2,\ldots,k-2\}}$ and ${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}I_{\exists}% }}={\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\{1,3,% \ldots,k-1\}}$ .

We begin by defining the transition system ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}^{\mathcal{P}}}$ from the fixed transition system ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}$ , in which paths additionally determine truth values for prophecy variables.

Definition 6 (System manipulation).

Let $\mathcal{P}=(\textup{P}_{i})_{i\in{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}I_{\forall}}}$ be a collection of sets of atomic propositions such that $\mathrm{AP}$ , the $\textup{P}_{i}$ , and $\{\texttt{m}_{i}\mid i\in{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}I_{\forall}}\}$ are all pairwise disjoint, where the $\texttt{m}_{i}$ are propositions used to mark copies of the transition system ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}=(V,E,V_{I},\lambda)$ .

For $i\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}I_{% \forall}}$ , we define ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}^{\textup{P}_{i}}=(V^{\textup{P}_{i}},E^{\textup{P}_{i}},V_{I}^{% \textup{P}_{i}},\lambda^{\textup{P}_{i}})$ over $\mathrm{AP}\uplus\textup{P}_{i}\uplus\{\texttt{m}_{i}\}$ where $V^{\textup{P}_{i}}=V\times 2^{\textup{P}_{i}}\times\{i\}$ , $E^{\textup{P}_{i}}=\{((s,A,i),(s^{\prime},A^{\prime},i))\mid(s,s^{\prime})\in E% \text{ and }A,A^{\prime}\in 2^{\textup{P}_{i}}\}$ , $V_{I}^{\textup{P}_{i}}=V_{I}\times 2^{\textup{P}_{i}}\times\{i\}$ and $\lambda^{\textup{P}_{i}}(s,A,i)=\lambda(s)\cup A\cup\{\texttt{m}_{i}\}$ .

Furthermore, we define ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}^{\mathcal{P}}=(V^{\mathcal{P}},E^{\mathcal{P}},V_{I}^{\mathcal{P% }},\lambda^{\mathcal{P}})$ as the disjoint union of the ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}^{\textup{P}_{i}}$ , where a vertex of ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}^{\mathcal{P}}$ is in $V_{I}^{\mathcal{P}}$ if and only if it is in some $V_{I}^{\textup{P}_{i}}$ . Consequently, we have ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{% Tr}}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}^{\mathcal{P}})=\bigcup_{i\in{\color[rgb]{0,0,0.7}\definecolor[% named]{pgfstrokecolor}{rgb}{0,0,0.7}I_{\forall}}}\{{t^{\smallfrown}{t^{\prime}% }^{\smallfrown}\{\texttt{m}_{i}\}^{\omega}}\mid t\in{\color[rgb]{0,0,0.7}% \definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{Tr}}({\color[rgb]{% 0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathfrak{T}})\text{ % and }t^{\prime}\in{(2^{{\textup{P}_{i}}})}^{\omega}\}$ .

An effect of this definition is that all paths trough the manipulated system select truth values for the prophecy variables with each move. Furthermore, each such path is marked by a proposition of the form $\texttt{m}_{i}$ indicating for which $i$ the prophecy variables are selected. This will later be used to ensure that Falsifier selects the correct prophecies (cf. Definition 7) for each path he picks for a universally quantified variable. For the Verifier-players, this additional information is simply ignored, as can be seen from the manipulated formula (cf. Definition 7) we introduce now.

We define the sentence ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\varphi^% {\mathcal{P},\Xi}}$ which ensures that Falsifier loses, if he breaks his commitments made via prophecy variables: for every prophecy variable, we have an associated prophecy, a language $\mathfrak{P}\subseteq((2^{\mathrm{AP}})^{i})^{\omega}$ for some $i$ . Note that Falsifier can only make commitments about his own moves, as the Verifier-players could otherwise falsify the commitments (made by Falsifier) about their moves: Prophecies can only refer to traces for universally quantified variables. Also, we will have prophecies for each universally quantified variable.

Definition 7 (Property manipulation).

Let $\Xi=(\Xi_{i})_{i\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0,0.7}I_{\forall}}}$ be a family $\Xi_{i}=\{\xi_{i,1},\ldots,\xi_{i,n_{i}}\}$ of sets of QPTL sentences (over $\mathrm{AP}$ ) such that each $\xi\in\Xi_{i}$ uses only trace variables $\pi_{j}$ with even $j\leq i$ . Let $\mathcal{P}=(\textup{P}_{i})_{i\in{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}I_{\forall}}}$ satisfy the disjointness requirements of Definition 6 and $\textup{P}_{i}=\{\texttt{p}_{i,1},\ldots,\texttt{p}_{i,n_{i}}\}$ , i.e., we have $|\Xi_{i}|=|\textup{P}_{i}|$ . We define the HyperQPTL sentence ${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\varphi^{% \mathcal{P},\Xi}}}$ as

\forall\pi_{0}\exists\pi_{1}\cdots\forall\pi_{k-2}\exists\pi_{k-1}.\ \left[% \bigwedge\nolimits_{i\in{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}I_{\forall}}}(\texttt{m}_{i})_{\pi_{i}}\wedge% \mathop{\mathbf{G}\vphantom{a}}\nolimits\left(\bigwedge\nolimits_{\ell=1}^{n_{% i}}(({\texttt{p}_{i,\ell}})_{\pi_{i}}\leftrightarrow\xi_{i,\ell})\right)\right% ]\rightarrow\psi.

We denote the trace quantifier-free part of ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\varphi^% {\mathcal{P},\Xi}}$ by ${\immediate\immediate\immediate{\color[rgb]{0,0,1}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,1}\psi^{\mathcal{P},\Xi}}}$ .

Note that ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\varphi^% {\mathcal{P},\Xi}}$ has the same quantifier prefix as ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\varphi}$ and that restricting each $\xi_{i,\ell}$ to trace variables $\pi_{j}$ with even $j\leq i$ ensures that the prophecies only refer to trace variables under the control of Falsifier. Also note that the truth values of prophecy variables on trace variables under the control of the Verifier-players are not used in the formula. Finally, Falsifier has to pick the $i$ -th path in ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}^{\textup{P}_{i}}$ (and thus select valuations for the prophecy variables in $\textup{P}_{i}$ ), otherwise he loses immediately.

Our construction is sound, independently of the choice of prophecies.

Lemma 8.

Let $\Xi$ and $\mathcal{P}$ satisfy the requirements of Definition 7. If the coalition of Verifier-players has a winning collection of strategies in ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {G}}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}^{\mathcal{P}}},{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\varphi^{\mathcal{P},\Xi}})$ , then ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}\models{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0,0.7}\varphi}$ .

4 Complete Prophecies for Safety Properties

We show that there are sets $\Xi$ and $\mathcal{P}$ such that if ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}\models{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0,0.7}\varphi}$ , then the coalition of Verifier-players wins ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {G}}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}^{\mathcal{P}}},{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\varphi^{\mathcal{P},\Xi}})$ . We first consider the case where ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\psi}$ is a safety property, i.e., the automaton ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{k-1}}$ , which checks ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\psi}$ , is a deterministic safety automaton. A safety automaton is a parity automaton using only two colors, an even one and an odd one, and moreover, all its states are even-colored except for an odd-colored sink state. In other words, all runs avoiding the single unsafe state are accepting. We start with safety as this allows us to work with “simpler” prophecies while presenting all underlying concepts needed for arbitrary quantifier prefixes. The idea for safety is that a prophecy should indicate which successor vertices are safe for the Verifier-players to move to, i.e., from which successor vertices it is possible to successfully continue the play without immediately losing. In the general case, we have to additionally handle a more complex acceptance condition. This is shown in Section 5.

Definition 9 (Prophecy construction for safety).

For each $i\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}I_{% \forall}}$ , each vector $\bar{v}=(v_{0},v_{1},\ldots,v_{i+1})$ of vertices of ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}$ , and each state $q$ of ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{i+1}}$ we define

\begin{split}&{\immediate\immediate\immediate{\color[rgb]{0,0,1}\definecolor[% named]{pgfstrokecolor}{rgb}{0,0,1}(\mathfrak{S}_{i})_{q}^{\bar{v}}}}=\{{\color% [rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{mrg}}(t% _{0},t_{2},\ldots,t_{i})\mid t_{0}\in{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{Tr}}({\color[rgb]{0,0,0.7}\definecolor[% named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathfrak{T}}_{v_{0}}),t_{2}\in{\color[rgb% ]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{Tr}}({% \color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathfrak% {T}}_{v_{2}}),\ldots,t_{i}\in{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{Tr}}({\color[rgb]{0,0,0.7}\definecolor[% named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathfrak{T}}_{v_{i}}),\text{ and there % are }\\ &\quad t_{1}\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0,0.7}\mathrm{Tr}}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0,0.7}\mathfrak{T}}_{v_{1}}),t_{3}\in{\color[rgb]{0,0,0.7}\definecolor[% named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{Tr}}({\color[rgb]{0,0,0.7}% \definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathfrak{T}}_{v_{3}}),\ldots% ,t_{i+1}\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0,0.7}\mathrm{Tr}}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0,0.7}\mathfrak{T}}_{v_{i+1}})\text{ s.t.\ }{\color[rgb]{0,0,0.7}% \definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{mrg}}(t_{0},\ldots,t_% {i+1})\in L({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0,0.7}(\mathcal{A}_{i+1}^{\mathfrak{T}})_{q}})\}.\end{split}

Note that the $t_{i}$ for $i\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}I_{% \exists}}$ may depend on all $t_{j}$ with $j\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}I_{% \forall}}$ . Our game definition ensures that the choice for an existential variable $\pi_{i}$ only depends on the choices for $\pi_{j}$ with $j<i$ .

Also note that each prophecy is an $\omega$ -regular language, as $\omega$ -regular languages are closed under projection, the analogue of existential quantification. So, due to Proposition 4, there are QPTL-sentences expressing the prophecies allowing us to verify them in the formula ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\varphi^% {\mathcal{P},\Xi}}$ .

Next, we define the sets $\Xi=(\Xi_{i})_{i\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0,0.7}I_{\forall}}}$ and $\mathcal{P}=(\textup{P}_{i})_{i\in{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}I_{\forall}}}$ of QPTL formulas expressing the prophecies defined above and the corresponding prophecy variables.

Definition 10.

Let $\Xi_{i}$ be the set of QPTL formulas that contains sentences $(\xi_{i})_{q}^{\bar{v}}$ for each state $q$ of ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{i+1}}$ and each vector $\bar{v}$ of vertices expressing the prophecy ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}(% \mathfrak{S}_{i})_{q}^{\bar{v}}}$ using only trace variables $\pi_{j}$ with even $j\leq i$ . Let $\textup{P}_{i}$ be the set that contains the prophecy variable $\immediate\immediate\immediate{\color[rgb]{0,0,1}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,1}(\texttt{p}_{i})_{q}^{\bar{v}}}$ for each state $q$ of ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{i+1}}$ and each vector $\bar{v}$ of vertices. The prophecy variable ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}(\texttt% {p}_{i})_{q}^{\bar{v}}}$ corresponds to $(\xi_{i})_{q}^{\bar{v}}$ .

Recall that ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\psi}$ is the maximal trace quantifier-free subformula of ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\varphi}$ . Our main technical lemma shows that the prophecies defined above are indeed complete.

Lemma 11.

Let ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}\models{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0,0.7}\varphi}$ such that ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\psi}$ is a safety property. Then the coalition of Verifier-players has a winning collection of strategies in ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {G}}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}^{\mathcal{P}}},{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\varphi^{\mathcal{P},\Xi}})$ with $\Xi$ and $\mathcal{P}$ as in Definition 10.

Before we turn to the proof of Lemma 11, we introduce some notation about the game ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {G}}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}^{\mathcal{P}}},{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\varphi^{\mathcal{P},\Xi}})$ and define the strategies we will prove winning.

Firstly, recall that ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}^{\mathcal{P}}}$ is the union $\biguplus_{i\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0,0.7}I_{\forall}}}{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0,0.7}\mathfrak{T}}^{P_{i}}$ . Thus, a vertex $v$ of ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}^{\mathcal{P}}}$ is of the form $(s,A,i)\in V\times 2^{\textup{P}_{i}}\times\{i\}$ for some $\textup{P}_{i}$ , where $V$ is the set of vertices of ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}$ , and the label $\lambda^{\textup{P}_{i}}(v)$ of $v$ is $\lambda(s)\cup A\cup\{\texttt{m}_{i}\}$ , i.e., the union of its original (meaning $\mathrm{AP}$ -based) label $\lambda(s)$ in ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}$ , its associated prophecy variables $A$ , and its marker $\texttt{m}_{i}$ indicating that $v$ belongs to ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}^{\textup{P}_{i}}$ . We need to access these bits of information. Hence, we define ${\immediate\immediate\immediate{\color[rgb]{0,0,1}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,1}\lambda_{\mathrm{AP}}}(v)}=\lambda(s)$ , ${\immediate{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}% \mathrm{Prophecies}}(v)}=A$ , and ${\immediate{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}% \mathrm{mark}}(v)}=\texttt{m}_{i}$ . Given a path $\rho=v_{0}v_{1}v_{2}\cdots$ through ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}^{\mathcal{P}}}$ , let ${{\color[rgb]{0,0,1}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,1}\lambda_{% \mathrm{AP}}}(\rho)}={\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0,0.7}\lambda_{\mathrm{AP}}}(v_{0}){\color[rgb]{0,0,0.7}\definecolor[% named]{pgfstrokecolor}{rgb}{0,0,0.7}\lambda_{\mathrm{AP}}}(v_{1}){\color[rgb]{% 0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\lambda_{\mathrm{AP}}% }(v_{2})\cdots$ . Moreover, for $v=(s,A,i)$ in ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}^{\textup{P}_{i}}$ , we are often interested in reasoning about $s$ in ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}$ . To simplify our notation, we will also write $v$ for the (unique) vertex $s$ in ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}$ induced by $v$ .

Secondly, recall that ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\psi^{% \mathcal{P},\Xi}}$ is the trace quantifier-free part of ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\varphi^% {\mathcal{P},\Xi}}$ . Let $\mathcal{B}$ denote the parity automaton $(Q_{\mathcal{B}},\Sigma,q_{I}^{\mathcal{B}},\delta_{\mathcal{B}},\Omega_{% \mathcal{B}})$ that accepts the trace assignments that satisfy ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\psi^{% \mathcal{P},\Xi}}$ .

Lastly, recall that a position of ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {G}}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}^{\mathcal{P}}},{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\varphi^{\mathcal{P},\Xi}})$ is of the form $((v^{\prime}_{0},\ldots,v^{\prime}_{i-1},v_{i},\ldots,v_{k-1}),q,i)$ where $v^{\prime}_{0},\ldots,v^{\prime}_{i-1},v_{i},\ldots,v_{k-1}$ are vertices in the transition system ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}^{\mathcal{P}}}$ , $q\in Q_{\mathcal{B}}$ is a state of the parity automaton $\mathcal{B}$ checking ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\psi^{% \mathcal{P},\Xi}}$ , and $i\in\{0,1,\ldots,\mathmbox{k-1}\}$ . Technically, in the initialization phase, a position is of the form $((v_{0},\ldots,v_{i-1},\underbrace{\bullet,\ldots,\bullet}_{k-i\text{ times}})% ,q_{I},i)$ where $v_{0},\ldots,v_{i-1}$ are vertices and $\bullet$ is a placeholder. For simplicity, we always refer to a position with $((v^{\prime}_{0},\ldots,v^{\prime}_{i-1},v_{i},\ldots,v_{k-1}),q,i)$ , even though $\bullet$ might be present. Also, for convenience, we define the successors $\mathrm{S}(\bullet)$ of the placeholder symbol $\bullet$ to be $V_{I}$ , the set of initial vertices of ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}$ .

We say a play in ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {G}}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}^{\mathcal{P}}},{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\varphi^{\mathcal{P},\Xi}})$ is in Round $(r,i)$ for $r\geq 0$ and $i\in\{0,1,\ldots,k-1\}$ if the play is in a position of the form $((v^{\prime}_{0},\ldots,v^{\prime}_{i-1},v_{i},\ldots,v_{k-1}),q,i)$ for the $(r+1)$ -th time. Also, we say we are in Round $r$ if the play is in Round $(r,i)$ for some $i$ .

Given a play $\alpha$ in ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {G}}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}^{\mathcal{P}}},{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\varphi^{\mathcal{P},\Xi}})$ , for $i\in\{0,1,\ldots,k-1\}$ , let $\rho_{i}^{\alpha}$ denote the path through ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}^{\mathcal{P}}}$ that is induced by $\alpha$ when considering the moves made in Round $(r,i)$ for $r\geq 0$ : Formally, if in Round $(r,i)$ the move from position $p=((v^{\prime}_{0},\ldots,v^{\prime}_{i-1},v_{i},\ldots,v_{k-1}),q,i)$ to $p^{\prime}=((v^{\prime}_{0},\ldots,v^{\prime}_{i-1},v^{\prime}_{i},\ldots,v_{k% -1}),q^{\prime},(i+1)\mod k)$ is made, then $\rho_{i}^{\alpha}(r)=v^{\prime}_{i}$ . Note that $q^{\prime}=q$ , unless $i=k-1$ , then $q^{\prime}=\delta_{\mathcal{B}}(q,{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{mrg}}(\lambda^{\mathcal{P}}(v^{\prime}_{0% }),\ldots,\lambda^{\mathcal{P}}(v^{\prime}_{k-1})))$ . Furthermore, note that the move $(p,p^{\prime})$ is uniquely identified by $p$ and $v^{\prime}_{i}$ . So in the future, we simply write the move from $v_{i}$ to $v^{\prime}_{i}$ when $p$ is clear from the context. We drop the index $\alpha$ from $\rho_{i}^{\alpha}$ and write $\rho_{i}$ when $\alpha$ is clear from the context.

We continue by defining a collection of strategies for the Verifier-players and then show that ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}\models{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0,0.7}\varphi}$ implies that this collection is winning in ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {G}}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}^{\mathcal{P}}},{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\varphi^{\mathcal{P},\Xi}})$ . Recall that ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\varphi^% {\mathcal{P},\Xi}}$ is $\forall\pi_{0}\exists\pi_{1}\cdots\forall\pi_{k-2}\exists\pi_{k-1}.\ {\color[% rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\psi^{\mathcal{P% },\Xi}}$ . Assume the play is in Round $(r,i)$ for $r\geq 0$ and $i\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}I_{% \exists}}$ . Thus, it is in a position of the form

((v^{\prime}_{0},\ldots,v^{\prime}_{i-1},v_{i},\ldots,v_{k-1}),q,i)

and Verifier $i$ has to move. We review some information Verifier $i$ can use to base her choice on. In Round $r$ , Verifier $i$ has access to the first $r$ letters of the traces ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\lambda_% {\mathrm{AP}}}(\rho_{0}),{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\lambda_{\mathrm{AP}}}(\rho_{1}),\ldots,{\color[% rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\lambda_{\mathrm% {AP}}}(\rho_{i})$ induced by the play.⁶⁶6For $j<i$ , she actually has access to $r+1$ letters, but our construction is independent of the last ones. Let $q_{i}$ be the state that ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{i}}$ has reached on ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{% mrg}}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \lambda_{\mathrm{AP}}}(\rho_{0})[0,r),{\color[rgb]{0,0,0.7}\definecolor[named]% {pgfstrokecolor}{rgb}{0,0,0.7}\lambda_{\mathrm{AP}}}(\rho_{1})[0,r),\ldots,{% \color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\lambda_{% \mathrm{AP}}}(\rho_{i})[0,r))$ for $i\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}I_{% \exists}}$ .

Definition 12 (Strategy definition for safety).

Let

M_{i}(v_{0}^{\prime},\ldots,v^{\prime}_{i-1},v_{i},q_{i})=\{v^{\prime}_{i}\in% \mathrm{S}(v_{i})\mid{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0,0.7}(\texttt{p}_{i-1})_{q_{i}}^{\bar{v}}}\in{\color[rgb]{0,0,0.7}% \definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{Prophecies}}(v^{% \prime}_{i-1})\}

where $\bar{v}=(v_{0}^{\prime},\ldots,v^{\prime}_{i})$ . If $M_{i}(v_{0}^{\prime},\ldots,v^{\prime}_{i-1},v_{i},q_{i})$ is nonempty, then Verifier $i$ can move to any $v^{\prime}_{i}$ in the set (the “Nonempty-case”). If it is empty, then Verifier $i$ can move to any $v^{\prime}_{i}\in\mathrm{S}(v_{i})$ (the “Empty-case”).

Proof sketch of Lemma 11..

We show that the just constructed strategies form a winning collection for the Verifier-players. Here, we reason about a play under the assumption that all prophecies are set correctly (i.e., the premise of ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\psi^{% \mathcal{P},\Xi}}$ is true) as otherwise, the play is trivially won by the Verifier-players. Under this assumption, and the basis that ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}\models{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0,0.7}\varphi}$ , we prove that the Verifier-players have always used the Nonempty-case to pick their moves. This implies that the play is winning for them: We have to argue that the conclusion of ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\psi^{% \mathcal{P},\Xi}}$ (which is ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\psi}$ ) is true. Recall that ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{k-1}}$ checks ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\psi}$ . Let $t_{0},\ldots,t_{k-1}$ be the traces induced by the play. We show that ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{k-1}}$ accepts ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{% mrg}}(t_{0},\ldots,t_{k-1})$ . In Round $(r,k-1)$ , ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{k-1}}$ has reached a state $q_{k-1}$ on the prefix of length $r$ of ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{% mrg}}(t_{0},\ldots,t_{k-1})$ , the prophecy ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}(% \mathfrak{S}_{k-1})_{q_{k-1}}^{\bar{v}}}$ for the correct $\bar{v}$ (cf. Definition 12) holds, which implies that $L({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}(% \mathcal{A}_{k-1}^{\mathfrak{T}})_{q_{k-1}}})\neq\emptyset$ . Hence, $q_{k-1}$ is a safe state, and not the single (unsafe) sink state. Thus, an induction shows that the run of ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{k-1}}$ on ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{% mrg}}(t_{0},\ldots,t_{k-1})$ is accepting. To establish that the Verifier-players have always used the Nonempty-case, we proceed by induction on the rounds. We show that, in Round $r$ , Verifier $i$ for each $i\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}I_{% \exists}}$ has so far produced a trace prefix of length $r$ such that it is possible to successfully continue the prefix in a way that allows the Verifier-players with higher indices to also continue successfully. Successful simply meaning the traces can be continued in a way such that ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{k-1}}$ accepts. This implies that they can also use the Nonempty-case in the next round. $\hfill\blacktriangleleft$

Combining Lemma 8 and Lemma 11, we obtain our main result of this section for formulas ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\varphi}$ where the maximal trace quantifier-free subformula ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\psi}$ is a safety property.

Theorem 13.

Let $\Xi$ , $\mathcal{P}$ be as in Definition 10, and let ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\psi}$ be a safety property. The coalition of Verifier-players has a winning collection of strategies for ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {G}}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}^{\mathcal{P}}},{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\varphi^{\mathcal{P},\Xi}})$ if and only if ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}\models{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0,0.7}\varphi}$ .

5 Complete Prophecies for $\omega$ -Regular Properties

In this section, we show how to construct complete prophecies for trace quantifier-free $\psi$ beyond the safety fragment. In the safety case, prophecies indicate moves which prevent the Verifier-players from losing. In the case of safety, not losing equals winning. However for general $\omega$ -regular objectives, this is not enough. It is also necessary to (again and again) make progress towards satisfying the acceptance condition.

In this section, we assume that the automata ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{i}}$ are Rabin automata. The class of languages recognized by (deterministic respectively nondeterministic) Rabin automata is the class of $\omega$ -regular languages. A (deterministic) Rabin automaton is a (deterministic) $\omega$ -automaton whose acceptance condition is given as a set $\{(B_{1},F_{1}),\ldots,(B_{m},F_{m})\}$ of pairs of sets $B_{i},F_{i}$ of states. A run is accepting if there exists an $i$ such that the run visits states in $B_{i}$ only finitely many times and states in $F_{i}$ infinitely many times.

5.1 One-Pair Rabin Automata

First, we present our construction for one-pair Rabin automata, then show how to generalize to Rabin automata with an arbitrary number of pairs in Section 5.2. Here, we assume that for each $i\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}I_{% \exists}}$ , the automaton ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{i}}$ is a one-pair Rabin automaton, not only ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{k}}$ . We always denote the single pair as $(B,F)$ , it will be clear from the context to which automaton it belongs. Intuitively, making progress towards winning in a one-pair Rabin automaton means avoiding states in $B$ and visiting states in $F$ .

Let $\kappa$ be an infinite run of such an automaton. We define ${\immediate\immediate\immediate{\color[rgb]{0,0,1}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,1}\mathrm{last}_{B}}(\kappa)}$ as $\bot$ if $\kappa$ never visits $B$ , as $i$ if $\kappa(i)$ is the last visit of $\kappa$ in $B$ , and as $\infty$ if $\kappa$ visits $B$ infinitely many times (meaning there is no last visit). Furthermore, we define ${\immediate\immediate\immediate{\color[rgb]{0,0,1}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,1}\mathrm{first}_{F}}(\kappa)}$ as $i$ if $\kappa(i)$ is the first visit of $\kappa$ in $F$ and as $\infty$ if $\kappa$ never visits $F$ . Finally, we define the value ${\immediate\immediate\immediate{\color[rgb]{0,0,1}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,1}\mathrm{val}}(\kappa)}$ of a run $\kappa$ as ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{% first}_{F}}(\kappa)$ if ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{% last}_{B}}(\kappa)=\bot$ and as $\max\{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathrm{last}_{B}}(\kappa),{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{first}_{F}}(\kappa)\}$ otherwise. Given two runs $\kappa,\kappa^{\prime}$ , we say that $\kappa$ “makes progress faster” than $\kappa^{\prime}$ if ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{% val}}(\kappa)<{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0,0.7}\mathrm{val}}(\kappa^{\prime})$ .

Before we can define our new prophecies, we need additional notation that gives us the value of a best run (over several traces) if we fix all but the last trace. For each $i\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}I_{% \exists}}$ , each vertex $v$ of ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}$ , each state $q$ of ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{i}}$ , and traces $t_{0},t_{1},\ldots,t_{i-1}\in{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{Tr}}({\color[rgb]{0,0,0.7}\definecolor[% named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathfrak{T}})$ , we define

{\immediate\immediate\immediate{\color[rgb]{0,0,1}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,1}\mathrm{opt}_{i}}(q,v,t_{0},\ldots,t_{i-1})}=\min% \nolimits_{t_{i}\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0,0.7}\mathrm{Tr}}({\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\mathfrak{T}}_{\mathrm{S}(v)})}{\color[rgb]{% 0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{val}}(\kappa_% {i}),

where $\kappa_{i}$ is the run of ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}(% \mathcal{A}_{i}^{\mathfrak{T}})_{q}}$ on ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{% mrg}}(t_{0},\ldots,t_{i-1},t_{i})$ .

We are now ready to introduce our prophecies.

Definition 14 (Prophecy construction).

For each $i\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}I_{% \forall}}$ , vectors $\bar{u}=(v_{0},v_{1},\ldots,v_{i+1})$ and $\bar{v}=(v^{\prime}_{0},v^{\prime}_{1},\ldots,v^{\prime}_{i+1})$ of vertices such that $v^{\prime}_{j}\in\mathrm{S}(v_{j})$ for $j\leq i+1$ , and each vector $\bar{q}=(q_{1},q_{3},\ldots,q_{i+1})$ of states $q_{j}$ of ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{j}}$ , we define

\begin{split}&{\immediate\immediate\immediate{\color[rgb]{0,0,1}\definecolor[% named]{pgfstrokecolor}{rgb}{0,0,1}(\mathfrak{P}_{i})_{\bar{q}}^{\bar{u},\bar{v% }}}}=\{{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathrm{mrg}}(t_{0},t_{2},\ldots,t_{i})\mid t_{0}\in{\color[rgb]{0,0,0.7}% \definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{Tr}}({\color[rgb]{% 0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathfrak{T}}_{v^{% \prime}_{0}}),t_{2}\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}% {rgb}{0,0,0.7}\mathrm{Tr}}({\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\mathfrak{T}}_{v^{\prime}_{2}}),\ldots,t_{i}\in{% \color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{% Tr}}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}_{v^{\prime}_{i}}),\text{ and}\\ &\quad\text{there exist }t_{1}\in{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{Tr}}({\color[rgb]{0,0,0.7}\definecolor[% named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathfrak{T}}_{v^{\prime}_{1}}),t_{3}\in{% \color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{% Tr}}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}_{v^{\prime}_{3}}),\ldots,t_{i+1}\in{\color[rgb]{0,0,0.7}% \definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{Tr}}({\color[rgb]{% 0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathfrak{T}}_{v^{% \prime}_{i+1}})\text{ such that }\\ &\quad\quad\text{the run }\kappa_{j}\text{ of }{\color[rgb]{0,0,0.7}% \definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}(\mathcal{A}_{j}^{\mathfrak{T% }})_{q_{j}}}\text{ on }{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor% }{rgb}{0,0,0.7}\mathrm{mrg}}(t_{0},\ldots,t_{j})\text{ is accepting and % satisfies}\\ &\quad\quad\quad{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{% 0,0,0.7}\mathrm{val}}(\kappa_{j})={\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{opt}_{j}}(q_{j},v_{j},t_{0},\ldots,t_{j-1% })\text{ for all odd }j\leq i+1\}.\end{split}

Intuitively, the prophecy ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}(% \mathfrak{P}_{i})_{\bar{q}}^{\bar{u},\bar{v}}}$ indicates that it is safe for Verifier $i+1$ to move from $v_{i+1}$ to $v^{\prime}_{i+1}$ as before, and additionally, among all successors of $v_{i+1}$ , picking $v^{\prime}_{i+1}$ allows Verifier $i+1$ to make the most progress. This prophecy is intended to be used, if for odd $j<i+1$ , Verifier $j$ already picked the move $v_{j}$ to $v^{\prime}_{j}$ which was optimal. In particular, the prophecy repeats the prophecies made (in the same round) for Verifier $j$ with odd $j<i+1$ .

These prophecies are $\omega$ -regular.

Lemma 15.

For each $i\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}I_{% \forall}}$ , each vector $\bar{q}$ of states and all vectors $\bar{u},\bar{v}$ such that the $\ell$ -th vertex of $\bar{v}$ is a successor of the $\ell$ -th vertex of $\bar{u}$ , the set ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}(% \mathfrak{P}_{i})_{\bar{q}}^{\bar{u},\bar{v}}}$ is $\omega$ -regular.

We set up the manipulated system and formula, then state the completeness result.

Definition 16.

We define $\Xi=(\Xi_{i})_{i\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0,0.7}I_{\forall}}}$ and $\mathcal{P}=(\textup{P}_{i})_{i\in{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}I_{\forall}}}$ . Let $\Xi_{i}$ be the set of QPTL formulas that contains sentences $(\xi_{i})_{\bar{q}}^{\bar{u},\bar{v}}$ for each vector $\bar{q}$ of states and vectors $\bar{u},\bar{v}$ such that the $\ell$ -th vertex of $\bar{v}$ is a successor of the $\ell$ -th vertex of $\bar{u}$ . The sentence $(\xi_{i})_{\bar{q}}^{\bar{u},\bar{v}}$ expresses the prophecy ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}(% \mathfrak{P}_{i})_{\bar{q}}^{\bar{u},\bar{v}}}$ using only even trace variables $\pi_{j}$ with $j\leq i$ .

Moreover, let $\textup{P}_{i}$ be such that it contains the prophecy variable ${\immediate\immediate\immediate{\color[rgb]{0,0,1}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,1}(\texttt{p}_{i})_{\bar{q}}^{\bar{u},\bar{v}}}}$ for each vector $\bar{q}$ of states and vectors $\bar{u},\bar{v}$ such that the $\ell$ -th vertex of $\bar{v}$ is a successor of the $\ell$ -th vertex of $\bar{u}$ . The prophecy variable ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}(\texttt% {p}_{i})_{\bar{q}}^{\bar{u},\bar{v}}}$ corresponds to $(\xi_{i})_{\bar{q}}^{\bar{u},\bar{v}}$ .

Lemma 17.

Assume ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}\models{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0,0.7}\varphi}$ and each ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{i}}$ is a one-pair Rabin automaton. Then the coalition of Verifier-players has a winning collection of strategies in ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {G}}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}^{\mathcal{P}}},{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\varphi^{\mathcal{P},\Xi}})$ with $\Xi$ and $\mathcal{P}$ as in Definition 16.

Our proof of this result generalizes the one for the safety case (see Lemma 11), using the same notation introduced there: We define a collection of strategies for the Verifier-players and then show, that ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}\models{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0,0.7}\varphi}$ implies that this collection is winning in ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {G}}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}^{\mathcal{P}}},{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\varphi^{\mathcal{P},\Xi}})$ .

Assume the play is in Round $(r,i)$ for $r\geq 0$ and $i\in{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}I_{% \exists}}$ . Thus, it is in a position

((v^{\prime}_{0},\ldots,v^{\prime}_{i-1},v_{i},\ldots,v_{k-1}),q,i)

and Verifier $i$ has to move. We review some information Verifier $i$ can use to base her choice on. In Round $r$ , Verifier $i$ has access to the first $r$ letters of the traces ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\lambda_% {\mathrm{AP}}}(\rho_{0}),{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\lambda_{\mathrm{AP}}}(\rho_{1}),\ldots,{\color[% rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\lambda_{\mathrm% {AP}}}(\rho_{i})$ induced by the play⁶. Let $q_{j}$ be the state that ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{j}}$ has reached on ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{% mrg}}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \lambda_{\mathrm{AP}}}(\rho_{0})[0,r),{\color[rgb]{0,0,0.7}\definecolor[named]% {pgfstrokecolor}{rgb}{0,0,0.7}\lambda_{\mathrm{AP}}}(\rho_{1})[0,r),\ldots,{% \color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\lambda_{% \mathrm{AP}}}(\rho_{j})[0,r))$ for odd $j\leq i$ . Also, let $((v_{0},\ldots,v_{i-1},v_{i},\ldots,v_{k-1}),q,0)$ be the position reached in Round $(r,0)$ .

Definition 18 (Strategy construction).

Let

M_{i}(\bar{u},\bar{v},\bar{q})=\{v^{\prime}_{i}\in\mathrm{S}(v_{i})\mid{\color% [rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}(\texttt{p}_{i-% 1})_{\bar{q}}^{\bar{u},\bar{w}}}\in{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{Prophecies}}(v^{\prime}_{i-1})\}

where $\bar{u}=(v_{0},\ldots,v_{i})$ , $\bar{v}=(v_{0}^{\prime},\ldots,v^{\prime}_{i-1},v_{i})$ , $\bar{w}=(v_{0}^{\prime},\ldots,v^{\prime}_{i-1},v^{\prime}_{i})$ and $\bar{q}=(q_{1},q_{3},\ldots,q_{i})$ .

If $M_{i}(\bar{u},\bar{v},\bar{q})$ is nonempty, then Verifier $i$ can move to any $v^{\prime}_{i}$ in the set (the “Nonempty-case”). If it is empty, then Verifier $i$ can move to any $v^{\prime}_{i}\in\mathrm{S}(v_{i})$ (the “Empty-case”).

Now, Lemma 17 can be proven by generalizing the proof of Lemma 11. Then, we directly obtain our main result by combining Lemma 8 and Lemma 17.

Theorem 19.

Let $\Xi$ and $\mathcal{P}$ as in Definition 16, and assume that each ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{i}}$ is a one-pair Rabin automaton. The coalition of Verifier-players has a winning collection of strategies for ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {G}}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}^{\mathcal{P}}},{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\varphi^{\mathcal{P},\Xi}})$ if and only if ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}}\models{\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{% rgb}{0,0,0.7}\varphi}$ .

5.2 Beyond One-Pair Rabin Automata

We have proven Theorem 19 for the case that all automata referred to in the prophecies are one-pair Rabin automata. We sketch how to drop this constraint closely following Beutner and Finkbeiner [5].

A Rabin automaton $\mathcal{R}$ with pairs $(B_{1},F_{1}),\ldots,(B_{m},F_{m})$ can be seen as a union of $m$ one-pair Rabin automata $(B_{i},F_{i})$ - $\mathcal{R}$ . A run that is accepting in $(B_{i},F_{i})$ - $\mathcal{R}$ is also accepting in $\mathcal{R}$ and each accepting run of $\mathcal{R}$ is accepting in some $(B_{i},F_{i})$ - $\mathcal{R}$ . Before we present how to go from one-pair to general Rabin automata, we recall that the prophecies exclusively talk about traces provided by Falsifier. Hence, if Falsifier signals that his future traces belong to prophecy $\mathcal{P}$ which, for example, implies that Rabin automaton $\mathcal{R}$ accepts them, then Falsifier can also specify the pair(s) for which $\mathcal{R}$ will accept. No further context from the Verifier-players is needed.

The idea is to annotate our prophecies (which refer to ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{1}},{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\mathcal{A}^{\mathfrak{T}}_{3}},\ldots,{\color[% rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal{A}^{% \mathfrak{T}}_{k-1}}$ ) with the indices of the pairs used for acceptance. More concretely, for a prophecy ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}(% \mathfrak{P}_{i})_{\bar{q}}^{\bar{u},\bar{v}}}$ , we introduce prophecies of the form ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}(% \mathfrak{P}_{i})_{\bar{q},\bar{a}}^{\bar{u},\bar{v}}}$ , where $\bar{a}$ is a vector of indices of the same length as $\bar{q}$ . Say the $j$ -th entry of $\bar{q}$ is $q_{\ell}$ , then the prophecy ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}(% \mathfrak{P}_{i})_{\bar{q}}^{\bar{u},\bar{v}}}$ refers to ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}(% \mathcal{A}_{\ell}^{\mathfrak{T}})_{q_{\ell}}}$ (among other automata), and say the $j$ -th entry of $\bar{a}$ is $a_{j}$ , then ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}(% \mathfrak{P}_{i})_{\bar{q},\bar{a}}^{\bar{u},\bar{v}}}$ refers to the one-pair Rabin automaton $(B_{a_{j}},F_{a_{j}})$ - ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}(% \mathcal{A}_{\ell}^{\mathfrak{T}})_{q_{\ell}}}$ (among other automata). Except for the refined prophecies, no other changes to the game are required.

In a play of the game ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {G}}({\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}% \mathfrak{T}^{\mathcal{P}}},{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\varphi^{\mathcal{P},\Xi}})$ , Falsifier specifies with his prophecies for which pairs the Rabin automata ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{1}},{\color[rgb]{0,0,0.7}\definecolor[named]{% pgfstrokecolor}{rgb}{0,0,0.7}\mathcal{A}^{\mathfrak{T}}_{3}},\ldots,{\color[% rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal{A}^{% \mathfrak{T}}_{k-1}}$ can accept.

In Round $(0,0)$ , it is specified for ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{1}}$ , in Round $(0,1)$ , Verifier $1$ chooses one option specified by Falsifier for ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{1}}$ . That choice is simply made by her move. In Round $(0,0)$ , Falsifier moves from $\bullet$ to $v_{0}$ , and in Round $(0,1)$ , Verifier $1$ moves from $\bullet$ to $v_{1}$ . Say ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{% Prophecies}}(v_{0})$ indicates that $(B_{i},F_{i})$ - ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{1}}$ accepts when Verifier $1$ moves to $v_{1}$ , then she has chosen $(B_{i},F_{i})$ - ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{1}}$ . She then (in order be guaranteed to build a winning play) has to stick to it for the rest of the play, meaning that from now on all her moves must have a target vertex $v$ such that the prophecy given by Falsifier in the move before indicates that $(B_{i},F_{i})$ - ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{1}}$ accepts if she moves to $v$ .

In Round $(0,2)$ , it is specified also for ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{3}}$ , in Round $(0,3)$ , Verifier $3$ chooses one option for ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{3}}$ and then has to stick to it for the rest of the play. Additionally, she must pick the option chosen by Verifier $1$ for ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{1}}$ to ensure consistency. In Round $(0,2)$ , Falsifier moves from $\bullet$ to $v_{2}$ . For example, say Verifier $3$ has the option to move from $\bullet$ to $v^{\prime}$ , $v^{\prime\prime}$ , or $v^{\prime\prime\prime}$ with ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathrm{% Prophecies}}(v_{2})$ indicating that $(B_{i},F_{i})$ - ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{1}}$ and $(B_{j},F_{j})$ - ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{3}}$ accept if she moves to $v^{\prime}$ , that $(B_{k},F_{k})$ - ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{1}}$ and $(B_{j},F_{j})$ - ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{3}}$ accept if she moves to $v^{\prime\prime}$ , and that $(B_{i},F_{i})$ - ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{1}}$ and $(B_{\ell},F_{\ell})$ - ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{3}}$ accept if she moves to $v^{\prime\prime\prime}$ . Then she must pick $v^{\prime}$ or $v^{\prime\prime\prime}$ because Verifier $1$ has committed to $(B_{i},F_{i})$ - ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{1}}$ which Verifier $3$ must honor. If Verifier $3$ moves to $v^{\prime}$ she picks $(B_{j},F_{j})$ - ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{3}}$ , if she moves to $v^{\prime\prime\prime}$ she picks $(B_{\ell},F_{\ell})$ - ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{3}}$ .

The same principle applies for the next rounds. After Round $(0,k-1)$ , for each automaton a pair has been fixed to which the Verifier-players stick for the rest of the play.

We end by substantiating the claim in Footnote 4 on Footnote 4 that our construction can also be applied to formulas with arbitrary, i.e., not strictly alternating, trace quantifier prefixes.

$\blacktriangleright$ Remark 20.

In case of of arbitrary trace quantifier prefixes, we have one player in the coalition for each maximal block of existentially quantified trace variables in the prefix, who selects traces for these variables. For example, for a formula of the form

\forall\pi_{0}\exists\pi_{1}\exists\pi_{2}\forall\pi_{3}\exists\pi_{4}\exists% \pi_{5}.\ \psi

with trace quantifier-free $\psi$ , we have just two players (say, Player $12$ and Player $45$ ) in the coalition. Player $12$ is in charge of the variables $\pi_{1}$ and $\pi_{2}$ , and Player $45$ is in charge of the variables $\pi_{4}$ and $\pi_{5}$ . These two players are in a coalition against Falsifier, who is in charge of the variables $\pi_{0}$ and $\pi_{3}$ . In each round, Falsifier picks a move for $\pi_{0}$ , then Player $12$ picks a move for $\pi_{1}$ and a move for $\pi_{2}$ , then Falsifier picks a move for $\pi_{3}$ , and then Player $45$ picks a move for $\pi_{4}$ and a move for $\pi_{5}$ .

Note that just adding universally quantified dummy trace variables between any pair of consecutive existentially quantified trace variables is logically equivalent, but increases the complexity of our approach (as that depends on the number of players).

6 Conclusion

We have presented the first sound and complete game-based algorithm for full HyperLTL (even HyperQPTL) model-checking via multi-player games with hierarchical information, thereby extending the prophecy-based framework of Coenen et al. and Beutner and Finkbeiner from the $\forall^{*}\exists^{*}$ -fragment to arbitrary quantifier prefixes. Similarly, we have extended Winter and Zimmermann’s game-based characterization of the existence of computable Skolem functions witnessing $\mathfrak{T}\models\varphi$ . One way of understanding our result is that we compute finite-state implementations of Skolem functions via transducers with $\omega$ -regular lookahead.

In further work, we aim to exhibit lower bounds on the number of prophecies needed for completeness. Recall that HyperLTL model-checking is Tower-complete. Even an elementary number of prophecies, while unlikely, would not contradict any complexity-lower bounds, as solving multi-player games of hierarchical information is already Tower-complete (in the number of players). However, as it is, the number of prophecies we use is only bounded by an $n$ -fold exponential, where $n$ is linear in the number of quantifier alternations (taking both trace and propositional quantification into account), as the size of the automata ${\color[rgb]{0,0,0.7}\definecolor[named]{pgfstrokecolor}{rgb}{0,0,0.7}\mathcal% {A}^{\mathfrak{T}}_{i}}$ grows like that.

One of the motivations for the introduction of the game-based approach using prophecies is the need for complementation of $\omega$ -automata in the classical automata-based HyperLTL model-checking algorithm. For $\forall^{*}\exists^{*}$ -formulas, the game-based approach “only” requires deterministic $\omega$ -automata, which can be directly computed from the quantifier-free part, which is essentially an LTL formula. On the other hand, the automata-based approach needs automata complementation, already for $\forall^{*}\exists^{*}$ -formulas. For arbitrary quantifier alternations, both approaches require complementation. In future work, we aim to study whether nondeterministic or history-deterministic automata are sufficient to construct complete prophecies.

Finally, we are currently extending the techniques developed here to even more expressive logics, e.g., HyperRecHML, recursive Hennessy-Milner logic with trace quantification [2].

References

[1] Martín Abadi and Leslie Lamport. The existence of refinement mappings. Theor. Comput. Sci., 82(2):253–284, 1991. doi:10.1016/0304-3975(91)90224-P.
[2] Luca Aceto, Antonis Achilleos, Elli Anastasiadi, and Adrian Francalanza. Monitoring hyperproperties with circuits. In Mohammad Reza Mousavi and Anna Philippou, editors, FORTE 2022, volume 13273 of LNCS, pages 1–10. Springer, 2022. doi:10.1007/978-3-031-08679-3_1.
[3] Rajeev Alur, Emmanuel Filiot, and Ashutosh Trivedi. Regular transformations of infinite strings. In LICS 2012, pages 65–74. IEEE Computer Society, 2012. doi:10.1109/LICS.2012.18.
[4] Dietmar Berwanger, Anup Basil Mathew, and Marie van den Bogaard. Hierarchical information and the synthesis of distributed strategies. Acta Informatica, 55(8):669–701, 2018. doi:10.1007/S00236-017-0306-5.
[5] Raven Beutner and Bernd Finkbeiner. Prophecy variables for hyperproperty verification. In CSF 2022, pages 471–485. IEEE, 2022. doi:10.1109/CSF54842.2022.9919658.
[6] Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez. Temporal logics for hyperproperties. In Martín Abadi and Steve Kremer, editors, POST 2014, volume 8414 of LNCS, pages 265–284. Springer, 2014. doi:10.1007/978-3-642-54792-8_15.
[7] Michael R. Clarkson and Fred B. Schneider. Hyperproperties. J. Comput. Secur., 18(6):1157–1210, 2010. doi:10.3233/JCS-2009-0393.
[8] Norine Coenen, Bernd Finkbeiner, César Sánchez, and Leander Tentrup. Verifying hyperliveness. In Isil Dillig and Serdar Tasiran, editors, CAV 2019, Part I, volume 11561 of LNCS, pages 121–139. Springer, 2019. doi:10.1007/978-3-030-25540-4_7.
[9] Samuel Eilenberg. Automata, languages, and machines. A. Pure and applied mathematics. Academic Press, 1974. URL: https://www.worldcat.org/oclc/310535248.
[10] E. Allen Emerson and Joseph Y. Halpern. “Sometimes” and “not never” revisited: on branching versus linear time temporal logic. J. ACM, 33(1):151–178, 1986. doi:10.1145/4904.4999.
[11] Joost Engelfriet. Top-down tree transducers with regular look-ahead. Math. Syst. Theory, 10:289–303, 1977. doi:10.1007/BF01683280.
[12] Emmanuel Filiot and Sarah Winter. Synthesizing computable functions from rational specifications over infinite words. Int. J. Found. Comput. Sci., 35(01n02):179–214, 2024. doi:10.1142/S012905412348009X.
[13] Bernd Finkbeiner, Christopher Hahn, Jana Hofmann, and Leander Tentrup. Realizing omega-regular hyperproperties. In Shuvendu K. Lahiri and Chao Wang, editors, CAV 2020, Part II, volume 12225 of LNCS, pages 40–63. Springer, 2020. doi:10.1007/978-3-030-53291-8_4.
[14] Bernd Finkbeiner, Markus N. Rabe, and César Sánchez. Algorithms for Model Checking HyperLTL and HyperCTL^∗. In Daniel Kroening and Corina S. Pasareanu, editors, CAV 2015, Part I, volume 9206 of LNCS, pages 30–48. Springer, 2015. doi:10.1007/978-3-319-21690-4_3.
[15] Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors. Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 of LNCS. Springer, 2002. doi:10.1007/3-540-36387-4.
[16] Frederick A. Hosch and Lawrence H. Landweber. Finite delay solutions for sequential conditions. In ICALP 1972, pages 45–60, 1972.
[17] Felix Klein and Martin Zimmermann. How much lookahead is needed to win infinite games? Log. Methods Comput. Sci., 12(3), 2016. doi:10.2168/LMCS-12(3:4)2016.
[18] Corto Mascle and Martin Zimmermann. The keys to decidable HyperLTL satisfiability: Small models or very simple formulas. In Maribel Fernández and Anca Muscholl, editors, CSL 2020, volume 152 of LIPIcs, pages 29:1–29:16. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2020. doi:10.4230/LIPIcs.CSL.2020.29.
[19] Daryl McCullough. Noninterference and the composability of security properties. In SSP 1988, pages 177–186. IEEE Computer Society, 1988. doi:10.1109/SECPRI.1988.8110.
[20] Amir Pnueli. The temporal logic of programs. In FOCS 1977, pages 46–57. IEEE, October 1977. doi:10.1109/SFCS.1977.32.
[21] Amir Pnueli and Roni Rosner. Distributed reactive systems are hard to synthesize. In FOCS 1990, Volume II, pages 746–757. IEEE Computer Society, 1990. doi:10.1109/FSCS.1990.89597.
[22] Markus N. Rabe. A temporal logic approach to information-flow control. PhD thesis, Saarland University, 2016. URL: http://scidok.sulb.uni-saarland.de/volltexte/2016/6387/.
[23] A. Prasad Sistla, Moshe Y. Vardi, and Pierre Wolper. The complementation problem for Büchi automata with appplications to temporal logic. Theor. Comput. Sci., 49:217–237, 1987. doi:10.1016/0304-3975(87)90008-9.
[24] Sarah Winter and Martin Zimmermann. Finite-state strategies in delay games. Inf. Comput., 272:104500, 2020. doi:10.1016/J.IC.2019.104500.
[25] Sarah Winter and Martin Zimmermann. Prophecies all the way: Game-based model-checking for HyperQPTL beyond $\forall^{*}\exists^{*}$ . arXiv, 2504.08575, 2025. doi:10.48550/arXiv.2504.08575.

[bib.bib1] [1] Martín Abadi and Leslie Lamport. The existence of refinement mappings. Theor. Comput. Sci., 82(2):253–284, 1991. doi:10.1016/0304-3975(91)90224-P.

[bib.bib2] [2] Luca Aceto, Antonis Achilleos, Elli Anastasiadi, and Adrian Francalanza. Monitoring hyperproperties with circuits. In Mohammad Reza Mousavi and Anna Philippou, editors, FORTE 2022, volume 13273 of LNCS, pages 1–10. Springer, 2022. doi:10.1007/978-3-031-08679-3_1.

[bib.bib3] [3] Rajeev Alur, Emmanuel Filiot, and Ashutosh Trivedi. Regular transformations of infinite strings. In LICS 2012, pages 65–74. IEEE Computer Society, 2012. doi:10.1109/LICS.2012.18.

[bib.bib4] [4] Dietmar Berwanger, Anup Basil Mathew, and Marie van den Bogaard. Hierarchical information and the synthesis of distributed strategies. Acta Informatica, 55(8):669–701, 2018. doi:10.1007/S00236-017-0306-5.

[bib.bib5] [5] Raven Beutner and Bernd Finkbeiner. Prophecy variables for hyperproperty verification. In CSF 2022, pages 471–485. IEEE, 2022. doi:10.1109/CSF54842.2022.9919658.

[bib.bib6] [6] Michael R. Clarkson, Bernd Finkbeiner, Masoud Koleini, Kristopher K. Micinski, Markus N. Rabe, and César Sánchez. Temporal logics for hyperproperties. In Martín Abadi and Steve Kremer, editors, POST 2014, volume 8414 of LNCS, pages 265–284. Springer, 2014. doi:10.1007/978-3-642-54792-8_15.

[bib.bib7] [7] Michael R. Clarkson and Fred B. Schneider. Hyperproperties. J. Comput. Secur., 18(6):1157–1210, 2010. doi:10.3233/JCS-2009-0393.

[bib.bib8] [8] Norine Coenen, Bernd Finkbeiner, César Sánchez, and Leander Tentrup. Verifying hyperliveness. In Isil Dillig and Serdar Tasiran, editors, CAV 2019, Part I, volume 11561 of LNCS, pages 121–139. Springer, 2019. doi:10.1007/978-3-030-25540-4_7.

[bib.bib9] [9] Samuel Eilenberg. Automata, languages, and machines. A. Pure and applied mathematics. Academic Press, 1974. URL: https://www.worldcat.org/oclc/310535248.

[bib.bib10] [10] E. Allen Emerson and Joseph Y. Halpern. “Sometimes” and “not never” revisited: on branching versus linear time temporal logic. J. ACM, 33(1):151–178, 1986. doi:10.1145/4904.4999.

[bib.bib11] [11] Joost Engelfriet. Top-down tree transducers with regular look-ahead. Math. Syst. Theory, 10:289–303, 1977. doi:10.1007/BF01683280.

[bib.bib12] [12] Emmanuel Filiot and Sarah Winter. Synthesizing computable functions from rational specifications over infinite words. Int. J. Found. Comput. Sci., 35(01n02):179–214, 2024. doi:10.1142/S012905412348009X.

[bib.bib13] [13] Bernd Finkbeiner, Christopher Hahn, Jana Hofmann, and Leander Tentrup. Realizing omega-regular hyperproperties. In Shuvendu K. Lahiri and Chao Wang, editors, CAV 2020, Part II, volume 12225 of LNCS, pages 40–63. Springer, 2020. doi:10.1007/978-3-030-53291-8_4.

[bib.bib14] [14] Bernd Finkbeiner, Markus N. Rabe, and César Sánchez. Algorithms for Model Checking HyperLTL and HyperCTL^∗. In Daniel Kroening and Corina S. Pasareanu, editors, CAV 2015, Part I, volume 9206 of LNCS, pages 30–48. Springer, 2015. doi:10.1007/978-3-319-21690-4_3.

[bib.bib15] [15] Erich Grädel, Wolfgang Thomas, and Thomas Wilke, editors. Automata, Logics, and Infinite Games: A Guide to Current Research, volume 2500 of LNCS. Springer, 2002. doi:10.1007/3-540-36387-4.

[bib.bib16] [16] Frederick A. Hosch and Lawrence H. Landweber. Finite delay solutions for sequential conditions. In ICALP 1972, pages 45–60, 1972.

[bib.bib17] [17] Felix Klein and Martin Zimmermann. How much lookahead is needed to win infinite games? Log. Methods Comput. Sci., 12(3), 2016. doi:10.2168/LMCS-12(3:4)2016.

[bib.bib18] [18] Corto Mascle and Martin Zimmermann. The keys to decidable HyperLTL satisfiability: Small models or very simple formulas. In Maribel Fernández and Anca Muscholl, editors, CSL 2020, volume 152 of LIPIcs, pages 29:1–29:16. Schloss Dagstuhl – Leibniz-Zentrum für Informatik, 2020. doi:10.4230/LIPIcs.CSL.2020.29.

[bib.bib19] [19] Daryl McCullough. Noninterference and the composability of security properties. In SSP 1988, pages 177–186. IEEE Computer Society, 1988. doi:10.1109/SECPRI.1988.8110.

[bib.bib20] [20] Amir Pnueli. The temporal logic of programs. In FOCS 1977, pages 46–57. IEEE, October 1977. doi:10.1109/SFCS.1977.32.

[bib.bib21] [21] Amir Pnueli and Roni Rosner. Distributed reactive systems are hard to synthesize. In FOCS 1990, Volume II, pages 746–757. IEEE Computer Society, 1990. doi:10.1109/FSCS.1990.89597.

[bib.bib22] [22] Markus N. Rabe. A temporal logic approach to information-flow control. PhD thesis, Saarland University, 2016. URL: http://scidok.sulb.uni-saarland.de/volltexte/2016/6387/.

[bib.bib23] [23] A. Prasad Sistla, Moshe Y. Vardi, and Pierre Wolper. The complementation problem for Büchi automata with appplications to temporal logic. Theor. Comput. Sci., 49:217–237, 1987. doi:10.1016/0304-3975(87)90008-9.

[bib.bib24] [24] Sarah Winter and Martin Zimmermann. Finite-state strategies in delay games. Inf. Comput., 272:104500, 2020. doi:10.1016/J.IC.2019.104500.

[bib.bib25] [25] Sarah Winter and Martin Zimmermann. Prophecies all the way: Game-based model-checking for HyperQPTL beyond $\forall^{*}\exists^{*}$ . arXiv, 2504.08575, 2025. doi:10.48550/arXiv.2504.08575.

Prophecies All the Way: Game-Based Model-Checking for HyperQPTL Beyond ∀∗∃∗