On Parity Game Preorders and the Logic of Matching Plays

Abstract

Parity games can be used to solve satisfiability, verification and controller synthesis problems. As part of an effort to better understand their nature, or the nature of the problems they solve, preorders on parity games have been studied. Defining these relations, and in particular proving their transitivity, has proven quite difficult on occasion. We propose a uniform way of lifting certain preorders on Kripke structures to parity games and study the resulting preorders. We explore their relation with parity game preorders from the literature and we study new relations. Finally, we investigate whether these preorders can also be obtained via modal characterisations of the preorders.

These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.

1 Introduction

Parity games [6, 15] are two player games played on a directed graph. These games are interesting as they underpin, e.g. solutions to verification, satisfiability and synthesis problems, see [2, 7] and they appear as solution to fundamental problems such as complementing tree automata [6]. The problem of solving a parity game (computing the set of vertices won by each player) is one of those rare problems that are in $\text {NP}\cap \text {coNP}$, and for which no polynomial time algorithm has yet been found.

In an effort to increase the general understanding of the parity game solving problem or of those problems mapped to parity game solving, preorders on parity games have been studied on various occasions and for different purposes. For instance, in [13], Namjoshi investigated simulation in the context of abstraction using a variant of parity games called model checking games, leading to a framework that was complete (in the sense of having finite abstract objects) for the $\mu$-calculus; in [8], Fritz and Wilke [8] defined and studied delayed simulation, an adaptation of simulation; Cranen et al. [3, 4] studied variations of stuttering bisimulation for parity games; Kissig and Venema [12] defined basic game bisimulation for studying complementation. Dawar and Grädel [5] defined yet two other forms of bisimulation on parity games by viewing these as relational structures; their purpose is to analyse the descriptive complexity of parity games.

For the most part, the preorders on parity games are inspired by similar relations on computational models such as Kripke structures or Labelled Transition Systems. However, there seems to be no systematic method by which the aforementioned parity game relation have been obtained from a relation on a computational model, as testified by the existence of several variations of bisimulation on parity games. Moreover, defining new relations on parity games, showing transitivity and proving that they approximate the winning set of some player can be quite cumbersome; for instance, proving transitivity of delayed simulation required analysing 24 different cases, see [8], and in [4], the proof that governed stuttering bisimilarity is an equivalence relation is technically involved, requiring a step-wise rephrasing of the definition and intricate arguments.

The contributions of this paper are as follows. We propose a novel, more generic method for obtaining a parity game relation from a relation on a computational model. It is based on the notion of matching paths, which we lift naturally to matching plays. In this approach, we can lift any preorder on a computational model that can be specified using the matching paths to a corresponding preorder in the parity game setting. Moreover, we identify conditions that guarantee that the resulting relation is a preorder and that it approximates the winning set of a particular player.

We exemplify our approach using a number of well-known and some less-known relations on Kripke structures and show that some of the thus obtained relations coincide with existing parity game relations. Finally, for all the relations we study in detail, we provide logical characterisations, by identifying sound and complete fragments of an alternating-time temporal logic for the respective relations. The logical characterisations reveal interesting differences between the behavioural relations and the induced parity game relations.

Structure. In Sect. 2, we recall the basics of parity games. Then, in Sect. 3, we introduce our generic scheme for obtaining parity game relations. In Sect. 4, we show how this theory can be applied to recover existing and define new parity game preorders; in Sect. 5, we provide modal characterisations of these relations. We finish with conclusions in Sect. 6. Proofs for all results can be found in [10].

2 Preliminaries

A parity game is an infinite duration game, played by players odd, denoted by $\square$ and even, denoted by $\Diamond$, on a directed, finite graph.

Definition 1

A parity game is a tuple $\langle V, E, \varOmega , (V_\Diamond ,V_\square ) \rangle$, where

• V is a set of vertices, partitioned in a set $V_\Diamond$ of vertices owned by player $\Diamond$, and a set of vertices $V_\square$ owned by player $\square$,

• $E \subseteq V \times V$ is a total edge relation, i.e. for all v, $(v,w) \in E$ for some w,

• $\varOmega {:}V \rightarrow \mathbb {N}$ is a priority function that assigns priorities to vertices.

We depict parity games as graphs in which diamond-shaped vertices represent vertices owned by player $\Diamond$, box-shaped vertices represent vertices owned by player $\square$ and priorities, associated with vertices, are written inside vertices; see Fig. 1(a) and (b) for examples.

Fig. 1.

(a) Left: A parity game with three different priorities. (b) Right: A parity game with four different priorities.

We use the following notational conventions: we write $v \rightarrow w$ instead of $(v,w) \in E$, and we write $v^{\bullet }$ for the set $\{w \in V ~|~ v \rightarrow w\}$. Henceforth, denotes an arbitrary player. We write for ’s opponent; i.e. and $\bar{\square }=\Diamond$. Finally, given the set of vertices V, the subset of vertices of V with priority n is denoted $V_n$: we have $V_n = \{v \in V ~|~ \varOmega (v) = n\}$.

A play starts by placing a token on some vertex $v \in V$. Players $\Diamond$ and $\square$ move the token indefinitely according to a single simple rule: if the token is on some vertex that belongs to player , that player gets to move the token to an adjacent vertex. The parity of the highest priority that occurs infinitely often on a play defines the winner of the play: player $\Diamond$ wins if, and only if this priority is even. This is known as the parity condition.

A strategy for player is a partial function $\sigma {:}V^* \rightarrow V$ satisfying that for all sequences of vertices $u_1 \cdots u_n \in V^*$ on which $\sigma$ is defined, both and $\sigma (u_1\cdots u_n) \in u_n^{\bullet }$. The set of all strategies for player is denoted .

Let $\pi = v_1\ v_2\ v_3 \cdots$, with $v_1 = v$ be a play starting in v. We denote the i-th vertex on $\pi$ by $\pi _i$; that is, $\pi _i = v_i$. Play $\pi$ is consistent with a strategy if all prefixes $v_1 \cdots v_n$ of $\pi$ for which $\sigma (v_1\ \cdots v_n)$ is defined, we have $v_{n+1} = \sigma (v_1 \cdots v_n)$. The set of plays consistent with strategy $\sigma$, starting in v is denoted $\textsf {Plays}(\sigma ,v)$; we sometimes refer to this set as the set of $\sigma$-plays. A strategy $\sigma$ is winning for player from vertex v iff all plays consistent with $\sigma$ are won by . Vertex v is won by player whenever she has a winning strategy for vertex v.

Example 1

In the parity game depicted in Fig. 1(a), $v_1,v_2,v_5$ are won by player $\Diamond$, and player $\square$ wins the remaining vertices.

Let $C, D \subseteq V$ be sets of vertices. We generalise the one-step reachability relation E to (forced) reachability, where reachability is confined to a set of vertices. Let $v \in V$.

Finally, let $R \subseteq V \times V$ be a relation on V. The set of vertices below some vertex v, denoted $R v$, is the set $\{w \in V ~|~ w\mathrel {R} v\}$; the set of vertices above v, denoted $v R$, is defined as $\{w \in V ~|~ v \mathrel {R} w\}$. Note that in the special case that R is an equivalence relation, we have $R v = v R$. For a set $U \subseteq V$, we write $U R$ for the set $\bigcup _{v \in U} v R$; likewise for $R U$, and if R is an equivalence relation, we write $V_{/R}$ for the set of equivalence classes (quotient set) of R.

3 Inducing Parity Game Preorders and Equivalences

In the past, behavioural relations for transition systems, such as the simulation preorder and bisimulation, have been ported to parity games, see [3–5, 8, 9, 12]. These efforts, however, did not appear to have followed a general guiding principle. In this section, we propose a scheme for lifting particular types of behavioural preorders for Kripke structures to parity game preorders. More specifically, the Kripke structure preorders and equivalences we consider are those that can be phrased in terms of matching paths.

Let $K = \langle S, T, \textsf {AP}, \mathcal {L} \rangle$ be an arbitrary Kripke structure, where S is a (possibly infinite) set of states, $T \subseteq S \times S$ is a total transition relation, $\textsf {AP}$ is a set of atomic propositions and $\mathcal {L} {:} S \rightarrow \mathcal {P}(\textsf {AP})$ is a state labelling function. A path through K, starting in some state $s_1 \in S$, is an infinite sequence of states $s_1\ s_2\ s_3\ \dots$ for which $(s_i,s_{i+1}) \in T$ for all i, and $\textsf {Paths}(s)$ denotes the set of paths starting in s.

Let, within the context of some Kripke structure K, ${\textsf {Rel}}(R)$ denote a predicate on relations $R \subseteq S \times S$ on K’s states. Think, for instance, of the predicate that a relation R is a simulation relation. For given predicate ${\textsf {Rel}}$ and relation R, a matching predicate is a predicate ${{\textsf {Rel}}-}\textsf {match}_{{R}}^{{\mathcal {L}}}(\pi _t,\pi _s)$ on paths $\pi _t$ and $\pi _s$ in K, and K’s labelling $\mathcal {L}$ and the relation R on K’s states satisfying:

$$ {\textsf {Rel}}(R) \text { iff } \forall (s,t) \in R:~ \forall \pi _s \in \textsf {Paths}(s):~ \exists \pi _t \in \textsf {Paths}(t):~ {{\textsf {Rel}}-}\textsf {match}_{{R}}^{{\mathcal {L}}}(\pi _t,\pi _s) $$

Note that matching predicates do not use K’s transition relation T.

Example 2

A typical instance of ${\textsf {Rel}}$ is the simulation predicate $\textsf {Sim}$: for $R \subseteq S \times S$, ${\textsf {Sim}}(R)$ holds iff for all $(s,t) \in R$ we have $\mathcal {L}(s) = \mathcal {L}(t)$ and for any $s' \in S$ with $(s,s') \in T$, there is a $t' \in S$ for which $(t,t') \in T$ and $(s',t') \in R$. An associated matching predicate ${\textsf {Sim}-}\textsf {match}_{{R}}^{{\mathcal {L}}}(\pi ,\pi ')$ is $\forall i:~ \mathcal {L}(\pi _i') = \mathcal {L}(\pi _i) \wedge \pi '_i \mathrel {R} \pi _i$.

In case a matching predicate is to be interpreted on a parity game, we use the priority function $\varOmega$ as the state labelling function, writing ${{\textsf {Rel}}-}\textsf {match}_{{R}}^{{\varOmega }}$. A matching predicate ${{\textsf {Rel}}-}\textsf {match}_{{}}^{{\mathcal {L}}}$ is monotonic if ${{\textsf {Rel}}-}\textsf {match}_{{R}}^{{\mathcal {L}}}(\pi _t,\pi _s)$ implies ${{\textsf {Rel}}-}\textsf {match}_{{R'}}^{{\mathcal {L}}}(\pi _t,\pi _s)$ for all $R \subseteq R'$.

Definition 2

Let $G = \langle V, E, \varOmega , (V_\Diamond , V_\square ) \rangle$ be a parity game and let ${{\textsf {Rel}}-}\textsf {match}_{{R}}^{{\mathcal {L}}}$ be a matching predicate for a predicate ${\textsf {Rel}}$ on Kripke structure relations. A relation $R\subseteq V \times V$ is a parity game ${\textsf {Rel}}$ -relation whenever $v\mathrel {R}w$ implies that for all strategies $\sigma _v \in \mathbb {S}^*_{\Diamond }$, there is a strategy $\sigma _w \in \mathbb {S}^*_{\Diamond }$ such that

$$ \forall \pi _w \in \textsf {Plays}(\sigma _w,w): \exists \pi _v \in \textsf {Plays}(\sigma _v,v): {{\textsf {Rel}}-}\textsf {match}_{{R}}^{{\varOmega }}(\pi _w,\pi _v) $$

We write $v \mathrel {\mathrel {\sqsubseteq _{{\textsf {Rel}}}}} w$ iff for some parity game ${\textsf {Rel}}$-relation R we have $v \mathrel {R} w$.

Example 3

A relation $R \subseteq V \times V$ is a parity game $\textsf {Sim}$ -relation whenever $v \mathrel {R} w$ implies that for all strategies $\sigma _v \in \mathbb {S}^*_{\Diamond }$, there is a strategy $\sigma _w \in \mathbb {S}^*_{\Diamond }$ such that

$$ \forall \pi _w \in \textsf {Plays}(\sigma _w,w):~ \exists \pi _v \in \textsf {Plays}(\sigma _v,v):~ \forall i:~ \varOmega (\pi _{v,i}) = \varOmega (\pi _{w,i}) \wedge \pi _{v,i} \mathrel {R} \pi _{w,i} $$

In Sects. 4.1 and 4.2, we study further instances of Definition 2, showing that the theory of this section can be used to recover existing parity game relations (Sect. 4.1) and how it can be used to obtain new parity game relations (Sect. 4.2). For the remainder of this section, we focus on establishing under which conditions one can prove the resulting parity game relations are preorders and when they can be used to approximate the winning partition for player $\Diamond$. The theorem below shows that an induced parity game ${\textsf {Rel}}$-relation is a preorder whenever a simple monotonicity criterion for the matching predicate holds.

Theorem 1

Assume that for all preorders R for which ${\textsf {Rel}}$ holds, ${{\textsf {Rel}}-}\textsf {match}_{{R}}^{{\mathcal {L}}}$ is a preorder, too. If ${{\textsf {Rel}}-}\textsf {match}_{{}}^{{\mathcal {L}}}$ is monotonic, then ${\mathrel {\sqsubseteq _{\textsf {Rel}}}}$ is a preorder.

Under similar conditions, one can prove that ${\mathrel {\sqsubseteq _{\textsf {Rel}}}}$ is an equivalence relation. The next theorem states that we can conclude that the parity game relations under-approximate the winning partition for player $\Diamond$ from a simple condition on the matching predicate.

Theorem 2

Let R be a parity game ${\textsf {Rel}}$-relation. Assume $v \mathrel {R} w$ and suppose that for all $\pi _v, \pi _w$, if ${{\textsf {Rel}}-}\textsf {match}_{{R}}^{{\varOmega }}(\pi _w,\pi _v)$ and $\pi _v$ is won by $\Diamond$ then so is $\pi _w$. If v is won by $\Diamond$, then w is won by $\Diamond$.

4 Applications

We first illustrate how the theory we developed in the previous section can be put to use to recover preorders and equivalences already present in the literature. More specifically, we show that governed simulation [11], also known as direct simulation [8, 9], governed bisimulation [11] and governed stuttering bisimulation [4] are all instances of our general theory. We then proceed to show that we can also obtain relations that did not appear in the literature.

4.1 Existing Parity Game Relations

Consider the Kripke structure ${\textsf {Rel}}$ predicates for simulation, bisimulation and stuttering bisimulation (aka stuttering equivalence), listed in Table 1. For lack of space, we refrain from giving the standard definition of these predicates, given that these can be found in most standard textbooks, and since these predicates are essentially also defined via their matching predicates next to them. Note that also the latter can be found in the literature (although less commonly).

Table 1. Matching predicates for well-known behavioural relations; R is a relation on states, $\mathcal {L}$ is a state labelling function, and $\pi , \pi '$ are infinite sequences of states

Using the ${\textsf {Rel}}$-predicates of Table 1 and Definition 2, we immediately obtain parity game simulation, parity game bisimulation and parity game stuttering bisimulation. One can check with little effort that the matching predicates for simulation, bisimulation and stuttering bisimulation meet the conditions of Theorems 1 and 2. As a result, we can claim the following:

Proposition 1

Relation ${\mathrel {\sqsubseteq _{\text {simulation}}}}$ is a preorder and relations ${\mathrel {\sqsubseteq _{\text {bisimulation}}}}$ and ${\mathrel {\sqsubseteq _{\text {stuttering bisimulation}}}}$ are equivalences. Moreover, all three relations under-approximate the winning set for player $\Diamond$.

Definition 3

A relation R is a governed simulation iff for all $v \mathrel {R} w$:

• 1. $\varOmega (v) = \varOmega (w)$,

• 2. if $v \in V_\Diamond$, then for each $v \rightarrow v'$ we have ,

• 3. if $v \in V_{\square }$, then .

We write $v \mathrel {\le }w$ iff there is a governed simulation R such that $v \mathrel {R} w$. A relation $R \subseteq V \times V$ is a governed bisimulation if both R and $R^{-1}$ are governed simulations. We write $v \;\underline{ \leftrightarrow }\;w$ iff for some governed bisimulation R, $v \mathrel {R} w$.

The example below illustrates governed simulation and governed bisimulation.

Example 4

Consider the parity game of Fig. 1(a). We have $v_3 \;\underline{ \leftrightarrow }\;v_4$, because, even though both vertices belong to different players, neither player can force play to vertices of different priorities. On the other hand, $v_1 \;\underline{ \leftrightarrow }\;v_2$ does not hold.

The theorem below confirms that governed similarity and governed bisimilarity coincide with the preorder and equivalence induced by Definition 2 using the simulation and bisimulation matching predicates of Table 1.

Theorem 3

We have $\mathrel {\le }= {\mathrel {\sqsubseteq _{\text {simulation}}}}$ and $\;\underline{ \leftrightarrow }\;= {\mathrel {\sqsubseteq _{\text {bisimulation}}}}$.

Next, we focus on the notion of governed stuttering bisimulation [4].

Definition 4

An equivalence relation $R \subseteq V \times V$ is a governed stuttering bisimulation iff $v \mathrel {R} w$ then

• 1. $\varOmega (v) = \varOmega (w)$,

• 2. for any $v \rightarrow \mathcal {C}$ with $\mathcal {C} \in V_{/R}\setminus \{v R\}$ and , then ,

• 3. for any player , we have iff .

We write $v \mathrel {{\;\underline{ \leftrightarrow }\;}_s} w$ iff there is a governed stuttering bisimulation R such that $v \mathrel {R} w$.

Example 5

Reconsider the parity game from Fig. 1(a). Observe that we did not have $v_1 \;\underline{ \leftrightarrow }\;v_2$. However, we do have $v_1 \mathrel {{\;\underline{ \leftrightarrow }\;}_s} v_2$: player $\Diamond$ is capable of enforcing divergent plays (plays that only pass through vertices with the same priority), and it is capable of enforcing plays to reach vertices with priority 1.    $\square$

Governed stuttering bisimulation coincides with parity game stuttering bisimulation; this confirms that governed stuttering bisimulation naturally generalises Kripke structure stuttering bisimulation to the parity game setting.

Theorem 4

We have $\mathrel {{\;\underline{ \leftrightarrow }\;}_s} = {\mathrel {\sqsubseteq _{\text {stuttering bisimulation}}}}$.

4.2 Two New Parity Game Relations

So far, we have illustrated that Definition 2 can be used to recover parity game relations from the literature, and that Theorems 1 and 2 are instrumental in establishing that the resulting parity game relations are preorders and that they approximate the winning set for player $\Diamond$. In this section, we show that Definition 2 immediately gives us definitions for parity game trace inclusion and parity game stuttering simulation; these relations have so far not appeared in the literature. Consider the matching predicates listed in Table 2.

Table 2. Matching predicates for behavioural relations; R is a relation on states, $\mathcal {L}$ is a state labelling function, and $\pi , \pi '$ are infinite sequences of states

Stuttering simulation for Kripke structures is coarser than simulation: it allows for abstracting from finite computations through states with the same information and computational branching structure. Trace inclusion is even coarser than stuttering simulation. Both stuttering similarity and trace inclusion for Kripke structures are known to be preorders. Theorem 1 allows us to establish that the parity game relations they induce are preorders too. Theorem 2 again allows us to conclude that both preorders under-approximate the winning partition for player $\Diamond$.

Proposition 2

Relations ${\mathrel {\sqsubseteq _{\text {stuttering simulation}}}}$ and ${\mathrel {\sqsubseteq _{\text {trace inclusion}}}}$ are preorders. Both preorders under-approximate the winning partition for player $\Diamond$.

We next focus on giving a coinductive definition for parity game stuttering simulation. Apart from providing a deeper understanding of this relation, and understanding how it compares to the ones from the previous section, the coinductive definition gives rise to a polynomial time algorithm for deciding this relations.

Definition 5

A preorder $R \subseteq V \times V$ is a governed stuttering simulation iff $v \mathrel {R} w$ implies:

• 1. $\varOmega (v) = \varOmega (w)$,

• 2. left-to-right even transfer:

  • (a) if $v \in V_\Diamond$, then for all $v \rightarrow v_s$ we have ,

  • (b) if $v \in V_\square$, then ,

• 3. right-to-left odd transfer:

  • (a) if $w \in V_\Diamond$, then

  • (b) if $w \in V_\square$, then for all $w \rightarrow w_s$, we have

We write $v \mathrel {{\;\underline{ \leftrightarrow }\;}_s} w$ iff there is a governed stuttering bisimulation R such that $v \mathrel {R} w$.

For the above coinductive definition of our parity game stuttering simulation relation one can deduce that a symmetric relation that meets its properties is a governed stuttering bisimulation relation—a basic sanity check for the correctness of the definition. The link with governed stuttering bisimulation is, however, not obvious. We have the following theorem relating governed stuttering simulation to parity game stuttering simulation.

Theorem 5

We have $\mathrel {\le }_s = {\mathrel {\sqsubseteq _{\text {stuttering simulation}}}}$.

Governed stuttering simulation can be computed in polynomial time; we sketch a naive algorithm based on fixpoint iteration. We start with a trivial relation R that relates all states with the same priorities. Upon every iteration, every pair $(s,t) \in R$ is checked as to whether the conditions of Definition 5 hold; if it is not the case, the pair is removed from R; thus every iteration a monotonic transformer is applied that after at most a quadratic number of steps will reach a fixpoint. As for checking that s, t and R meet the conditions of Definition 5, the main source of the complexity is in computing the relation. The latter can be done in $\mathcal {O}(|V|+|E|)$ time using a modified attractor computation [4] and such a computation is performed for O(|V|) successors. This means that deciding governed stuttering simulation can be done in at most $\mathcal {O}(|V|^5 \cdot (|V| + |E|))$.

We remark that we did not strive to have optimal running times for deciding the preorders in this section. We leave it for future research to tighten our bounds. For deciding governed stuttering simulation, it may be fruitful to incorporate ideas from [14], which describes, as far as we could trace, the first algorithm for stuttering simulation in the Kripke structure setting.

5 Logical Characterisations of Parity Game Relations

An alternative approach to defining a behavioural preorder is by identifying an appropriate fragment of a modal logic. A natural question is thus whether, given a fragment of a modal logic for Kripke structures that coincides with a given preorder, there is a uniform way of obtaining a fragment of a modal logic for parity games that coincides with the parity game relation. While a logical characterisation of a behavioural relation offers an alternative angle for understanding it, and, as such, is interesting to study in its own right, our results in this section suggest it is unlikely such a uniform method exists.

5.1 A Modal Logic for Parity Games

The logic we consider is called the Alternating-time Hennessy-Milner logic with Until. It is essentially based on the alternating-time temporal logic of [1], but its syntax is inspired by Hennessy-Milner logic for Labelled Transition Systems. Our syntax facilitates characterising all relations we study in this paper by imposing restrictions on our base grammar.

Definition 6

The Alternating-time Hennessy-Milner logic with Until, henceforth referred to as the logic $\textsf {AHML}$, is defined as follows:

where $n \in \mathbb {N}$ and . The semantics of $\textsf {AHML}$ formulae is defined inductively in the context of a parity game $G = \langle V,E,\varOmega , (V_\Diamond ,V_\square )\rangle$:

where, for $W \subseteq V$ and $n \in \mathbb {N}$, operator yields the set . We write $v \models \phi$ iff $v \in \llbracket \phi \rrbracket$.

Intuitively, holds in vertices with priority n (i.e. those from the set $V_n$) for which can force play to vertices satisfying $\phi$. The strong until operator holds in vertices with priority n for which can govern the plays through $\phi$ vertices, ultimately reaching $\psi$ vertices. The weak until operator is more or less the same but also holds whenever governs plays through $\phi$-invariant vertices. Observe that our use of fixpoints in the semantics is permitted as the associated predicate transformers to which they are applied are monotonic and the set $(2^V,\subseteq )$ is a complete lattice. The example below illustrates typical properties one can express using $\textsf {AHML}$.

Example 6

Reconsider the parity game depicted in Fig. 1(a). Observe that $v_1 \models \langle 0 \rangle \!_{\Diamond }\top$ and $v_1 \models \langle 0 \rangle \!_{\square }\top$. We have $v_3 \models \top \mathop {\langle \!\langle 1 \rangle \!\rangle \!_{\Diamond }^\infty }\bot$ and $v_3 \models \top \mathop {\langle \!\langle 1 \rangle \!\rangle \!_{\square }^\infty }\bot$; we also have $v_2 \models \top \mathop {\langle \!\langle 0 \rangle \!\rangle \!_{\Diamond }^\infty }\bot$ but $v_2 \not \models \top \mathop {\langle \!\langle 0 \rangle \!\rangle \!_{\square }^\infty }\bot$. Moreover, we have $v_7 \models (\langle 1 \rangle \!_{\Diamond }\top )\mathop {\langle \!\langle 2 \rangle \!\rangle \!_{\Diamond }}{\lnot (\langle 0 \rangle \!_{\Diamond }\top )}$ because $v_7$ has (1) priority 2 as demanded by the until operator and (2) satisfies the goal formula $\lnot (\langle 0 \rangle \!_{\Diamond }\top )$.   $\square$

In general, we are interested in comparing the “observations” that we can make in different vertices in a parity game; that is, we wish to compare the set of modal formulae satisfied by different vertices. We formalise observations as follows.

Definition 7

Let L be a fragment of $\textsf {AHML}$. We write $\mathcal {O}^{L}(v)$ to denote the set of formulae $\phi \in L$ for which $v \models \phi$.

5.2 Characterising Preorders Using $\textsf {AHML}$

Throughout this section, we assume that $G = \langle V, E, \varOmega , (V_\Diamond , V_\square )\rangle$ is an arbitrary parity game. In Table 3, we list the sound and complete fragments of the modal logic of Sect. 5.1 and the relations of Sects. 4.1 and 4.2.

Table 3. Parity game preorders and equivalences and their corresponding sound and complete fragments of $\textsf {AHML}$ with their grammars. In these grammars, $n \in \mathbb {N}$

Before we address the soundness and completeness of the fragments of the modal logic listed in Table 3, we first point out that there are interesting and fundamental differences with the modal characterisations for the preorders on computational models such as Kripke structures. For instance, disjunction is a necessary part of the logic for the simulation relations in the parity game setting: without it, one cannot show that $w \mathrel {\le }v$ does not hold in the following game:

While disjunction can be part of the characteristic logic for the corresponding Kripke structure preorders, there, it is redundant: it does not add to the distinguishing power of the modal logic. This can be explained by the phenomenon that in the Kripke structure setting, it suffices to describe one fixed behaviour. In the parity game setting, one must be able to express that a player can guarantee (i.e. regardless of the strategies of her opponent) a certain set of behaviours; this requires disjunctions. As we will show in Example 9, it is also not the case that disjunction can be added harmlessly to the characteristic logic for a parity game preorder. This suggests there is no easy way to obtain a modal characterisation for a parity game preorder from a modal characterisation of a Kripke structure preorder.

We next state the relation between the fragments identified in Table 3 and the studied preorders, and we illustrate these correspondences using small examples.

Theorem 6

Let v, w be arbitrary vertices in G. Then:

• 1. $v \mathrel {\le }w$ iff $\mathcal {O}^{\textsf {AHML} ^{\mathrel {\le }}}(v) \subseteq \mathcal {O}^{\textsf {AHML} ^{\mathrel {\le }}}(w)$;

• 2. $v \;\underline{ \leftrightarrow }\;w$ iff $\mathcal {O}^{\textsf {AHML} ^{\;\underline{ \leftrightarrow }\;}}(v) = \mathcal {O}^{\textsf {AHML} ^{\;\underline{ \leftrightarrow }\;}}(w)$;

Example 7

Consider the parity game of Fig. 1(a). Recall that ${v_1}\mathrel {\le }{v_2}$, see Example 4. We thus have $\mathcal {O}^{\textsf {AHML} ^{\mathrel {\le }}}(v_1) \subseteq \mathcal {O}^{\textsf {AHML} ^{\mathrel {\le }}}(v_2)$. For instance, both $v_1$ and $v_2$ satisfy $\langle 0 \rangle \!_{\Diamond }{\langle 0 \rangle \!_{\Diamond }\top }$. However, we do not have $v_2 \mathrel {\le }v_1$. This follows from the fact that $\langle 0 \rangle \!_{\Diamond }{\langle 1 \rangle \!_{\Diamond }{\top }}$ is a distinguishing formula that holds in $v_2$, but fails for $v_1$.    $\square$

Theorem 7

Let v, w be arbitrary vertices in G. Then

• 1. $v \mathrel {\le }_s w$ iff $\mathcal {O}^{\textsf {AHML} ^{\mathrel {\le }_s}}(v) \subseteq \mathcal {O}^{\textsf {AHML} ^{\mathrel {\le }_s}}(w)$.

• 2. $v \mathrel {{\;\underline{ \leftrightarrow }\;}_s} w$ iff $\mathcal {O}^{\textsf {AHML} ^{\mathrel {{\;\underline{ \leftrightarrow }\;}_s}}}(v) = \mathcal {O}^{\textsf {AHML} ^{\mathrel {{\;\underline{ \leftrightarrow }\;}_s}}}(w)$.

Example 8

One can check that in the parity game of Fig. 1(a), we do not have $v_5 \mathrel {\le }_s v_2$. This is confirmed by the formula $(\top \mathop {\langle \!\langle 0 \rangle \!\rangle \!_{\Diamond }}\top )\mathop {\langle \!\langle 0 \rangle \!\rangle \!_{\Diamond }}(\top \mathop {\langle \!\langle 2 \rangle \!\rangle \!_{\Diamond }}\top )$ that expresses that through vertices with priority 0, a vertex with priority 2 can be reached. It holds in $v_5$, but not in $v_2$.   $\square$

The relation between parity game trace inclusion and $\textsf {AHML} ^{\le _t}$ is given below.

Theorem 8

For all $v,w \in V$, we have $v {\mathrel {\sqsubseteq _{\text {trace inclusion}}}} w$ iff $\mathcal {O}^{\textsf {AHML} ^{\le _t}}(v) \subseteq \mathcal {O}^{\textsf {AHML} ^{\le _t}}(w)$.

The fragment of $\textsf {AHML}$ needed to characterise the parity game trace inclusion preorder is non-obvious. In particular, the restriction on $\textsf {AHML} ^{\le _t}$ to at all depths of the formulae only allow for $\langle n \rangle \!_{\Diamond }\_$ for which the priorities are distinct is needed to reduce player $\Diamond$’s powers. Omitting this constraint and allowing for arbitrary disjunctions will lead to a finer relation, as shown by the example below.

Example 9

Consider the parity game depicted below.

Clearly, we have $v \le _t w$. By Theorem 8 we have $\mathcal {O}^{\textsf {AHML} ^{\le _t}}(v) \subseteq \mathcal {O}^{\textsf {AHML} ^{\le _t}}(w)$. Note that we also have $w \le _t v$. However, we have but . Omitting the constraint on the disjunctions would therefore lead to incorrect distinguishing formulae.   $\square$

6 Conclusions

We proposed a scheme for lifting preorders on Kripke structures that can be defined through matching paths to preorders on parity games. We showed that our scheme can be used to recover preorders for parity games that have already been defined in the literature. Moreover, we demonstrated that we can easily construct new ones, such as parity game trace inclusion and parity game stuttering simulation, and prove such new relations are preorders (or equivalences) and that they approximate the winning partition of player $\Diamond$.

Our scheme for obtaining parity game relations from existing behavioural relations also extends to other relations by choosing different parameters for the matching predicate. For instance, the bisimulation of [5] on parity games with a finite number of priorities can be recovered using the matching predicate ${\text {bisimulation}-}\textsf {match}_{{R}}^{{\mathcal {L}}}$, where ; that is, the vertex labelling is extended with information which player owns the vertex. Observe that the resulting relation is finer than the ones studied in this paper.

Lastly, we provided modal characterisations of all parity game relations studied. Given the fundamental differences between these modal characterisations and their Kripke structure counterparts, we deem it highly unlikely that a logical approach to a systematic way of obtaining parity game relations from Kripke structure relations will be successful.