On the size of disjunctive formulas in the $\mu$ -calculus

Clemens Kupke Partially supported by Leverhulme grant RPG-2020-232.University of Strathclyde
Glasgow, Scotland [email protected] ILLC, University of Amsterdam
Amsterdam, The Netherlands Johannes Marti Yde Venema The research of this author has been made possible by a grant from the Dutch Research Council NWO, project nr. 617.001.857.ILLC, University of Amsterdam
Amsterdam, The Netherlands [email protected] [email protected]

Abstract

A key result in the theory of the modal $\mu$ -calculus is the disjunctive normal form theorem by Janin & Walukiewicz, stating that every $\mu$ -calculus formula is semantically equivalent to a so-called disjunctive formula. These disjunctive formulas have good computational properties and play a pivotal role in the theory of the modal $\mu$ -calculus. It is therefore an interesting question what the best normalisation procedure is for rewriting a formula into an equivalent disjunctive formula of minimal size. The best constructions that are known from the literature are automata-theoretic in nature and consist of a guarded transformation, i.e., the constructing of an equivalent guarded alternating automaton from a $\mu$ -calculus formula, followed by a Simulation Theorem stating that any such alternating automaton can be transformed into an equivalent non-deterministic one. Both of these transformations are exponential constructions, making the best normalisation procedure doubly exponential. Our key contribution presented here shows that the two parts of the normalisation procedure can be integrated, leading to a procedure that is single-exponential in the closure size of the formula.

1 Introduction

The modal $\mu$ -calculus [2] is a general modal logic enriched with fixpoint operators that allow to reason about the ongoing, possibly infinite behaviour of a system. The generality and complexity of the modal $\mu$ -calculus calls for research into fragments of the logic. On the one hand, this concerns fragments tailor-made for certain application domains such as the temporal logics LTL, CTL or dynamic logics [21]. On the other hand, one focuses on fragments of the $\mu$ -calculus that are either semantically or syntactically well-behaved and where a better understanding increases our knowledge about the full $\mu$ -calculus. One key fragment of the latter kind is formed by the so-called disjunctive formulas [14] . These are formulas, where the use of conjunctions is strictly limited to conjunctions of propositional atoms and the formula $\top$ (thought of as the empty conjunction). We state the formal definition here - the meaning of the $\nabla$ -operator will be discussed later.

Definition 1.1

The set $\mu\mathrm{DML}$ of disjunctive $\mu$ -calculus formulas is given by the following grammar:

\varphi\mathrel{::=}\bot\mid\top\mid\bigwedge L\land\nabla\Phi\mid(\varphi_{\_}1\lor\varphi_{\_}2)\mid\mu p.\varphi\mid\nu p.\varphi

where $L$ is a finite set of literals (i.e., propositional variables or their negations), $\Phi$ is a finite set of formulas in $\mu\mathrm{DML}$ , and $p$ is a propositional variable. Furthermore we require that in a formula $\eta p.\varphi$ all occurrences of $p$ in $\varphi$ are positive, guarded and not in the context of a conjunction $p\land\psi$ .

While disjunctive formulas correspond to a proper syntactic fragment of the $\mu$ -calculus, it is a somewhat surprising fact that each formula of the $\mu$ -calculus is semantically equivalent to a disjunctive one. This has many applications, e.g., satisfiability checking of a disjunctive formula can be carried out efficiently [14] (being ExpTime-complete in for arbitrary formulas [8, 9]) and disjunctive formulas facilitate the computation of uniform interpolants [5, 6]. Furthermore, disjunctive formulas play a pivotal role in the completeness theory of the modal $\mu$ -calculus [24, 10]. Finally, disjunctive formulas also provide insights for characterising important semantic fragments such as the continuous, additive and monotone fragments of the modal $\mu$ -calculus [11].

Recipes to rewrite a given arbitrary $\mu$ -calculus formula into an equivalent disjunctive one are well-known [14]. The size of the resulting disjunctive formula is crucial, in particular, in connection with satisfiability and uniform interpolation. The construction of a disjunctive formula usually proceeds in two stages: first a given $\mu$ -calculus formula is transformed into an equivalent, possibly alternating modal automaton, which is then transformed into an equivalent non-deterministic “disjunctive” modal automaton. The latter can be easily translated back into a disjunctive formula. We will argue that the outlined two-stage construction will inevitably lead to a double-exponential blow-up in the size of the formula. This is, because the first move from formulas to automata involves bringing the formula into a guarded format, i.e., a form where each fixpoint variable is in the scope of at least one modality. That guarding is problematic has been observed in the work by Bruse et al. [3] - we will argue that it necessarily entails an exponential blow-up in the size of the structures involved.

This sets the stage for our main result: a procedure that directly turns an arbitrary, possibly unguarded formula in the modal $\mu$ -calculus into an equivalent disjunctive automaton of exponential size. The latter can be turned easily into a disjunctive formula, which leads to our main theorem.

Theorem 1.2

For any $\mu$ -calculus formula $\varphi$ we can construct an equivalent disjunctive $\mu$ -calulus formula $\varphi^{d}$ of size $2^{\mathcal{O}(n^{2}k\cdot\log(nk))}$ and alternation depth $\mathcal{O}(n\cdot k)$ , where $n=|\varphi|$ and where $k$ is the alternation depth of $\varphi$ .

In the above theorem, the size of a formula refers to the size of its Fisher-Ladner closure, which has been shown in [3] to provide the tightest measure of formula size. For a discussion and comparison of different size measures see [16] where we also propose so-called “parity formulas” as a versatile tool to study the complexity of formula constructions. Parity formulas are a graph-shaped variant of $\mu$ -calculus formulas which is closely related to Wilke’s alternating automata [25] and hierarchical equation systems [7]. While we stated the above theorem with reference to standard formulas, we will work throughout the paper with parity formulas instead. At the same time we will explain why Thm. 1.2 is a consequence of our work.

The outline of our paper is thus as follows: we will first introduce the necessary terminology for parity formulas, modal automata and their respective disjunctive variants. After that, in Section 3, we will discuss why guarding a parity formula can lead to an exponential blow-up. We then demonstrate that turning an arbitrary formula into an equivalent modal automaton is at least as costly as guarding a formula which means that the earlier mentioned two-stage method of constructing a disjunctive formula will in general lead to a double-exponential blow-up. Section 5 contains the central result of this paper, a construction that turns any given parity formula into an equivalent disjunctive modal automaton. This will provide a proof of Thm. 1.2.

Related Work. In addition to the already mentioned papers we would like to highlight a few more closely related lines of research. In spirit, our construction is related to the work by Friedmann & Lange on tableaux for unguarded $\mu$ -calculus formulas [12] but the cited paper is not concerned with disjunctive normal forms. Similarly, our automata theoretic result could be obtainable from a more general result in [22] - a key definition in that paper, however, appears to make an implicit assumption on the names of fixpoint variables (“cleanness”) whereas our results from [16] demonstrate that cleaning a formula can lead to an exponential blow-up in (closure) size. In addition, it is not clear how to extract a disjunctive formula from the purely automata-theoretic constructions in [22]. Finally, the work by Lehtinen [18] studies how the alternation depth of a formula relates to the alternation depth of an equivalent disjunctive formula. While it turns out that the difference in alternation depth can be arbitrarily big, we note that this is not in conflict with the bound in our theorem, as we refer to a particular disjunctive equivalent as opposed to an arbitrary one.

Acknowledgements. We would like to thank the anonymous referees for valuable comments that helped to improve this paper.

2 Preliminaries

2.1 The $\mu$ -calculus and parity formulas

We will now recall the standard syntax of the modal $\mu$ -calculus and its reformulation in terms of parity formulas. It will be convenient for us to assume that $\mu$ -calculus formulas are in so-called negation normal form. We assume an infinite set of propositional variables, and define a literal to be either a propositional variable $p$ or its negation $\overline{p}$ .

Definition 2.1

The formulas of the modal $\mu$ -calculus $\mu\mathtt{ML}$ are given by the following grammar:

\displaystyle\varphi

\displaystyle\mathrel{::=}

\displaystyle\ell\;\mid\;\bot\;\mid\;\top\;\mid\;(\varphi_{\_}{1}\lor\varphi_{\_}{2})\;\mid\;(\varphi_{\_}{1}\land\varphi_{\_}{2})\;\mid\;\Diamond\varphi\;\mid\;\Box\varphi\;\mid\;\mu p.\varphi\;\mid\;\nu p.\varphi,

where $\ell$ is a literal, $p$ is a propositional variable, and the formation of the formulas $\mu p.\varphi$ and $\nu p.\varphi$ is subject to the constraint that $\varphi$ is positive in $p$ , i.e., there are no occurrences of $\overline{p}$ in $\varphi$ . With $|\varphi|$ we denote the size of a formula measure in the number of distinct formulas in its Fisher-Ladner closure.

We often restrict attention to formulas of which the free variables belong to some fixed finite set $\mathsf{P}$ ; these are interpreted over Kripke models over $\mathsf{P}$ (in the following referred to as models), i.e., triples $\mathbb{S}=(S,R,\mathrm{Val})$ where $S$ is a set of points, $R$ is a binary relation and $\mathrm{Val}:\mathsf{P}\to\wp S$ . We sometimes refer to the propositional type $c_{\_}{s}\mathrel{:=}\{p\in\mathsf{P}\mid s\in\mathrm{Val}(p)\}$ of $s\in S$ as the colour of $s$ . A pointed model is a model $\mathbb{S}$ together with a designated point $s_{\_}I\in S$ . Finally, it will be convenient to extend $\mathrm{Val}$ to all literals by putting $\mathrm{Val}(\overline{p})=S\setminus\mathrm{Val}(p)$ .

In this paper, we will not work with $\mu$ -calculus formulas in their usual shape, but with formulas represented as graphs, so-called “parity formulas”. Parity formulas will facilitate discussing the complexity of our constructions. In addition, the fact that parity formulas resemble automata will simplify our proofs, as key constructions in our paper turn formulas into automata and vice versa. While parity formulas were introduced in [16] they are closely related to alternating automata [25] and hierarchical equation systems, see for instance [7]. A detailed discussion of the connections can be found in [16, Section 5]. Before giving the definition it will be useful to fix some terminology for directed graphs (which we will also apply to structures such as parity formulas that possess a directed graph structure). For binary relations $R\subseteq X\times X$ and $x\in X$ we will use the notation $R[x]$ to denote the set $\{x^{\prime}\in X\mid(x,x^{\prime})\in R\}$ .

Definition 2.2

Let $(V,E)$ be a directed graph. A path $\pi$ through $(V,E)$ is a finite, non-empty sequence $\pi=v_{\_}0\dots v_{\_}n\in V^{*}$ such that $v_{\_}{i+1}\in E[v_{\_}i]$ for all $i\in\{0,\dots,n-1\}$ . We denote by $\mathit{first}(\pi)$ and $\mathit{last}(\pi)$ the first and last element of the path $\pi$ , respectively. Concretely, for the above path we have $\mathit{first}(\pi)=v_{\_}0$ and $\mathit{last}(\pi)=v_{\_}n$ . A path $\pi$ with $\mathit{first}(\pi)=\mathit{last}(\pi)$ is called a cycle if it consists of at least two nodes.

Given the set $\mathsf{P}$ of proposition letters, we let $\mathtt{Lit}(\mathsf{P})$ and $\mathtt{At}(\mathsf{P})\mathrel{:=}\mathtt{Lit}(\mathsf{P})\cup\{\bot,\top\}$ denote the set of literals and atomic formulas over $\mathsf{P}$ , respectively.

Definition 2.3

Let $\mathsf{P}$ be a finite set of proposition letters. A parity formula over $\mathsf{P}$ is a quintuple $\mathbb{G}=(V,E,L,\Omega,v_{\_}{I})$ , where

•

$(V,E)$ is a finite, directed graph, with $|E[v]|\leq 2$ for every vertex $v$ ;
•

$L:V\to\mathtt{At}(\mathsf{P})\cup\{\land,\lor,\Diamond,\Box,\epsilon\}$ is a labelling function;
•

$\Omega:V\stackrel{{\scriptstyle\circ}}{{\to}}\omega$ is a partial map, the priority map of $\mathbb{G}$ ; and
•

$v_{\_}{I}$ is a vertex in $V$ , referred to as the initial node of $\mathbb{G}$ ;

such that

1.

$|E[v]|=0$ if $L(v)\in\mathtt{At}(\mathsf{P})$ , and $|E[v]|=1$ if $L(v)\in\{\Diamond,\Box\}\cup\{\epsilon\}$ ;
2.

every cycle of $(V,E)$ contains at least one node in $\mathsf{Dom}(\Omega)$ .

A node $v\in V$ is called atomic if it is either constant or literal, boolean if $L(v)\in\{\land,\lor\}$ , and modal if $L(v)\in\{\Diamond,\Box\}$ . We denote by $V_{\_}a$ , $V_{\_}b$ and $V_{\_}m$ the collections of atomic, boolean and modal nodes, respectively. The elements of $\mathsf{Dom}(\Omega)$ will be called states. The size of a parity formula $\mathbb{G}=(V,E,L,\Omega,v_{\_}{I})$ is defined as its number of nodes: $|\mathbb{G}|\mathrel{:=}|V|$ .

Definition 2.4

Let $\mathbb{S}=(S,R,\mathrm{Val})$ be a Kripke model for a set $\mathsf{P}$ of proposition letters, and let $\mathbb{G}=(V,E,L,\Omega,v_{\_}{I})$ be a parity formula over $\mathsf{P}$ . We define the evaluation game $\mathcal{E}(\mathbb{G},\mathbb{S})$ as the parity game $(G,E,\Omega^{\prime})$ of which the board consists of the set $V\times S$ , the priority map $\Omega^{\prime}:V\times S\to\omega$ is given by

\Omega^{\prime}(v,s)\mathrel{:=}\left\{\begin{array}[]{ll}\Omega(v)&\text{if }v\in\mathsf{Dom}(\Omega)\\ 0&\text{otherwise},\end{array}\right.

and the game graph is given in Table 1. Here all possible game positions are listed in the left column, the owner of a position is either $\forall$ or $\exists$ ¹¹1Note that we do not need to assign a player to positions that admit a single move only. and the set of possible moves is specified in the right column. As usual, finite plays of the game are lost by the player who owns the last position of the play from which no more move is possible (“the player who gets stuck loses”). An infinite play is won by $\exists$ if the maximum priority occurring infinitely often along the play is even, and by $\forall$ if it is odd.

The parity formula $\mathbb{G}$ holds at a point $s$ if the pair $(v_{\_}{I},s)$ is winning for $\exists$ in the evaluation game.

Position		Player	Admissible moves
$(v,s)$	with $L(v)=l$ and $s\in\mathrm{Val}(l)$	$\forall$	$\varnothing$
$(v,s)$	with $L(v)=l$ and $s\notin\mathrm{Val}(l)$	$\exists$	$\varnothing$
$(v,s)$	with $L(v)=\epsilon$	-	$E[v]\times\{s\}$
$(v,s)$	with $L(v)=\lor$	$\exists$	$E[v]\times\{s\}$
$(v,s)$	with $L(v)=\land$	$\forall$	$E[v]\times\{s\}$
$(v,s)$	with $L(v)=\Diamond$	$\exists$	$E[v]\times R[s]$
$(v,s)$	with $L(v)=\Box$	$\forall$	$E[v]\times R[s]$

Table 1: The evaluation game

\mathcal{E}(\mathbb{G},\mathbb{S})

A central complexity measure for both parity formulas and modal automata will be the so-called index. We define the index of a parity formula as the size of the range of its priority function $\Omega$ . We will rely on the following result from [16] that ensures that throughout the paper we are able to work on parity formulas instead of formulas in standard syntax.

Proposition 2.5

There is an algorithm that constructs for any formula $\varphi\in\mu\mathtt{ML}$ an equivalent parity formula $\mathbb{G}_{\_}\varphi$ such that $|\mathbb{G}_{\_}\varphi|=|\varphi|$ and such that the index of $\mathbb{G}_{\_}\varphi$ is smaller or equal to the alternation depth of $\varphi$ . Conversely, there is an algorithm that constructs for a given parity formula $\mathbb{G}$ an equivalent formula $\varphi_{\_}\mathbb{G}\in\mu\mathtt{ML}$ such that $|\varphi_{\_}\mathbb{G}|\leq 2\cdot|\mathbb{G}|$ and such that the alternation depth of $\varphi_{\_}\mathbb{G}$ is smaller or equal to the index of $\mathbb{G}$ .

2.2 Modal Automata

Intuitively, modal automata correspond to parity formulas in a certain normal form - the precise connection will be discussed in Section 4 below. Modal automata are based on the modal one-step language. This language consists of very simple modal formulas, built up from a collection $A$ of variables, which represent the states of the automaton and correspond to the fixpoint variables of a formula.

Definition 2.6

Given a set $A$ . The set $\mathtt{1ML}(A)$ of modal one-step formulas over $A$ is inductively given as follows:

\alpha\mathrel{::=}\bot\;\mid\;\top\;\mid\;\Diamond a\;\mid\;\Box a\;\mid\;\alpha\land\alpha\;\mid\;\alpha\lor\alpha,

where $a\in A$ . We let $\mathit{Sfor}(\alpha)$ denote the collection of subformulas of a one-step formula $\alpha$ .

Definition 2.7

Let $\mathsf{P}$ be a finite set of propositional variables. A modal $\mathsf{P}$ -automaton $\mathbb{A}$ is a quadruple $(A,\Delta,\Omega,a_{\_}{I})$ where $A$ is a non-empty finite set of states, of which $a_{\_}{I}\in A$ is the initial state, $\Omega:A\to\omega$ is the priority map, and the transition map $\Delta:A\times\wp\mathsf{P}\to\mathtt{1ML}(A)$ maps pair of states and colors to one-step formulas.

The size of a modal automaton is defined as follows.

Definition 2.8

Let $\mathbb{A}=(A,\Delta,\Omega,a_{\_}{I})$ be a modal automaton. We define its state size $|\mathbb{A}|^{s}\mathrel{:=}|A|$ , its size as

|\mathbb{A}|\mathrel{:=}\left|\bigcup\{\mathit{Sfor}(\alpha)\mid\alpha\in\mathsf{Ran}(\Delta)\}\right|+|\mathbb{A}|^{s},

and its index as $\mathit{ind}(\mathbb{A})\mathrel{:=}|\mathsf{Ran}(\Omega)|$ .

Modal automata operate on pointed models, acceptance is defined via parity graph games.

Definition 2.9

Let $\mathbb{A}=(A,\Delta,\Omega,a_{\_}{I})$ be a modal automaton and let $(\mathbb{S},s_{\_}{I})$ be a model. The acceptance game $\mathcal{A}(\mathbb{A},\mathbb{S})$ of $\mathbb{A}$ has the game board displayed in Table 2.

Position	Player	Admissible moves
$(a,s)\in A\times S$	$-$	$\{(\Delta(a,c_{\_}s),s)\}\mbox{ with }c_{\_}s=\{p\in Q\mid s\in\mathrm{Val}(p)\}$
$(\bot,s)\in\mathtt{1ML}(A)\times S$	$\exists$	$\emptyset$
$(\top,s)\in\mathtt{1ML}(A)\times S$	$\forall$	$\emptyset$
$(\alpha_{\_}1\lor\alpha_{\_}2,s)$	$\exists$	$\{(\alpha_{\_}1,s),(\alpha_{\_}2,s)\}$
$(\alpha_{\_}1\land\alpha_{\_}2,s)$	$\forall$	$\{(\alpha_{\_}1,s),(\alpha_{\_}2,s)\}$
$(\Diamond a,s)$	$\exists$	$\{(a,s^{\prime})\mid s^{\prime}\in R[s]\}$
$(\Box a,s)$	$\forall$	$\{(a,s^{\prime})\mid s^{\prime}\in R[s]\}$

Table 2: The game board of the accepance game of a modal automaton.

A pointed model $(\mathbb{S},s_{\_}I)$ is accepted by $\mathbb{A}$ if $\exists$ has a winning strategy at position $(a_{\_}I,s_{\_}I)$ in $\mathcal{A}(\mathbb{A},\mathbb{S})$ .

2.3 Disjunctive Formulas & Automata

In this section we introduce disjunctive formulas and their automata-theoretic pendant, so-called disjunctive automata. Disjunctive formulas can be best characterised in a modal language that has one “cover modality” $\nabla$ that takes a finite set of formulas as its argument. Given such a set $\Phi$ , one may think of the formula $\nabla\Phi$ as the abbreviation

\nabla\Phi\equiv\bigwedge_{\_}{\varphi\in\Phi}\Diamond\varphi\land\Box\bigvee_{\_}{\varphi\in\Phi}\varphi.

It is called the “cover modality” since, intuitively, the formula $\nabla\Phi$ holds at a point $s$ if the set of successors of $s$ and the set of elements of $\Phi$ cover each other, in a sense that can be made precise using the notion of relation lifting. For a relation $Z\subseteq X\times Y$ we define its lifting $\overline{Z}\subseteq\wp X\times\wp Y$ by putting

(U,V)\in\overline{Z}\quad\mbox{ if }\quad\forall x\in U.\exists y\in V.(x,y)\in Z\mbox{ and }\forall y\in V.\exists x\in U.(x,y)\in Z.

It is then easy to verify that the formula $\nabla\Phi$ holds at a point $s$ if the pair $(R[s],\Phi)$ belongs to the lifting of the truth relation between points and formulas. The operator $\nabla$ is well-known from the literature, cf. e.g. [14, 23, 18].

Definition 2.10

Let $\mathsf{P}$ be a finite set of propositional variables. A disjunctive parity formula over $\mathsf{P}$ is a quintuple $\mathbb{G}=(V,E,L,\Omega,v_{\_}{I})$ such that

•

$L:V\to\{\land_{\_}l\mid l\in\mathtt{Lit}(\mathsf{P})\}\cup\{\nabla,\lor,\top,\epsilon\}$ is a labelling function;
•

for all $v\in V$ with $L(v)\not=\nabla$ we have $|E[v]|\leq 2$

and such that all other conditions of the definition of parity formulas in Def. 2.3 are met. The board of the evaluation game $\mathcal{E}(\mathbb{G},\mathbb{S})$ of a disjunctive parity formula on a model $\mathbb{S}$ is displayed in Table 3.

Position		Player	Admissible moves
$(v,s)$	with $L(v)=\epsilon$	-	$E[v]\times\{s\}$
$(v,s)$	with $L(v)=\top$	$\forall$	$\varnothing$
$(v,s)$	with $L(v)=\lor$	$\exists$	$E[v]\times\{s\}$
$(v,s)$	with $L(v)=\land_{\_}l$ and $s\not\in\mathrm{Val}(l)$	$\exists$	$\varnothing$
$(v,s)$	with $L(v)=\land_{\_}{l}$ and $s\in\mathrm{Val}(l)$	$\forall$	$E[v]\times\{s\}$
$(v,s)$	with $L(v)=\nabla$	$\exists$	$\{Z\subseteq V\times S\mid(E[v],R[v])\in\overline{Z}\}$
Z	$\subseteq V\times S$	$\forall$	$\{(v^{\prime},s^{\prime})\mid(v^{\prime},s^{\prime})\in Z\}$

Table 3: The evaluation game

\mathcal{E}(\mathbb{G},\mathbb{S})

Intuitively, a node $v$ labelled with $\nabla$ represents the formula $\nabla\{\varphi_{\_}{w}\mid w\in E[v]\}$ , where for each $w\in E[v]$ we write $\varphi_{\_}w$ for the formula represented by $w$ . Furthermore $\land_{\_}l$ is intended to be a unary operator that represents the conjunction of its argument with $l$ . In other words, disjunctive formulas are formulas that contain conjunctions only in the form of conjunctions with literals and in the form of $\top$ that can be thought of as the empty conjunction. Disjunctive formulas have their automata-theoretic pendant, the so-call disjunctive modal automata – the so-called $\mu$ -automata of Janin & Walukiewicz [14]. These are defined by restricting the shape of transition conditions.

Definition 2.11

Given a finite set $A$ , we define the set $\mathtt{1DML}(A)$ of disjunctive modal one-step formulas over $A$ via the following grammar:

\alpha\mathrel{::=}\bot\;\mid\;\top\;\mid\;\nabla B\;\mid\;\alpha\lor\alpha,

where $B\subseteq A$ . A disjunctive modal $\mathsf{P}$ -automaton is a tuple $\mathbb{A}=(A,\Delta,\Omega,a_{\_}{I})$ such that $\Delta:A\times\wp\mathsf{P}\to\mathtt{1DML}(A)$ . The acceptance game $\mathcal{A}(\mathbb{A},\mathbb{S})$ on a model $\mathbb{S}$ is defined as for general modal automata with the difference that the rule for $\land$ no longer applies and that the rules for $\Box$ and $\Diamond$ are replaced by

Position	Player	Admissible moves
$(\nabla B,s)$	$\exists$	$\{Z\subseteq A\times S\mid(B,R[s])\in\overline{Z}\}$
$Z\subseteq A\times S$	$\forall$	$\{(v^{\prime},s^{\prime})\mid(v^{\prime},s^{\prime})\in Z\}$

3 Guarding Revisited

Existing approaches for turning a $\mu$ -calculus formula into a modal automaton rely on the assumption that the input formula is guarded. As [3] have shown this assumption is problematic because existing algorithms for guarding formulas, which have long been thought to be polynomial, are in fact exponential. In this section we discuss two results on the complexity of guarding formulas. We do this in the setting of parity formulas.

Definition 3.1

A path $\pi=v_{\_}{0}v_{\_}{1}\cdots v_{\_}{n}$ through $\mathbb{G}$ is unguarded if $n\geq 1$ , $v_{\_}{0},v_{\_}{n}\in\mathsf{Dom}(\Omega)$ while there is no $i$ , with $0<i\leq n$ , such that $v_{\_}{i}$ is a modal node. A parity formula is guarded if it has no unguarded cycles, and strongly guarded if it has no unguarded paths.

Adapting the well-known construction for guarding formulas one can show that it is possible to guard parity formulas, with an exponential blow-up in the number of states [16].

Theorem 3.2

There is an algorithm that transforms a parity formula $\mathbb{G}=(V,E,L,\Omega,v_{\_}{I})$ into a strongly guarded parity formula $\mathbb{G}^{g}$ such that

1)

$\mathbb{G}^{g}\equiv\mathbb{G}$ ;
2)

$|\mathbb{G}^{g}|\leq 2^{1+|\mathsf{Dom}(\Omega)|}\cdot|\mathbb{G}|$ ;
3)

$\mathit{ind}(\mathbb{G}^{g})\leq\mathit{ind}(\mathbb{G})$ .

It is unclear whether this result can be improved such that the number of states of $\mathbb{G}^{g}$ is polynomial in the number of states in $\mathbb{G}$ . The results in section 4 of Bruse, Friedmann & Lange [3] show that certain guarded transformation procedures are as hard²²2It is an open question whether parity games can be solved in polynomial time. Despite considerable efforts no polynomial algorithm has been found so far. In the recent literature, however, various quasi-polynomial algorithms have been given, following the breakthrough work of Calude et alii [4]. as solving parity games. Theorem 3.3 below can be seen as our parity-formula version of this observation. Our proof is in fact simpler because we can exploit the close connection between parity games and parity formulas and thus do not need the product construction from [15] that is used for the results from [3].

Theorem 3.3

If there is a procedure that runs in polynomial time and transforms a parity formula $\mathbb{G}$ to a guarded parity formula $\mathbb{G}^{\gamma}$ with $\mathbb{G}^{\gamma}\equiv\mathbb{G}$ then solving parity games is in ptime.

For a proof of Theorem 3.3 we refer to [16], where we also discuss in some detail the relation with other results in [3].

4 Modal Automata and Strongly Guarded Parity Formulas

In this section we establish a close connection between modal automata and parity formulas. We will first see that a modal automaton can be turned into a strongly guarded parity formula that is of linear size if we ignore propositional variables. In particular this shows that turning a parity formula into an equivalent modal automaton is at least as hard as the guarding construction from the previous section (hardness of the latter does not depend on formulas containing propositional variables). We close by showing how to turn a parity formula into an equivalent modal automaton of exponential size. Collectively the results from this section will show that constructing a disjunctive modal automaton from a parity formula by first turning the latter into an equivalent modal automaton to which we then apply a known “non-determinisation” construction would yield a doubly exponential blow-up (in closure size). This sets the stage for our main result in the next section where a new construction that is single exponential in closure size from parity automata to disjunctive modal automata is provided.

Theorem 4.1

There is an algorithm that constructs, given a modal automaton $\mathbb{A}$ , a strongly guarded parity formula $\mathbb{G}$ such that

1) $\mathbb{G}\equiv\mathbb{A}$ ;

2) $|\mathbb{G}|\leq 2^{|\mathsf{P}|}\cdot|\mathbb{A}|$ ;

3) $\mathit{ind}(\mathbb{G})\leq\mathit{ind}(\mathbb{A})$ .

4) If $\mathbb{A}$ is disjunctive then so is $\mathbb{G}$ .

Proof 4.2.

We only sketch the construction. For each $a\in A$ we let $\Delta^{\prime}(a)=\bigvee_{\_}{c\in\wp\mathsf{P}}(\bigwedge_{\_}{p\in c}p\land\bigwedge_{\_}{p\not\in c}\overline{p}\land\Delta(a,c))$ . Given a modal automaton $\mathbb{A}=(A,\Delta,\Omega,a_{\_}I)$ we define the set of nodes of $\mathbb{G}$ by

V=A\cup\bigcup\{\mathit{Sfor}(\alpha)\mid\alpha\in\mathsf{Ran}(\Delta^{\prime})\}

To defined the edge relation $E$ of $\mathbb{G}$ we put $E[a]=\Delta^{\prime}(a)$ for all $a\in A$ . For all other elements of $V$ we let $E$ be the “immediate subformula” relation, e.g. $E[\alpha_{\_}1\land\alpha_{\_}2]=\{\alpha_{\_}1,\alpha_{\_}2\}$ , $E[\Diamond a]=\{a\}$ , etc. The priority map $\Omega_{\_}\mathbb{G}$ of $\mathbb{G}$ assigns to each element $a\in A$ the priority $\Omega(a)$ . The initial state $v_{\_}I$ of $\mathbb{G}$ is defined as $v_{\_}I=a_{\_}I$ . Finally, the map $L$ assigns to each element $a\in A$ the label $\epsilon$ and for each formula $\alpha$ the label consists of the top-most operator of $\alpha$ . It is easy to see that $\mathbb{G}$ thus defined satisfies conditions 2) and 3). The proof of condition 1) is following a standard argument and is omitted here. Concerning 4) it suffices to note that for a disjunctive $a\in A$ we put

\Delta^{\prime}(a)=\bigvee_{\_}{c\in\wp\mathsf{P}}\left(\land_{\_}{l_{\_}1}\left(\cdots\land_{\_}{l_{\_}m}(\Delta(a,c))\right)\right)

where $l_{\_}1,\dots,l_{\_}n$ is an enumeration of all propositional variables in $c$ and the negation of all variables not in $c$ . Otherwise $\mathbb{G}$ is defined as in the non-disjunctive case and the result is a disjunctive formula.

Theorem 4.3.

There is an algorithm that constructs, given a parity formula $\mathbb{G}$ , a modal automaton $\mathbb{A}$ such that

1) $\mathbb{A}\equiv\mathbb{G}$ ;

2) $|\mathbb{A}|^{s}\leq 2^{1+|\mathsf{Dom}(\Omega)|}\cdot|\mathbb{G}|$ and $|\mathbb{A}|\leq 2^{|\mathsf{P}|+1+|\mathsf{Dom}(\Omega)|}\cdot|\mathbb{G}|$ ;

3) $\mathit{ind}(\mathbb{A})\leq\mathit{ind}(\mathbb{G})$ .

Proof 4.4.

By Theorem 3.2 we may effectively construct from $\mathbb{G}$ an equivalent, strongly guarded parity formula $\mathbb{H}=(V,E,L,\Omega,v_{\_}{I})$ such that $|\mathbb{H}|\leq 2^{1+|\mathsf{Dom}(\Omega)|}\cdot|\mathbb{G}|$ and $\mathit{ind}(\mathbb{H})\leq\mathit{ind}(\mathbb{G})$ . As shown in [16], we may additionally assume that in $\mathbb{H}$ , every predecessor of a node $v\in\mathsf{Dom}(\Omega)$ is a modal node. The state space of the modal automaton $\mathbb{A}$ will be given as the set $A\mathrel{:=}E[V_{\_}{m}]\cup\{v_{\_}{I}\}$ , so that by the assumption on $\mathbb{H}$ every state of $\mathbb{H}$ is a state of $\mathbb{A}$ . In addition, $v_{\_}{I}$ and possible other successors of modal nodes are states of $\mathbb{A}$ as well. We can then simply define $\Omega_{\_}{\mathbb{A}}\mathrel{:=}\Omega$ , and take $v_{\_}{I}$ as the initial state of $\mathbb{A}$ . It remains to define the transition function $\Delta$ of $\mathbb{A}$ .

Our first step will be to associate, with each node $v\in V$ , a formula $\alpha(v)$ , which belongs to the collection $\mathtt{1AML}(\mathsf{P},A)$ of alternative one-step formulas given by the following grammar:

\alpha\mathrel{::=}\bot\;\mid\;\top\;\mid\;p\;\mid\;\overline{p}\;\mid\;\Diamond a\;\mid\;\Box a\;\mid\;\alpha\land\alpha\;\mid\;\alpha\lor\alpha,

where $p\in\mathsf{P}$ and $a\in A$ . As the formula $\mathbb{H}$ is strongly guarded and by the additional property that $E^{-1}[\mathsf{Dom}(\Omega)]\subseteq V_{\_}{m}$ , there is a unique map $\alpha:V\to\mathtt{1AML}(\mathsf{P},A)$ which satisfies the following conditions:

\alpha(v)=\left\{\begin{array}[]{lll}L(v)&\text{if }v\in V_{\_}{l}\\ \heartsuit a\quad\text{where }L(v)=\heartsuit\text{ and }E[v]=\{a\}&\text{if }v\in V_{\_}{m}\\ \bigodot\big{\{}\alpha(u)\mid u\in E[v]\big{\}}\;\text{where }L(v)=\odot&\text{if }v\in V_{\_}{b}\\ \alpha(u)\quad\text{where }E[v]=\{u\}&\text{if }v\in V_{\_}{\epsilon}\end{array}\right.

We can now define the transition map $\Delta:A\times\wp(\mathsf{P})\to\mathtt{1ML}(A)$ as follows. For each state $a\in A$ and color $c\in\wp(\mathsf{P})$ we define the formula $\Delta(a,c)$ as $\Delta(a,c)\mathrel{:=}\alpha(a)[\sigma_{\_}{c}]$ , where the substitution $\sigma_{\_}{c}:\mathtt{1AML}(\mathsf{P},A)\to\mathtt{1ML}(A)$ is given by putting

\sigma_{\_}{c}(p)\mathrel{:=}\left\{\begin{array}[]{ll}\top&\text{if }p\in c\\ \bot&\text{if }p\not\in c.\end{array}\right.

This completes the definition of the automaton $\mathbb{A}$ . It is easy to see that $|\mathbb{A}|^{s}\leq|V|\leq 2^{1+|\mathsf{Dom}(\Omega)|}\cdot|\mathbb{G}|$ , that $|\mathbb{A}|\leq 2^{|\mathsf{P}|}\times V\leq 2^{|\mathsf{P}|+1+|\mathsf{Dom}(\Omega)|}\cdot|\mathbb{G}|$ and that $\mathit{ind}(\mathbb{A})=\mathit{ind}(\mathbb{H})\leq\mathit{ind}(\mathbb{G})$ , which proves the items 2) and 3) of the theorem. The equivalence of $\mathbb{A}$ and $\mathbb{H}$ (and thus, of $\mathbb{A}$ and $\mathbb{G}$ ) can be proved by a routine argument.

5 The Simulation Theorem

The main result of this section, and the main technical contribution of the paper, is the following theorem.

Theorem 5.1.

Let $\mathbb{G}$ be a parity formula of size $n$ and index $k$ with propositional variables contained in $\mathsf{P}$ with $|\mathsf{P}|=l$ . Then we can effectively construct a disjunctive modal automaton³³3For the time being this will be an automaton with a regular acceptance condition. We will transform this into an automaton with a parity condition later. $\mathbb{A}=(A,\Theta,\Omega,a_{\_}I)$ with $|A|\leq 2^{n^{2}k}$ , $|\mathbb{A}|\leq n2^{n^{2}k+l+n}$ and $\mathbb{G}\equiv\mathbb{A}$ .

Convention. In the remainder of this section we fix a parity formula $\mathbb{G}$ with $\mathbb{G}=(V,E,L,\Omega,v_{\_}I)$ with $|V|=n$ and $|\mathsf{Ran}(\Omega)|=k$ . It will be convenient to make the following assumptions on $\mathbb{G}$ : (i) $\Omega$ is total, (ii) $L^{-1}(\epsilon)=\varnothing$ , and (iii) $E[v]\neq\varnothing$ if $L(v)\in\{\land,\lor\}$ . We leave it for the reader to convince themselves that this is without loss of generality. Furthermore we define $V_{\_}{\lor}\mathrel{:=}L^{-1}(\lor)$ , etc. We now turn to the proof of Theorem 5.1.

5.1 Macrostates

We shall construct the simulating automaton via a powerset construction. That is, for the states of $\mathbb{A}$ we will in principle take subsets of $\mathbb{G}$ . However, in order to handle infinite matches correctly we need to store some more information in these states: A state of $\mathbb{A}$ will be a a macrostate over $\mathbb{G}$ , that is, a ternary relation $m\subseteq V\times\mathsf{Ran}(\Omega)\times V$ , representing various pieces of information. Basically, each triple $(u,k,v)\in m$ represents the projection on $\mathbb{G}$ of a partial play of the evaluation game of $\mathbb{G}$ which starts at $u$ , ends at $v$ , and reaches $k$ as its highest priority (after $u$ ). More precisely, the triple $(u,k,v)$ represents a path $\pi$ through $\mathbb{G}$ with $\mathit{first}(\pi)=u$ , $\mathit{last}(\pi)=v$ , and such that $k$ is the highest priority reached on $\pi$ after $u$ . Consequently, one single match of the acceptance game of $\mathbb{A}$ on a pointed Kripke structure will represent a certain bundle of matches of evaluation game of $\mathbb{G}$ .

Before defining and discussing macrostates formally, we need some auxiliary terminology.

Definition 5.2.

A subset $U\subseteq V$ is inconsistent if there is $u\in U$ with $L(u)=\bot$ , or if there are nodes $u,v\in U$ with $L(u)=p$ and $L(v)=\overline{p}$ for some $p\in\mathsf{P}$ . Given a color $c\in\wp\mathsf{P}$ we say that $U$ is compatible with $c$ if $L(u)\neq\bot$ , $L(u)=p$ implies $p\in c$ , and $L(u)=\overline{p}$ implies $p\not\in c$ , for all $u\in U$ and $p\in\mathsf{P}$ .

Definition 5.3.

We define the set $M_{\_}\Omega$ of macrostates of $\mathbb{G}$ by putting $M_{\_}{\Omega}\mathrel{:=}\wp(V\times\mathsf{Ran}(\Omega)\times V)$ . The range $\mathsf{Ran}(m)$ of a macrostate $m\in M_{\_}{\Omega}$ is the set of all $v\in V$ such that $(u,k,v)\in m$ for some $u\in V$ and $k\in\mathsf{Ran}(\Omega)$ . With $m,m^{\prime}\in M_{\_}{\Omega}$ , we define the composition $m\mathrel{;}m^{\prime}\in M_{\_}{\Omega}$ as the set of triples $(v,k,v^{\prime\prime})\in V\times\mathsf{Ran}(\Omega)\times V$ for which we can find $(v,k^{\prime},v^{\prime})\in m$ and $(v^{\prime},k^{\prime\prime},v^{\prime\prime})\in m^{\prime}$ such that $k=\max(k^{\prime},k^{\prime\prime})$ . For a subset $U\subseteq V$ , we define $\Delta_{\_}{U}\mathrel{:=}\{(u,0,u)\mid u\in U\}$ ; where $v\in V$ , we abbreviate $\Delta_{\_}{v}\mathrel{:=}\Delta_{\_}{\{v\}}$ .

A macrostate $m$ is called consistent, respectively compatible with a color $c\in\wp\mathsf{P}$ , if $\mathsf{Ran}(m)\subseteq V$ satisfies the mentioned property w.r.t. $c$ , in the sense of Definition 5.2.

Given a stream $\alpha=(m_{\_}{i})_{\_}{i\in\omega}$ of macrostates, we say that a stream $(v_{\_}{i},k_{\_}{i})_{\_}{i\in\omega}\in(V\times\mathsf{Ran}(\Omega))^{\omega}$ is a trace on $\alpha$ if $(v_{\_}{i},k_{\_}{i},v_{\_}{i+1})\in m_{\_}{i}$ , for all $i\in\omega$ . Such a trace is good (bad, respectively) if the maximum number $k$ occurring as $k_{\_}{i}$ for infinitely many $i$ is even (odd, respectively). We let $\mathrm{NBT}_{\_}{\Omega}$ denote the collection of $M_{\_}{\Omega}$ -streams that do not carry a bad trace.

Proposition 5.4.

The set $\mathrm{NBT}_{\_}{\Omega}$ is an $\omega$ -regular language over $M_{\_}{\Omega}$ . Concretely, there is a deterministic parity automaton $\mathbb{P}$ over $M_{\_}{\Omega}$ such that $L_{\omega}(\mathbb{P})=\mathrm{NBT}_{\_}{\Omega}$ and $\mathbb{P}$ has size $2^{\mathcal{O}(nk\cdot\log(nk))}$ and index $\mathcal{O}(nk)$ .

Proof 5.5.

We first observe that there is a non-deterministic parity word automaton $\mathbb{W}=(Q,q_{\_}I,\Delta_{\_}\mathbb{W},\Omega_{\_}\mathbb{W})$ that accepts the language $\mathcal{L}_{\_}\mathrm{bad}\mathrel{:=}(M_{\_}{\Omega})^{\omega}\setminus\mathrm{NBT}_{\_}{\Omega}$ , i.e., all infinite streams of macrostates that do contain a bad trace. To define $\mathbb{W}$ we put $Q\mathrel{:=}V$ , $q_{\_}I\mathrel{:=}v_{\_}I$ , $\Delta_{\_}\mathbb{W}(v,m)\mathrel{:=}\{u\in V\mid\exists k.(v,k,u)\in m\}$ and $\Omega_{\_}\mathbb{W}(v)\mathrel{:=}\Omega(v)+1$ for all $v\in V$ and all $m\in M_{\_}\Omega$ . It is easy to verify $\mathbb{W}$ is a parity automaton with $n$ states and index $k$ that accepts $\mathcal{L}_{\_}\mathrm{bad}$ . Standard constructions can be used to first transform $\mathbb{W}$ into an equivalent non-deterministic Büchi automaton $\mathbb{W}^{\prime}$ of size $\mathcal{O}(n\cdot k)$ (cf. e.g. [13]) which can be in turn transformed into an equivalent deterministic parity word automaton $\mathbb{W}^{\prime\prime}$ that meets the size bounds of the proposition (cf. [19, 20]). The automaton $\mathbb{P}$ is now constructed as the deterministic parity word automaton that accepts the complement of the language of $\mathbb{W}^{\prime\prime}$ by adding 1 to all the priorities of states in $\mathbb{W}^{\prime\prime}$ .

5.2 Local strategies & the disjunctive modal automaton

In our approach of dealing with the possible unguardedness of the input parity formula, the key concept is that of a (positional) local strategy for $\exists$ . A local strategy represents a complete set of choices of $\exists$ for all disjunction nodes in $\mathbb{G}$ . Intuitively, one may think of a local strategy as some part of a positional strategy of $\exists$ where we stay put at a point in the model. More precisely, a local strategy $\chi$ induces, in the evaluation game of $\mathbb{G}$ , for any point in the model and any vertex in $\mathbb{G}$ , a unique (partial) play that does not leave the mentioned point and stops whenever a modal vertex in $\mathbb{G}$ is met. The projections of these matches will be called stationary plays. Formally we define these notion, together with some related concepts that we will discuss in a moment, as follows.

Definition 5.6.

A local strategy on $\mathbb{G}$ is a map $\chi:V_{\_}{\lor}\to V$ such that $\chi(v)\in E[v]$ , for all $v\in V_{\_}{\lor}$ . The collection of local strategies on $\mathbb{G}$ is denoted by $\mathit{LS}_{\_}{\mathbb{G}}$ .

Now fix such a local strategy $\chi$ . Given a vertex $v\in V$ we define the set $\mathit{SP}_{\_}{\chi}(v)$ of stationary $\chi$ -plays from $v$ as the smallest set $S\subseteq V^{*}$ such that
(1a) if $v\in V_{\_}{\lor}$ then $v\cdot\chi(v)\in S$ ;
(1b) if $v\in V_{\_}{\land}$ then $v\cdot w\in S$ , for each $w\in E[v]$ ;
(2a) if $\pi\in S$ and $u\mathrel{:=}\mathit{last}(\pi)\in V_{\_}{\lor}$ , then $\pi\cdot\chi(u)\in S$ ; and
(2b) if $\pi\in S$ and $u\mathrel{:=}\mathit{last}(\pi)\in V_{\_}{\land}$ , then $\pi\cdot w\in S$ , for each $w\in E[u]$ .
Given $\pi=vv_{\_}{1}\cdots v_{\_}{k}\in\mathit{SP}_{\_}{\chi}(v)$ , define $\widetilde{\Omega}(\pi)\mathrel{:=}\max\{\Omega(v_{\_}{i})\mid 1\leq i\leq k\}$ . Via these stationary plays we define the following macrostates:

\begin{array}[]{llll}e_{\_}{\chi}^{-}&\mathrel{:=}&\big{\{}(v,n,u)&\mid v\in V_{\_}{b}\text{ and }u=\mathit{last}(\pi)\text{ for some }\pi\in\textit{SP}_{\_}{\chi}(v)\text{ with }n=\widetilde{\Omega}(\pi)\big{\}}\\ e_{\_}{\chi}&\mathrel{:=}&e_{\_}{\chi}^{-}\cup\Delta_{\_}{V}\end{array}

We say that on a macrostate $m$ , $\chi$ is locally compatible with a color $c\in\wp\mathsf{P}$ if (i) $\mathsf{Ran}(m\mathrel{;}e_{\_}{\chi})$ is compatible with $c$ and (ii) the stream $m\mathrel{;}(e^{-}_{\_}{\chi})^{\omega}$ does not contain any bad trace.

Here are some intuitions about these notions. First, note that $\mathit{SP}_{\_}{\chi}(v)$ only contains paths of length $>1$ , corresponding to matches where actually a move is made at $v$ . The macrostate $e_{\_}{\chi}^{-}$ represents the relevant information about all finite stationary $\chi$ -plays; hence, the collection of all infinite stationary $\chi$ -plays corresponds to the set of all traces over the $M_{\_}{\Omega}$ -stream $(e_{\_}{\chi}^{-})^{\omega}$ .

Now fix a macro-state $m$ . The macrostate $m\mathrel{;}e_{\_}{\chi}^{-}$ represents the version of $m$ that absorbs all continuations of matches in $m$ with one of these finite stationary $\chi$ -plays; thus the set $m\cup(m\mathrel{;}e_{\_}{\chi}^{-})$ represents all triples in $m$ that are possibly continued with such a play. For technical reasons it is convenient to define this set using the macro-state $e_{\_}{\chi}$ , in the sense that $m\mathrel{;}e_{\_}{\chi}=m\mathrel{;}(e_{\_}{\chi}^{-}\cup\Delta_{\_}{V})=(m\mathrel{;}e_{\_}{\chi}^{-})\cup(m\mathrel{;}\Delta_{\_}{V})=(m\mathrel{;}e_{\_}{\chi}^{-})\cup m$ . The stream $m\mathrel{;}(e_{\_}{\chi}^{-})^{\omega}$ represents all infinite plays that start with an $m$ -play, and then continue with an infinite stationary $\chi$ -play. To say that there is a bad trace on such a stream means that for some $v\in\mathsf{Ran}(m)$ , $\exists$ ’s opponent $\forall$ has a strategy such that, played against $\chi$ , the resulting match (path through the graph of $\mathbb{G}$ ) is bad, in the sense of the highest priority met infinitely often being odd. To say that, relative to $m$ , $\chi$ is locally compatible with a color $c$ indicates, roughly, that after any $m$ -match, if the local point of the Kripke model has color $c$ , then it is safe for $\exists$ (until the next modal vertex in $\mathbb{G}$ is encountered) to continue by playing $\chi$ . Finally, it may also be useful to observe that for all $m$ and $\chi$ we find $\mathsf{Ran}(m)\cap V_{\_}{p}\subseteq\mathsf{Ran}(m\mathrel{;}e_{\_}{\chi})\cap V_{\_}{p}$ and $\mathsf{Ran}(m)\cap V_{\_}{m}\subseteq\mathsf{Ran}(m\mathrel{;}e_{\_}{\chi})\cap V_{\_}{m}$ .

We turn to the definition of the disjunctive modal automaton $\mathbb{A}_{\_}{\mathbb{G}}$ . For the definition of its transition map $\Theta$ , note a macrostate $m$ may be thought of as representing the conjunction of states in $\mathsf{Ran}(m)$ that are visited by “parallel” plays of the evaluation game for $\mathbb{G}$ . The transition function $\Theta$ will implement the intuition that a modal step needs to satisfy the “demands” posed by the modal nodes in $\mathsf{Ran}(m)$ . These demands are formulated separately for all box nodes and for each individual diamond node.

Definition 5.7.

Let $m\in M_{\_}{\Omega}$ be some macrostate, and let $x\in\mathsf{Ran}(m)\cap V_{\_}{\Diamond}$ . Then we define

\begin{array}[]{lll}d_{\_}{\Box}(m)&\mathrel{:=}&\{(u,\Omega(v),v)\mid u\in\mathsf{Ran}(m)\cap V_{\_}{\Box}\text{ and }v\in E[u]\},\\ d_{\_}{x}(m)&\mathrel{:=}&\{(x,\Omega(v),v)\mid v\in E[x]\}\cup d_{\_}{\Box}(m).\end{array}

The macrostates $d_{\_}{\Box}(m)$ and $d_{\_}{x}(m)$ correspond to, respectively, the universal and existential requirements made by the vertices in the range of $m$ .

Definition 5.8.

Let $\mathbb{G}=(V,E,L,\Omega,v_{\_}I)$ be a parity formula. We define the automaton $\mathbb{A}_{\_}{\mathbb{G}}=(A,\Theta,\mathit{Acc},m_{\_}I)$ as follows. To start with, its carrier is the collection of all macrostates: $A\mathrel{:=}M_{\_}{\Omega}$ and its initial state is given as $m_{\_}I=\Delta_{\_}{v_{\_}{I}}=\{(v_{\_}I,0,v_{\_}I)\}$ . The transition map $\Theta$ is given as follows. For a macrostate $m\in M_{\_}{\Omega}$ and a local strategy $\chi$ we define $A_{\_}{m,\chi}\subseteq M_{\_}{\Omega}$ :

\displaystyle A_{\_}{m,\chi}

\displaystyle\mathrel{:=}

\displaystyle\{e_{\_}{\chi}\mathrel{;}d_{\_}{\Box}(m\mathrel{;}e_{\_}{\chi})\}\;\cup\;\{e_{\_}{\chi}\mathrel{;}d_{\_}{x}(m\mathrel{;}e_{\_}{\chi})\mid x\in\mathsf{Ran}(m\mathrel{;}e_{\_}{\chi})\cap V_{\_}{\Diamond}\},

and for a macrostate $m\in M_{\_}{\Omega}$ and a color $c\in\wp\mathsf{P}$ we put:

\Theta(m,c)\mathrel{:=}\bigvee\big{\{}\theta(m,.c,\chi)\mid\chi\in\mathit{LS}_{\_}{\mathbb{G}}\text{ is locally compatible with $c$ on }m\big{\}},

where

\theta(m,c,\chi)\mathrel{:=}\left\{\begin{array}[]{ll}\nabla A_{\_}{m,\chi}&\text{if }\mathsf{Ran}(m\mathrel{;}e_{\_}{\chi})\cap V_{\_}{\Diamond}\neq\varnothing\\ \nabla A_{\_}{m,\chi}\lor\nabla\varnothing&\text{if }\mathsf{Ran}(m\mathrel{;}e_{\_}{\chi})\cap V_{\_}{\Diamond}=\varnothing.\end{array}\right.

Finally, for its acceptance condition $\mathit{Acc}$ we take the $\omega$ -regular language $\mathrm{NBT}_{\_}{\Omega}$ , i.e, an infinite play of $\mathcal{A}$ will be winning for $\exists$ if the corresponding stream of macrostates is in $\mathrm{NBT}_{\_}\Omega$ .

To get some intuitions: to define $\Theta(m,c)$ , we nondeterministically guess a local strategy $\chi$ that is compatible with $c$ on $m$ – this guess is reflected by the disjunction in the definition of $\Theta(m,c)$ . For each such $\chi$ , we absorb its stationary plays into $m$ and turn to the set of modal nodes in the range of the resulting macro-state $m\mathrel{;}e_{\_}{\chi}$ . We gather the universal and existential requirements of $m\mathrel{;}e_{\_}{\chi}$ into an appropriate collection $A_{\_}{m,\chi}$ of “next” macro-states. This set $A_{\_}{m,\chi}$ is then to be covered by the collection of successors of the point in the Kripke model under inspection, as encoded by the formula $\nabla A_{\_}{m,\chi}$ . In the special case where $m\mathrel{;}e_{\_}{\chi}$ makes no existential demands (i.e., if $\mathsf{Ran}(m\mathrel{;}e_{\_}{\chi})\cap V_{\_}{\Diamond}=\varnothing$ ), we add the disjunct $\nabla\varnothing\equiv\Box\bot$ , allowing for the possibility that the point has no successors at all. To see how this all works out precisely, the reader is advised to look at the proof of Proposition 5.9 below.

5.3 Proof of Theorem 5.1

Turning to the proof of the main theorem, we first show that the disjunctive modal automaton from Definition 5.8 is equivalent to the parity formula $\mathbb{G}$ that we started with. After that we prove Theorem 5.1 by showing that $\mathbb{A}_{\_}{\mathbb{G}}$ is within the desired size bounds.

Proposition 5.9.

For any parity formula $\mathbb{G}$ , we have $\mathbb{G}\equiv\mathbb{A},$ where $\mathbb{A}\mathrel{:=}\mathbb{A}_{\_}{\mathbb{G}}$ is given as in Definition 5.8.

Proof 5.10.

We show that

(v_{\_}{I},s_{\_}{I})\in\mathrm{Win}_{\_}{\exists}(\mathcal{E}(\mathbb{G},\mathbb{S}))\text{ iff }(m_{\_}{I},s_{\_}{I})\in\mathrm{Win}_{\_}{\exists}(\mathcal{A}(\mathbb{A},\mathbb{S})),

(1)

where $(\mathbb{S},s_{\_}{I})$ is an arbitrary but fixed pointed model, $m_{\_}{I}\mathrel{:=}\Delta_{\_}{v_{\_}{I}}$ , and we write $\mathrm{Win}_{\_}{\exists}$ for the set of winning positions for $\exists$ in a game. In the sequel we will abbreviate $\mathcal{E}\mathrel{:=}\mathcal{E}(\mathbb{G},\mathbb{S})$ and $\mathcal{A}\mathrel{:=}\mathcal{A}(\mathbb{A},\mathbb{S})$ .

For the direction from left to right of (1), fix a positional winning strategy $f$ for $\exists$ in $\mathcal{E}$ . For any point $s\in S$ , we may associate a map $\chi_{\_}{s}:V_{\_}{\lor}\to V$ with $f$ , as follows. Given a vertex $u\in V_{\_}{\lor}$ , if $(u,s)\in\mathrm{Win}_{\_}{\exists}(\mathcal{E})$ then $\chi_{\_}{s}$ maps $u$ to the element $v\in E[u]$ such that $(v,s)=f(u,s)$ ; if $(u,s)\not\in\mathrm{Win}_{\_}{\exists}(\mathcal{E})$ we define $\chi_{\_}{s}(u)$ to be an arbitrary element in $E[u]$ . Clearly $\chi_{\_}{s}$ is a local strategy in the sense of Definition 5.6, and it is not hard to prove that $\chi_{\_}{s}$ is locally compatible with the color $\mathrm{Val}(s)$ of $s$ , on any $m\in M_{\_}{\Omega}$ such that $(v,s)\in\mathrm{Win}_{\_}{\exists}(\mathcal{E})$ for any $v\in\mathsf{Ran}(m)$ . We define the following (positional) strategy $f^{\prime}$ for $\exists$ in $\mathcal{A}$ . Let $\Sigma$ be a partial $\mathcal{A}$ -match with $\mathit{last}(\Sigma)=(m,s)$ . In case $\mathsf{Ran}(m)\times\{s\}\not\subseteq\mathrm{Win}_{\_}{\exists}(\mathcal{E})$ then $\exists$ plays randomly (one may show that this will never happen). If, on the other hand, $\mathsf{Ran}(m)\times\{s\}\subseteq\mathrm{Win}_{\_}{\exists}(\mathcal{E})$ , then we already saw that $\chi_{\_}s$ is locally compatible with $\mathrm{Val}(s)$ on $m$ . Compute $e\mathrel{:=}e_{\_}{\chi_{\_}{s}}$ and recall that with each element $(u,k,v)\in e$ we may associate a partial $f$ -guided match $\pi:(u,s)\cdots(v,s)$ , which is stationary at $s$ and such that $k$ is the highest priority met on $\pi$ after $u$ : $k=\widetilde{\Omega}(\pi)$ . It is then not hard to see that, for an arbitrary element $w\in\mathsf{Ran}(m\mathrel{;}e)$ we have $(w,s)\in\mathrm{Win}_{\_}{\exists}(\mathcal{E})$ . In particular, if such a $w$ belongs to $V_{\_}{\Diamond}$ , then $\exists$ ’s winning strategy $f$ in $\mathcal{E}$ selects a successor $t_{\_}{w}\in R[s]$ . This assignment, $V_{\_}{\Diamond}\ni w\mapsto t_{\_}{w}$ , determines $\exists$ ’s strategy $f^{\prime}$ in $\mathcal{A}$ . That is, at any partial match $\Sigma$ with $\mathit{last}(\Sigma)=(m,s)$ , let $\exists$ play

f^{\prime}(m,s)\mathrel{:=}\Big{\{}\big{(}e\mathrel{;}d_{\_}{\Box}(m\mathrel{;}e),t\big{)}\mid t\in R[s]\Big{\}}\cup\Big{\{}\big{(}e\mathrel{;}d_{\_}{w}(m\mathrel{;}e),t_{\_}{w}\big{)}\mid w\in V_{\_}{\Diamond}\cap\mathsf{Ran}(m\mathrel{;}e)\Big{\}}.

(2)

It is easy to see that this move is legitimate. To show that $f^{\prime}$ is actually winning for $\exists$ consider an arbitrary $f^{\prime}$ -guided partial match $\Sigma=(m_{\_}{0},s_{\_}{0})\cdots(m_{\_}{n},s_{\_}{n})$ with $(m_{\_}{0},s_{\_}{0})=(m_{\_}{I},s_{\_}{I})$ . Via an inductive proof one can show that $\mathsf{Ran}(m_{\_}{i})\subseteq\{v\in V\mid(v,s_{\_}{i})\in\mathrm{Win}_{\_}{\exists}(\mathcal{E})\}$ , for each $i\leq m$ . Therefore $\exists$ ’s moves in $\Sigma$ are indeed legitimately guided as in (2) and she wins every finite $f^{\prime}$ -guided match of $\mathcal{A}$ starting at $(m_{\_}{I},s_{\_}{I})$ .

To see that $\exists$ also wins the infinite $f^{\prime}$ -guided matches, let $\Sigma=(m_{\_}{i},s_{\_}{i})_{\_}{i\in\omega}$ be an arbitrary such match, and consider an arbitrary trace $(v_{\_}{i},k_{\_}{i})_{\_}{i\in\omega}$ on $\Sigma$ . Let $k$ be the maximum number occurring as $k_{\_}{i}$ for infinitely many $i$ ; it then suffices to show that $k$ is even. For every $i<\omega$ one may associate $f$ -guided partial $\mathcal{E}$ -matches $\sigma_{\_}{i}=(u^{i}_{\_}{0},s_{\_}{i})(u^{i}_{\_}{1},s_{\_}i)\cdots(u^{i}_{\_}{n_{\_}{i}},s_{\_}{i})$ and $\sigma_{\_}{i}^{+}\mathrel{:=}\sigma_{\_}{i}\cdot(u^{i+1}_{\_}{0},s_{\_}{i+1})$ such that $v_{\_}{i}=u^{i}_{\_}{0}$ , $v_{\_}{i+1}=u^{i+1}_{\_}{0}$ and $k=\widetilde{\Omega}(\sigma_{\_}{i}^{+})$ . Putting these partial plays together, with the trace $(v_{\_}{i},k_{\_}{i})_{\_}{i\in\omega}$ we have thus associated a (full) infinite $f$ -guided $\mathcal{E}$ -match $\sigma=\sigma_{\_}{0}\sigma_{\_}{1}\cdots$ , such that $\sigma_{\_}{i}=(u^{i}_{\_}{0},s_{\_}{i})(u^{i}_{\_}{1},s_{\_}{i})\cdots(u^{i}_{\_}{n_{\_}{i}},s_{\_}{i})$ and $k_{\_}{i}=\max\big{\{}\Omega(\sigma^{i}_{\_}{1}),\ldots,\Omega(\sigma^{i}_{\_}{n_{\_}{i}}),\Omega(\sigma^{i+1}_{\_}{0})\big{\}}$ . This means that $k$ is the highest priority that occurs infinitely often in $\sigma$ , and since $\sigma$ is guided by $\exists$ ’s winning strategy $f$ , $k$ must be even indeed.

For the other direction of (1), fix a winning strategy $h$ for $\exists$ in $\mathcal{A}$ . W.l.o.g. we may assume that $\mathbb{S}$ is an $\omega$ -expanded tree⁴⁴4A pointed model $(\mathbb{S},s_{\_}{I})$ is $\omega$ -expanded if $R$ is the parent-child relation of a tree $(S,R)$ which has $s_{\_}{I}$ as its root, and is such that every non-root node $s$ in $\mathbb{S}$ has at least $\omega$ many bisimilar siblings. It is not hard to see that every pointed model can be unravelled to a bisimilar model that is $\omega$ -expanded. with root $s_{\_}{I}$ , so that with each $s\in S$ we may associate a unique state $m_{\_}{s}$ such that $(m_{\_}{s},s)$ can be reached during an $h$ -guided match of $\mathcal{A}$ starting from $(m_{\_}{I},s_{\_}{I})$ . By definition of $\mathbb{A}_{\_}{\mathbb{G}}$ and $\mathcal{A}$ then, with each $s\in S$ we may also associate a local strategy $\chi_{\_}{s}$ , which is locally compatible with the color $\mathrm{Val}(s)$ on $m_{\_}{s}$ and such that $\exists$ ’s strategy $h$ is aimed at satisfying the one-step formula $\nabla A_{\_}{m_{\_}{s},\chi_{\_}{s}}$ .

To define $\exists$ ’s strategy $h^{\prime}$ in $\mathcal{E}$ , consider an arbitrary finite $\mathcal{E}$ -match $\sigma$ . It is not hard to see that $\sigma$ admits a unique modal decomposition $\sigma=\sigma_{\_}{0}\cdots\sigma_{\_}{l}$ , where for all $i<l$ , $\mathit{last}(\sigma_{\_}{i})$ is the unique modal position in $\sigma_{\_}{i}$ , and $\sigma_{\_}{l}$ either contains no modal positions, or a unique one at $\mathit{last}(\sigma_{\_}{l})$ . This means that we may present each $\sigma_{\_}{i}$ as $\sigma_{\_}{i}=(v^{i}_{\_}{0},s_{\_}{i})(v^{i}_{\_}{1},s_{\_}{i})\cdots(v^{i}_{\_}{n_{\_}{i}},s_{\_}{i})$ for some fixed point $s_{\_}{i}$ in $\mathbb{S}$ . The key idea underlying the definition of $h^{\prime}$ is that with every $h^{\prime}$ -guided finite match $\sigma$ , with $\sigma=\sigma_{\_}{0}\cdots\sigma_{\_}{l}$ as above, we associate an $h$ -guided $\mathcal{A}$ -match $\Sigma_{\_}{\sigma}=(m_{\_}{0},s_{\_}{0})\cdots(m_{\_}{l},s_{\_}{l})$ satisfying the condition (†) given below:

(†1)

for each $i\leq l$ , $j\leq n_{\_}{i}$ , we have $v^{i}_{\_}{j}\in\mathsf{Ran}(m_{\_}{i}\mathrel{;}e_{\_}{\chi_{\_}{s_{\_}{i}}})$ .
(†2)

for each $i\leq l$ , $m_{\_}{i}=m_{\_}{s_{\_}{i}}$ , and the sequence $v^{i}_{\_}{0}\cdots v^{i}_{\_}{n_{\_}{i}}$ is $\chi_{\_}{s_{\_}{i}}$ -guided; for each pair $j,k$ with $j<k\leq n_{\_}{i}$ , we have $(v^{i}_{\_}{j},N^{i}_{\_}{j,k},v^{i}_{\_}{k})\in e^{-}_{\_}{\chi_{\_}{s_{\_}{i}}}$ , where $N^{i}_{\_}{j,k}=\max\{\Omega(v^{i}_{\_}{r})\mid j<r\leq k\}$ ;
(†3)

for each $i<l$ , with $w\mathrel{:=}v^{i}_{\_}{n_{\_}{i}}$ , if $w\in V_{\_}{\Diamond}$ , then $m_{\_}{i+1}=e_{\_}{\chi_{\_}{s_{\_}{i}}}\mathrel{;}d_{\_}{w}(m_{\_}{i}\mathrel{;}e_{\_}{\chi_{\_}{s_{\_}{i}}})$ and $(v^{i}_{\_}{0},M_{\_}{i},v^{i+1}_{\_}{0})\in m_{\_}{i+1}$ , where $M_{\_}{i}=\max\{\Omega(v^{i}_{\_}{1}),\ldots,\Omega(v^{i}_{\_}{n_{\_}{i}}),\Omega(v^{i+1}_{\_}{0})\}$ .
(†4)

for each $i<l$ , with $w\mathrel{:=}v^{i}_{\_}{n_{\_}{i}}$ , if $w\in V_{\_}{\Box}$ , then $m_{\_}{i+1}=e_{\_}{\chi_{\_}{s_{\_}{i}}}\mathrel{;}d_{\_}{\Box}(m_{\_}{i}\mathrel{;}e_{\_}{\chi_{\_}{s_{\_}{i}}})$ and $(v^{i}_{\_}{0},M_{\_}{i},v^{i+1}_{\_}{0})\in m_{\_}{i+1}$ , where $M_{\_}{i}=\max\{\Omega(v^{i}_{\_}{1}),\ldots,\Omega(v^{i}_{\_}{n_{\_}{i}}),\Omega(v^{i+1}_{\_}{0})\}$ .

Based on this connection, we define the following strategy $h^{\prime}$ for $\exists$ in $\mathcal{E}$ ; we show at the same time that, playing $h^{\prime}$ , $\exists$ can maintain the condition (†) and wins all finite matches. Consider a partial $h^{\prime}$ -guided match $\sigma$ , modally decomposed as $\sigma=\sigma_{\_}{0}\cdots\sigma_{\_}{l}$ as above, where $\sigma_{\_}{l}=(v^{l}_{\_}{0},s_{\_}{l})\cdots(v^{l}_{\_}{k},s_{\_}{l})$ , and let $\Sigma_{\_}{\sigma}=(m_{\_}{0},s_{\_}{0})\cdots(m_{\_}{l},s_{\_}{l})$ be an associated $\mathcal{A}$ -match satisfying (†). We distinguish cases, writing $v\mathrel{:=}v^{l}_{\_}{k}$ and $\chi\mathrel{:=}\chi_{\_}{s_{\_}{l}}$ for brevity.

•

If $v$ is a propositional node, we need to show that $\sigma$ is won by $\exists$ . This is immediate in case $L(v)=\top$ , so assume that $L(v)=\bot$ or $L(v)\in\{p,\overline{p}\}$ for some proposition letter $p$ . We only treat the case where $L(v)=p$ , the other cases being similar. By (†2) we have $m_{\_}{l}=m_{\_}{s_{\_}{l}}$ , so that $\chi=\chi_{\_}{s_{\_}{l}}$ is locally compatible with the color $\mathrm{Val}(s_{\_}{l})$ on $m_{\_}{l}\mathrel{;}e_{\_}{\chi}$ . But then (†1) implies that $L(v)\in\mathrm{Val}(s)$ .
•

If $v\in V_{\_}{\lor}$ , define $h^{\prime}(\sigma)\mathrel{:=}(\chi(v),s_{\_}{l})$ . It is easy to see that $\sigma\cdot(\chi(v),s_{\_}{l})$ and $\Sigma_{\_}{\sigma}$ are related by (†).
•

If $v\in V_{\_}{\land}$ , suppose that $\forall$ picks a conjunct $u$ of $v$ . Then $\sigma\cdot(u,s_{\_}{l})$ and $\Sigma_{\_}{\sigma}$ are related by (†).
•

If $v\in V_{\_}{\Diamond}$ , first define $m_{\_}{l+1}\mathrel{:=}e_{\_}{\chi}\mathrel{;}d_{\_}{v}(m_{\_}{l}\mathrel{;}e_{\_}{\chi})$ . Note that, since $v\in\mathsf{Ran}(m_{\_}{l}\mathrel{;}e_{\_}{\chi})$ by the inductive hypothesis (†1), we find $m_{\_}{l+1}\in A_{\_}{m_{\_}{l},\chi}$ . Furthermore, recall that by our assumption on $h$ , $\exists$ ’s move at position $(m_{\_}{l},s_{\_}{l})$ in $\mathcal{A}$ is aimed at satisfying the one-step formula $\nabla A_{\_}{m_{\_}{l},\chi}$ , and so this move must contain a pair of the form $(m_{\_}{l+1},t)$ for some $t\in R[s_{\_}{l}]$ . Now define $h^{\prime}(\sigma)\mathrel{:=}(u,t)$ , where $u$ is the (unique) element of $E[v]$ . The modal decomposition of $\sigma^{\prime}\mathrel{:=}\sigma\cdot(u,t)$ is then $\sigma^{\prime}=\sigma_{\_}{1}\cdots\sigma_{\_}{m}\sigma_{\_}{m+1}$ , where $\sigma_{\_}{m+1}=(u,t)$ . (That is, in the terminology of (†) we have $v^{l+1}_{\_}{0}=u$ and $s_{\_}{l+1}=t$ .)

We now check that $\sigma^{\prime}$ and $\Sigma^{\prime}\mathrel{:=}\Sigma\cdot(m_{\_}{l+1},t)$ are related by (†). For (†1), it suffices to show that $u\in\mathsf{Ran}(m_{\_}{l+1}\mathrel{;}e_{\_}{\chi_{\_}{t}})$ . But this is immediate by $(v,\Omega(u),u)\in d_{\_}{v}(m_{\_}{l}\mathrel{;}e_{\_}{\chi})=\Delta_{\_}{V}\mathrel{;}d_{\_}{v}(m_{\_}{l}\mathrel{;}e_{\_}{\chi})\subseteq e_{\_}{\chi}\mathrel{;}d_{\_}{v}(m_{\_}{l}\mathrel{;}e_{\_}{\chi})=m_{\_}{l+1}\subseteq m_{\_}{l+1}\mathrel{;}\Delta_{\_}{V}\subseteq m_{\_}{l+1}\mathrel{;}e_{\_}{\chi_{\_}{t}}$ . For (†2) it suffices to show that $m_{\_}{l+1}=m_{\_}{t}$ but this holds by construction. For (†3) we likewise have $m_{\_}{l+1}=e_{\_}{\chi}\mathrel{;}d_{\_}{v}(m_{\_}{l}\mathrel{;}e_{\_}{\chi})$ by construction. We already saw that $(v,\Omega(u),u)\in d_{\_}{v}(m_{\_}{l}\mathrel{;}e_{\_}{\chi})$ , and we have $(v^{l}_{\_}{0},N^{l}_{\_}{0,k},v^{l}_{\_}{k})\in e_{\_}{\chi}^{-}$ by the induction hypothesis (†2). From this, and the observation that $M_{\_}{l}=\max(N^{l}_{\_}{0,k},\Omega(u))$ we obtain $(v^{l}_{\_}{0},M_{\_}{l},u)\in e_{\_}{\chi}^{-}\mathrel{;}d_{\_}{v}(m_{\_}{l}\mathrel{;}e_{\_}{\chi})\subseteq e_{\_}{\chi}\mathrel{;}d_{\_}{v}(m_{\_}{l}\mathrel{;}e_{\_}{\chi})=m_{\_}{l+1}$ . Finally, for (†4) there is nothing to prove.
•

The case where $v\in V_{\_}{\Box}$ is similar to the previous one, so we skip some details. Let $u\in E[v]$ be the unique successor of $v$ in $\mathbb{G}$ , and suppose that in our $\mathcal{E}$ -match, $\forall$ picks a successor $t$ of $s_{\_}{l}$ ; that is, we now look at the continuation $\sigma^{\prime}\mathrel{:=}\sigma\cdot(u,t)$ of the $\mathcal{E}$ -match $\sigma$ . Consider $\exists$ ’s move in $\mathcal{A}$ at position $(m_{\_}{l},s_{\_}{l})$ , which makes the one-step formula $\nabla A_{\_}{m_{\_}{l},\chi}$ true, and thus contains a pair $(m,t)$ for some $m\in A_{\_}{m_{\_}{l},\chi}$ . Now define $m_{\_}{l+1}\mathrel{:=}m$ , and let $\Sigma^{\prime}\mathrel{:=}(m,t)$ ; this is an $h$ -guided continuation of $\Sigma$ .

To verify that $\sigma^{\prime}$ and $\Sigma^{\prime}$ satisfy (†), first note that by definition of the set $A_{\_}{m_{\_}{l},\chi}$ , $m$ must be of the form $e_{\_}{\chi}\mathrel{;}d_{\_}{x}(m_{\_}{l}\mathrel{;}e_{\_}{\chi})$ , where either $x=\Box$ or $x\in\mathsf{Ran}(m_{\_}{l}\mathrel{;}e_{\_}{\chi})$ . Based on this observation, checking the conditions (†1), (†2) and (†4) are similar to the respective conditions (†1), (†2) and (†3) in the previous case (with the only difference that we now must also take the possibility that $x=\Box$ into account). Finally, condition (†3) needs no check since it is not applicable.

To see that $h^{\prime}$ is winning for $\exists$ consider a full $h^{\prime}$ -guided match, and distinguish cases. For finite matches one can check that $\exists$ never gets stuck. In case $\sigma$ is an infinite $h^{\prime}$ -guided match, we make a further distinction as to whether the number of modal positions that $\sigma$ passes through is finite or infinite. If $\sigma$ passes through infinitely many modal positions, there is a unique way of decomposing $\sigma$ as $\sigma=\sigma_{\_}{0}\sigma_{\_}{1}\cdots$ , where $(\mathit{last}(\sigma_{\_}{i}))_{\_}{i\in\omega}$ is the sequence of (all) modal positions in $\sigma$ . By construction there is an associated infinite $h$ -guided $\mathcal{A}$ -match $\Sigma_{\_}{\sigma}=(m_{\_}{i},s_{\_}{i})_{\_}{i\in\omega}$ related to $\sigma$ via the condition (†). It is now possible to prove that $\exists$ is the winner of $\sigma$ by using that $h$ is winning for $\exists$ in $\mathcal{A}$ (details omitted due to space limitations). If $\sigma$ only passes finitely many modal positions, we may represent $\sigma=\sigma_{\_}{0}\cdots\sigma_{\_}{l}$ , where each $\sigma_{\_}{i}$ with $i<l$ is finite, $\sigma_{\_}{l}$ is infinite, and $(\mathit{last}(\sigma_{\_}{i}))_{\_}{i<l}$ is the sequence of all modal positions in $\sigma$ . We only consider the subcase where $l>0$ . Let $\Sigma_{\_}{\sigma}=(m_{\_}{0},s_{\_}{0})\cdots(m_{\_}{l},s_{\_}{l})$ be the $h$ -guided $\mathcal{A}$ -match that we have associated with $\sigma$ (or, to be more precise, with the initial segments of $\sigma$ that are long enough to have passed the last modal node of $\sigma$ ). Observe that since $\Sigma_{\_}{\sigma}$ is $h$ -guided, the position $(m_{\_}{l},s_{\_}{l})$ must be winning for $\exists$ , and that by (†2) the macrostate $m_{\_}{l}$ is the unique state $m$ in $A$ such that $(m_{\_}{l},s_{\_}{l})$ is met during an $h$ -guided $\mathcal{A}$ -match. Write $\sigma_{\_}{m}=(u_{\_}{0},s)(u_{\_}{1},s)(u_{\_}{2},s)\cdots$ ; that is, we write $u_{\_}{j}\mathrel{:=}v^{l}_{\_}{j}$ and $s\mathrel{:=}s_{\_}{l}$ . The sequence $u_{\_}{0}u_{\_}{1}u_{\_}{2}\cdots$ is a trace on the stream $m_{\_}{l}\mathrel{;}(e^{-}_{\_}{\chi_{\_}{s}})^{\omega}$ ; but then, by the compatibility of $\chi_{\_}{s}$ with $m_{\_}{l}$ on $\mathrm{Val}(s)$ , $u_{\_}{0}u_{\_}{1}u_{\_}{2}\cdots$ must be a good trace. Since $(u_{\_}{0},s)(u_{\_}{1},s)\cdots$ is a tail of $\sigma$ , this means that $\sigma$ is won by $\exists$ , as required.

Proof of Theorem 5.1.

The equivalence part of the disjunctive modal automaton $\mathbb{A}_{\_}{\mathbb{G},v_{\_}I}$ to $\mathbb{G}$ was proved in Proposition 5.9. It remains to check the sizes of the components of the automaton $\mathbb{A}$ . But this is fairly straightforward. To start with, from the definition of $\mathbb{A}$ we have $M_{\_}{\Omega}=\wp(V\times\mathsf{Ran}(\Omega)\times V)$ it immediately follows that $|A|\leq 2^{|V\times\mathsf{Ran}(\Omega)\times V|}=2^{n^{2}k}.$ To compute the size of $\Theta$ , first observe that the number of local strategies is equal to $2^{|A_{\_}{\lor}|}$ , and that for each macrostate $m$ , local strategy $\chi$ and color $c\in\wp\mathsf{P}$ we find $|A_{\_}{m,\chi}|\leq|V_{\_}{\Diamond}|+1\leq n$ . From this it is immediate that for each formula $\Theta(m,c)$ we have $|\Theta(m,c)|\leq 2^{|A_{\_}{\lor}|}\cdot(|V_{\_}{\Diamond}|+1)\leq n2^{n}$ . Finally, the table of $\Theta$ has $|A|\cdot 2^{|\mathsf{P}|}\leq 2^{n^{2}k}\cdot 2^{l}=2^{n^{2}k+l}$ entries, so that its total size is bounded by $n2^{n}\cdot 2^{n^{2}k+l}=n2^{n^{2}k+l+n}$ , as stated by the theorem. qed

Corollary 5.11.

The disjunctive modal automaton $\mathbb{A}_{\_}{\mathbb{G},v_{\_}I}$ can be turned into an equivalent disjunctive parity automaton $\mathbb{A}$ with index $\mathcal{O}(n\cdot k)$ and size $2^{\mathcal{O}(n^{2}k\cdot\log(nk))}$ .

Proof 5.12.

A standard construction, the so-called wreath product, can be used to turn the automaton $\mathbb{A}_{\_}{\mathbb{G},v_{\_}I}$ together with the automaton $\mathbb{P}=(P,\delta,\Omega_{\_}P,p_{\_}I)$ from Proposition 5.4 into a parity automaton (cf. e.g. [17, Definition 4.3]). The transition map of the resulting automaton $\mathbb{A}$ will have the same size as the one of $\mathbb{A}_{\_}{\mathbb{G}}$ , the set of states is given as the product $M_{\_}\Omega\times P$ and the index of $\mathbb{A}$ is equal to the index of $\mathbb{P}$ . Hence the parity automaton has size $2^{\mathcal{O}(nk\cdot\log(nk))}\cdot n2^{n^{2}k+l+n}=2^{\mathcal{O}(n^{2}k\cdot\log(nk))}$ , and index $\mathcal{O}(nk)$ .

We finish with the main result of our paper: there is an algorithm turning a parity formula into an equivalent disjunctive one in exponential size of the original formula. Due to our size preserving translations from parity formulas to $\mu$ -calculus formulas in the standard syntax, the result carries directly over to formulas in standard syntax if we measure the size of this formula in terms of its closure.

Corollary 5.13.

For any parity formula $\mathbb{G}$ we can construct an equivalent disjunctive parity formula $\mathbb{G}^{d}$ with $|\mathbb{G}^{d}|\leq 2^{\mathcal{O}(n^{2}k\cdot\log(nk))}$ and with index $\mathcal{O}(n\cdot k)$ . Here $n=|\mathbb{G}|$ and $k$ is the index of $\mathbb{G}$ .

The corollary is an immediate consequence of Corollary 5.11 and Theorem 4.1. An application of Prop. 2.5 shows that the corollary implies Thm. 1.2.

6 Conclusions

We have presented an algorithm that constructs for a given arbitrary formula in the modal $\mu$ -calculus an equivalent disjunctive formula with a single exponential blow-up when measuring the size of a formula in closure size. While the complexity of this construction is likely to be optimal, it is an interesting question for future work whether or not the construction can be optimised to obtain “nice” disjunctive formulas. In particular, the move from modal automata to parity formulas potentially adds a large number of unnecessary disjuncts. Obtaining a nicer formula could be relevant for computing uniform interpolants. Another nagging question is the exact repercussion of our work for satisfiability checking. While satisfiability checking for disjunctive formulas is linear in subformula size, our formulas are measured in closure size, which is potentially an exponential smaller. It has to be checked whether one can use our result for ExpTime satisfiability checking when the input formula is measured in closure size.

References

[1]
[2] J. Bradfield & C. Stirling (2006): Modal $\mu$ -calculi. In J. van Benthem, P. Blackburn & F. Wolter, editors: Handbook of Modal Logic, Elsevier, pp. 721–756.
[3] F. Bruse, O. Friedmann & M. Lange (2015): On guarded transformation in the modal $\mu$ -calculus. Logic Journal of the IGPL 23(2), pp. 194–216, 10.1093/jigpal/jzu030.
[4] C.S. Calude, S. Jain, B. Khoussainov, W. Li & F. Stephan (2017): Deciding parity games in quasipolynomial time. In H. Hatami, P. McKenzie & V. King, editors: Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing, (STOC 2017), ACM, pp. 252–263, 10.1145/3055399.3055409.
[5] G. D’Agostino & M. Hollenberg: Logical questions concerning the $\mu$ -calculus. Journal of Symbolic Logic 65, pp. 310–332, 10.1080/11663081.1991.10510772.
[6] G. D’Agostino & G. Lenzi (2006): On modal mu-calculus with explicit interpolants. Journal of Applied Logic 4(3), pp. 256–278, 10.1016/j.jal.2005.06.008.
[7] S. Demri, V. Goranko & M. Lange (2016): Temporal Logics in Computer Science: Finite-State Systems. Cambridge Tracts in Theoretical Computer Science, Cambridge University Press, 10.1017/CBO9781139236119.
[8] E.A. Emerson & C.S. Jutla (1988): The complexity of tree automata and logics of programs (extended abstract). In: Proceedings of the 29th Symposium on the Foundations of Computer Science, IEEE Computer Society Press, pp. 328–337.
[9] E.A. Emerson & C.S. Jutla (1991): Tree automata, mu-calculus and determinacy (extended abstract). In: Proceedings of the 32nd Symposium on the Foundations of Computer Science, IEEE Computer Society Press, pp. 368–377.
[10] S. Enqvist, F. Seifan & Y. Venema (2018): Completeness for the modal $\mu$ -calculus: Separating the combinatorics from the dynamics. Theoretical Computer Science 727, pp. 37–100, 10.1016/j.tcs.2018.03.001.
[11] G. Fontaine & Y. Venema (2018): Some model theory for the modal mu-calculus: syntactic characterizations of semantic properties. Logical Methods in Computer Science 14(1).
[12] O. Friedmann & M. Lange (2013): Deciding the unguarded modal $\mathrm{\mu}$ -calculus. Journal of Applied Non-Classical Logics 23(4), pp. 353–371, 10.1080/11663081.2013.861181.
[13] E. Grädel, W. Thomas & T. Wilke, editors (2002): Automata, Logic, and Infinite Games. LNCS 2500, Springer.
[14] D. Janin & I. Walukiewicz (1995): Automata for the modal $\mu$ -calculus and related results. In: Proceedings of the Twentieth International Symposium on Mathematical Foundations of Computer Science, MFCS’95, LNCS 969, Springer, pp. 552–562.
[15] O. Kupferman & M.Y. Vardi (2005): From Linear Time to Branching Time. ACM Transactions on Computational Logic 6(2), pp. 273–294, 10.1145/1055686.1055689.
[16] C. Kupke, J. Marti & Y. Venema (2020): Size matters in the modal $\mu$ -calculus. CoRR abs/2010.14430.
[17] C. Kupke & Y. Venema (2008): Coalgebraic Automata Theory: Basic Results. Logical Methods in Computer Science 4(4), 10.2168/LMCS-4(4:10)2008.
[18] K. Lehtinen (2015): Disjunctive form and the modal $\mu$ alternation hierarchy. In: Proceedings of FICS 2015, EPTCS 191, pp. 117–131, 10.4204/EPTCS.191.11.
[19] N. Piterman (2007): From Nondeterministic Büchi and Streett Automata to Deterministic Parity Automata. LMCS 3(3), 10.2168/LMCS-3(3:5)2007.
[20] S. Schewe (2009): Tighter Bounds for the Determinisation of Büchi Automata. In Luca de Alfaro, editor: Proceedings of FOSSACS 2009, LNCS 5504, Springer, pp. 167–181, 10.1007/978-3-642-00596-1_13.
[21] C. Stirling: Modal and Temporal Properties of Processes. Texts in Computer Science, Springer-Verlag, 10.1007/978-1-4757-3550-5.
[22] M. Y. Vardi (1998): Reasoning about the Past with Two-Way Automata. In: Proceedings of ICALP’98, LNCS 1443, Springer, pp. 628–641, 10.1007/BFb0055090.
[23] Y. Venema (2006): Automata and Fixed Point Logic: a Coalgebraic Perspective. Information and Computation 204, pp. 637–678, 10.1016/j.ic.2005.06.003.
[24] I. Walukiewicz (2000): Completeness of Kozen’s axiomatisation of the propositional $\mu$ -calculus. Information and Computation 157, pp. 142–182, 10.1006/inco.1999.2836.
[25] T. Wilke (2001): Alternating tree automata, parity games, and modal $\mu$ -calculus. Bulletin of the Belgian Mathematical Society 8, pp. 359–391.

On the size of disjunctive formulas in the μ\mu-calculus