11institutetext: ILLC, University of Amsterdam, Netherlands

# Proof Systems for the Modal $\mu$-Calculus Obtained by Determinizing
Automata

Maurice Dekker  Johannes Kloibhofer  Johannes Marti  Yde Venema

###### Abstract

Automata operating on infinite objects feature prominently in the theory of
the modal $\mu$-calculus. One such application concerns the tableau games
introduced by Niwiński & Walukiewicz, of which the winning condition for
infinite plays can be naturally checked by a nondeterministic parity stream
automaton. Inspired by work of Jungteerapanich and Stirling we show how
determinization constructions of this automaton may be used to directly obtain
proof systems for the $\mu$-calculus. More concretely, we introduce a binary
tree construction for determinizing nondeterministic parity stream automata.
Using this construction we define the annotated cyclic proof system
$\mathsf{BT}$, where formulas are annotated by tuples of binary strings.
Soundness and Completeness of this system follow almost immediately from the
correctness of the determinization method.

###### Keywords:

modal mu-calculus derivation system determinisation of Büchi and parity
automata non-wellfounded and cyclic proofs

##  1 Introduction

#### The modal $\mu$-calculus

The modal $\mu$-calculus is a natural extension of basic modal logic with
explicit least and greatest fixpoint operators. Allowing the formulation of
various recursive phenomena, this extension raises the expressive power of the
language (at least when it comes to bisimulation-invariant properties of
transition systems) to that of monadic second-order logic [11]. The
$\mu$-calculus is generally regarded as a universal specification language,
since it embeds most other logics that are used for this purpose, such as LTL,
CTL, CTL∗ and PDL. Despite its expressive power the $\mu$-calculus has still
reasonable computational properties; its model checking problem is in quasi-
polynomial time [4] and its satisfiability problem is exptime-complete [6].
Another interesting feature of the theory of the modal $\mu$-calculus lies in
its connections with other fields, in particular the theory of finite automata
operating on infinite objects, and that of infinite games.

#### Derivation systems

Given the importance of the modal $\mu$-calculus, there is a natural interest
in the development and study of derivation systems for its validities. And
indeed, already in [14] Kozen proposed an axiomatization. Despite the
naturality of this axiom system, he only established a partial completeness
result, and it took a substantial amount of time before Walukiewicz [24]
managed to prove soundness and completeness for the full language.

Kozen’s axiomatization amounts to a Hilbert-style derivation system, making it
less attractive for proof search. If one is interested in a cut-free system, a
good starting point is the two-player tableau-style game introduced by
Niwiński & Walukiewicz [18]. Here we will present their system in the shape of
a derivation system $\mathsf{NW}$ (this change of perspective can be justified
by identifying winning strategies for one of the players in the game with
$\mathsf{NW}$-proofs). $\mathsf{NW}$ is a one-sided sequent system which
allows for infinite proofs: although its proof rules are completely standard
(and finitary), due to the unfolding rules for the fixpoint operators,
derivations may have infinite branches. A crucial aspect of the
$\mathsf{NW}$-system is that one has to keep track of the _traces_ of
individual formulas along the infinite branches. A derivation will only count
as a proper proof if each of its infinite branches is _successful_ , in the
sense that it carries a so-called $\nu$-trace: a trace which is dominated by a
_greatest_ fixpoint operator.

This condition is easy to formulate but not so nice to work with. One could
describe the subsequent developments in the proof theory for the modal
$\mu$-calculus as a series of modifications of the system $\mathsf{NW}$ which
aim to get a grip on the complexities and intricacies of the above-mentioned
traces, and in particular, to use the resulting “trace management” for the
introduction of finitary, cyclic proof systems. Landmark results were obtained
by Jungteerapanich [12] and Stirling [22], who introduced cyclic proof systems
for the $\mu$-calculus, two calculi that we will identify here under the name
$\mathsf{JS}$.

#### Automata & Derivation systems

Applications of automata theory are ubiquitous in the theory of the modal
$\mu$-calculus, and the area of proof theory is no exception. In particular,
Niwiński & Walukiewicz [18] observed that infinite matches of their game,
corresponding to infinite branches in an $\mathsf{NW}$-derivation, can be seen
as infinite words or _streams_ over some finite alphabet. It follows that
_stream automata_ (automata operating on infinite words) can be used to
determine whether such a match/branch carries a $\nu$-trace. Niwiński &
Walukiewicz used this perspective to link their results to the exponential-
time complexity of the satisfiability problem for the $\mu$-calculus.

A key contribution of Jungteerapanich and Stirling [12, 22] was to bring
automata _inside_ the proof system. The basic idea would be to decorate each
sequent in a derivation with a state of the stream automaton which recognizes
whether an infinite branch is successful or not; starting from the root, the
successive states decorating the sequents on a given branch simply correspond
to a run of the automaton on this branch. For this idea to work one needs the
stream automaton to be _deterministic_. To see this, observe that two
successful but distinct branches in a derivation would generally require two
distinct runs, and in the case of a nondeterministic automaton, these two runs
might already diverge before the two branches split.

Interestingly, there is a natural stream automaton recognizing the successful
branches of an $\mathsf{NW}$-derivation: One may simply take the states of
such an automaton to be the formulas in the (Fischer-Ladner) _closure_ of the
root sequent. But given the _nondeterministic_ format of this automaton,
before it can be used in a proof system, we need to transform it into an
equivalent deterministic one. This explains the relevance of constructions for
determinizing stream automata to the proof theory of the modal $\mu$-calculus.

#### Determinization of stream automata

Using the ideas we just sketched, one may obtain sound and complete derivation
systems for the modal $\mu$-calculus in an easy way. For any deterministic
automaton $\mathbb{A}$ that recognizes the successful branches in
$\mathsf{NW}$-derivations, one could simply introduce new-style sequents
consisting of an $\mathsf{NW}$-sequent decorated with a state of $\mathbb{A}$,
and adapt the proof rules of $\mathsf{NW}$ incorporating the transition map of
$\mathbb{A}$. This could be done in such a way that the stream of decorations
of an infinite branch corresponds to the run of $\mathbb{A}$ on the stream of
sequents of the same branch. The trace condition of $\mathsf{NW}$-derivations
could then be replaced by the acceptance condition of $\mathbb{A}$ (which is
generally much simpler, since it does not refer to traces).

More interesting is to use specific determinization constructions, in order to
design more attractive proof systems or to prove results _about_ the
derivation system (and thus, potentially, about the $\mu$-calculus). In
particular, some determinization constructions are based on a _power
construction_ , meaning that the states of the deterministic automaton consist
of _macrostates_ (_subsets_ of the nondeterministic original) with some
additional structure. Such constructions allow for proof calculi where this
additional structure is incorporated into the sequents. For instance, the
derivation system $\mathsf{JS}$ is based on the well-known Safra construction
[19], in which the states of the deterministic automaton consist of
macrostates of the original automaton that are organised by means of so-called
_Safra trees_. Concretely, the (augmented) sequents in $\mathsf{JS}$ consist
of a set of _annotated formulas_ , with the annotations indicating the
position of the formula in the Safra tree and a so-called _control_ which
provides additional information on the Safra tree.

#### Our contribution

Our overall goal is to explicitize the role of automata theory in the design
of derivation systems for the modal $\mu$-calculus (and other fixpoint
logics). Our point is that distinct determinization constructions lead to
distinct sequent system, and that we may look for alternatives to the Safra
construction. Concretely the contribution of this paper is threefold:

  1. 1.

We provide a new determinization construction for both Büchi and parity stream
automata which is based on binary trees. Our construction is similar to
constructions related to so-called profile trees [7, 16].

  2. 2.

We apply our construction to obtain a new derivation system $\mathsf{BT}$ for
the modal $\mu$-calculus. While our system is similar in spirit to the system
$\mathsf{JS}$, a key difference is that our sequents consist of annotated
formulas, and nothing else.

  3. 3.

We establish the soundness and completeness of $\mathsf{BT}$. A distinguishing
feature of our approach is that (up to some optimizations) this result is a
_direct_ consequence of the soundness and completeness of $\mathsf{NW}$ and
the adequacy of our determinization construction.

#### Related work

There is an extensive literature on applications of automata theory in the
theory of the modal $\mu$-calculus, among others [5, 10, 11, 25].
Jungteerapanich and Stirling [12, 22] were the first to obtain an annotated
proof system inspired by the determinization of automata. The proof system
$\mathsf{Focus}$ for the alternation-free $\mu$-calculus designed by Marti &
Venema [17] originates with a rather simple determinization construction for
so-called weak automata. In [15], Leigh & Wehr also take a rather general
approach towards the use of determinization constructions in the design of
derivation systems, but they confine attention to the Safra construction.

#### Overview of paper

In the next section we provide the necessary background material on binary
trees, on $\omega$-automata, on the modal $\mu$-calculus and the proof system
$\mathsf{NW}$; doing so we fix our notation. In Section 3 we introduce a new
determinization method for nondeterministic Büchi and parity automata. We will
use this construction to prove the soundness and completeness of the proof
system $\mathsf{BT}$, which we introduce in Section 4. All missing proofs can
be found in the appendix.

##  2 Preliminaries

#### Binary trees

We let $2^{*}$ denote the set of _binary strings_ ; we write $<$ for the
lexicographical order of $2^{*}$, and $\sqsubseteq$ for the (initial)
substring relation given by $s\sqsubseteq t$ if $sr=t$ for some $r$.
_Substitution_ for binary strings is defined in the following way: Let
$s,t,\tilde{s},r\in 2^{*}$ be such that $s=t\tilde{s}$, then $s[t\backslash
r]$ denotes the binary string $r\tilde{s}$. A _binary tree_ is a finite set of
binary strings $T\subseteq 2^{*}$ such that $s0\in T\Rightarrow s\in T$ and
$s0\in T\Leftrightarrow s1\in T$. Here we let $\mathrm{leaves}(T)=\\{s\in
T~{}|~{}s0\notin T\\}$ denote its set of _leaves_ , and $\mathrm{minL}(T)$ its
_minimal_ leaf of $T$, i.e. the unique leaf of the form $0\cdots 0$. A set of
binary strings $L$ is a _set of leaves of a binary trees_ if for all $s\neq
t\in L$ we have $s\not\sqsubseteq t$ and $\mathrm{tree}(L)=\\{s\in
2^{*}~{}|~{}\exists t\in L:s\sqsubseteq t\\}$ is a binary tree.

#### Stream automata

A _non-deterministic automaton_ over a finite alphabet $\Sigma$ is a quadruple
$\mathbb{A}=\langle A,\Delta,a_{I},\mathrm{Acc}\rangle$, where $A$ is a finite
set, $\Delta:A\times\Sigma\rightarrow\mathcal{P}(A)$ is the transition
function of $\mathbb{A}$, $a_{I}\in A$ its initial state and
$\mathrm{Acc}\subseteq A^{\omega}$ its acceptance condition. An automaton is
called _deterministic_ if $|\Delta(a,y)|=1$ for all pairs $(a,y)\in
A\times\Sigma$. A _run_ of an automaton $\mathbb{A}$ on a stream
$w=y_{0}y_{1}y_{2}...\in\Sigma^{\omega}$ is a stream $a_{0}a_{1}a_{2}...\in
A^{\omega}$ such that $a_{0}=a_{I}$ and $a_{i+1}\in\Delta(a_{i},y_{i})$ for
all $i\in\omega$. A stream $w$ is _accepted_ by $\mathbb{A}$ if there is a run
of $\mathbb{A}$ on $w$, which is in $\mathrm{Acc}$; we define
$\mathcal{L}(\mathbb{A})$ to be the set of all accepting streams of
$\mathbb{A}$.

The acceptance condition can be given in different ways: A _Büchi_ condition
is given as a subset $F\subseteq A$. The corresponding acceptance condition is
the set of runs, which contain infinitely many states in $F$. A _parity_
condition is given as a map $\Omega:A\rightarrow\omega$. The corresponding
acceptance condition is the set of runs $\alpha$ such that
$\min\\{\Omega(a)~{}|~{}a\text{ occurs infinitely often in }\alpha\\}$ is
even. A _Rabin_ condition is given as a set $R=((G_{i},B_{i}))_{i\in I}$ of
pairs of subsets of $A$. The corresponding acceptance condition is the set of
runs $\alpha$ for which there exists $i\in I$ such that $\alpha$ contains
infinitely many states in $G_{i}$ and finitely many in $B_{i}$. Automata with
these acceptance conditions are called _Büchi_ , _parity_ and _Rabin automata_
, respectively.

#### Modal $\mu$-calculus: Syntax

The set $\mathcal{L}_{\mu}$ of _formulas_ of the modal $\mu$-calculus is
generated by the grammar

$\varphi\;::=\;p\;\mid\;\overline{p}\;\mid\;\bot\;\mid\;\top\;\mid\;(\varphi\vee\varphi)\;\mid\;(\varphi\wedge\varphi)\;\mid\;\Diamond\varphi\;\mid\;\Box\varphi\;\mid\;\mu
x.\varphi\;\mid\;\nu x.\varphi,$

where $p$ and $x$ are taken from a fixed set $\mathsf{Prop}$ of propositional
variables and in formulas of the form $\mu x.\varphi$ and $\nu x.\varphi$
there are no occurrences of $\overline{x}$ in $\varphi$.

Formulas of the form $\mu x.\varphi$ ($\nu x.\varphi$) are called _$\mu$
-formulas_ (_$\nu$ -formulas_, respectively); formulas of either kind are
called _fixpoint formulas_. We write $\eta,\lambda\in\\{\mu,\nu\\}$ to denote
an arbitrary fixpoint operator. We use standard terminology and notation for
the binding of variables by the fixpoint operators and for substitutions, and
make sure only to apply substitution in situations where no variable capture
will occur. An important use of the substitution operation concerns the
_unfolding_ $\chi[\xi/x]$ of a fixpoint formula $\xi=\eta x.\chi$.

Given two formulas $\varphi,\psi\in\mathcal{L}_{\mu}$ we write
$\varphi\to_{C}\psi$ if $\psi$ is either a direct boolean or modal subformula
of $\varphi$, or else $\varphi$ is a fixpoint formula and $\psi$ is its
unfolding. The _closure_ $\mathsf{Clos}(\Phi)\subseteq\mathcal{L}_{\mu}$ of
$\Phi\subseteq\mathcal{L}_{\mu}$ is the least superset of $\Phi$ that is
closed under this relation. It is well known that $\mathsf{Clos}(\Phi)$ is
finite iff $\Phi$ is finite. A _trace_ is a sequence
$(\varphi_{n})_{n<\kappa}$, with $\kappa\leq\omega$, such that
$\varphi_{n}\to_{C}\varphi_{n+1}$, for all $n+1<\kappa$.

We define a _dependence order_ on the fixpoint formulas occurring in $\Phi$,
written $\mathsf{Fix}(\Phi)$, by setting $\eta x.\varphi<_{\Phi}\lambda
y.\psi$ (where smaller in $<_{\Phi}$ means being of higher priority) if
$\mathsf{Clos}(\eta x.\varphi)=\mathsf{Clos}(\lambda y.\psi)$ and $\eta
x.\varphi$ is a subformula of $\lambda y.\psi$. One may define a _parity
function_ $\Omega:\mathsf{Fix}(\Phi)\rightarrow\omega$, which respects this
order (i.e., $\Omega(\eta x.\varphi)<\Omega(\lambda y.\psi)$ if $\eta
x.\varphi<_{\Phi}\lambda y\psi$) and satisfies $\Omega(\eta x.\varphi)$ is
even iff $\eta=\nu$. Let $\max_{\Omega}(\Phi)=\max\\{\Omega(\nu
x.\varphi)~{}|~{}\nu x.\varphi\in\mathsf{Fix}(\Phi)\\}$.

It is well known that any infinite trace $\tau=(\varphi_{n})_{n<\kappa}$
features a unique formula $\varphi$ that occurs infinitely often on $\tau$ and
is a subformula of $\varphi_{n}$ for cofinitely many $n$. This formula is
always a fixpoint formula, and where it is of the form $\eta x.\psi$ we call
$\tau$ an _$\eta$ -trace_.

Since the semantics of the modal $\mu$-calculus only plays an indirect role in
our paper, we refrain from giving the definition.

#### Non-wellfounded proofs

A sequent $\Gamma$ is a finite set of $\mu$-calculus formulas, possibly with
additional structure such as annotations. Rules have the following form,
possibly with additional side conditions:

Γ_1 ⋯ Γ_n [left label=$R$: ]3[]Γ

[Γ]^$\mathsf{x}$ [no rule]1⋮ [no rule]1Γ [left label=
$\mathsf{D}^{\mathsf{x}}$: ]1[]Γ

A rule $R$, where $n=0$, is called an axiom. The rules
$\mathsf{D}^{\mathsf{x}}$ are called _discharge_ rules. Each discharge rule is
marked by a unique _discharge token_ taken from a fixed infinite set
$\mathcal{D}=\\{\mathsf{x},\mathsf{y},...\\}$.

###### Definition 1

A _derivation system_ $\mathcal{P}$ is a set of rules. A $\mathcal{P}$
_derivation_ $\pi=(T,P,\mathsf{S},\mathsf{R},\mathsf{f})$ is a quintuple such
that $(T,P)$ is a, possibly infinite, tree with nodes $T$ and parent relation
$P$; $\mathsf{S}$ is a function that maps every node $u\in T$ to a non-empty
sequent $\Sigma_{u}$; $\mathsf{R}$ is a function that maps every node $u\in T$
to its _label_ $\mathsf{R}(u)$, which is either (i) the name of a rule in
$\mathcal{P}$ or (ii) a discharge token; and $\mathsf{f}$ is a partial
function that maps some nodes $u\in T$ to its _principal formula_
$\mathsf{f}(u)\in\mathsf{S}(u)$. If a specific formula $\varphi$ in the
conclusion of a rule is designated, then $\mathsf{f}(u)=\varphi$ and otherwise
$\mathsf{f}(u)$ is undefined. To qualify as a derivation, such a quintuple is
required to satisfy the following conditions:

  1. 1.

If a node is labeled with the name of a rule then it has as many children as
the rule has premises, and the annotated sequents at the node and its children
match the specification of the rules.

  2. 2.

If a node is labeled with a discharge token then it is a leaf. For every leaf
$l$ that is labeled with a discharge token $\mathsf{x}\in\mathcal{D}$ there is
exactly one node $u\in T$ that is labeled with $\mathsf{D}^{\mathsf{x}}$. This
node $u$ and its child are proper ancestors of $l$. In this situation we call
$l$ a _discharged leaf_ , and $u$ its _companion_ ; we write $c$ for the
function that maps a discharged leaf $l$ to its companion $c(l)$ and write
$p(l)$ for the path in $T$ from $c(l)$ to $l$.

A derivation
$\pi^{\prime}=(T^{\prime},P^{\prime},\mathsf{S}^{\prime},\mathsf{R}^{\prime},\mathsf{f}^{\prime})$
is a _subderivation_ of $\pi=(T,P,\mathsf{S},\mathsf{R},\mathsf{f})$ if
$(T^{\prime},P^{\prime})$ is a subtree of $(T,P)$ and
$\mathsf{S}^{\prime},\mathsf{R}^{\prime},\mathsf{f}^{\prime}$ and
$\mathsf{S},\mathsf{R},\mathsf{f}$ are equal on $(T^{\prime},P^{\prime})$. A
derivation $\pi$ is called _regular_ if it has finitely many distinct
subderivations.

###### Definition 2

Let $\pi=(T,P,\mathsf{S},\mathsf{R},\mathsf{f})$ be a derivation. We define
two graphs we are interested in: (i) The usual _proof tree_
$\mathcal{T}_{\pi}=(T,P)$ and (ii) the _proof tree with back edges_
$\mathcal{T}_{\pi}^{C}=(T,P^{C})$, where $P^{C}=P\cup\\{(l,c(l))\mid l\text{
is a discharged leaf}\\}$ is the parent relation plus back-edges for every
discharged leaf.

A _strongly connected subgraph_ in $\mathcal{T}_{\pi}^{C}$ is a set $S$ of
nodes, such that for every $u,v\in S$ there is a $P^{C}$-path from $u$ to $v$.

#### The $\mathsf{NW}$ proof system

The rules of the derivation system $\mathsf{NW}$, which is directly based on
the tableau games introduced by Niwiński & Walukiewicz [18], are given in
Figure 1.

X [left label= $\mathsf{Ax1}$ ]1p, ¯p, Γ

X [left label= $\mathsf{Ax2}$ ]1⊤, Γ

φ,ψ,Γ [left label = $\mathsf{R}_{\vee}$ ]1φ∨ψ,Γ

φ, Γ ψ,Γ [left label = $\mathsf{R}_{\wedge}$ ]2φ∧ψ,Γ

φ,Γ [left label= $\mathsf{\mathsf{R}_{\Box}}$ ]1[] □φ, ◇Γ, Δ

φ[μx . φ/ x], Γ [left label = $\mathsf{R}_{\mu}$ ]1μx . φ, Γ

φ[νx . φ/ x], Γ [left label = $\mathsf{R}_{\nu}$ ]1νx . φ, Γ

Figure 1: Rules of $\mathsf{NW}$

In order to decide whether an $\mathsf{NW}$ derivation qualifies as a proper
_proof_ , one has to keep track of the development of individual formulas
along infinite branches of the proofs.

###### Definition 3

Let $\Gamma,\Gamma^{\prime}$ be sequents, $\xi$ be a formula such that
$\Gamma$ is the conclusion and $\Gamma^{\prime}$ is a premise of a rule in
Figure 1 with principal formula $\xi$. We define the _active_ and _passive
trail relation_
$\mathsf{A}_{\Gamma,\xi,\Gamma^{\prime}},\mathsf{P}_{\Gamma,\xi,\Gamma^{\prime}}\subseteq\Gamma\times\Gamma^{\prime}$.
Both relations are defined via a case distinction on $\xi$:

_Case $\xi=\Box\varphi$:_ Then $\Gamma=\Box\varphi,\Diamond\Lambda,\Delta$ and
$\Gamma^{\prime}=\varphi,\Lambda$. We define
$\mathsf{A}_{\Gamma,\xi,\Gamma^{\prime}},=\\{(\Box\varphi,\varphi)\\}\cup\\{(\Diamond\chi,\chi)\mid\chi\in\Lambda\\}$
and $\mathsf{P}_{\Gamma,\xi,\Gamma^{\prime}}=\varnothing$.

_Case $\xi=\varphi\vee\psi$:_ Then $\Gamma=\varphi\vee\psi,\Lambda$ and
$\Gamma^{\prime}=\varphi,\psi,\Lambda$. We define
$\mathsf{A}_{\Gamma,\xi,\Gamma^{\prime}}=\\{(\varphi\vee\psi,\varphi),(\varphi\vee\psi,\psi)\\}$
and
$\mathsf{P}_{\Gamma,\xi,\Gamma^{\prime}}=\\{(\chi,\chi)\mid\chi\in\Lambda\\}$.

The relations for the remaining rules are defined analogously.

The _trail relation_
$\mathsf{T}_{\Gamma,\xi,\Gamma^{\prime}}\subseteq\Gamma\times\Gamma^{\prime}$
is defined as
$\mathsf{A}_{\Gamma,\xi,\Gamma^{\prime}}\cup\mathsf{P}_{\Gamma,\xi,\Gamma^{\prime}}$.
Finally, for nodes $u,v$ in an $\mathsf{NW}$ proof $\pi$, such that $P(u,v)$,
we define
$\mathsf{T}_{u,v}=\mathsf{T}_{\mathsf{S}(u),\mathsf{f}(u),\mathsf{S}(v)}$

Note that for any two nodes $u,v$ with $P(u,v)$ and
$(\varphi,\psi)\in\mathsf{T}_{u,v}$, we have either
$(\varphi,\psi)\in\mathsf{A}_{{u,v}}$ and $\varphi\to_{C}\psi$, or else
$(\varphi,\psi)\in\mathsf{P}_{{u,v}}$ and $\varphi=\psi$. The idea is that
$\mathsf{A}$ connects the active formulas in the premise and conclusion,
whereas $\mathsf{P}$ connects the side formulas.

###### Definition 4

Let $\pi=(T,P,\mathsf{S},\mathsf{R},\mathsf{f})$ be an $\mathsf{NW}$
derivation. A _branch_ of $\pi$ is simply a (finite or infinite) branch of the
underlying tree $(T,P)$ of $\pi$. A _trail_ on a branch
$\alpha=(v_{n})_{n<\kappa}$ is a sequence $\tau=(\varphi_{n})_{n<\kappa}$ of
formulas such that $(\varphi_{i},\varphi_{i+1})\in\mathsf{T}_{v_{i},v_{i+1}}$,
whenever $i+1<\kappa$. We obtain the _tightening_ $\widehat{\tau}$ of such a
$\tau$ by erasing all $\varphi_{i+1}$ from $\tau$ for which
$(\varphi_{i},\varphi_{i+1})$ belongs to the passive trail relation
$\mathsf{P}_{v_{i},v_{i+1}}$. We call $\tau$ a _$\nu$ -trail_ if its
tightening $\widehat{\tau}$ is a $\nu$-trace (and so, in particular, it is
infinite).

###### Definition 5

An _$\mathsf{NW}$ proof_ $\pi$ is an $\mathsf{NW}$ derivation such that on
every infinite branch of $\pi$ there is a $\nu$-trail. We write
$\mathsf{NW}\vdash\Gamma$ if there is an $\mathsf{NW}$ proof of $\Gamma$,
i.e., an $\mathsf{NW}$ proof, where $\Gamma$ is the sequent at the root of the
proof.

Soundness and Completeness of $\mathsf{NW}$ for guarded formulas, (i.e., where
in every subformula $\eta x.\psi$ all free occurrences of $x$ in $\psi$ are in
the scope of a modality) follows from the results by Niwiński & Walukiewicz
[18]. As pointed out in [2], it follows from [23] and [9] that the result in
fact holds for arbitrary formulas. By Theorem 6.3 in [18],
$\mathsf{NW}$-proofs can be assumed to be regular, and this observation
applies to unguarded formulas as well.

######  Theorem 2.1 (Soundness & Completeness)

Let $\Gamma$ be a sequent, then $\bigvee\Gamma$ is valid iff
$\mathsf{NW}\vdash\Gamma$ iff $\Gamma$ has a regular $\mathsf{NW}$-proof.

##  3 Determinization of automata with binary trees

###  3.1 Büchi automata

Let $\Sigma$ be an alphabet and $\mathbb{B}=\langle B,{\Delta},b_{I},F\rangle$
a nondeterministic Büchi automaton over $\Sigma$. We want to present an
equivalent deterministic Rabin automaton.

The _run tree_ of $\mathbb{B}$ on a word $w=(w_{i})_{i\in\omega}$ is a pair
$\mathsf{R}=(R,l)$, where $R$ is the full infinite binary tree and $l$ labels
every node $s$ with $B_{s}\subseteq B$, such that $l(\epsilon)=\\{b_{I}\\}$
and for $|s|=i$: $l(s1)=\Delta(B_{s},w_{i})\cap F$ and
$l(s0)=\Delta(B_{s},w_{i})\cap\overline{F}$, where we define
$\Delta(B_{s},y)=\bigcup_{b\in B_{s}}\Delta(b,y)$. It describes all possible
runs of $\mathbb{B}$ on $w$, using the 1s to keep track of visited states in
$F$.

The _profile tree_ , introduced in [8], is a pruned version of the run tree,
where 1) at each level all but the (lexicographically) greatest occurrence of
a state $b$ are removed and 2) nodes labelled by the empty set are deleted.
This results in a tree of bounded width, where every node has $0$,$1$ or $2$
children. It can be proved that $\mathbb{B}$ accepts a stream $w$ iff the
corresponding profile tree has a branch with infinitely many 1s.

In [7] a determinization method was defined, where macrostates encode levels
of the profile tree. In our approach macrostates encode a compressed version
of the whole profile tree up to some level: Nodes $u$, $v$ are identified
(iteratively), if $v$ is the unique child of $u$. This results in finite
binary trees, where leaves are labelled by subsets of $B$. In every step of
the transition function we add one level of the run tree and then prune and
compress the tree to obtain a binary tree again. Whenever a $1$ is compressed
(in the sense of a node being identified with its right child) we know that a
state in $F$ has been visited and mark the node green. A run of the
deterministic automaton is accepted if there is a node, which never gets
removed and is marked green infinitely often. Figure 2 contains an example of
this determinization construction.

$q_{0}$$q_{1}$$q_{2}$$a$$a$$a$$a$

$q_{0}$$m_{0}$$q_{1}$$q_{1}$$m_{1}$$q_{2}$$q_{1}$$q_{2}$$q_{1}$$m_{2}$$q_{1}$$q_{2}$$q_{1}$$q_{2}$$q_{1}$$m_{3}$$a$$a$$a$$a$

$m_{0}$$m_{1}$$m_{2}$$m_{3}$$a$$a$$a$$a$

Figure 2: A nondeterministic Büchi automaton $\mathbb{B}$ on the left and its
determinization $\mathbb{B}^{D}$ on the right. The diagram in the middle shows
the internal structure of the macrostates $m_{0}$, $m_{1}$, $m_{2}$ and
$m_{3}$ of $\mathbb{B}^{D}$. Binary trees are represented in the obvious way
(i.e., the root is the string $\epsilon$, and for every node the left child
appends $0$ and the right child appends $1$). The transitions of
$\mathbb{B}^{D}$ are split in two parts: In the first part one level of the
run tree is added, corresponding to the steps 1 and 2 in the definition of the
transition function. In the second part (the dashed arrows) the tree is pruned
and compressed, corresponding to the steps 3 and 4. The acceptance condition
of $\mathbb{B}^{D}$ is such that the word $a^{\omega}$ is accepted by
$\mathbb{B}^{D}$ because the string $\epsilon$ is always in play, marked green
infinitely often and never red.

Formally we define the deterministic Rabin automaton $\mathbb{B}^{D}=\langle
B^{D},\delta,b^{\prime}_{I},R\rangle$ as follows: An element $S$ in the
carrier $B^{D}$ of $\mathbb{B}^{D}$ is called a _macrostate_ and consists of

  * •

a subset $B_{S}$ of $B$,

  * •

a map $f:B_{S}\rightarrow 2^{*}$, such that111Here $\mathrm{ran}(f)$ denotes
the co-domain of $f$. $\mathrm{ran}(f)$ is a set of leaves of a binary tree
and

  * •

a colouring map
$c:\mathrm{tree}(\mathrm{ran}(f))\rightarrow\\{\mathrm{green},\mathrm{red},\mathrm{white}\\}$.

We define $T^{S}$ to be the binary tree $\mathrm{tree}(\mathrm{ran}(f))$, that
has $\mathrm{ran}(f)$ as its leaves and say that a binary string $s$ is _in
play_ if $s\in T^{S}$. If it is clear from the context we occasionally
abbreviate $T^{S}$ by $T$. We will sometimes denote a macrostate by a set of
pairs $(b,s)$, usually written as $b^{s}$, where $b\in B_{S}$ and $s=f(b)$ and
deal with the colouring $c$ implicitly.

The initial macrostate $b^{\prime}_{I}$ consists of the singleton
$\\{b_{I}^{\epsilon}\\}$, where $c(\epsilon)=\mathrm{white}$. To define the
transition function $\delta$ let $S$ be in $B^{D}$ and $y\in\Sigma$. We define
$\delta(S,y)=S^{\prime}$, where starting from the empty set we build up
$S^{\prime}$ in the following steps:

  1. 1.

Move: For every $a^{s}\in S$ and $b\in\Delta(a,y)$, add $b^{s}$ to
$S^{\prime}$.

  2. 2.

Append: For every $a^{s}\in S^{\prime}$, where $a\notin F$, change $a^{s}$ to
$a^{s0}$. For every $a^{s}\in S^{\prime}$, where $a\in F$, change $a^{s}$ to
$a^{s1}$.

  3. 3.

Resolve: If $a^{s}$ and $a^{t}$ are in $S^{\prime}$, where $s<t$, delete
$a^{s}$.

  4. 4.

Compress/Colour: Let $c(t)=\mathrm{white}$ for every $t\in T^{S^{\prime}}$.
Now we compress and colour $T$ in the following way, until there exists no
_witness_ $t\in T$, such that (a) or (b) is applicable:222As shown in
Proposition 1 in the appendix this procedure does not depend on the order in
which witnesses are chosen, and thus produces a unique binary tree.

    1. (a)

For any $t\in T$, such that $t0\in T$ and $t1\notin T$, change every $a^{s}\in
S^{\prime}$, where $t0\sqsubseteq s$, to $a^{s[t0\backslash t]}$. For any
$s\in T$, where $t\sqsubset s$, let $c(s)=\mathrm{red}$.

    2. (b)

For any $t\in T$, such that $t0\notin T$ and $t1\in T$, change every $a^{s}\in
S^{\prime}$, where $t1\sqsubseteq s$, to $a^{s[t1\backslash t]}$. For any
$s\in T$ such that $t=s0\cdots 0$, let $c(s)=\mathrm{green}$, if
$c(s)\neq\mathrm{red}$. In particular let $c(t)=\mathrm{green}$ if
$c(t)\neq\mathrm{red}$. For any $s\in T$, where $t\sqsubset s$, let
$c(s)=\mathrm{red}$.

We define $B^{D}$ as the set of macrostates that can be reached from
$b^{\prime}_{I}$ in this way.

A run of $\mathbb{B}^{D}$ is accepting if there is a binary string $s$, which
is in play cofinitely often such that $c(s)$ is $\mathrm{green}$ infinitely
often and $\mathrm{red}$ only finitely often.

###### Theorem 3.1

$\mathbb{B}$ accepts a word $w$ iff $\mathbb{B}^{D}$ accepts $w$.

###### Remark 1

For a Büchi automaton of $n$ states, our construction yields a deterministic
automaton $\mathbb{B}^{D}$ with $n^{\mathcal{O}(n)}$ states and a Rabin
condition of $\mathcal{O}(2^{n})$ pairs, see Lemma 5 in the appendix. With
some adaptations we could also match the optimal Rabin condition, which is
known to be linear-size [19].

This can be achieved by adding an labelling function as follows: Let
$L=\\{1,...,2n-1\\}$ be the set of potential labels. Macrostates are defined
as before, where an additional injective function $l:T^{S}\rightarrow L$ is
added. For the initial state we let $l(\epsilon)=1$. The steps 1 - 4 in the
transition function remain the same, where we add a final step 5 in which we
define the new labeling function $l^{\prime}$: We let $l^{\prime}(s)=l(s)$ for
all $s$ that already occurred in $T^{S}$ and for all $s\in
T^{S^{\prime}}\setminus T^{S}$ we let $c(s)=\mathrm{red}$ and choose new,
distinct labels in $L$, i.e. ones which do not occur in $\mathrm{ran}(l)$. The
binary tree $T^{S^{\prime}}$ has at most $n$ leaves, hence it has at most
$2n-1$ many nodes and this is always possible.

The new acceptance condition has the following form: A run of the automaton is
accepting if there is a label $k\in L$, such that $c(l^{-1}(k))$ is
$\mathrm{green}$ infinitely often and $\mathrm{red}$ only finitely often. Here
$c(l^{-1}(k))$ is defined to be $\mathrm{red}$ if $k\notin\mathrm{ran}(l)$.
This is a Rabin condition with $\mathcal{O}(n)$ pairs. Notably we still have
$n^{\mathcal{O}(n)}$ macrostates, thus the determination method is optimal.

###  3.2 Parity automata

We now extend the approach to parity automata. Let $\Sigma$ be an alphabet and
$\mathbb{A}=\langle A,\Delta_{A},a_{I},\Omega\rangle$ be a nondeterministic
parity automaton.

In order to present the intuitive idea behind the construction we first
transform $\mathbb{A}$ into an equivalent nondeterministic Büchi automaton
$\mathbb{B}$. Let $m$ be the maximal even priority of $\Omega$. For even
$k=0,2,...m$ we define $\mathbb{A}_{0},\mathbb{A}_{2},...,\mathbb{A}_{n}$ as
copies of $\mathbb{A}$ without the states of priority smaller than $k$, i.e.
$\mathbb{A}_{k}=\langle A_{k},\Delta_{k},F_{k}\rangle$ with
$A_{k}=\\{a_{k}~{}|~{}a\in A\wedge\Omega(a)\geq k\\}$,
$\Delta_{k}=\Delta_{A}|_{A_{k}}$ and $F_{k}=\\{a_{k}\in
A_{k}~{}|~{}\Omega(a)=k\\}$. Now we define the nondeterministic Büchi
automaton $\mathbb{B}=\langle B,{\Delta_{B}},b_{I},F\rangle$:333For easier
notation we represent the transition function
$B\times\Sigma\rightarrow\mathcal{P}(B)$ by its corresponding relation (i.e.,
subset of $B\times\Sigma\times B$).

$\displaystyle B=$ $\displaystyle A\cup\bigcup_{\begin{subarray}{c}k=0\\\
k~{}\text{even}\end{subarray}}^{m}A_{k},\quad\quad\quad\quad\quad
b_{I}=a_{I},\quad\quad\quad\quad\quad F=\bigcup_{\begin{subarray}{c}k=0\\\
k~{}\text{even}\end{subarray}}^{m}F_{k},$ $\displaystyle{\Delta_{B}}=$
$\displaystyle\Delta_{A}\cup\bigcup_{\begin{subarray}{c}k=0\\\
k~{}\text{even}\end{subarray}}^{m}\Delta_{k}\cup\\{(a,y,b_{k})\in
A\times\Sigma\times A_{k}~{}|~{}b\in\Delta_{A}(a,y),k=0,2,...,m\\}.$

Although $\mathbb{A}_{k}$ is not an automaton, as it does not have an initial
state, we can define the Büchi automaton $\mathbb{A}\cup\mathbb{A}_{k}=\langle
A\cup A_{k},\Delta_{B}|_{A\cup A_{k}},a_{I},F_{k}\rangle$ for $k=0,...,m$.

The intuition behind the determinization of the parity automaton $\mathbb{A}$
is the following: We apply the binary tree construction to every automaton
$\mathbb{A}\cup\mathbb{A}_{k}$ for $k=0,2,...,m$, which is possible as there
are no paths from $A_{k}$ to $A_{j}$ if $k\neq j$ and none of the accepting
states of $\mathbb{B}$ are in the set $A$. The annotation of a state
$a\in\mathbb{A}$ will then be the tuple $(s_{0},s_{2},...,s_{m})$, where
$s_{k}$ is the annotation at the state $a_{k}\in\mathbb{A}\cup\mathbb{A}_{k}$.
Note that the automaton $\mathbb{A}^{D}$ will be different from the automaton
obtained from the binary tree construction on the whole $\mathbb{B}$.

To make that formal we need some definitions. A _treetop_ $L$ is a set of
leaves of a binary tree, where potentially the minimal leaf is missing, i.e.
$L$ is a finite set of binary strings such that for all $s\neq t\in L$ it
holds $s\not\sqsubseteq t$ and $\mathrm{tree}(L)=\\{s\in 2^{*}~{}|~{}\exists
t\in L:s\sqsubseteq t\\}\cup\\{s0~{}|~{}s=0\cdots 0\text{ and }s1\in L\\}$ is
a binary tree.

For even $m$ let
$\mathrm{TSeq}(m)=\\{(s_{0},s_{2},...,s_{m})~{}|~{}s_{0},s_{2},...,s_{m}\in
2^{*}\\}$ be the set of sequences of length $\frac{m}{2}+1$, where
$s_{0},...,s_{m}$ are binary strings. Let $\pi_{k}$ be the projection
function, which maps $\sigma=(s_{0},...,s_{m})$ to $s_{k}$ for $k=0,2,...,m$.
We define a partial order $<$ on $\mathrm{TSeq}(m)$: Let
$(s_{0},...,s_{m})<(t_{0},...,t_{m})$ if there exists $l\in\\{0,...,m\\}$ such
that $s_{l}<t_{l}$ and $s_{j}=t_{j}$ for $j=0,...,l-2$.

We now define the deterministic Rabin automaton $\mathbb{A}^{D}=\langle
A^{D},\delta_{A},a^{\prime}_{I},R_{A}\rangle$. Let $m$ be the maximal even
priority of $\Omega$ in $\mathbb{A}$. An element $S$ in the carrier $A^{D}$ of
$\mathbb{A}^{D}$ consists of a tuple $(A_{S},f,c_{0},...,c_{m})$, where

  * •

$A_{S}$ is a subset of $A$,

  * •

$f:A_{S}\rightarrow\mathrm{TSeq}(m)$, such that $\mathrm{ran}(\pi_{k}\circ f)$
is a treetop for $k=0,...,m$ and

  * •

$c_{k}$ is a colouring map from $\mathrm{tree}(\mathrm{ran}(\pi_{k}\circ
f))\rightarrow\\{\mathrm{green},\mathrm{red},\mathrm{white}\\}$ for
$k=0,2,...,m$.

We define $T^{S}_{k}$ to be the binary tree
$\mathrm{tree}(\mathrm{ran}(\pi_{k}\circ f))$ for $k=0,2,...,m$ and say a
binary string $s$ is _in play at position_ $k$ if $s\in T^{S}_{k}$. If the
context is clear we will abbreviate $T^{S}_{k}$ with $T_{k}$. Again we
sometimes denote a macrostate by a set of pairs $(a,\sigma)$, usually written
as $a^{\sigma}$, where $a\in A_{S}$ and $\sigma=f(a)$ and deal with the
colourings $c_{k}$ implicitly.

The initial macrostate $a^{\prime}_{I}$ consists of the singleton
$\\{a_{I}^{(\epsilon,...,\epsilon)}\\}$. To define the transition function
$\delta_{A}$ let $S$ be in $A^{D}$ and $y\in\Sigma$. We define
$\delta_{A}(S,y)=S^{\prime}$, where $S^{\prime}$ is constructed in the
following steps:

  1. 1.

    1. (a)

Move: For every $a^{\sigma}\in S$ and $b\in\Delta_{A}(a,y)$, add $b^{\sigma}$
to $S^{\prime}$.

    2. (b)

Reduce: For every $a^{\sigma}\in S^{\prime}$, change $a^{\sigma}$ to
$a^{\sigma^{\prime}}$, where $\sigma^{\prime}$ is obtained from
$\sigma=(s_{0},...,s_{m})$ by replacing every $s_{j}$ with $j>\Omega(a)$ by
$\mathrm{minL}(T_{j})$.

  2. 2.

Append: For every $a^{\sigma}\in S^{\prime}$ and $\sigma=(s_{0},...,s_{m})$,
change $a^{\sigma}$ to $a^{\sigma^{\prime}}$, where
$\sigma^{\prime}=(s_{0}0,...,s_{k-2}0,s_{k}1,s_{k+2}0,...,s_{m}0)$ if
$\Omega(a)=k$ is even, and $\sigma^{\prime}=(s_{0}0,...,s_{m}0)$ if
$\Omega(a)=k$ is odd.

  3. 3.

Resolve: If $a^{\sigma}$ and $a^{\tau}$ are in $S^{\prime}$ and $\sigma<\tau$,
delete $a^{\sigma}$.

  4. 4.

Compress/Colour: Do for every $k=0,2,...,m$: Let $c_{k}(t)=\mathrm{white}$ for
any $t\in T_{k}$. Now we compress and colour $T_{k}$ inductively in the
following way, until there exists no _witness_ $t\in T_{k}$, such that (a) or
(b) is applicable:

    1. (a)

For any $t\in T_{k}$, such that $t0\in T_{k}$ and $t1\notin T_{k}$, change
every $a^{\sigma}\in S^{\prime}$, where $\sigma=(s_{0},...,s_{m})$, and
$t0\sqsubseteq s_{k}$, to $a^{\sigma^{\prime}}$, where
$\sigma^{\prime}=(s_{0},...,s_{k}[t0\backslash t],...,s_{m})$. For any $s\in
T_{k}$, where $t\sqsubset s$, let $c_{k}(s)=\mathrm{red}$.

    2. (b)

For any $t\in T_{k}$, such that $t0\notin T_{k}$, $t1\in T_{k}$ and $t\neq
0\cdots 0$, change every $a^{\sigma}\in S^{\prime}$, where
$\sigma=(s_{0},...s_{m})$, and $t1\sqsubseteq s_{k}$, to
$a^{\sigma^{\prime}}$, where $\sigma^{\prime}=(s_{0},...,s_{k}[t1\backslash
t],...,s_{m})$. For any $s\in T_{k}$ such that $t=s0\cdots 0$, let
$c_{k}(s)=\mathrm{green}$, if $c_{k}(s)\neq\mathrm{red}$. In particular let
$c_{k}(t)=\mathrm{green}$ if $c_{k}(t)\neq\mathrm{red}$. For any $s\in T_{k}$,
where $t\sqsubset s$, let $c_{k}(s)=\mathrm{red}$.

A run of $\mathbb{A}^{D}$ is accepting if there is $k\in\\{0,2,...,m\\}$ and a
binary string $s$, which is in play at position $k$ cofinitely often such that
$c_{k}(s)$ is $\mathrm{green}$ infinitely often and $\mathrm{red}$ only
finitely often.

###### Theorem 3.2

Let $\mathbb{A}$ be a parity automaton and ${\mathbb{A}}^{D}$ the
deterministic Rabin automaton defined from $\mathbb{A}$. Then
$L(\mathbb{A})=L({\mathbb{A}}^{D})$.

###### Remark 2

For a parity automaton $\mathbb{A}$ of size $n$ with highest even priority
$m$, our construction produces a deterministic Rabin automaton with
$n^{\mathcal{O}(m\cdot n)}$ macrostates and $\mathcal{O}(m\cdot 2^{n})$ Rabin
pairs, see Lemma 6 in the appendix.

##  4 $\mathsf{BT}$ proofs

###  4.1 Proof systems

We present two non-wellfounded proof systems for the modal $\mu$-calculus,
namely $\mathsf{BT}$ and $\mathsf{BT}^{\infty}$. The idea is that annotated
sequents in the $\mathsf{BT}$ system correspond to macrostates of
$\mathbb{A}^{D}$, where $\mathbb{A}$ is a nondeterministic parity automaton
checking the trace condition in an $\mathsf{NW}$ proof. The rules of
$\mathsf{BT}$ resemble the transition function of $\mathbb{A}^{D}$.

Let $\Phi$ be a set of formulas, the sequent we want to prove, and let
$m=\max_{\Omega}(\Phi)$ be the maximal even priority of $\Omega$. _Annotated
sequents_ are sets of pairs $(\varphi,\sigma)$, usually written as
$\varphi^{\sigma}$, where $\varphi\in\mathsf{Clos}(\Phi)$ and
$\sigma\in\mathrm{TSeq}(m)$. For an annotated sequent $\Gamma$ we let
$\Gamma^{N}$ be the set of annotations occurring in $\Gamma$, i.e.
$\Gamma^{N}=\\{\sigma\in\mathrm{TSeq}(m)~{}|~{}\exists\varphi\text{ s.t.
}\varphi^{\sigma}\in\Gamma\\}$. We let $\Gamma_{k}^{N}$ be the set of binary
strings occurring at the $k$-th position of the annotations in $\Gamma$, i.e.,
$\Gamma_{k}^{N}=\pi_{k}[\Gamma^{N}]$. We say that a string $s$ _occurs in
$\Gamma_{k}^{N}$_ if there exists $t\in\Gamma_{k}^{N}$ such that $s\sqsubseteq
t$.

For $\sigma=(s_{0},...,s_{m})\in\mathrm{TSeq}(m)$ we define $\sigma\cdot
1_{k}=(s_{0},...,s_{k}1,...,s_{m})$ and $\sigma\cdot
0_{k}=(s_{0},...,s_{k}0,...,s_{m})$. For an annotated sequent $\Gamma$ we let
$\Gamma^{\cdot 0_{k}}$ denote the annotated sequent $\\{\varphi^{\sigma\cdot
0_{k}}~{}|~{}\varphi^{\sigma}\in\Gamma\\}$.

Let $\Gamma$ be an annotated sequent and $\varphi^{\sigma}\in\Gamma$. We
define $\sigma\upharpoonright k^{\Gamma}$ to be the tuple of binary strings
obtained from $\sigma=(s_{0},...,s_{m})$ by replacing every $s_{j}$ with $j>k$
by $\mathrm{minL}(\mathrm{tree}(\Gamma_{j}^{N})$. If the context $\Gamma$ is
clear we write $\sigma\upharpoonright k$ instead of $\sigma\upharpoonright
k^{\Gamma}$.

[left label=$\mathsf{Ax1}$:]0 p^σ,¯p^τ, Γ

[left label=$\mathsf{Ax2}$:]0 ⊤^σ, Γ

φ^σ,ψ^σ, Γ [left label= $\mathsf{R}_{\vee}$:]1 (φ∨ψ)^σ, Γ

φ^σ,Γ ψ^σ, Γ [left label= $\mathsf{R}_{\wedge}$:]1 (φ∧ψ)^σ, Γ

φ[x \μx.φ ]^σ↾Ω(μx.φ),Γ [left label=$\mathsf{R}_{\mu}$:]1 μx.φ^σ, Γ

φ[x \νx.φ ]^σ↾k ⋅1_k,Γ^⋅0_k [left label=$\mathsf{R}_{\nu}$:]1[ where
$k=\Omega(\nu x.\varphi)$] νx.φ^σ, Γ

φ^σ,Γ [left label= $\mathsf{\mathsf{R}_{\Box}}$:]1[] □φ^σ, ◇Γ, Δ

φ^σ, Γ [left label=$\mathsf{Resolve}$:]1[ where $\sigma>\tau$] φ^σ, φ^τ,Γ

[Γ]^$\mathsf{x}$ [no rule]1⋮ [no rule]1Γ [left
label=$\mathsf{D}^{\mathsf{x}}$:]1Γ

φ_1^(…,st_1,…),…,φ_n^(…,st_n,…), Γ [left
label=$\mathsf{Compress}_{k}^{s0}$:]1[ where $s$ does not occur in
$\Gamma_{k}^{N}$] φ_1^(…,s0t_1,…),…,φ_n^(…,s0t_n,…), Γ

φ_1^(…,st_1,…),…,φ_n^(…,st_n,…), Γ [left
label=$\mathsf{Compress}_{k}^{s1}$:]1[ where $s$ does not occur in
$\Gamma_{k}^{N}$ and $s\neq 0\cdots 0$] φ_1^(…,s1t_1,…),…,φ_n^(…,s1t_n,…), Γ

Figure 3: Rules of $\mathsf{BT}$

The rules $\mathsf{Compress}_{k}^{s0}$ and $\mathsf{Compress}_{k}^{s1}$ are
schemata for $k=0,2,...,m$ and $s\in 2^{*}$. In these rules the notation
$\varphi_{i}^{(\dots,st_{i},\dots)}$ is to be read such that $st_{i}$ is the
binary string in the $k$-th position of the annotation. We will write
$\mathsf{Compress}$ for any of those rules and write
$\mathsf{Compress}_{k}^{s}$ for either $\mathsf{Compress}_{k}^{s0}$ or
$\mathsf{Compress}_{k}^{s1}$.

Note that, if one ignores the annotations, the rules $\mathsf{Ax1}$,
$\mathsf{Ax2}$, $\mathsf{R}_{\vee}$, $\mathsf{R}_{\wedge}$,
$\mathsf{R}_{\mu}$, $\mathsf{R}_{\nu}$ and $\mathsf{\mathsf{R}_{\Box}}$ in
Figure 3 are the same as the rules of $\mathsf{NW}$. As mentioned above
annotated sequents in the $\mathsf{BT}$ system correspond to macrostates of
$\mathbb{A}^{D}$, where $\mathbb{A}$ is a nondeterministic parity automaton
checking the trace condition in an $\mathsf{NW}$ proof. The rules of
$\mathsf{BT}$ correspond to the transition function $\delta_{A}$ of
$\mathbb{A}^{D}$, where the transformations of $\delta_{A}$ are distributed
over multiple rules: Step 1(a) of $\delta_{A}$ is carried out in every rule
and step 1(b) and step 2 correspond to the modification of the annotations in
the rules Rμ and Rν. Notably, we do not add zeros to the annotations if the
zeros would get deleted anyway in step 4 of the transition function. The rules
$\mathsf{Resolve}$ and $\mathsf{Compress}$ are additional and correspond to
steps 3 and 4 of $\delta_{A}$.

###### Definition 6

A $\mathsf{BT}$ _derivation_ $\pi$ is a derivation defined from the rules in
Figure 3, such that the rules are applied with the following priority: first
$\mathsf{Resolve}$, then $\mathsf{Compress}$, and then all other rules.

Just as annotated sequents correspond to macrostates of the deterministic
automaton $\mathbb{A}^{D}$, the soundness condition of $\mathsf{BT}^{\infty}$
and $\mathsf{BT}$ correspond to the acceptance condition of $\mathbb{A}^{D}$:
We say that a pair $(k,s)$ is preserved at a node, if $s$ is in play at
position $k$ at the corresponding macrostate and not marked red; and
progresses if it is marked green.

###### Definition 7

Let $\pi$ be a $\mathsf{BT}$ derivation of $\Phi$, $m=\max_{\Omega}(\Phi)$ and
$S$ be a set of nodes in $\pi$. Let $k\in\\{0,2,...,m\\}$ and $s\in 2^{*}$. We
say that the pair $(k,s)$

  * •

is _preserved_ on $S$ if

    * –

$s$ occurs in $\mathsf{S}(v)_{k}^{N}$ for every $v$ in $S$ and

    * –

if $\mathsf{R}(v)=\mathsf{Compress}_{k}^{t}$ for a node $v$ in $S$, then
$t\not\sqsubset s$,

  * •

_progresses_ (infinitely often) on $S$ if there is $s^{\prime}=s0\cdots 0$
such that $\mathsf{R}(v)=\mathsf{Compress}_{k}^{s^{\prime}1}$ for some $v$ in
$S$ (for infinitely many $v\in S$).

###### Definition 8

Let $\pi$ be a $\mathsf{BT}$ derivation. An infinite branch
$\alpha=(u_{i})_{i\in\omega}$ in $\pi$ is _successful_ if there are $N$ and
$(k,s)$ such that $(k,s)$ is preserved and progresses infinitely often on
$\\{u_{i}~{}|~{}i\geq N\\}$. A _$\mathsf{BT}^{\infty}$ proof_ is a
$\mathsf{BT}$ derivation without occurrences of $\mathsf{D}^{\mathsf{x}}$ and
such that all infinite branches are successful. A _$\mathsf{BT}$ proof_ is a
finite $\mathsf{BT}$ derivation such that for each _strongly connected
subgraph_ $S$ in $\mathcal{T}_{\pi}^{C}$ there exists $(k,s)$ that is
preserved and progresses on $S$.

We write $\mathsf{BT}\vdash\Gamma$ ($\mathsf{BT}^{\infty}\vdash\Gamma$) if
there is a $\mathsf{BT}$ ($\mathsf{BT}^{\infty}$) proof of $\Gamma$, i.e., a
proof, where $\Gamma$ is the sequent at the root of the proof.

###### Remark 3

In the proof system $\mathsf{JS}$ introduced by Jungteerapanich and Stirling
[12, 22] annotated sequents are of the form
$\theta\vdash\varphi_{1}^{a_{1}},...,\varphi_{n}^{a_{n}}$, where
$a_{1},...,a_{n}$ are sequences of names and the so-called _control_ $\theta$
is a linear order on all names occurring in the sequent. In contrast to
$\mathsf{JS}$ our sequents consist of formulas with annotations and nothing
else, that is, no control. On the other hand the soundness condition of
$\mathsf{BT}$ is less local: It speaks about strongly connected subgraphs,
whereas in $\mathsf{JS}$ only paths between leafs and its companions have to
be checked. We see that the control in $\mathsf{JS}$ gives information on the
structure of the cyclic proof tree. Interestingly, we could also add a control
to our sequents and obtain a soundness condition that talks about paths, if
desired. Similarly, in [1] a control was added to a cyclic system for the
first-order $\mu$-calculus introduced by [21] to obtain a path-based system.

###  4.2 Soundness and Completeness

The intuitive idea behind the $\mathsf{BT}^{\infty}$ proof system is the
following: Starting with an $\mathsf{NW}$ proof, we can define a
nondeterministic parity automaton $\mathbb{A}$, that checks if an infinite
branch carries a $\nu$-trail. Using the determinization method from Section 3
we simulate macrostates of $\mathbb{A}^{D}$ by annotated formulas in the proof
system. Thus an infinite branch in $\mathsf{BT}^{\infty}$ resembles an
infinite run of $\mathbb{A}^{D}$. This will be formalised in the Soundness and
Completeness proofs.

#### Tracking automaton

Let $\Phi$ be a sequent of formulas, $\eta x_{1}.\psi_{1},...,\eta
x_{n}.\psi_{n}$ the fixpoint formulas in $\mathsf{Fix}(\Phi)$ and $\Omega$ the
parity function on $\mathsf{Fix}(\Phi)$.

We define a nondeterministic parity automaton that checks if there is a
$\nu$-trail on an infinite branch of some $\mathsf{NW}$ proof of $\Phi$. The
alphabet $\Sigma$ consists of all triples $(\Gamma,\xi,\Gamma^{\prime})$,
where $\Gamma\subseteq\mathsf{Clos}(\Phi)$ is the conclusion and
$\Gamma^{\prime}\subseteq\mathsf{Clos}(\Phi)$ is the premise of a rule in
Figure 1 with principal formula $\xi$. We define the following
nondeterministic parity automaton $\mathbb{A}=(A,\Delta,a_{I},\Omega_{A})$:

  * •

$A=a_{I}\cup\mathsf{Clos}(\Phi)\cup\\{\eta x.\psi^{*}~{}|~{}\eta
x.\psi\in\mathsf{Clos}(\Phi)\\}$,

  * •

For each $\gamma\in A$ and $(\Gamma,\xi,\Gamma^{\prime})\in\Sigma$:

    1. 1.

if $\gamma=a_{I}$, then $\Delta(\gamma,(\Gamma,\xi,\Gamma^{\prime}))=\Phi$,

    2. 2.

if $\gamma=\xi=\eta x.\psi$ then
$\Delta(\gamma,(\Gamma,\xi,\Gamma^{\prime}))=\\{\eta x.\psi^{*}\\}$,

    3. 3.

if $\gamma=\eta x.\psi^{*}$, then
$\Delta(\gamma,(\Gamma,\xi,\Gamma^{\prime}))=\\{\gamma^{\prime}~{}|~{}(\psi[x\backslash\eta
x.\psi],\gamma^{\prime})\in\mathsf{T}_{\Gamma,\xi,\Gamma^{\prime}}\\}$ and

    4. 4.

else
$\Delta(\gamma,(\Gamma,\xi,\Gamma^{\prime}))=\\{\gamma^{\prime}~{}|~{}(\gamma,\gamma^{\prime})\in\mathsf{T}_{\Gamma,\xi,\Gamma^{\prime}}\\}$.

  * •

For all states $\eta x.\psi^{*}$ let $\Omega_{A}(\eta x.\psi^{*})=\Omega(\eta
x.\psi)$. For all other states $a$ let $\Omega_{A}(a)=\max_{\Omega}(\Phi)$ if
$\max_{\Omega}(\Phi)$ is odd and $\Omega_{A}(a)=\max_{\Omega}(\Phi)+1$ else.

Let $\alpha=(v_{n})_{n\in\omega}$ be an infinite branch in an
$\mathsf{NW}$-proof $\pi$. We define $w(\alpha)\in\Sigma^{\omega}$ to be the
infinite word
$(\mathsf{S}(v_{0}),\mathsf{f}(v_{0}),\mathsf{S}(v_{0}))(\mathsf{S}(v_{0}),\mathsf{f}(v_{0}),\mathsf{S}(v_{1}))(\mathsf{S}(v_{1}),\mathsf{f}(v_{1}),\mathsf{S}(v_{2}))...$.

###### Lemma 1

Let $\alpha$ be an infinite branch in an $\mathsf{NW}$ proof. Then $\alpha$
carries a $\nu$-trail iff $w(\alpha)\in\mathcal{L}(\mathbb{A})$.

Combining Lemma 1 and Theorem 3.2 from Section 3 we get

###### Lemma 2

Let $\pi$ be an $\mathsf{NW}$ derivation. Then $\pi$ is an $\mathsf{NW}$ proof
iff for every infinite branch $\alpha$ in $\pi$ it holds
$w(\alpha)\in\mathcal{L}(\mathbb{A}^{D})$.

###### Lemma 3

Let $\Gamma$ be a sequent. Then $\mathsf{NW}\vdash\Gamma$ iff
$\mathsf{BT}\vdash\Gamma^{\epsilon}$.

######  Proof (Sketch)

Let $\pi$ be an $\mathsf{NW}$ proof of a sequent $\Gamma$. Inductively we
translate every node $v$ in $\pi$ to a node $v^{\prime}$ plus some additional
nodes, such that $v^{\prime}$ is labeled by the same sequent as $v$ plus
annotations. This can be achieved by replacing every rule in $\mathsf{NW}$ by
its corresponding rule in $\mathsf{BT}$ and adding the rules
$\mathsf{Resolve}$ and $\mathsf{Compress}$ whenever applicable. This yields a
$\mathsf{BT}$ derivation $\rho$. It remains to show that every infinite branch
$\alpha=(v_{i})_{i\in\omega}$ in $\rho$ is successful. Let $\hat{\alpha}$ be
the corresponding infinite branch in $\pi$. Due to Lemma 2 it holds that
$\hat{\alpha}\in\mathcal{L}(\mathbb{A}^{D})$. Thus there is $(k,s)$ such that
$s$ is in play at position $k$ cofinitely often and $c_{k}(s)$ is
$\mathrm{green}$ infinitely often and $\mathrm{red}$ only finitely often. As
the annotations in $\alpha$ resemble the annotations in the run of
$\mathbb{A}^{D}$ on $\hat{\alpha}$ it follows that there is some $N\in\omega$
such that $(k,s)$ is preserved and progresses infinitely often on
$\\{v_{i}~{}|~{}i\geq N\\}$.

Conversely let $\rho$ be a $\mathsf{BT}$ proof of $\Gamma^{\epsilon}$. We let
$\pi$ be the $\mathsf{NW}$ derivation defined from $\rho$ by omitting the
rules $\mathsf{Resolve}$ and $\mathsf{Compress}$ and reducing the other rules
to the corresponding $\mathsf{NW}$ rules. We have to show that every infinite
branch $\alpha$ in $\pi$ is successful. Let
$\alpha^{\prime}=(v_{i})_{i\in\omega}$ be the corresponding infinite branch in
$\rho$. Because $\rho$ is a $\mathsf{BT}$ proof there is $N$,$(k,s)$ such that
$(k,s)$ is preserved and progresses infinitely often on $\\{v_{i}~{}|~{}i\geq
N\\}$. Again the annotations in $\alpha^{\prime}$ resemble the annotations in
the run of $\mathbb{A}^{D}$ on $\alpha$, thus $(k,s)$ witnesses the acceptance
of the run of $\mathcal{L}(\mathbb{A}^{D})$ on $\alpha$ and Lemma 2 concludes
the proof.

######  Theorem 4.1 (Soundness and Completeness)

Let $\Gamma$ be a sequent. Then there is a $\mathsf{BT}^{\infty}$-proof of
$\Gamma^{\epsilon}$ iff $\bigvee\Gamma$ is valid.

###### Proof

This follows from Lemma 3 and Theorem 2.1.

###  4.3 Cyclic $\mathsf{BT}$ proofs

As $\mathsf{NW}$ proofs can be assumed to be regular and annotations are added
deterministically we can also assume $\mathsf{BT}^{\infty}$ proofs to be
regular. A standard argument then transforms regular $\mathsf{BT}^{\infty}$
proofs into $\mathsf{BT}$ proofs and vice versa.

###### Lemma 4

An annotated sequent is provable in $\mathsf{BT}$ iff it is provable in
$\mathsf{BT}^{\infty}$.

######  Theorem 4.2 (Soundness and Completeness)

Let $\Gamma$ be a sequent. Then there is a $\mathsf{BT}$-proof of
$\Gamma^{\epsilon}$ iff $\bigvee\Gamma$ is valid..

###### Remark 4

The number of distinct subtrees in a regular $\mathsf{BT}^{\infty}$ proof can
be bounded by the number of distinct annotated sequents. This follows because
the same statement holds for $\mathsf{NW}$ proofs [18] and because in the
proof of Lemma 3 annotations and extra rules are added deterministically to
sequents in $\mathsf{NW}$ proofs.

Let $\Phi$ be a sequent, $n=|\mathsf{Clos}(\Phi)|$ and
$m=\max_{\Omega}(\Phi)$. There are at most $n^{\mathcal{O}(m\cdot n)}$ many
distinct annotated sequents occurring in a proof of $\Phi$, because annotated
sequents resemble macrostates in $\mathbb{A}^{D}$ and as seen in Remark 2
there are at most $n^{\mathcal{O}(m\cdot n)}$ distinct macrostates in
$\mathbb{A}^{D}$.

Combining these two observations with the proof of Lemma 4 yields that the
height of a $\mathsf{BT}$ proof of a sequent $\Phi$ can be bound by
$n^{\mathcal{O}(m\cdot n)}$. This is the same complexity as in $\mathsf{JS}$
[12].

###### Remark 5

Given a $\mathsf{BT}$ derivation $\pi$, we can check if $\pi$ is a
$\mathsf{BT}$ proof in $\mathrm{coNP}$. We can give the following algorithm in
$\mathrm{NP}$, that checks if $\pi$ is not a $\mathsf{BT}$ proof: Choose non-
deterministically a strongly connected subgraph $S$ and check if there exists
$(k,s)$ that is preserved and progresses on $S$, the latter can be done in
polynomial time. The complexity of proof checking can be compared to linear
time in $\mathsf{JS}$ and $\mathrm{PSPACE}$ in $\mathsf{NW}$. Note that, if we
add a control to the $\mathsf{BT}$ proof system, the soundness condition boils
down to checking paths between leafs and its companions. In that case proof
checking could also be done in linear time.

##  5 Conclusions and Future Work

We hope that this paper contributes to the theory of non-wellfounded and
cyclic proof systems by discussing applications of automata theory in the
field. We have argued for the relevance of the notion of determinizing stream
automata in the design of proof systems for the modal $\mu$-calculus. More
concretely, we have introduced a determinization construction based on binary
trees and used this to obtain a new derivation system $\mathsf{BT}$ which is
cyclic, cutfree, and sound and complete for the collection of valid
$\mathcal{L}_{\mu}$-formulas. In the remainder of this concluding section we
point out some directions for future research.

First of all, our approach is not restricted to the modal $\mu$-calculus, but
will apply to non-wellfounded and cyclic derivation systems for many other
logics as well. For instance, in the proof systems $\mathrm{LKID}^{\omega}$
[3] for first-order logic with inductive definitions, cyclic arithmetic
$\mathrm{CA}$ [20] and similar systems the trace condition is of the form that
on every infinite branch there is a term/variable which progresses infinitely
often. This condition can be checked by a nondeterministic Büchi automaton and
thus our method would yield an annotated proof system, where the annotations
are binary strings, which label the terms/variables.

Second, in Remark 3 we discussed some relative advantages and disadvantages of
the systems $\mathsf{JS}$ and $\mathsf{BT}$. It would be interesting to either
design a system that combines the advantages of both systems (i.e. sequents
consisting of annotated formulas only as in $\mathsf{BT}$, and a local
condition for proof checking as in $\mathsf{JS}$), or prove that such a system
cannot exist.

Finally, it would be interesting (and in fact, it was one of the original aims
of our work), to connect annotation-based sequent calculi such as
$\mathsf{JS}$ and $\mathsf{BT}$ to Kozen’s Hilbert-style proof system and to
see whether a more structured automata-theoretic approach would yield an
alternative proof of Walukiewicz’ completeness result. Note that this was also
the goal of Afshari & Leigh [2]; unfortunately, it was recently shown by the
second author [13] that the system $\mathsf{Clo}$, a key system in Afshari &
Leigh’s approach linking $\mathsf{JS}$ to Kozen’s axiomatization, is in fact
incomplete.

## References

  * [1] Afshari, B., Enqvist, S., Leigh, G.E.: Cyclic proofs for the first-order $\mu$-calculus. Logic Journal of the IGPL (2022). https://doi.org/10.1093/jigpal/jzac053, https://doi.org/10.1093/jigpal/jzac053
  * [2] Afshari, B., Leigh, G.E.: Cut-free completeness for modal mu-calculus. In: Proceedings of the 32nd Annual ACM/IEEE Symposium on Logic in Computer Science. LICS ’17, IEEE Press, Reykjavík, Iceland (2017)
  * [3] Brotherston, J.: Sequent calculus proof systems for inductive definitions. Ph.D. thesis (Nov 2006), https://era.ed.ac.uk/handle/1842/1458
  * [4] Calude, C., Jain, S., Khoussainov, B., Li, W., Stephan, F.: Deciding parity games in quasipolynomial time. In: Hatami, H., McKenzie, P., King, V. (eds.) Proceedings of the 49th Annual ACM SIGACT Symposium on Theory of Computing, (STOC 2017). pp. 252–263 (2017)
  * [5] Doumane, A.: Constructive completeness for the linear-time μ-calculus. In: 2017 32nd Annual ACM/IEEE Symposium on Logic in Computer Science (LICS). pp. 1–12 (2017). https://doi.org/10.1109/LICS.2017.8005075
  * [6] Emerson, E., Jutla, C.: The complexity of tree automata and logics of programs. SIAM Journal of Computing 29(1), 132–158 (1999)
  * [7] Fogarty, S., Kupferman, O., Vardi, M.Y., Wilke, T.: Profile trees for Büchi word automata, with application to determinization. Information and Computation 245, 136–151 (2015)
  * [8] Fogarty, S., Kupferman, O., Wilke, T., Vardi, M.: Unifying Büchi complementation constructions. Logical Methods in Computer Science 9(1) (2013), https://doi.org/10.2168%2Flmcs-9%281%3A13%292013
  * [9] Friedmann, O., Lange, M.: Deciding the unguarded modal μ-calculus. Journal of Applied Non-Classical Logics 23(4), 353–371 (oct 2013). https://doi.org/10.1080/11663081.2013.861181
  * [10] Janin, D., Walukiewicz, I.: 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, vol. 969, pp. 552–562. Springer (1995)
  * [11] Janin, D., Walukiewicz, I.: On the expressive completeness of the propositional $\mu$-calculus w.r.t. monadic second-order logic. In: Proceedings of the Seventh International Conference on Concurrency Theory, CONCUR ’96. LNCS, vol. 1119, pp. 263–277 (1996)
  * [12] Jungteerapanich, N.: Tableau systems for the modal $\mu$-calculus. Ph.D. thesis, School of Informatics; The University of Edinburgh (2010), http://hdl.handle.net/1842/4208
  * [13] Kloibhofer, J.: A note on the incompleteness of Afshari & Leigh’s system Clo (2023), https://doi.org/10.48550/arXiv.2307.06846
  * [14] Kozen, D.: Results on the propositional $\mu$-calculus. Theoretical Computer Science 27, 333–354 (1983)
  * [15] Leigh, G.E., Wehr, D.: From GTC to Reset: Generating Reset Proof Systems from Cyclic Proof Systems. Tech. rep. (Jan 2023). https://doi.org/10.48550/arXiv.2301.07544, http://arxiv.org/abs/2301.07544
  * [16] Löding, C., Pirogov, A.: Determinization of Büchi Automata: Unifying the Approaches of Safra and Muller-Schupp. Schloss Dagstuhl - Leibniz-Zentrum für Informatik GmbH, Wadern/Saarbruecken, Germany (2019), http://drops.dagstuhl.de/opus/volltexte/2019/10696/
  * [17] Marti, J., Venema, Y.: A focus system for the alternation-free $\mu$-calculus. In: TABLEAUX 2021, Proceedings. pp. 371–388. Lecture Notes in Computer Science, Springer (2021). https://doi.org/10.1007/978-3-030-86059-2_22
  * [18] Niwinski, D., Walukiewicz, I.: Games for the mu-Calculus. Theor. Comput. Sci. 163(1&2), 99–116 (1996). https://doi.org/10.1016/0304-3975(95)00136-0
  * [19] Safra, S.: On the complexity of $\omega$-automata. In: Proceedings of the 29th Symposium on the Foundations of Computer Science. pp. 319–327. IEEE Computer Society Press (1988)
  * [20] Simpson, A.: Cyclic Arithmetic Is Equivalent to Peano Arithmetic. In: Foundations of Software Science and Computation Structures. pp. 283–300. Lecture Notes in Computer Science, Springer (2017). https://doi.org/10.1007/978-3-662-54458-7_17
  * [21] Sprenger, C., Dam, M.: On the Structure of Inductive Reasoning: Circular and Tree-Shaped Proofs in the μCalculus (2003). https://doi.org/10.1007/3-540-36576-1_27
  * [22] Stirling, C.: A tableau proof system with names for modal mu-calculus. In: Voronkov, A., Korovina, M. (eds.) HOWARD-60. A Festschrift on the Occasion of Howard Barringer’s 60th Birthday. EPiC Series in Computing, vol. 42, pp. 306–318. EasyChair (2014). https://doi.org/10.29007/lwqm
  * [23] Studer, T.: On the proof theory of the modal mu-calculus. Studia Logica 89(3), 343–363 (aug 2008). https://doi.org/10.1007/s11225-008-9133-6
  * [24] Walukiewicz, I.: Completeness of Kozen’s axiomatisation of the propositional $\mu$-calculus. Information and Computation 157, 142–182 (2000)
  * [25] Wilke, T.: Alternating tree automata, parity games, and modal $\mu$-calculus. Bulletin of the Belgian Mathematical Society 8, 359–391 (2001)

##  Appendix 0.A Appendix

###  0.A.1 Determinization of automata with binary trees

###### Proposition 1

  1. 1.

The transition function $\delta$ is well-defined. In particular, the result of
step 4 does not depend on the order in which the witnesses $t\in T$ are
chosen.

  2. 2.

The string $\epsilon$ is never marked red.

  3. 3.

The lengths of the binary strings occurring in $\mathrm{ran}(f)$ are bounded
by the size of $B$.

###### Proof

1. After steps 1-3 of the transition function $S^{\prime}$ consists of a finite set of binary strings such that for all $s\neq t$ in $S^{\prime}$ it holds $s\not\sqsubseteq t$. Thus $T^{S^{\prime}}$ describes a tree, where every node has at most two children and the leaves are labeled by disjoint sets of states. Step 4 of $\delta$ identifies a node $t$ with its child $t^{\prime}$, if $t^{\prime}$ is its unique child. This results in a unique binary tree $T^{\prime}$. It remains to show that the colouring of $T^{\prime}$ does not depend on which nodes are identified first. Therefore we will give an equivalent presentation of step 4 of $\delta$. Let $\sim$ be the equivalence relation on $T^{S^{\prime}}$ generated by all pairs of nodes $(s,t)$ such that $t$ is the unique child of $s$. Let $T^{E}$ be the quotient of $T^{S^{\prime}}$ over $\sim$, i.e. $T^{E}=\\{[s]_{\sim}~{}|~{}s\in T^{S^{\prime}}\\}$. We can define a parent relation on $T^{E}$ as follows: $[s]_{\sim}$ is the parent of $[t]_{\sim}$ iff $s\not\sim t$ and there is $s^{\prime}\sim s$ and $t^{\prime}\sim t$ such that $s^{\prime}$ is the parent of $t^{\prime}$. If $[s]_{\sim}$ and $[t]_{\sim}$ are siblings in $T^{E}$, then there are $s^{\prime}\sim s$ and $t^{\prime}\sim t$ such that $s^{\prime}$ and $t^{\prime}$ are siblings in $T^{S^{\prime}}$, hence they inherit an order on the siblings. Thus $T^{E}$ is a binary tree, which can be given as a set of binary strings. We can define a colouring map $c$ on $T^{E}$ as follows: $[s]_{\sim}$ is coloured red if it has an ancestor $[t]_{\sim}$ with $|[t]_{\sim}|>1$. An equivalence class $[s]_{\sim}$ is coloured green if it is not red and it has a minimal descendant (i.e. every child in the ancestor path is the minimal child wrt. the sibling order) $[t]_{\sim}$ such that there are $t^{\prime}\sim t^{\prime\prime}\sim t$ where more $1$s are occurring in $t^{\prime}$ than in $t^{\prime\prime}$. All other nodes are marked white. It can be easily seen that the coloured binary tree $T^{E}$ is isomorphic to $T^{S^{\prime}}$ after step 4 independent of which nodes are identified first.

2. The string $\epsilon$ is not a real superstring of any other string, thus it can never be marked red. 3 follows, as the length of a path from the root to a leaf is bounded by the size of the tree.

###### Theorem 0.A.0

$\mathbb{B}$ accepts a word $w$ iff $\mathbb{B}^{D}$ accepts $w$.

###### Proof

Let $w=y_{0}y_{1}...\in\Sigma^{\omega}$ and $\rho^{S}=S_{0}S_{1}S_{2}...$ be
the run of $\mathbb{B}^{D}$ on $w$.

Suppose there is an accepting run $\rho=b_{0}b_{1}b_{2}..$ of $\mathbb{B}$ on
$w$. Let $s_{n}$ be the binary string such that $b_{n}^{s_{n}}\in S_{n}$ for
$n\in\omega$. Let $t$ be the maximal string which is a substring of cofinitely
many $s_{n}$ and only marked red finitely often. Note that such a string
exists, as $\epsilon$ always satisfies these conditions due to Proposition
1.2. By definition $t$ is in play cofinitely often and red only finitely
often, we will show that $c(t)$ is green infinitely often. Let $t^{\prime}$ be
the maximal string of the form $t0\cdots 0$, such that $t^{\prime}\sqsubseteq
s_{n}$ for cofinitely many $n$. Let $N$ be such that $t^{\prime}\sqsubseteq
s_{n}$ and $c(t)\neq\mathrm{red}$ in $S_{n}$ for all $n>N$.

Now we distinguish the following cases: $t^{\prime}=s_{n}$ for infinitely many
$n$ (first case), $t^{\prime}1\sqsubseteq s_{n}$ for cofinitely many $n$
(second case) and $t^{\prime}1\sqsubseteq s_{n}$ for infinitely many $n$ and
$t^{\prime}0\sqsubseteq s_{n}$ for infinitely many $n$, while
$t^{\prime}=s_{n}$ for only finitely many $n$ (third case). These three cases
cover all possibilities, as $t^{\prime}$ is the maximal string of the form
$t0\cdots 0$, such that $t^{\prime}\sqsubseteq s_{n}$ for cofinitely many $n$.

First assume that $s_{n}=t^{\prime}$ for infinitely many $n$. Let $m>N$, such
that $s_{m}=t^{\prime}$. As $\rho$ is an accepting run, $1$ will be appended
to $s_{n}$ at step 2 of $\delta$ for some $n>m$. This $1$ will need to be
removed at some possibly later stage, as $s_{n}=t^{\prime}$ infinitely often.
But the $1$ can only get removed in step 4(b), which means that $t$ is marked
green, as $c(t)$ is never red. Thus $c(t)=\mathrm{green}$ infinitely often.

Secondly let $t^{\prime}1\sqsubseteq s_{n}$ for cofinitely many $n$. Let
$N_{1}>N$, such that $t^{\prime}1\sqsubseteq s_{n}$ for all $n>N_{1}$. The
definition of $t$ implies that $t^{\prime}1$ is marked red infinitely often.
This can only happen if there is a witness $r\sqsubseteq t^{\prime}$ in step 4
of $\delta$. As $t$ is never marked red it follows that $t\sqsubseteq r$. If
$t\sqsubseteq r\sqsubset t^{\prime}$, then we are in step 4(a) and $s_{n}$ is
replaced by $s_{n}[r0\backslash r]$. Yet $t^{\prime}\not\sqsubseteq
s_{n}[r0\backslash r]$, which contradicts our assumption. Thus the witness in
step 4 of $\delta$ has to be $t^{\prime}$. In this case $t^{\prime}1\in
T^{S_{n}}$ and $t^{\prime}0\notin T^{S_{n}}$, thus $t$ is marked green.

Thirdly consider the case where $t^{\prime}0\sqsubseteq s_{n}$ for infinitely
many $n$ and $t^{\prime}1\sqsubseteq s_{n}$ for infinitely many $n$, while
$s_{n}=t^{\prime}$ for only finitely many $n$. Then it holds for infinitely
many $n>N$, that $t^{\prime}1\sqsubseteq s_{n}$ and $t^{\prime}0\sqsubseteq
s_{n+1}$. As $s_{n+1}<s_{n}$, this is only possible if $t^{\prime}$ is the
witness in step 4(b) of the transition function, i.e. $t^{\prime}1\in T$ and
$t^{\prime}0\notin T$, which means that $t$ is marked green as it is never
marked red.

Thus in every case $t$ is marked green infinitely often and the first
direction is proven.

Conversely, suppose that there is a binary string $t$ which is in play
cofinitely often and which is labeled green infinitely often and red only
finitely often. Let $N$ be such that $t$ is in play and never marked red for
any $n\geq N$. For $i\geq N$ we define

$A_{i}=\\{b^{s}\in S_{i}~{}|~{}t\sqsubseteq s\\}.$

We first show

$\displaystyle\text{For all }b^{s}\in A_{N}\text{ there is a path from
}b_{I}\text{ to }b\text{ in }\mathbb{B}\text{ on input }y_{0}\cdots y_{N-1}.$
(1) $\displaystyle\text{For all }i>N\text{ and }b^{s_{b}}\in A_{i+1}\text{
there exists }a^{s_{a}}\in A_{i}\text{ such that }b\in\Delta(a,y_{i})$ (2)

Statement (1) follows, as the transition function is just a refined version of
a macro-move. For (2) let $b^{s_{b}}\in A_{i+1}$. Due to step 1 of the
transition function there is $a^{s_{a}}\in S_{i}$ with $b\in\Delta(a,y_{i})$.
We choose $a^{s_{a}}$ with that property such that $s_{a}$ is maximal and
claim that $t\sqsubseteq s_{a}$. To see that we take a look at
$\delta(S_{i},y)$. After step 2 there is $b^{s_{a}0}$ or $b^{s_{a}1}$ in
$S^{\prime}_{i}$, which will not be removed in step 3 as we chose the maximal
$s_{a}$. Now let $r$ be maximal such that $r\sqsubseteq s_{a}$ and
$r\sqsubseteq t$. Note that $s_{a}\sqsubset t$ can not hold, because this
would imply $A_{i}=\varnothing$. If $r=t$ we are done. Else $r$ has to be a
witness in step 4 of the transition function, as $t\sqsubseteq s_{b}$. As
$s_{a}\in T^{S^{\prime}_{i}}$ this implies that $t\notin T^{S^{\prime}_{i}}$.
Yet $t\in T^{S_{i+1}}$, but this is only possible if $c(t)=\mathrm{red}$ at
the end of step 4, which contradicts our definition of $t$.

We are now able to define the trace tree $\mathcal{T}^{\mathbb{B}}$. It will
consist of the root $b_{I}$ and nodes $(a^{s_{a}},i)$, where $a^{s_{a}}\in
A_{i}$ for $i\geq N$. We define a partial order $<_{\mathcal{T}}$ on the nodes
of $\mathcal{T}^{\mathbb{B}}$ in the following way:
$(a^{s_{a}},i)<_{\mathcal{T}}(b^{s_{b}},i)$ iff $s_{a}<s_{b}$. The parent of
$(a^{s_{a}},N)$ is $b_{I}$. For $i\geq N$ the unique parent of
$(b^{s_{b}},i+1)$ is an element $(a^{s_{a}},i)$ such that
$b\in\Delta(a,y_{i})$ which is maximal with respect to $<_{\mathcal{T}}$. Such
an element always exists due to (2), if there exist more than one, choose one
of them.

The trace tree $\mathcal{T}^{\mathbb{B}}$ is an infinite, finitely branching
tree. So by König’s Lemma there exists an infinite branch
$b_{I}(a^{s_{N}}_{N},N)(a^{s_{N+1}}_{N+1},N+1)...$. We let
$\rho^{\mathcal{T}}$ be the infinite branch such that the infinite string
$s_{N}s_{N+1}...$ is minimal with respect to the lexicographical order. Due to
(1) there exists a path $\rho^{\prime}$ from $b_{I}$ to $a_{N}$ in
$\mathbb{B}$ on input $y_{0}...y_{N-1}$. Combining that with (2) we obtain
that $\rho=\rho^{\prime}a_{N}a_{N+1}...$ is a run of $\mathbb{B}$ on
$w=y_{0}y_{1}...$.

It remains to show that $\rho$ is successful, i.e. that $a_{j}\in F$ for
infinitely many $j\geq N$. To do so, assume that there is $m\geq N$, such that
$a_{i}\notin F$ for all $i\geq m$. We have $a_{i}^{s_{i}}\in A_{i}$ for $i\geq
m$, where $s_{m}=tr_{m}$ for some $r_{m}$. Let $r_{i}$ be minimal such that
$s_{i}=tr_{i}0\cdots 0$ for $i>m$. As $a_{i}\notin F$ for all $i\geq m$, only
zeros are added to $s_{i}$, hence the length of $r_{i}$ is decreasing. Now
$\rho^{\mathcal{T}}$ is the minimal infinite path in
$\mathcal{T}^{\mathbb{B}}$, thus all paths left of $\rho^{\mathcal{T}}$ are
finite, which implies that at some point $k\geq m$ it holds $s_{k}=t0\cdots
0$. Now the next time when $t$ gets labeled green, $t0\cdots 0$ has to be the
witness in step 4(b), which is only possible if $a_{j}\in F$ for some $j\geq
k$.

###### Lemma 5

For a Büchi automaton with $n$ states, the automaton $\mathbb{B}^{D}$ has
$n^{\mathcal{O}(n)}$ macrostates and the Rabin condition consists of
$\mathcal{O}(2^{n})$ pairs.

###### Proof

The number of binary trees with $k+1$ leaves $C_{k}$ is called the $k$-th
Catalan number. It holds that $C_{k}=\frac{1}{k+1}\binom{2k}{k}\leq 2^{2k}$. A
binary tree with $k$ leaves has $2k-1$ nodes, thus there are $3^{2k-1}$
possible colouring maps $c$. The $k$ leaves can be labeled by disjoint subsets
of $n$ in $(k+1)^{n}$ different ways, in particular there are at most
$(k+1)^{n}$ possibilities to label $k$ leaves with disjoint nonempty subsets
of $n$. A macrostate can be represented by a labeled, coloured binary tree of
size $k$, where $k$ ranges from $0,...,n$. In total we have

$\displaystyle|B^{D}|$ $\displaystyle\leq\sum_{k=0}^{n}C_{k-1}\cdot
3^{2n-1}\cdot(k+1)^{n}$ $\displaystyle\leq
6^{2n-1}\cdot(n+1)^{n+1}=n^{\mathcal{O}(n)}.$

The number of Rabin pairs is the number of binary strings, which may occur in
a macrostate. Due to Proposition 1.3 this is $\sum_{k=0}^{n}2^{k}\leq
2^{n+1}$.

###### Theorem 0.A.0

Let $\mathbb{A}$ be a parity automaton and ${\mathbb{A}}^{D}$ the
deterministic Rabin automaton defined from $\mathbb{A}$. Then
$L(\mathbb{A})=L({\mathbb{A}}^{D})$.

###### Proof

This proof follows the same lines as the proof of Theorem 3.1. We will focus
on the differences in the case of parity automata and omit some steps which
are analogous to the Büchi case.

Let $w=y_{0}y_{1}...\in\Sigma^{\omega}$ and $\rho^{S}=S_{0}S_{1}S_{2}...$ be
the run of $\tilde{\mathbb{A}}^{D}$ on $w$.

Suppose there is an accepting run $\rho=a_{0}a_{1}a_{2}..$ of $\mathbb{A}$ on
$w$ and let $k\in\\{0,...,m\\}$ be minimal such that $\Omega(a_{j})=k$ for
infinitely many $j\in\omega$. Because $\rho$ is accepting, $k$ is even. Let
$s_{n}$ be the binary string such that $a_{n}^{\sigma_{n}}\in S_{n}$ and
$s_{n}=(\sigma_{n})_{k}$ for $n\in\omega$. Let $t$ be the maximal string which
is a substring of cofinitely many $s_{n}$ and $c_{k}(t)=\mathrm{red}$ only
finitely often. Note that $t\neq 0\cdots 0$: Assume that $t=0\cdots 0$. As
$\rho$ is an accepting run a $1$ is appended to $s_{n}$ at some point after
the last time $c_{k}(t)=\mathrm{red}$. This $1$ can never get deleted again,
and $c_{k}(t1)$ is never $\mathrm{red}$ because this would imply $c_{k}(t)$.
Thus $t1$ is also a substring of cofinitely many $s_{n}$ and
$c_{k}(t1)=\mathrm{red}$ only finitely often.

By definition $t$ is in play at position $k$ cofinitely often and
$c_{k}(t)=\mathrm{red}$ only finitely often, we will show that $c_{k}(t)$ is
green infinitely often. Let $t^{\prime}$ be the maximal string of the form
$t0\cdots 0$, such that $t^{\prime}\sqsubseteq s_{n}$ for cofinitely many $n$.
Let $N$ be such that $t^{\prime}\sqsubseteq s_{n}$, $c_{k}(t)\neq\mathrm{red}$
in $S_{n}$ and $\Omega(a_{n})\geq k$ for all $n>N$.

Now the first direction can be proven the same way as in the proof of Theorem
3.1.

Conversely, suppose that there is $k\in\\{0,2,...,m\\}$ and a binary string
$t$, which is in play at position $k$ cofinitely often such that $c_{k}(t)$ is
$\mathrm{green}$ infinitely often and $\mathrm{red}$ only finitely often, in
particular $t\neq 0\cdots 0$. Let $N$ be such that $t$ is in play at position
$k$ and $c_{k}(t)\neq\mathrm{red}$ for all $n\geq N$. For $i\geq N$ we define

$A_{i}=\\{a^{\sigma}\in S_{i}~{}|~{}t\sqsubseteq\sigma_{k}\\}.$

We first show

$\displaystyle\text{For all }i>N\text{ and }a^{\sigma}\in A_{i}\text{ it holds
}\Omega(a)\geq k.$ (3) $\displaystyle\text{For all }a^{\sigma}\in A_{N}\text{
there is a path from }a_{I}\text{ to }a\text{ in }\mathbb{A}\text{ on input
}y_{0}\cdots y_{N-1}.$ (4) $\displaystyle\text{For all }i>N\text{ and
}b^{\sigma_{b}}\in A_{i+1}\text{ there exists }a^{\sigma_{a}}\in A_{i}\text{
such that }b\in\Delta(a,y_{i})$ (5)

For (3) assume that $\Omega(a)<k$. Then $\sigma_{k}$ is replaced by
$\mathrm{minL}(T_{k})$ at step 1(b) of the transition function, which results
in $\sigma_{k}=0\cdots 0$ at the end of the transition function. Yet $t\neq
0\cdots 0$, hence $t\not\sqsubseteq\sigma_{k}$. Statement (4) follows, as the
transition function is just a refined version of a macro-move. For (5) let
$b^{\sigma_{b}}\in A_{i+1}$. Due to step 1 of the transition function there is
$a^{\sigma_{a}}\in S_{i}$ with $b\in\Delta(a,y_{i})$. We choose
$a^{\sigma_{a}}$ with that property such that $\sigma_{a}$ is maximal, let
$s_{a}=(\sigma_{a})_{k}$ and claim that $t\sqsubseteq s_{a}$. To see that we
take a look at $\delta(S_{i},y)$. Due to (3) after step 2 there is
$b^{\sigma}$ in $S^{\prime}_{i}$, where $\sigma_{k}=s_{a}0$ or
$\sigma_{k}=s_{a}1$. $\sigma$ will not be removed in step 3 as we chose the
maximal $\sigma_{a}$. Now let $r$ be maximal such that $r\sqsubseteq s_{a}$
and $r\sqsubseteq t$. Note that $s_{a}\sqsubset t$ can not hold, because this
would imply $A_{i}=\varnothing$. If $r=t$ we are done. Else $r$ has to be a
witness in step 4 of the transition function, as $t\sqsubseteq
s_{b}=(\sigma_{b})_{k}$. Because $s_{a}\in T^{S^{\prime}_{i}}_{k}$ this
implies that $t\notin T^{S^{\prime}_{i}}_{k}$. Yet $t\in T^{S_{i+1}}_{k}$, but
this is only possible if $c_{k}(t)=\mathrm{red}$ at the end of step 4, which
contradicts our definition of $t$.

Using König’s Lemma we obtain a run $\rho=\rho^{\prime}a_{N}a_{N+1}$ of
$\mathbb{A}$ on input $w$ analogously as in the proof of Theorem 3.1. It
remains to show that $\rho$ is successful. It suffices to show that
$\Omega(a_{j})=k$ for infinitely many $j\geq N$ as $\Omega(a_{j})\geq k$ for
all $j\geq N$ due to (3). This can be done as in the proof of Theorem 3.1.

###### Lemma 6

Let $\mathbb{A}$ be a parity automaton of size $n$ and highest even parity $m$
and $\mathbb{A}^{D}$ be the deterministic Rabin automaton defined from
$\mathbb{A}$. Then $\mathbb{A}^{D}$ has $n^{\mathcal{O}(m\cdot n)}$
macrostates and $\mathcal{O}(m\cdot 2^{n})$ Rabin pairs.

###### Proof

Another way to describe a macrostate in $\mathbb{A}^{D}$ is as a collection of
macrostates in the automata $(\mathbb{A}\cup\mathbb{A}_{k})^{D}$ for
$k=0,2,...,m$, where $\mathbb{A}\cup\mathbb{A}_{k}$ is the Büchi automaton
defined above. Hence Lemma 5 yields that there are $n^{\mathcal{O}(m\cdot n)}$
possible macrostates in $\mathbb{A}^{D}$. The number of Rabin pairs is the
number of possible binary strings for $k=0,2,...,m$, in total
$m\cdot\mathcal{O}(2^{n})$.

###  0.A.2 $\mathsf{BT}$ proofs

###### Definition 9

Let $\pi$ be a $\mathsf{BT}$ proof. The _infinite unfolding_ $\pi^{*}$ of
$\pi$ is the $\mathsf{BT}$ pre-proof obtained by recursively replacing every
discharged leaf $l$ by the subtree of $\pi$ rooted at the child node of
$c(l)$.

###### Lemma 7

There is a $\mathsf{BT}^{\infty}$ proof of a sequent $\Gamma$ iff there is a
regular $\mathsf{BT}^{\infty}$ proof of $\Gamma$.

###### Proof

The same statement holds for $\mathsf{NW}$ proofs. In the proof of Lemma 3
annotations are added in a deterministic way, thus we end up with a regular
$\mathsf{BT}^{\infty}$ proof.

###### Lemma 0

An annotated sequent is provable in $\mathsf{BT}$ iff it is provable in
$\mathsf{BT}^{\infty}$.

###### Proof

Let $\pi$ be a regular $\mathsf{BT}^{\infty}$-proof of an annotated sequent
$\Phi$. For a node $v\in\pi$ we let $\pi_{v}$ be the subtree of $\pi$ rooted
at $v$. We define the equivalence relation $\sim$ by setting $v\sim u$ if
$\pi_{v}=\pi_{u}$. As $\pi$ is regular there are only finitely many distinct
equivalence classes.

Let $P_{\pi}$ be the set of infinite paths in $\pi$. We will define functions
$f_{c},f_{l}$ from $P_{\pi}\rightarrow\omega$ that select appropriate
positions for discharge rules and corresponding leaves. Let
$\alpha=(\alpha_{i})_{i\in\omega}$ be in $P_{\pi}$. As $\alpha$ is successful
there exist $t<t^{\prime}$ such that

  * •

there exists $(k,s)$ which is preserved and progresses on
$\\{v_{t},...,v_{t^{\prime}}\\}$ and

  * •

$v_{t}\sim v_{t^{\prime}}$.

Choose $(t,t^{\prime})$ minimally with respect to the lexicographic order and
define $f_{c}(\alpha)=t$ and $f_{l}(\alpha)=t^{\prime}$. Let
$C=\\{\alpha_{f_{c}(\alpha)}~{}|~{}\alpha\in P_{\pi}\\}$ and
$L=\\{\alpha_{f_{l}(\alpha)}~{}|~{}\alpha\in P_{\pi}\\}$ be the set of
companions and leaves of our new proof, respectively. We let the companion of
$l=\alpha_{f^{l}(\alpha)}$ be $c(l)=\alpha_{f^{c}(\alpha)}$. We define
$\pi_{L}$ to be the subtree of $\pi$ up to the leaves $L$. Then we insert a
$\mathsf{D}^{\mathsf{x}}$ rule at every companion node $u\in C$ with
discharged assumptions $l\in L$ such that $c(l)=u$. Using König’s Lemma we can
show that $\pi_{L}$ is indeed a finite tree.

It remains to show that

  * •

On every strongly connected subgraph $S$ of $\mathcal{T}_{\pi_{L}}^{C}$ there
exists $(k,s)$ such that $(k,s)$ is preserved and progresses on $S$.

It is easy to see that every infinite path $\alpha$ in $\pi_{L}$ corresponds
to an infinite path $\beta$ in $\pi$. Now let $S$ be a strongly connected
subgraph $S$ of $\mathcal{T}_{\pi}^{C}$ and $\alpha=(\alpha_{i})_{i\in\omega}$
be an infinite path in $\pi_{L}$ that visits every node in $S$ infinitely
often and no other node infinitely often. Let $\beta$ be the corresponding
infinite path in $\pi$. As $\beta$ is successful there is $N$ and $(k,s)$ such
that $(k,s)$ is preserved and progresses infinitely often on
$\\{\beta_{i}~{}|~{}i\geq N\\}$. Yet this yields that $(k,s)$ is preserved and
progresses on $S$.

For the other direction we can show that the infinite unfolding $\pi^{*}$ of a
$\mathsf{BT}$-proof $\pi$ is a $\mathsf{BT}^{\infty}$-proof. This follows as
every infinite branch in $\pi^{*}$ can be seen as a path in a strongly
connected subgraph of $\pi$, thus the condition for the infinite branches
follows from the same condition for every strongly connected subgraph of
$\pi$.