New Algorithms for Combinations of Objectives
using Separating Automata

We consider edge labelled directed graphs: a graph $G$ is given by a (finite) set $V$ of vertices and a (finite) set $E\subseteq V\times C\times V$ of edges, with $C$ a set of colours, so we write $G=(V,E)$. An edge $(v,c,v^{\prime})$ is from the vertex $v$ to the vertex $v^{\prime}$ and is labelled by the colour $c$. We sometimes refer to $V(G)$ for $V$ and $E(G)$ for $E$ to avoid any ambiguity. The size of a graph is its number of vertices. A vertex $v$ for which there exists no outgoing edges $(v,c,v^{\prime})\in E$ is called a sink.

A path $\pi$ is a (finite or infinite) sequence

where for all $i$ we have $(v_{\_}i,c_{\_}i,v_{\_}{i+1})\in E$. If it is finite, that is, $\pi=v_{\_}0c_{\_}0\dots c_{\_}{i-1}v_{\_}i$, we call $\textrm{len}(\pi)=i\geq 0$ the length of $\pi$, and use $\textrm{last}(\pi)$ to denote the last vertex $v_{\_}i$. The length of an infinite path is $\textrm{len}(\pi)=\infty$. We say that $\pi$ starts from $v_{\_}0$ or is a path from $v_{\_}0$, and in the case where $\pi$ is finite we say that $\pi$ is a path ending in $\textrm{last}(\pi)$ or simply a path to $\textrm{last}(\pi)$. We say that $v^{\prime}$ is reachable from $v$ if there exists a path from $v$ to $v^{\prime}$. We let $\pi_{\_}{\leq i}$ denote the prefix of $\pi$ of length $i$, meaning $\pi_{\_}{\leq i}=v_{\_}0c_{\_}0v_{\_}1\dots c_{\_}{i-1}v_{\_}i$. A cycle is a path from a vertex to itself of length at least one.

We use $\textrm{Path}_{\textrm{fin}}(G),\textrm{Path}_{\infty}(G)$ and $\textrm{Path}(G)$ to denote respectively the sets of finite paths of $G$, infinite paths of $G$, and their union. We sometimes drop $G$ when it is clear from context. For $v_{\_}0\in V$ we also use $\textrm{Path}_{\textrm{fin}}(G,v_{\_}0),\textrm{Path}_{\infty}(G,v_{\_}0)$ and $\textrm{Path}(G,v_{\_}0)$ to refer to the sets of paths starting from $v_{\_}0$. We use $\textrm{col}(\pi)$ to denote the (finite or infinite) sequence of colours $c_{\_}0c_{\_}1\dots$ induced by $\pi$.

An objective is a set $\Omega\subseteq C^{\omega}$ of infinite sequences of colours. We say that a sequence of colours belonging to $\Omega$ satisfies $\Omega$, and extend this terminology to infinite paths: $\pi$ satisfies $\Omega$ if $\textrm{col}(\pi)\in\Omega$.

A deterministic safety automaton over the alphabet $C$ is given by a finite set of states $Q$, an initial state $q_{\_}0\in Q$, and a transition function $\delta:Q\times C\to Q$, so we write $\mathcal{A}=(Q,q_{\_}0,\delta)$. Note that $\delta$ is a partial function, meaning that it may be that $\delta(q,c)$ is undefined for some $q,c\in Q\times C$. Such an automaton induces a graph whose set of vertices is $Q$ and set of edges is $E=\left\{(q,\delta(q,c)):q\in Q,c\in C\right\}$; we therefore use the terminology for graphs to speak about automata, and identify an automaton and the graph it induces. Since we are only considering deterministic safety automata in this paper, we omit the adjectives deterministic and safety and simply speak of an automaton. We extend $\delta$ to sequences of colours by the formulas $\delta^{*}(q,\epsilon)=q$ and $\delta^{*}(q,wc)=\delta(\delta^{*}(q,w),c)$. The language recognised by an automaton $\mathcal{A}$ is $L(\mathcal{A})$ defined by

Note that if $w$ is a finite prefix of a word in $L(\mathcal{A})$, then $\delta^{*}(q_{\_}0,w)$ is well defined.

An arena is given by a graph $G$ together with a partition $V=\textrm{V}_{\textrm{Eve}}\uplus\textrm{V}_{\textrm{Adam}}$ of its set of vertices describing which player controls each vertex.

A game is given by an arena and an objective $\Omega$. We often let $\mathcal{G}$ denote a game, its size is the size of the underlying graph. It is played as follows. A token is initially placed on some vertex $v_{\_}0$, and the player who controls this vertex pushes the token along an edge, reaching a new vertex; the player who controls this new vertex takes over and this interaction goes on either forever and describing an infinite path or until reaching a sink.

We say that a path is winning¹¹1We always take the point of view of Eve, so winning means winning for Eve, and similarly a strategy is a strategy for Eve. if it is infinite and satisfies $\Omega$, or finite and ends in a sink. The definition of a winning path includes the following usual convention: if a player cannot move they lose, in other words sinks controlled by Adam are winning (for Eve) and sinks controlled by Eve are losing.

We extend the notations $\textrm{Path}_{\textrm{fin}},\textrm{Path}_{\infty}$ and Path to games by considering the underlying graph.

A strategy in $\mathcal{G}$ is a partial map $\sigma:\textrm{Path}_{\textrm{fin}}(\mathcal{G})\to E$ such that $\sigma(\pi)$ is an outgoing edge of $\textrm{last}(\pi)$ when it is defined. We say that a path $\pi=v_{\_}0c_{\_}0v_{\_}1\dots$ is consistent with $\sigma$ if for all $i<\textrm{len}(\pi)$, if $v_{\_}i\in\textrm{V}_{\textrm{Eve}}$ then $\sigma$ is defined over $\pi_{\_}{\leq i}$ and $\sigma(\pi_{\_}{\leq i})=(v_{\_}i,c_{\_}i,v_{\_}{i+1})$. A consistent path with $\sigma$ is maximal if it is not the strict prefix of a consistent path with $\sigma$ (in particular infinite consistent paths are maximal).

A strategy $\sigma$ is winning from $v_{\_}0$ if all maximal paths consistent with $\sigma$ are winning. Note that in particular, if a finite path $\pi$ is consistent with a winning strategy $\sigma$ and ends in a vertex which belongs to Eve, then $\sigma$ is defined over $\pi$. We say that $v_{\_}0$ is a winning vertex of $\mathcal{G}$ or that Eve wins from $v$ in $\mathcal{G}$ if there exists a winning strategy from $v_{\_}0$.

Positional strategies make decisions only considering the current vertex. Such a strategy is given by $\widehat{\sigma}:\textrm{V}_{\textrm{Eve}}\to E$. A positional strategy induces a strategy $\sigma:\textrm{Path}_{\textrm{fin}}\to E$ from any vertex $v_{\_}0$ by setting ${\sigma}(\pi)=\widehat{\sigma}(\textrm{last}(\pi))$ when $\textrm{last}(\pi)\in\textrm{V}_{\textrm{Eve}}$.

Given a game $\mathcal{G}$, a vertex $v_{\_}0$, and a positional strategy $\sigma$ we let $\mathcal{G}[\sigma,v_{\_}0]$ denote the graph obtained by restricting $\mathcal{G}$ to vertices reachable from $v_{\_}0$ by playing $\sigma$ and to the moves prescribed by $\sigma$. Formally, the set of vertices and edges is

In this paper we will consider prefix independent objectives for technical convenience.

The decision problem we consider in this paper, called solving a game, is the following: given a game $\mathcal{G}$ and an initial vertex $v_{\_}0$, does Eve have a winning strategy from $v_{\_}0$ in $\mathcal{G}$? Each objective yields a class of games, so we speak for instance of “solving mean payoff games”.

The complexity of solving a game depends on a number of parameters originating either from the underlying graph or the objective. Some of the objectives involve rational numbers. The typical parameters from the underlying graph are the number $n$ of vertices and the number $m$ of edges.

We use the classical Random Access Model (RAM) of computation with fixed word size, which is the size of a memory cell on which arithmetic operations take constant time. We specify for each class of objectives the word size.

The safety objective $\mathtt{Safe}$ is defined over the set of colours $C=\left\{\varepsilon\right\}$ by $\mathtt{Safe}=\left\{\varepsilon^{\omega}\right\}$: in words, all infinite paths are winning, so losing for Eve can only result from reaching a sink that she controls. Since there is a unique colour, when manipulating safety games we ignore the colour component for edges.

Note that in safety games, strategies can equivalently be defined as maps to $V$ (and not $E$): only the target of an edge matters when the source is fixed, since there is a unique colour. We use this abuse of notations for the sake of simplicity and conciseness.

Let $\mathcal{A}=(Q,q_{\_}0,\delta)$ be an automaton and $\mathcal{G}$ a game with objective $\Omega$. We define the chained game $\mathcal{G}\triangleright\mathcal{A}$ as the safety game with vertices $V^{\prime}=\textrm{V}_{\textrm{Eve}}^{\prime}\uplus\textrm{V}_{\textrm{Adam}}^{\prime}$ and edges $E^{\prime}$ given by

In words, from $(v,q)\in V\times Q$, the player whom $v$ belongs to chooses an edge $(v,c,v^{\prime})\in E$, and the game progresses to $(v^{\prime},\delta(q,c))$ if $q$ has an outgoing edge with colour $c$ in $\mathcal{A}$, and to $\bot$ otherwise, which is losing for Eve.

Note that the obtained game $\mathcal{G}\triangleright\mathcal{A}$ is a safety game: Eve wins if she can play forever or end up in a sink controlled by Adam.

It is not hard to see that if $\mathcal{A}$ is deterministic and recognises exactly $\Omega$, then $\mathcal{G}$ and $\mathcal{G}\triangleright\mathcal{A}$ are equivalent. However, for many objectives $\Omega$ (for instance, parity or mean payoff objectives), a simple topological argument shows that such deterministic automata do not exist. Separating automata are defined by introducing $n$ as a parameter, and relaxing the condition $L(\mathcal{A})=\Omega$ to the weaker condition $\Omega^{\mid n}\subseteq L(\mathcal{A})\subseteq\Omega$, where $\Omega^{\mid n}$ is the set of infinite sequence of colours that label paths from graphs of size at most $n$ satisfying $\Omega$. Formally²²2Here we use the fact that $\Omega$ is prefix independent to simplify the definition: we are considering infinite paths from any vertex of the graph. To extend this definition beyond prefix independent objectives we would need to fix an initial vertex.,

The definition given here differs from the original one given by Bojańczyk and Czerwiński [2], who use a different relaxation $\Omega_{\_}{\mid n}$ satisfying $\Omega^{\mid n}\subseteq\Omega_{\_}{\mid n}\subseteq\Omega$. Therefore a separating automaton in the sense of [2] is also a separating automaton in our sense (but not conversely).

The parity objective is defined over the set of colours $[0,d]\subseteq\mathbb{N}$, as follows:

As mentioned above, the definition of separating automata given in [2] is slightly different, but the result below indeed holds for both definitions, as explained in [8].

The mean payoff objective is defined over the set of colours $[-N,N]\subseteq\mathbb{Z}$, as follows: