Mikołaj Bojańczyk

Hugo Gimbert
email: hugo.gimbert@labri.fr

Edon Kelmendi
email: edon.kelmendi@labri.fr

Emptiness of zero automata is decidable *

Keywords: 1998 ACM Subject Classification F.4.3 Formal Languages, F.4.1 Mathematical Logic tree automata, probabilistic automata, monadic second-order logic

Zero automata are a probabilistic extension of parity automata on infinite trees. The satisfiability of a certain probabilistic variant of mso, called tmso + zero, reduces to the emptiness problem for zero automata. We introduce a variant of zero automata called nonzero automata. We prove that for every zero automaton there is an equivalent nonzero automaton of quadratic size and the emptiness problem of nonzero automata is decidable, with complexity np ∩ co-np. These results imply that tmso + zero has decidable satisfiability.

Introduction

In this paper, we prove that emptiness is decidable for two classes of automata, namely zero and nonzero automata. Zero automata were introduced as a tool for recognizing models of a probabilistic extension of MSO on infinite trees [START_REF] Bojańczyk | Thin mso with a probabilistic path quantifier[END_REF]. Nonzero automata, introduced in this paper, are equivalent to zero automata, but have simpler semantics. Both zero and nonzero automata are probabilistic extensions of parity automata on infinite trees. Here we focus on the case of binary trees. The automaton performs a random walk on the infinite binary input tree: when the automaton is in a state q on a node labelled with a, it selects non-deterministically a transition (q, a, r 0 , r 1 ) and moves with equal probability 1 2 either to the left node in state r 0 or to the right node in state r 1 . The set of branches of the infinite binary tree is equipped with the uniform probability measure, which is used to define the acceptance condition. There are two variants of the acceptance condition, one for zero automata and one for nonzero automata A nonzero automaton is equipped with a total order ≤ on its set of states Q and three accepting subsets of states F ∀ , F 1 and F >0 . A run is accepting if: a) on every branch the limsup state (i.e. the maximal state seen infinitely often) is in F ∀ , b) with probability 1 the limsup state is in F 1 , c) every time the run visits a state in F >0 there is nonzero probability that all subsequent states are in F >0 . Condition (a) is the classical parity condition for tree automata and condition (b) is equivalent to the qualitative condition from [START_REF] Carayol | Randomization in automata on infinite trees[END_REF]. Condition (c) seems to be new. Conditions (a) and (b) are used to define the acceptance condition of zero automata as well, the difference between zero and nonzero automata lies in condition (c).

The paper [START_REF] Bojańczyk | Thin mso with a probabilistic path quantifier[END_REF] introduced a variant of mso on infinite trees with a probabilistic quantifier, called tmso+zero, inspired by probabilistic mso from [START_REF] Michalewski | Measure quantifier in monadic second order logic[END_REF]. In the case where zero is the unary predicate which checks whether a set of branches has probability 0, the contribution of [START_REF] Bojańczyk | Thin mso with a probabilistic path quantifier[END_REF] was a proof that for every formula of this logic one can compute a zero automaton which accepts the same trees. The logic is powerful enough to formulate properties like "every node in the tree has a descendant node labelled with b and the set of branches with infinitely many b has probability 0". As argued in [START_REF] Bojańczyk | Thin mso with a probabilistic path quantifier[END_REF], the motivation for this logic is twofold. First, it extends various probabilistic logics known in the literature, e.g. qualitative probabilistic ctl* [7], or qualitative probabilistic ctl* extended with ω-regular path properties [START_REF] Brázdil | Controller synthesis and verification for mdps with qualitative branching time objectives[END_REF]. Second, the logic, although less general that mso, represents a robust class of languages of infinite trees that goes beyond classical mso, and thus falls under the scope of the programme of searching for decidable extensions of mso.

The emptiness problem for zero automata was not solved in [START_REF] Bojańczyk | Thin mso with a probabilistic path quantifier[END_REF], thus leaving open the logic's decidability. A step toward an emptiness algorithm was made in [START_REF] Michalewski | On the regular emptiness problem of subzero automata[END_REF], where it was shown that for subzero automata -the special case of zero automata where only conditions (a) and (b) are used -one can decide if the recognised language contains a regular tree. In this paper we prove that zero and nonzero automata have decidable emptiness, and therefore also the logic from [START_REF] Bojańczyk | Thin mso with a probabilistic path quantifier[END_REF] has decidable satisfiability.

The main results of this paper are: i) For every zero automaton there is an equivalent nonzero automaton of quadratic size.

ii) A nonzero automaton with F ∀ = Q is nonempty if and only if its language contains a regular tree of size |Q|. This is decidable in polynomial time. iii) The emptiness problem of nonzero automata is in np ∩ co-np.

To prove iii) we provide a reduction of the emptiness problem to the computation of the winner of a parity game called the jumping game. For that we rely on ii): the states of the jumping game are regular runs of a nonzero automaton where F ∀ = Q. According to i) the emptiness problem for zero automata is in np ∩ co-npas well.

The plan of the paper is as follows. In Section 2 we introduce zero and nonzero automata and state our main result iii) (Theorem 3). In Section 3 we show i) (Lemma 5). In Section 4 we focus on the special case where Q = F ∀ and show ii) (Theorem 10). In Section 5 we introduce jumping games and combine the previous results to provide a proof of iii).

Zero and nonzero automata

This section introduces trees and nonzero and zero automata.

Trees, branches and subtrees.

The automata of this paper describe properties of infinite binary labelled trees. A node in a tree is a sequence in {0, 1} * . A tree over an alphabet Σ is a function t : {0, 1} * → Σ. We use standard terminology for trees: node, root, left child, right child, leaf, ancestor and descendant. A branch is a sequence in {0, 1} ω , viewed as an infinite sequence of left or right turns. A branch visits a node if the node is a prefix of the branch.

A subtree is a non-empty and ancestor-closed set of nodes. A subtree is leaf-free if each of its nodes has at least one child in the subtree. A branch of a subtree is a branch which visits only nodes of the subtree.

Probability measure over branches.

We use the coin-flipping measure on {0, 1} ω : each bit is chosen independently at random, with 0 and 1 having equal probability, and every Borel subset of {0, 1} ω is measurable. The probability of a subtree is the probability of the set of branches of the subtree. The inner regularity of the coin-flipping measure (see e.g. [START_REF] Kechris | Classical Descriptive Set Theory[END_REF]Theorem 17.10]) implies:

◮ Lemma 1. The probability of a measurable set E is the supremum of the probabilities of the subtrees whose every branch belongs to E.

Nonzero automata

Intuitively, a nonzero automaton is a nondeterministic parity tree automaton which has the extra ability to check whether the set of branches satisfying the parity condition has zero or nonzero probability.

◮ Definition 2. The syntax of a nonzero automaton is a tuple

Q states Σ input alphabet δ ⊆ Q × Σ × Q 2 transitions
, with all components finite, together with a total order ≤ on Q and three subsets

F ∀ , F 1 , F >0 ⊆ Q .
A run of the automaton on an input tree t : {0, 1} * → Σ is an infinite binary tree r : {0, 1} * → Q whose root is labelled by the maximal state of Q, also called the initial state and which is consistent with the transition relation in the usual sense, i.e. ∀v ∈ {0, 1} * , (r(v), t(v), r(v0), r(v1)) ∈ ∆. Define the limsup of a branch of the run to be the maximal state that appears infinitely often on the branch.

The run is accepting if it is surely, almost-surely and nonzero accepting: surely accepting: every branch has limsup in F ∀ . almost-surely accepting: the set of branches with limsup in F 1 has probability 1. nonzero accepting: for every node v with state in F >0 , the set of branches which visit v and visit only F >0 -labelled nodes below v has nonzero probability.

The emptiness problem

The emptiness problem asks whether an automaton has an accepting run. Our main result:

◮ Theorem 3. The emptiness problem of nonzero automata is decidable in np ∩ co-np.
Proof. This is a corollary of a series of intermediary results. In section 4 we focus on the special case where F ∀ = Q and provide an polynomial time algorithm to decide emptiness in this special case (Theorem 10). In section 5 we reduce the emptiness problem for nonzero automata to the computation of the winner in a parity game called the jumping game (Lemma 17) and give an np ∩ co-npalgorithm to compute the winner of the jumping game (Lemma 18). ◭

Zero automata

Nonzero automata are a variant of zero automata introduced in [START_REF] Bojańczyk | Thin mso with a probabilistic path quantifier[END_REF]. A zero automaton differs slightly from a nonzero automaton in that it uses a notion of "seed state" for the nonzero acceptance condition. On top of F ∀ , F 1 and F >0 there is a subset Q seed ⊆ Q. A run is accepting if it is surely, almost-surely and zero accepting:

zero accepting: for every node v with state q ∈ Q seed , there is nonzero probability that the run visits only states ≤ q below v and has limsup in F >0 .

In the next section, we show that every zero automaton can be transformed in an equivalent nonzero automaton of quadratic size (Lemma 5). Combined with Theorem 3, ◮ Corollary 4. The emptiness problem of zero automata is in np ∩ co-np.

According to [START_REF] Bojańczyk | Thin mso with a probabilistic path quantifier[END_REF], this implies that tmso + zero has decidable satisfiability when zero is the unary predicate checking that a set of branches has probability 0.

An example: the dense but not very dense language

A tree over alphabet {a, b} is dense but not very dense if:

1. every node has a descendant with label a; and 2. there is zero probability that a branch visit infinitely many nodes with letter a. This language is non-empty, contains no regular tree and is recognised by a nonzero automaton. This automaton has three states, totally ordered as follows:

s searching for a < n not searching for a < f just found a .
The automaton begins in state f in the root. When the automaton reads a node with label b, then it sends s to some child and n to the other child, regardless of its current state.

Choosing which child gets s and which child gets n is the only source of nondeterminism in this automaton. When the automaton sees letter a, it sends f to both children regardless of its current state. The acceptance condition is:

F ∀ = {n, f } F 1 = {n} F >0 = ∅ .

From zero to nonzero automata

In this section we show that nonzero automata are as expressive as zero automata.

◮ Lemma 5. For every zero automaton one can compute a nonzero automaton of quadratic size which accepts the same trees.

The rest of the section is dedicated to the proof of Lemma 5, which is a direct corollary of Lemma 7 and Lemma 8 below.

Without loss of generality, we assume that in every zero automaton

F >0 ⊆ F 1 ⊆ F ∀ . Changing F 1 for F 1 ∩ F ∀ and F >0 for F >0 ∩ F 1 does
not modify the set of accepting runs of a zero automaton, since all branches should have limsup in F ∀ and if the limsup is equal with nonzero probability to some q ∈ F >0 then necessarilly q ∈ F 1 . By contrast, for nonzero automata there is no obvious reason for the same remark to hold.

We make use of an intermediary acceptance condition. Let r be a run. We say that a path from a node v to a node w is seed-consistent if whenever the path visits a seed state s, subsequent states are ≤ s.

Strong zero acceptance condition: for every node v labelled by a seed state, there is a seed-consistent path from v to a strict descendant w of v such that the state r(w) of w is in F >0 and there is nonzero probability that the run visits only states ≤ r(w) below w, has limsup r(w), in case r(w) ∈ Q seed , visits no seed state below w, in case r(w) ∈ Q seed , visits no seed state other than r(w) below w.

Actually, the strong zero and zero acceptance conditions coincide (proof in appendix):

◮ Lemma 6. A run is zero accepting if and only if it is strongly zero accepting.

Construction of the nonzero automaton

Intuitively, every zero automaton can be simulated by a nonzero automaton which guesses on the fly a run of the zero automaton and checks simultaneously that the guessed run is strongly zero accepting. Whenever the automaton visits a node v with a seed state then it enters in the next step a path-finding state and guesses a seed-consistent path to a node w which is a witness of the strong zero condition. Once on the node w the automaton enters a subtree-guessing state and starts guessing a leaf-free subtree of the run, whose nodes are labelled by states ≤ r(w), whose branches have limsup r(w) and which has nonzero probability.

There are some verifications to do in order to certify that the guessed run is strongly zero accepting. The surely accepting condition is used to prevent the automaton to stay forever in the path-finding mode and also to check that every branch of the subtree has limsup r(w). The nonzero condition is used to check that the subtree has nonzero probability. To perform these verifications, the nonzero automaton stores some data in its control state. In path-finding mode the automaton records the smallest seed state seen so far in order to check on-the-fly that the path from v to w is seed-consistent. In subtree-guessing mode the automaton keeps track of the state r(w).

The set of states of this automaton is denoted R, every state in R has as a first component a control state Q of the zero automaton. Precisely, R is the union of three sets:

normal states: Q path-finding states: {(q, s) | q ∈ Q, s ∈ Q seed , q ≤ s}, subtree-guessing states:

{(q, f, * ) | q ∈ Q, f ∈ F >0 , q ≤ f, (q ∈ Q seed ∨ q = f )}.
We equip R with any order ≺ such that the projection on the first component Π 1 : (R, ≺) → (Q, <) is monotonic, (q, s) ≺ q for every q ∈ Q and s ∈ Q seed with q ≤ s. The zero, almost-surely and surely accepting conditions are defined respectively as: G >0 = the set of subtree-guessing states,

G 1 = F 1 ∪ {(f, f, * ) | f ∈ F >0 }, G ∀ = F ∀ ∪ {(f, f, * ) | f ∈ F >0 } .
The transitions of the automaton can be informally described as follows. The nonzero automaton guesses on the fly a run ρ : {0, 1} * → Q of the zero automaton by storing the value of ρ(v) as the first component of its own control state on the node v. The nonzero automaton stays in the set of normal states as long as the run does not enter a seed state. On a node v labelled by s ∈ Q seed , the nonzero automaton starts looking for a path to a descendant node w that satisfies the strong zero condition. For that in the next step the automaton enters either a path-finding or a subtree-guessing state. While in a pathfinding state, the automaton guesses on the fly a seed-consistent path. Whenever the run is in a nonzero state f ∈ F >0 the nonzero automaton can enter the subtree-guessing state C V I T 2 0 1 6 (f, f, * ), or not. While in subtree-guessing mode the second component is constant, and the automaton control state is of type (q, f, * ) with q ≤ f and q ∈ Q seed unless q = f ∈ Q seed . From a subtree-guessing state the automaton may switch back any time to a normal state.

Formally, for every transition q → r 0 , r 1 of the zero automaton, there is a transition

q ′ → r ′ 0 , r ′ 1
in the nonzero automaton if the first component of q ′ is q and

r ′ 0 =           
r 0 whenever q ′ is not path-finding (r 0 , r 0 , * ) whenever q ∈ Q seed , q ′ = q and r 0 ∈ F >0 and r 0 ≤ q or q ′ = (q, s) and r 0 ∈ F >0 and r 0 ≤ s, (r 0 , f, * ) whenever q ′ = (q, f, * ) and r 0 ≤ f and (r

0 ∈ Q seed ∨ r 0 = f ).
The possible values of r ′ 1 are symmetric. There are also left path-finding transitions: for every seed states s, s ′ ∈ Q seed such that q ≤ s and r 0 ≤ s there are transitions q ′ → (r 0 , s ′ ), r 1 where q ′ = q or (q, q) if q = s (q, s) otherwise and

s ′ = s if r 0 ∈ Q seed r 0 if r 0 ∈ Q seed .
There may also be a symmetric right path-finding transition (q, s) → r 0 , (r 1 , s ′ ) when the symmetric conditions hold.

The next two lemmas relate the accepting runs of the zero and the nonzero automata, their proofs can be found in the appendix.

Emptiness of F ∀ -trivial automata is in NP

A run of a nonzero automaton needs to satisfy simultaneously three conditions, which correspond to the accepting sets F ∀ , F 1 , F >0 . For a subset

I ⊆ {F ∀ , F 1 , F >0 }
define I-automata to be the special case of nonzero automata where only the acceptance conditions corresponding to I need to be satisfied. These are indeed special cases: ignoring F >0 can be achieved by making it empty, ignoring F 1 can be achieved by making it equal to F ∀ , and ignoring F ∀ can be achieved by making it equal to all states Q.

Generalising parity automata, with standard and qualitative semantics

A {F ∀ }-automaton is a parity automaton. Thus solving emptiness for nonzero automata is at least as hard as emptiness for parity automata on trees, which is polynomial time equivalent to solving parity games, in np ∩ conp or in quasi-polynomial time [START_REF] Calude | Deciding parity games in quasipolynomial time[END_REF].

A {F 1 }-automaton is the same as a parity automaton with qualitative semantics as introduced in [START_REF] Carayol | Randomization in automata on infinite trees[END_REF]. Emptiness for such automata can be solved in polynomial time using standard linear programming algorithms for Markov decision processes.

Subzero automata

A {F 1 , F ∀ }-automaton is the same as a subzero automaton as considered in [START_REF] Michalewski | On the regular emptiness problem of subzero automata[END_REF]. In [START_REF] Michalewski | On the regular emptiness problem of subzero automata[END_REF], it was shown how to decide if a subzero automaton accepts some regular tree. Since some subzero automata are nonempty but accept no regular trees, see e.g. the example in [START_REF] Bojańczyk | Thin mso with a probabilistic path quantifier[END_REF], the result from [START_REF] Michalewski | On the regular emptiness problem of subzero automata[END_REF] does not solve nonemptiness for subzero automata.

F ∀ -trivial automata

In a {F 1 , F >0 }-automaton, the surely accepting condition is trivial, i.e. F ∀ = Q. We call such automata F ∀ -trivial. The acceptance of a run of a F ∀ -trivial automaton depends only on the probability measure on Q ω induced by the run, individual branches do not matter.

◮ Definition 9 (Positional run). A run is positional if whenever the states of two nodes coincide then the states of their left children coincide and the states of their right children coincide.

◮ Theorem 10. If a F ∀ -trivial automaton has an accepting run, then it has a positional accepting run. Emptiness of F ∀ -trivial automata can be decided in polynomial time.

The proof of this theorem relies on the notion of acceptance witnesses.

◮ Definition 11 (Transition graph and acceptance witness). Let D be a set of transitions.

The transition graph of D, denoted G D , is the directed graph whose vertices are all states appearing in one of the transitions in D, denoted Q D , and whose edges are induced by the transitions in D: for every (q, a, l, r) ∈ D both (q, l) and (q, r) are edges of G D .

The set D is an acceptance witness if it satisfies the four following conditions: i) Q D contains the initial state of the automaton and G D has no dead-end, ii) the maximum of every bottom strongly connected component (BSCC

) of G D is in F 1 , iii) every BSCC of G D is either contained in F >0 or does not intersect F >0 , iv) from every state in F >0 ∩ Q D there is a path in F >0 ∩ Q D to a BSCC contained in F >0 .
◮ Lemma 12. If a F ∀ -trivial automaton has an acceptance witness, it has a positional accepting run.

Proof. The proof is by induction on

N D = |D| -|Q D |. Since G D has no dead-end, every state in Q D is the source of a transition in D thus N D ≥ 0.
If N D = 0 then for every state q ∈ Q D there is a unique transition δ q = (q, a q , l q , r q ). Let ρ be the positional run whose root has the initial state and every node with vertex q ∈ Q D has children l q and r q , which is well-defined according to property i). We show that ρ is an accepting run. The graph G D can be seen as a Markov chain, with probability either 1 or 1 2 on every edge, depending on the outdegree. The probability measure on Q ω D produced by the random walk on ρ coincide with the probability measure on Q ω D produced by this finite Markov chain: indeed both measures coincide on finite cylinders q 0

• • • q n Q ω D .
Basic theory of finite homogenous Markov chain implies that almost-surely every branch of the run ends up in one of the BSCCs of G D and visits all its states infinitely often. Thus property ii) ensures that the run ρ is almost-surely accepting. Properties iii) and iv) guarantee that the run is moreover nonzero-accepting.

Assume now that N D > 0. We show that there is a strictly smaller acceptance witness D ′ D. Let q ∈ Q D which is the source of several transitions in D, then D ′ is obtained by removing from D all these transitions except one. To choose which transition δ to keep, we pick up the shortest path q = q 0 . . . q n in G D of length ≥ 1 which leads to the maximal C V I T 2 0 1 6

23:8

Emptiness of zero automata is decidable state of one of the BSCCs of G D . Moreover if q ∈ F >0 we require the whole path to stay in F >0 . By definition of G D there is at least one transition in D whose origin is q and one of the two successors is q 1 . To get D ′ we delete all other transitions with source q from D.

Clearly property i) is preserved by this operation. To address properties ii)-iv), we show that every BSCC B ′ of G D ′ is either a BSCC of G D or contained in the BSCC B of G D whose maximum is q n , in which case max B = max B ′ = q n . There are two cases. If B ′ does not contain q n then it does not contain q either (because q = q 0 . . . q n is still a path in G D ′ ). Since the only difference between G D and G D ′ are the outgoing transitions from q then B ′ is actually a BSCC of G D . If B ′ contains q n then B ′ ⊆ B (because there are less edges in G D ′ than in G D ) and since q n = max B then max B = max B ′ .

As a consequence property ii) and iii) are preserved. And property iv) is preserved as well: in case q ∈ F >0 then there is nothing to prove and in case q ∈ F >0 then q = q 0 . . . q n is still a path in G D ′ , with all vertices in F >0 . Moreover the set of vertices from which q n is accessible is the same in G D and

G D ′ thus q n is in a BSCC of G D ′ . ◭
A strong version of the converse implication of Lemma 12 holds:

◮ Lemma 13. If a F ∀ -trivial automaton has an accepting run, it has an acceptance witness.

Proof. We fix an accepting run ρ on some input tree t. To extract an acceptance witness from ρ, we make use of the notion of end-component introduced in [START_REF] Alfaro | Formal Verification of Probabilistic Systems[END_REF].

◮ Definition 14 (End-component). The transition of a node v is d(v) = (ρ(v), t(v), ρ(v0), ρ(v1)).
For every branch b, we denote ∆ ∞ (b) the set of transitions labelling infinitely many nodes of the branch. For every subset D ⊆ ∆ we denote

B D the set of branches b such that ∆ ∞ (b) = D. A set of transitions D ⊆ ∆ is an end-component of the run if B D has nonzero probability.
Call a branch b even if for every transition δ = (q, a, l, r) ∈ ∆ ∞ (b), not only the state q but also the states l and ρ appear infinitely often on the branch in the run ρ. Almost-surely every branch is even, because each time a branch visits a node with transition δ it proceeds left or right with equal probability 1 2 . As a consequence, Let D be the collection of all end-components of the run ρ. We define two subsets of D, denoted respectively D 0 and D 1 , which collect the end-components whose states are respectively included in F >0 and disjoint from F >0 . Let D 0 ⊆ ∆ (resp. D 1 ⊆ ∆) be the union of all end-components in D 0 (resp. in D 1 ). These transitions are easy to reach: ◮ Lemma 16. Every node v has a descendant w whose transition belongs to D 0 ∪ D 1 . Moreover if the state of v is in F >0 then w can be chosen such that the path v to w is labelled by F >0 and the transition is in D 0 .

◮
Proof. Let v be a node and S v the set of branches which visit v and, in case v is labelled by F >0 , visit only F >0 -labelled nodes below v. Since the run is accepting then S v has positive probability. By definition of end-components, almost-every branch is in D∈D B D . Thus there exists an end-component D such that B D ∩ S v has positive probability. As a consequence, v has a descendant w whose transition is in D. Since almost-every branch is even and B D ∩ S v has positive probability then there is at least one branch in B D ∩ S v which visits infinitely often all states appearing in Q D . In case v is labelled by F >0 , this implies that Q D ⊆ F >0 thus D ∈ D 0 , and terminates the proof of the second statement. In case v has no descendant labelled by F >0 this implies that Q D ∩ F >0 = ∅ thus D ∈ D 1 , and the first statement holds in this case. In the remaining case, v has a descendant v ′ labelled with F >0 , which itself has a descendant w whose transition belongs to some D ∈ D 0 , thus the first statement holds for v. ◭

We terminate the proof of Lemma 13. Let G 0 (resp. G 1 ) the transition graph of D 0 (resp. D 1 ) and denote Q 0 (resp Q 1 ) the set of states of G 0 (resp. G 1 ). Let D be the set of all transitions appearing in the run. According to Lemma 16, in the transition graph

G D , Q 0 ∪ Q 1 is accessible from every state q ∈ Q D and moreover Q 0 is accessible from every state q ∈ Q D ∩ F >0 following a path in Q D ∩ F >0 .
We say that an edge (q, r) of G D is progressive if q ∈ Q 0 ∪ Q 1 and either (q ∈ F >0 and r ∈ F >0 and (q, r) decrements the distance to Q 0 in G D ) or (q ∈ F >0 and (q, r) decrements the distance to

Q 0 ∪ Q 1 in G D ). Every state in Q D \ (Q 0 ∪ Q 1 )
is the source of at least one progressive edge.

We denote D + the union of D 0 and D 1 plus all the transitions δ = (q, a, r 0 , r 1 ) ∈ D such that either (q, r 0 ) or (q, r 1 ) is progressive. Then D + has all four properties of Lemma 12. Denote G + the transition graph associated to D + . Property i) holds because every state in Q D , including the initial state, is either in Q 0 ∪ Q 1 or is the source of a progressive edge.

Remark that the BSCCs of G + are exactly the BSCCs of G 0 and G 1 . Since both G 0 and G 1 are unions of strongly connected graphs, they are equal to the union of their BSCCs. The BSCCs of G 0 and G 1 are still BSCCs in G + because no edges are added inside them (progressive edges have their source outside G 0 and G 1 ). Following the progressive edges leads to G 0 or G 1 from every state in G + , thus there are no other BSCCs in G + .

This implies property ii) because, according to Lemma 15, both graphs G 0 and G 1 are the union of strongly connected graphs whose maximal states are in F 1 . This also implies property iii) since Q 0 ⊆ F >0 and Q 1 ∩ F >0 = ∅. Property iv) is obvious for states in Q 0 because Q 0 is a union of BSCCs included in F >0 . Property iv) holds as well for states in (Q D ∩F >0 )\Q 0 , the path to Q 0 is obtained following the progressive edges in F >0 ×F >0 . ◭ Proof of Theorem 10. According to Lemma 13 and Lemma 12, non-emptiness of a F ∀trivial automaton is equivalent to the existence of an acceptance witness, which implies the existence of a positional accepting run. Guessing a subset of transitions and checking it is an acceptance witness can be done in non-deterministic polynomial time.

Actually it is possible to check the existence of an acceptance witness in polynomial time. Using standard algorithms for Markov decision processes, one can compute the set R 0 (resp. R 1 ) of states q such that there exists an almost-surely accepting run with root state q and whose states are labelled by F >0 (resp. by Q \ F >0 ) (see [START_REF] Carayol | Randomization in automata on infinite trees[END_REF]Corollary 18] for more details).

We transform the F ∀ -trivial automaton A into another F ∀ -trivial automaton A ′ as follows. In A ′ every state q in R 0 ∪ R 1 is turned into an absorbing state: for every letter a there is a transition (q, a, q, q) and no other transition with source q. Moreover we change the almost-sure condition and set it equal to R 0 ∪R 1 . The positive condition is not modified.

C V I T 2 0 1 6

23:10

Emptiness of zero automata is decidable

We claim that A has an accepting run if and only if A ′ has one. Assume A has an accepting run. Then it has an acceptance witness D. According to ii), every BSCC

B of D is included either in R 0 (if B ⊆ F >0 ) or in R 1 (if B ∩ F >0 = ∅).
Thus D can be turned into an acceptance witness of A ′ by exchanging any transition (q, a, l, r) with q ∈ R 0 ∪ R 1 into the absorbing transition (q, a, q, q). Conversely, assume A ′ has an accepting run ρ ′ . Then by definition of R 0 and R 1 every state q ∈ R 0 ∪ R 1 is an acceptance witness of some almostsurely accepting run ρ q with root q and all nodes in F >0 or out of F >0 . Then we can build an accepting run of A by modifying ρ ′ as follows: for every node labelled by q ∈ R 0 ∪ R 1 with no ancestor labelled by R 0 ∪ R 1 we replace the subtree by ρ q . Since almost-surely every path reaches R 0 ∪ R 1 then the new run is almost-surely and positively accepting.

The criteria for D to be an acceptance witness of A ′ are simple: Q D should contain the initial state and moreover: a) G D has no dead-end, b) from every state in

Q D there is a path in Q D to R 1 ∪ R 0 . c) from every state in F >0 ∩ Q D there is a path in F >0 ∩ Q D to R 0 .
Notice that properties a), b) and c) are closed by union: if both D 1 and D 2 have these three properties then D 1 ∪ D 2 as well. And the largest set of transitions D max with properties a) b) and c) is easy to compute in polynomial time: start with D max equal to all transitions and as long as possible remove:

any transition leading to a dead-end, all transitions inside a BSSC disjoint from R 0 and R 1 , all transitions (q, a, q 0 , q 1 ) such that q ∈ F >0 and R 0 is not reachable from q by a path in F >0 ∩ Q Dmax . An invariant of this process is that all transitions of any acceptance witness are preserved. Finally, A ′ has an accepting run if and only if Q Dmax contains the initial state. ◭

Emptiness of nonzero automata is in np ∩ co-np

In this section we show how to decide the emptiness of nonzero automata. The main ingredient are jumping games. Call a run {F 1 , F >0 }-accepting if it satisfies the almost-surely and the nonzero acceptance condition, but it does not necessarily satisfy the surely accepting condition, and the root may not be labelled by the initial state either.

The jumping game.

For a run ρ, define its profile Π to be following set of state pairs: Π = {(q, m) : some non-root node in ρ has state q and m is the maximal state of its strict ancestors} .

The jumping game is a parity game played by two players, Automaton and Pathfinder. Positions of Automaton are states of the automaton and positions of Pathfinder are profiles of {F 1 , F >0 }-accepting runs. The game is an edge-labelled parity game, i.e. the priorities are written on the edges. The edges originating in Automaton positions are of the form q q → Π such that Π is the profile of some {F 1 , F >0 }-accepting run with root state q.

The edges originating in Pathfinder positions are of the form Π m → q such that (q, m) ∈ Π.

We say that Automaton wins the jumping game if he has a winning strategy from the position which is the initial state of the automaton. If the play ever reaches a dead-end, i.e. a state which is not the root of any {F 1 , F >0 }-accepting run, then the game is over and Automaton loses. Otherwise Automaton wins iff the limsup of the states is in F ∀ . Lemmas 17 and 18 below establish that nonemptiness of a nonzero automaton is equivalent to Automaton winning the jumping game, and this can be decided in np.

ρ accepting m 1 q 1 m 2 q 2 m 3 lim sup ∈ F ∀ q 0 ρ q0 d q0 P ≥ 1 2 lim sup ∈ F 1 q 1 q 2 q 3 d q0 d q1 d q3 d q2 lim sup ∈ F ∀ Figure 1
The left picture illustrates how an accepting run is turned into a winning strategy for Automaton in the jumping game, the two other pictures illustrate the converse transformation.

◮ Lemma 17. The automaton is nonempty if and only if Automaton wins the jumping game.

Proof. The proof transforms an accepting run ρ of the nonzero automaton into a winning strategy σ of Automaton, and back, this is illustrated by Fig. 1.

Assume first that the nonzero automaton has an accepting run ρ. Automaton can win the jumping game by playing profiles of runs obtained as subtrees of ρ rooted at deeper and deeper depths. For a start, Automaton plays the profile Π 0 of ρ. Then Pathfinder chooses some pair (q 1 , m 1 ) ∈ Π 0 , by definition of profiles this corresponds to some non-root node v 1 of ρ labelled by q 1 , m 1 is the maximal state of the strict ancestors of v 1 . At each step n > 0, Pathfinder chooses a pair (q n , m n ) ∈ Π n corresponding to some node v n+1 whose v n is a strict ancestor, then Automaton plays the profile Π n+1 of the subtree ρ n rooted in v n . Since ρ is accepting then a fortiori ρ n is {F 1 , F >0 }-accepting. The nodes v 1 , v 2 , . . . and their ancestors form a branch of ρ, whose limsup is in F ∀ because ρ is surely accepting. This limsup is equal to lim sup n m n thus Automaton wins the play.

Conversely, we use a positional winning strategy of Automaton to build an accepting run of the nonzero automaton. Denote W the set of states winning for Automaton. With every state q in W we associate the profile Π q chosen by the positional winning strategy of Automaton and a {F 1 , F >0 }-accepting run ρ q with profile Π q .

We show the existence of a leaf-free subtree d q of ρ q such that: a) the set of branches of d q has probability ≥ 1 2 , b) every branch of d q has limsup in F 1 , c) for every node v of d q with state in F >0 , the set of branches of d q which visit v and visit only F >0 -labelled nodes below v has nonzero probability.

Since ρ q is almost-surely accepting, then according to Lemma 1, there is a subtree d q of ρ q whose set of branches has probability ≥ 1 2 and all of them have limsup in F 1 (while in the C V I T 2 0 1 6

23:12

Emptiness of zero automata is decidable run ρ q there may be a non-empty set of branches with limsup in F ∀ \ F 1 , with probability zero). Since we are only interested in branches of d q , we can assume that d q is leaf-free. This guarantees properties a) and b) but not c). For every node v, define L v the set of branches that visit v, have limsup in F 1 and visit only F >0 -labelled nodes below v. Since ρ q is {F 1 , F >0 }-accepting, for every node v of ρ q with state in F >0 , L v has nonzero probability and according to Lemma 1 again, there exists a leaf-free subtree d ′ v whose every branch belongs to L v . We extend the definition domain of d q with d ′ v . This preserves properties a) and b) (because d ′ v itself has property b)) and guarantees property c). Now we combine together the partial runs (d q ) q∈W in order to get an infinite graph. Since d q is leaf-free, every node can have either both children in d q or only one child in d q .

In case one child is missing, we plug instead the partial run d r , where r is the state of the missing child in ρ. This is well-defined because r ∈ W : in a parity game, all states visited when playing a wining strategy are winning, and after Automaton plays the profile Π q the next state of the game maybe any state appearing in ρ q , including r.

The unravelling of this infinite graph, starting from the initial state, is an accepting run of the automaton. Each time a branch enters a subtree d q , there is probability ≥ 1 2 to stay in d q forever. Thus almost every branch of the unravelling eventually stays in one of the subtrees (d q ) q∈W , thus has limsup in F 1 according to property b). As a consequence the unravelling is almost-surely accepting.

Still, with probability 0, some branches switch infinitely often from a subtree to another. Such a branch enters the n-th subtree d n in its root state q n , follow a path in d n with maximal state m n+1 and exits d n to enter d n+1 in state q n+1 . Since d n is a subtree of ρ n , then (q n+1 , m n+1 ) is in the profile Π qn and q

0 q0 → Π q0 m1 → q 1 → Π q1 m2
. . . is a play consistent with the winning strategy of Automaton. Since the strategy of Automaton is winning then lim sup n m n+1 ∈ F ∀ . Hence the unravelling is surely accepting.

Moreover the unravelling is nonzero accepting as well according to c). ◭ ◮ Lemma 18. Deciding whether Automaton wins the jumping game is in np ∩ co-np.

Proof. The jumping game is a parity game thus the winner of the jumping game can be found by guessing a positional strategy for either Automaton or Pathfinder and checking that this strategy is winning. However, since there are exponentially many profiles, this algorithm is in nexptime ∩ co-nexptime rather than in np ∩ co-np.

To overcome this difficulty, we use winning witnesses which are condensed versions of winning positional strategies of Automaton and Pathfinder. A winning witness is a pair (W, s) with W ⊆ Q and s :

W → 2 W ×W .
Under extra-conditions, some of these witnesses are proofs that Automaton or Pathfinder is the winner of the jumping game. A sequence m 0 , m 1 , . . . ∈ W * is generated by (W, s) if there exists q 0 , q 1 , . . . ∈ W * such that ∀n, (q n+1 , m n+1 ) ∈ σ(q n ). For every state q, denote R q the set of profiles of {F 1 , F >0 }-accepting runs with root state q. Then (W, s) is a winning witness for Automaton if: (α) Every sequence generated by (W, s) has its limsup in F ∀ and ∀q ∈ W, s(q) = ∅. (β) For every state q ∈ W there exists a profile Π ∈ R q such that Π ⊆ s(q). And (W, t) is a winning witness for Pathfinder if: (γ) No sequence generated by (W, t) has its lim sup in F ∀ . (δ) For every state q ∈ W and every profile Π ∈ R q , t(q) ∩ Π = ∅. ◮ Lemma 19. Let (W A , W P ) be the partition of Q between states winning for Automaton or Pathfinder in the jumping game. Then there exists winning witnesses (W A , s) and (W P , t) for Automaton and Pathfinder.

Proof. We start with the direct implication. In a parity game, a play consistent with a winning strategy never exits the set of winning vertices, thus Automaton and Pathfinder have positional winning strategies σ : W A → 2 WA×WA and τ : 2 WP ×WP → W P . Then (W A , σ) is a winning witness for Automaton: property (α) holds because σ is winning and property (β) holds because, by definition of the jumping game, ∀q ∈ W A , σ(q) ∈ R q . The winning witness (W P , t) for Pathfinder is defined by

t(q) = {(q ′ , m) | ∃Π ∈ R q , Π m → q ′ is consistent with τ } .
Then (W P , t) is a winning witness for Pathfinder: property (γ) holds because τ is winning and property (δ) holds by definition of t.

We show the converse implication. Let (W A , s) be a winning witness for Automaton. Then according to (β), for every q ∈ W A there exists a profile σ(q) ∈ R q such that σ(q) ⊆ s(q). Then σ is a strategy in the jumping game and according to (α) the strategy σ is winning on W A . From a winning witness (W P , t) for Pathfinder we extract a positional strategy τ winning on W P . Let q ∈ W P and Π a profile in R q . According to (δ) there exists (q, m) ∈ Π ∩ t(q), and τ plays the move Π m → q . Then τ is winning according to (γ). ◭

Now we show how to check in polynomial time whether a pair (W, s) is a winning witness for Automaton or Pathfinder. Checking properties (α) or (γ) consists in solving a one-player parity game which can be done in polynomial time.

To check properties (β) or (δ), we modify the automaton to store in its state space the maximal state of the strict ancestors of the current node. The new state space is Q×({⊥}∪Q) and for every m ∈ {⊥} ∪ Q, every transition q → a (q 0 , q 1 ) in the original automaton gives rise to a transition (q, m) → a ((q 0 , m ′ ), (q 1 , m ′ )) in the modified automaton with m ′ = q if m = ⊥ and m ′ = max{m, q} otherwise. This extra component has no incidence on the acceptance condition. This transformation guarantees that for every state q ∈ Q and every subset Π ⊆ Q × Q, (⋆) Π ∈ R q if and only if the modified automaton has a {F 1 , F >0 }-accepting run ρ with root state (q, ⊥) and Π is the set of states appearing on non-root nodes of ρ. According to (⋆), property (β) is equivalent to checking that for every q ∈ W , the modified automaton restricted to states in {(q, ⊥)} ∪ s(q) has a {F 1 , F >0 }-accepting run, which can be done in polynomial time according to Theorem 10.

And according to (⋆), property (δ) is equivalent to checking that for every q ∈ W , the modified automaton restricted to states in {(q, ⊥)} ∪Q × Q \ s(q) has no {F 1 , F >0 }-accepting run, which can be done in polynomial time according to Theorem 10. ◭

Example: the everywhere positive language

A tree t on the alphabet {a, b} is everywhere positive if for every node v,

1.
there is positive probability to see only the letter t(v) below v, 2. there is positive probability to see finitely many times the letter t(v) below v.

This language is non-empty and contains no regular tree. The language of everywhere positive trees with root state a is recognized by a nonzero automaton with six states

{s b < s a < n b < n a < f b < f a } .
On a node labelled by letter a, the automaton can perform a transition from any of the three states {s b , n b , f a }, meaning intuitively "searching for b", "not searching for b" and "just C V I T 2 0 1 6

23:14

Emptiness of zero automata is decidable found a". From these states the automaton can choose any pair of successor states which intersects {s b , f b }. Transitions on letter b are symmetrical. The acceptance condition is:

F ∀ = {n a , n b , f a , f b } F 1 = F ∀ F >0 = {na, sa, nb, sb} .
Due to space constraints, we can not provide a full description of the jumping game (see the appendix for more details). Automaton can win by playing only the moves s a /n a → {(f a , f a ), (n b , f a ), (s b , f a ), (n a , n a ), (s a , n a )} and f a → {(n b , f a ), (s b , f a )} and their symmetric counterparts from states {s b , n b , f b }. This forces Pathfinder to take only edges labelled by the states {f a , n a , f b , n b }. These states dominate the states {s a , s b } thus the limsup of the corresponding plays is in F ∀ and this is a winning strategy for Automaton.

Conclusion

We have shown that the emptiness problem for zero and nonzero automata is decidable and in np ∩ co-np. As a consequence, the satisfiability for the logic MSO + zero from [START_REF] Bojańczyk | Thin mso with a probabilistic path quantifier[END_REF] is decidable (in non-elementary time), when zero is the unary predicate that checks a set of branches has probability 0. As shown by Stockmeyer, the satisfiability problem for first-order logic on finite words cannot be solved in elementary time. Therefore any translation from a logic stronger than first-order logic on finite words (such as tmso+zero on infinite trees) to an automaton model with elementary emptiness (such as nonzero automata) is necessarily nonelementary. This does not make the relatively low np ∩ co-np complexity of nonzero automata any less interesting. One can imagine other logics than TMSO+zero, either less expressive or maybe even equally expressive but less succint, which will have a relatively low complexity by virtue of a translation into nonzero automata. One natural direction is the study of temporal logics. state then by design the automaton follows in either direction a path seed-consistent in r as long as it does not enter a subtree-guessing state (r(w), r(w), * ). Since there is no pathfinding state in G ∀ , for sure the automaton eventually enters such a state, otherwise d would not be accepting. If d(v) is a normal state then according to the transition table either the left or right child w ′ ∈ {v0, v1} of v is in the path-finding state (r(w ′ ), r(v)) or the subtreeguessing state (r(w ′ ), r(w ′ ), * ). In both cases r(w ′ ) ≤ r(v). In the subtree-guessing case we set w = w ′ and we are done. In the pathfinding case, from w ′ the automaton follows a path seed-consistent in r until it eventually enters the subtree-guessing state (r(w), r(w), * ). By design of the transition table all states on the path from w ′ to w are ≤ r(v) thus the path from v to w is seed-consistent in r.

Since (r(w), r(w), * ) ∈ G >0 , the nonzero condition ensures that there is nonzero probability to continue the run r below w in the set of states G >0 . According to the transition table, in this case the states below w are labelled by {q ∈ Q | q ≤ r(w)} × {r(w)} × { * }. Since d is almost-surely accepting then by definition of G 1 , almost-surely the limsup of such a path is (r(w), r(w), * ). Since r(w) ∈ F >0 then the nonzero condition holds in v, with witness w. ◭

Extended example: the everywhere positive language

A tree t on the alphabet {a, b} is everywhere positive if for every node v, 1. there is positive probability to see only the letter t(v) below v, 2. there is positive probability to see finitely many times the letter t(v) below v.

This language is non-empty and contains no regular tree. The language of everywhere positive trees with root state a is recognized by a nonzero automaton with six states

{s b < s a < n b < n a < f b < f a } .
On a node labelled by letter a, the automaton can perform a transition from any of the three states {s b , n b , f a }, meaning intuitively "searching for b", "not searching for b" and "just found a". From these states the automaton can choose any pair of successor states which intersects {s b , f b }. Transitions on letter b are symmetrical. The acceptance condition is:

F ∀ = {n a , n b , f a , f b } F 1 = F ∀ F >0 = {na, sa, nb, sb} .
We do not provide a full description of the jumping game but we provide a few examples of moves available to player Automaton, as well as a positional winning strategy for player Automaton.

Among the simplest moves of Automaton in the jumping game are the two moves

n b → {(n b , n b )(s b , n b )} s b → {(n b , n b )(s b , n b )} .
These moves are legal because they are the profiles of the following {F 1 , F >0 }-accepting runs. Both runs are on the tree whose all nodes have letter a and everywhere in the tree the automaton applies the same two transitions

23:18

Emptiness of zero automata is decidable limsup s b , which is neither in F ∀ nor in F 1 . But such branches happen with probability zero: almost-every branch makes infinitely many turns left and right and has limsup n b , thus the run is almost-surely accepting: This run is nonzero-accepting as well because every node labelled by F >0 has all its descendants labelled by F >0 . Yet legal, these two moves are not good options for Automaton in the jumping game because then Pathfinder can generate the play Automaton should use more elaborate moves in order to win the jumping game, in particular the three moves

s b s b → {(n b , n b )(s b , n b )} n b → s b s b → {(n b , n b )(s b , n b )} s b → s b s b → . . .
s a /n a → {(f a , f a ), (n b , f a ), (s b , f a ), (n a , n a ), (s a , n a )} ( 1
)
f a → {(n b , f a ), (s b , f a )} (2)
are interesting. Before explaining which these are legal moves, remark that these three moves and their symmetric counterparts from states {s b , n b , f b } ensure the victory to Automaton, because they force Pathfinder to take edges labelled by the states {f a , n a , f b , n b }. These four states dominate the states {s a , s b } and belong to F ∀ thus the limsup of the corresponding plays are in F ∀ , which ensures a win to Automaton. We show that (1) and ( 2) are legal moves for Automaton in the jumping game, by providing positional runs of the extended automaton which generate the profiles {(n b , f a ), (s b , f a )} and {(f a , f a ), (n b , f a ), (s b , f a ), (n a , n a ), (s a , n a )}.

We start with a brief description of the extended automaton. To save space, we write s * for the pair {s a , s b } and use a similar convention for n * and f * as well. With this convention, the states are {s * , n * , f * } × {⊥, s * , n * , f * } .

On the first component, the transitions of the extended automaton are identical to the transitions of the original automaton. The second component is used to store the largest state seen so far. It is initialized to ⊥ and then updated with the maximum of itself and the origin state of the transition.

We give three examples of transitions of the extended automaton The automaton starts the computation looking for an a and keeps looking for an a on the left direction:

(s a , ⊥) → b (s a , s a )(n a , s a ) .

The automaton is not looking for an a but it finds an a in the left child and keeps looking for an a in the right direction:

(n a , s a ) → b (f a , n a )(s a , n a ) .

The automaton has already found b in the past, it is right now looking for an a, and finds one a in both direction:

(s a , f b ) → b (f a , f b )(f a , f b ) .
This last transition is a killer for the nonzero condition, because s a ∈ F >0 but f a ∈ F >0 . Using this transition falsifies the condition "there is positive probability to see only the letter b below v" is not satisfied. Actually this transition could be removed from the set of transitions without changing the set of accepting runs.

To prove that the move f a → {(n b , f a ), (s b , f a )} is valid, we consider the run on a tree whose all nodes are labelled by a. The extended automaton first find an a in the root, in state (f a , ⊥) and then looks hopelessly for a b in the right direction using the transitions (f a , ⊥) → a (n b , f a )(s b , f a ) (nb/s b , f a ) → a (n b , f a )(s b , f a ) . This run is almost-surely accepting because every branch which takes infinitely many turns left has limsup (n b , f a ), and this is almost-every branch. This run is nonzero-accepting because every node labelled by F >0 has all its descendants labelled by F >0 .

To prove that the move s a → {(f a , f a ), (n b , f a ), (s b , f a ), (n a , n a ), (s a , n a )} is legal, consider a tree whose root is labelled by b, all the nodes in the left subtree are labelled by b as well while all the nodes in the left subtree are labelled by a. The extended automaton starts on state (s a , ⊥) in the root. In the right subtree the automaton finds b on the right child of the root (i.e. node 1) and then looks hopelessly for a in the right direction using transitions n a /s a → a (n a , s a ) (dual to the previous case f a → {(n b , f a ), (s b , f a )}). In the left subtree the automaton looks hopelessly for b in the right direction using transitions This run is almost-surely accepting for the same reasons than in the previous case. It is nonzero accepting because from the root node, whose state (s a , ⊥) is in F >0 there is probability 1 2 to continue in the right subtree where all states are in F >0 . And every nonroot node labelled by F >0 has all its descendants labelled by F >0 .

The positional run for the move n a → {(f a , f a ), (n b , f a ), (s b , f a ), (n a , n a ), (s a , n a )} is almost the same than for the move s a → {(f a , f a ), (n b , f a ), (s b , f a ), (n a , n a ), (s a , n a )} except the root has state (n a , ⊥). The transitions of this positional run are

◮ Lemma 7 .◮ Lemma 8 .

 78 Let d : {0, 1} * → R be an accepting run of the nonzero automaton. Then its projection r = Π 1 (d) on the first component is an accepting run of the zero automaton. If the zero automaton has an accepting run r : {0, 1} * → Q then the nonzero automaton has an accepting run d : {0, 1} * → R such that r = Π 1 (d).

  Lemma 15. Let D be an end-component of the run. Then the transition graph of D has no dead-end, is strongly connected and its maximal state is in F 1 . Proof. Denote G D the transition graph of D, with states Q D . Since D is an end-component then B D has non-zero probability, and since almost every branch is even then B D contains at least one even branch b. The set of states appearing infinitely often on b is exactly Q D . By removing a prefix long enough of b so that only states in Q D occur on the remaining suffix then one obtains a path in G D which visits every state in Q D infinitely often. Thus G D has no dead-end and is strongly connected. Moreover every even branch in B D has limsup max Q D and since the run is almost-surely accepting then max Q D ∈ F 1 .◭

  n b → b (n b , s b ) and s b → b (n b , s b ). In other words, the automaton always looks for a letter b in the right direction (state s b ), and does not look for b in the left direction (state n b ). Since the tree has no b then the quest for a letter b is hopeless, and on are branches of the run that ultimately always turn right (i.e. branches in {0, 1} * 1 ω ), the automaton ultimately stays in state s b and the branch has C V I T 2 0 1 6

  which has limsup n b = max{s b , n b } and is losing for Automaton since n b ∈ F ∀ .

  n b /s b → b (n b , s b ). The transitions of this positional run are (s a , ⊥) → a (f a , s a )(n a , s a ) (used once in the root) (n a , s a ) → a (n a , n a )(s a , n a ) (used once in the right subtree) (n a /s a , n a ) → a (n a , n a )(s a , n a ) (used ∞ often in the right subtree) (f a , s a ) → a (n b , f a )(s b , f a ) (used once in the left subtree) (n b /s b , f a ) → a (n b , f a )(s b , f a ) (used ∞ often in the left subtree) .

(

  n a , ⊥) → a (f a , n a )(n a , n a ) (used once in the root) (f a , n a ) → a (n b , f a )(s b , f a ) (used once in the left subtree) (n b /s b , f a ) → a (n b , f a )(s b , f a ) (used ∞ often in the left subtree) (n a /s a , n a ) → a (n a , n a )(s a , n a ) (used ∞ often in the right subtree) .It is {F 1 , F >0 }-accepting for the same reasons than in the previous case.C V I T 2 0 1 6

Daniel Lehmann and Saharon Shelah. Reasoning with time and chance. Information and Control, 53(3):165-1983, 1982.

Acknowledgments

We thank Paulin Fournier, Henryk Michalewski and Matteo Mio for helpful discussions.

The research of M. Bojańczyk is supported by the ERC grant LIPA under the Horizon 2020 framework. H. Gimbert and E. Kelmendi are supported by the French ANR project "Stoch-MC" and "LaBEX CPU" of Université de Bordeaux.

Appendix

Proof of Lemma 6

Proof. Clearly every strongly zero accepting run is also zero accepting.

Conversely, assume a run r is zero accepting, then we show it is strongly zero accepting. Let v be a node labelled by a seed state. Among all descendant nodes z of v, including v itself, such that the path from v to z is seed-consistent and z is labelled by a seed state, choose any z such that the seed state labelling z is minimal.

For every node w let Z w denote the set of branches which visit w and afterwards see only states ≤ r(w) and have limsup r(w).

We first show that there exists a strict descendant w of z such that a) r(w) ∈ F >0 , b) the path from z to w is labelled by states ≤ r(z) and c) Z w has nonzero probability. Since r is zero accepting and z is labelled by a seed state, there is at least one descendant node w ′ of z, labelled by a state in F >0 , such that the path from z to w ′ is labelled by states ≤ r(z) and Z w ′ has nonzero probability. If w ′ is a strict descendant of z then we set w = w ′ . Otherwise we choose w as a strict descendant of w ′ , as follows. Denote W the set of strict descendants of w ′ which are labelled by r(w ′ ) and the path from w ′ to w is labelled by states ≤ r(z). Then Z w ′ = w∈W Z w thus by σ-additivity there exists a strict descendant w of w ′ such that Z w also has non-zero probability.

To establish that the strongly zero accepting condition is satisfied for v, we choose a witness w satisfying properties a) b) and c) and we prove two other properties of w: d) the path from v to w is seed-consistent, e) the only seed state that may be visited below w by a branch in Z w is r(w) itself.

Property d) holds because both paths from v to z and from z to w are seed-consistent and the concatenation of two seed-consistent pathes on a Q seed -labelled node is itself a seedconsistent path. The path from v to z is seed-consistent by choice of z. By hypothesis the path from z to w is labelled by states ≤ r(z) and by minimality of r(z) it does not meet any other seed state than r(z) thus it is seed consistent.

Property e) holds for a similar reason: if a branch in Z w visit a descendant z ′ of w such that r(z ′ ) ∈ Q seed then by definition of Z w , r(z ′ ) ≤ r(w). Since r(w) ≤ r(z), the path from z to z ′ is labelled by states ≤ r(z) and the minimality of r(z) it implies r(z) ≤ r(z ′ ) thus finally r(z ′ ) = r(w) = r(z). ◭

Proof of Lemma 7

Proof. By hypothesis Π 1 : (R, ) → (Q, ≤) is monotonic, thus if b is a branch of the infinite binary tree then its limsup in r is the projection of its limsup in d.

Since F >0 ⊆ F 1 ⊆ F ∀ then the projection of G 1 is F 1 and the projection of G ∀ is F ∀ thus r is both almost-surely and surely accepting.

We show that r is zero accepting. Let v a node such that r(v) is a seed state. For a start, we show that there is a node w below v such that the path from v to w is seed-consistent in r (thus in particular r(w) ≤ r(v)) and d(w) is the subtree-guessing state (r(w), r(w), * ). There are three cases, depending whether d(v) is a subtree-guessing, pathfinding or normal state. If d(v) is a subtree guessing state then according to the definition of R, since r(v) ∈ Q seed then d(v) = (r(v), r(v), * ) and we set w = v. If d(v) is a path-finding


M Montassier
email: montassier@lirmm.fr

P Ochem
email: ochem@lirmm.fr

Near-colorings: non-colorable graphs and NP-completeness

Keywords:

A graph G is (d 1 , . . . , d l )-colorable if the vertex set of G can be partitioned into subsets V 1 , . . . , V l such that the graph G[V i ] induced by the vertices of V i has maximum degree at most d i for all 1 i l. In this paper, we focus on complexity aspects of such colorings when l = 2, 3. More precisely, we prove that, for any fixed integers k, j, g with (k, j) = (0, 0) and g 3, either every planar graph with girth at least g is (k, j)-colorable or it is NP-complete to determine whether a planar graph with girth at least g is (k, j)-colorable. Also, for every fixed integer k, it is NP-complete to determine whether a planar graph that is either (0, 0, 0)-colorable or non-(k, k, 1)-colorable is (0, 0, 0)-colorable. Additionally, we exhibit non-(3, 1)colorable planar graphs with girth 5 and non-(2, 0)-colorable planar graphs with girth 7.

Introduction

A graph G is (d 1 , . . . , d k )-colorable if the vertex set of G can be partitioned into subsets V 1 , . . . , V k such that the graph G[V i ] induced by the vertices of V i has maximum degree at most d i for all 1 i k. This notion generalizes those of proper k-coloring (when

d 1 = • • • = d k = 0) and d-improper k-coloring (when d 1 = • • • = d k = d 1).
Planar graphs are known to be (0, 0, 0, 0)-colorable (Appel and Haken [START_REF] Appel | Every planar map is four colorable[END_REF][START_REF] Appel | Every planar map is four colorable[END_REF]) and (2, 2, 2)-colorable (Cowen, Cowen, and Woodall [START_REF] Cowen | Defective colorings of graphs in surfaces: partitions into subgraphs of bounded valency[END_REF]). The (2, 2, 2)-colorability is optimal (for any integer k, there exist non-(k, k, 1)-colorable planar graphs) and holds in the choosability case (Eaton and Hull [15] or Škrekovski [START_REF] Škrekovski | List improper coloring of planar graphs[END_REF]). Improper colorings have then been considered for planar graphs with large girth or graphs with low maximum average degree. We recall that the girth of a graph G, denoted by g(G), is the length of a shortest cycle in G, and the maximum average degree of a graph G, denoted by mad(G), is the maximum of the average degrees of all subgraphs of G, i.e. mad(G) = max {2|E(H)|/|V (H)| , H ⊆ G}.

(1, 0)-coloring. Glebov and Zambalaeva [START_REF] Glebov | Path partitions of planar graphs[END_REF] proved that every planar graph with girth at least 16 is (1, 0)-colorable. This was then strengthened by Borodin and Ivanova [START_REF] Borodin | Near proper 2-coloring the vertices of sparse graphs[END_REF] who proved that every graph G with mad(G) < 7 3 is (1, 0)-colorable. This implies that every planar graph G with girth at least 14 is (1, 0)-colorable. Borodin and Kostochka [START_REF] Borodin | Vertex partitions of sparse graphs into an independent vertex set and subgraph of maximum degree at most one[END_REF] then proved that every graph G with mad(G) [START_REF] Choi | Planar graphs with girth at least 5 are (3,5)-colorable[END_REF] 5 is (1, 0)-colorable. In particular, it follows that every planar graph with girth at least 12 is (1, 0)-colorable. On the other hand, they constructed graphs G with mad(G) arbitrarily close (from above) to 12 5 that are not (1, 0)-colorable; hence their upper bound on the maximum average degree is best possible. The last result was strengthened for triangle-free graphs: Kim, Kostochka, and Zhu [START_REF] Kim | Improper coloring of sparse graphs with a given girth, I: (0,1)-colorings of triangle-free graphs[END_REF] proved that triangle-free graphs G satisfying 11|V (G)| -9|E(G)| -4 are (1, 0)-colorable. This implies that planar graphs with girth at least 11 are (1, 0)-colorable. On the other hand, Esperet, Montassier, Ochem, and Pinlou [START_REF] Esperet | A complexity dichotomy for the coloring of sparse graphs[END_REF] proved that determining whether a planar graph with girth 9 is (1, 0)-colorable is NP-complete. To our knowledge, the question whether all planar graphs with girth at least 10 are (1, 0)-colorable is still open.

(k, 0)-coloring with k 2. Borodin, Ivanova, Montassier, Ochem, and Raspaud [START_REF] Borodin | Vertex decompositions of sparse graphs into an edgeless subgraph and a subgraph of maximum degree at most k[END_REF] proved that every graph G with mad(G) < 3k+4 k+2 is (k, 0)-colorable. The proof in [START_REF] Borodin | Vertex decompositions of sparse graphs into an edgeless subgraph and a subgraph of maximum degree at most k[END_REF] extends the one in [START_REF] Borodin | Near proper 2-coloring the vertices of sparse graphs[END_REF] but does not work for k = 1. Moreover, they exhibited a non-(k, 0)-colorable planar graph with girth 6. Finally, Borodin and Kostochka [START_REF] Borodin | Defective 2-coloring of sparse graphs[END_REF] proved that for k 2, every graph G with mad(G) 3k+2 k+1 is (k, 0)-colorable. This result is tight in terms of maximum average degree.

(k, 1)-coloring. Recently, Borodin, Kostochka, and Yancey [START_REF] Borodin | On 1-improper 2-coloring of sparse graphs[END_REF] proved that every graph with mad(G) 14 5 is (1, 1)-colorable, and the restriction on mad(G) is sharp. In [START_REF] Borodin | k, 1)-coloring of sparse graphs[END_REF], it is proven that every graph G with mad(G) < 10k+22 3k+9 is (k, 1)-colorable for k 2.

(k, j)-coloring. A first step was made by Havet and Sereni [START_REF] Havet | Improper choosability of graphs and maximum average degree[END_REF] who showed that, for every k 0, every graph G with mad(G)

< 4k+4 k+2 is (k, k)-colorable (in fact (k, k)-choosable).
More generally, they studied k-improper l-choosability and proved that every graph G with mad(G) < l+ lk l+k (l 2, k 0) is k-improper l-choosable; this implies that such graphs are (k, . . . , k)-colorable (where the number of partite sets is l). Borodin, Ivanova, Montassier, and Raspaud [START_REF] Borodin | k, j)-coloring of sparse graphs[END_REF] gave some sufficient conditions of (k, j)-colorability depending on the density of the graphs using linear programming. Finally, Borodin and Kostochka [START_REF] Borodin | Defective 2-coloring of sparse graphs[END_REF] solved the problem for a wide range of j and k: let j 0 and k 2j + 2; every graph

G with mad(G) 2(2 -k+2 (j+2)(k+1) ) is (k, j)-colorable.
This result is tight in terms of the maximum average degree and improves some results in [START_REF] Borodin | Vertex decompositions of sparse graphs into an edgeless subgraph and a subgraph of maximum degree at most k[END_REF][START_REF] Borodin | k, 1)-coloring of sparse graphs[END_REF][START_REF] Borodin | k, j)-coloring of sparse graphs[END_REF].

the electronic journal of combinatorics 22(1) (2015), #P1.57

Using the fact that every planar graph G with girth g(G) has mad(G) < 2g(G)/(g(G)-2), the previous results give results for planar graphs. They are summarized in Table 1, which also shows the recent results that planar graphs with girth 5 are (5, 3)-colorable (Choi and Raspaud [START_REF] Choi | Planar graphs with girth at least 5 are (3,5)-colorable[END_REF]) and (10, 1)-colorable (Choi, Choi, Jeong, and Suh [START_REF] Choi | 1, k)-coloring of graphs with girth at least 5 on a surface[END_REF]). (1, 0) [START_REF] Kim | Improper coloring of sparse graphs with a given girth, I: (0,1)-colorings of triangle-free graphs[END_REF] Table 1: The girth and the (k, j)-colorability of planar graphs. The symbol "×" means that there exist non-(k, j)-colorable planar graphs for every k.

girth (k, 0) (k, 1) (k, 2) (k, 3) (k, 4) 3,4 × × × × × 5 × ( 10
From the previous discussion, the following questions are natural:

Question 1.

1. Are planar graphs with girth 10 (1, 0)-colorable?

2. Are planar graphs with girth 7 (3, 0)-colorable?

3. Are planar graphs with girth 6 (1, 1)-colorable?

4. Are planar graphs with girth 5 (4, 1)-colorable?

5. Are planar graphs with girth 5 (2, 2)-colorable?

(d 1 , . . . , d k )-coloring. Finally we would like to mention two studies. Chang, Havet, Montassier, and Raspaud [START_REF] Chang | Steinberg's Conjecture and near-colorings[END_REF] gave some approximation results to Steinberg's Conjecture using (k, j, i)-colorings. Dorbec, Kaiser, Montassier, and Raspaud [START_REF] Dorbec | Limits of near-coloring of sparse graphs[END_REF] studied the particular case of (d 1 , . . . , d k )coloring where the value of each d i (1 i k) is either 0 or some value d, making the link between (d, 0)-coloring [START_REF] Borodin | Defective 2-coloring of sparse graphs[END_REF] and (d, . . . , d)-coloring [START_REF] Havet | Improper choosability of graphs and maximum average degree[END_REF].

The aim of this paper is to provide complexity results on the subject and to obtain non-colorable planar graphs showing that some above-mentioned results are optimal. Claim 2. There exist 2-degenerate planar graphs that are:

1. non-(k, k)-colorable with girth 4, for every k 0, Claim 2.4 shows that the (2, 0)-colorability of planar graphs with girth at least 8 [START_REF] Borodin | Defective 2-coloring of sparse graphs[END_REF] is a tight result. Claim 2.3 has been obtained in [START_REF] Borodin | Vertex decompositions of sparse graphs into an edgeless subgraph and a subgraph of maximum degree at most k[END_REF] and the corresponding graph is depicted in Figure 1. Theorem 3. Let k, j, and g be fixed integers such that (k, j) = (0, 0) and g 3. Either every planar graph with girth at least g is (k, j)-colorable or it is NP-complete to determine whether a planar graph with girth at least g is (k, j)-colorable.

2k + 1 2k + 1 2k + 1 2k + 1
Theorem 4. Let k be a fixed integer. It is NP-complete to determine whether a 3degenerate planar graph that is either (0, 0, 0)-colorable or non-(k, k, 1)-colorable is (0, 0, 0)colorable.

We construct a non-(k, k)-colorable planar graph with girth 4 in Section 2, a non-(3, 1)-colorable planar graph with girth 5 in Section 3, and a non-(2, 0)-colorable planar graph with girth 7 in Section 4. We prove Theorem 3 in Section 5 and we prove Theorem 4 in Section 6.

Notation.

In the following, when we consider a (d 1 , . . . , d k )-coloring of a graph G, we color the vertices of V i with color d i for 1 i k: for example in a (3, 0)-coloring, we will use color 3 to color the vertices of V 1 inducing a subgraph with maximum degree 3 and use color 0 to color the vertices of V 2 inducing a stable set. A vertex is said to be colored i j if it is colored i and has j neighbors colored i, that is, it has degree j in the subgraph induced by its color. A vertex is saturated if it is colored i i , that is, if it has maximum degree in the subgraph induced by its color. A cycle (resp. face

) of length k is called a k-cycle (resp. k-face). A k-vertex (resp. k --vertex, k + -vertex) is a vertex of degree k (resp. at most k, at least k).
The minimum degree of a graph G is denoted by δ(G).

A non-(k, k)-colorable planar graph with girth 4

For every k 0, we construct a non-(k, k)-colorable planar graph J 4 with girth 4. Let H x,y be a copy of K 2,2k+1 , as depicted in Figure 2. In any (k, k)-coloring of H x,y , the the electronic journal of combinatorics 22(1) (2015), #P1.57 vertices x and y must receive the same color. We obtain J 4 from a vertex u and a star S with center v 0 and k + 1 leaves v 1 , . . . , v k+1 by linking u to every vertex v i with a copy H u,v i of H x,y . The graph J 4 is not (k, k)-colorable: by the property of H x,y , every vertex v i should get the same color as u. This gives a monochromatic S, which is forbidden. Notice that J 4 is a planar graph with girth 4 and is 2-degenerate.

A non-(3, 1)-colorable planar graph with girth 5

We construct a non-(3, 1)-colorable planar graph J 5 with girth 5. Consider the graph H x,y depicted in Figure 3. If x and y are colored 3 but have no neighbor colored 3, then it is

z 1 z 2 z 3 J 5
x y

x y H x,y not possible to extend this partial coloring to H x,y . Now, we construct the graph S z as follows. Let z be a vertex and t 1 t 2 t 3 be a path on three vertices. Take 21 copies H x i ,y j of H x,y with 1 i 7 and 1 j 3. Identify every x i with z and identify every y i with t i . Finally, we obtain J 5 from three copies S z 1 , S z 2 , and S z 3 of S z by adding the edges z 1 z 2 and z 2 z 3 (Figure 3). Notice that J 5 is planar with girth 5 and is 2-degenerate. Let us show that J 5 is not (3, 1)-colorable. In every (3, 1)-coloring of J 5 , the path z 1 z 2 z 3 contains a vertex z colored 3. In the copy of S z corresponding to z, the path t 1 t 2 t 3 contains a vertex t colored 3. Since z (resp. t) has at most 3 neighbors colored 3, one of the seven copies of H x,y between z and t, does not contain a neighbor of z or t colored 3. This copy of H x,y is not (3, 1)-colorable, and thus J 5 is not (3, 1)-colorable.

A non-(2, 0)-colorable planar graph with girth 7

We construct of a non-(2, 0)-colorable planar graph J 7 with girth 7. Consider the graphs T x,y,z and S in Figure 4. If the vertices x, y, and z of T x,y,z are colored 2 and have no neighbor colored 2, then w is colored 2 2 . Suppose that the vertices a, b, c, d, e, f, g of S are respectively colored 2, 0, 2, 2, 2, 2, 0, and that a has no neighbor colored 2. Using successively the property of T x,y,z , we have that w 1 , w 2 , and w 3 must be colored 2 2 . It follows that w 4 is colored 0, w 5 is colored 2, and so w 6 is colored 2 2 . Again, by the property of T x,y,z , w 7 must be colored 2 2 . Finally, w 8 must be colored 0 and there is no choice of color for w 9 . Hence, such a coloring of the outer 7-cycle abcdef g cannot be extended.

the electronic journal of combinatorics 22(1) (2015), #P1.57 We link a vertex z to every vertex of a 7-cycle v 1 . . . v 7 with a path of three edges. Then we embed the graph S in every 7-face F i (1 i 7) incident to z by identifying the outer 7-cycle of S with the 7-cycle of F i such that a is identified to z. Finally, the graph J 7 depicted on the right of Figure 5 is obtained from two adjacent vertices u and v and six copies H z 1 , . . . , H z 6 of H z by identifying z 1 , z 2 , z 3 with u and z 4 , z 5 , z 6 with v. Notice that J 7 is planar with has girth 7. Let us prove that J 7 is not (2, 0)-colorable.

F 1 F 2 F 3 F 4 F 5 F 6 F 7 H z z z v 1 v 2 v 3 v 4 v 5 v 6 v 7 J 7
• We assume that u is colored 2 since u and v cannot be both colored 0.

• In one of the three copies of H z attached to u, say H z 1 , u has no neighbor colored 2.

• Since a 7-cycle is not 2-colorable, the 7-cycle v 1 . . . v 7 of H z 1 contains a monochromatic edge colored 2, say v 1 v 2 .

• The coloring of the face F 2 cannot be extended to the copy of S embedded in F 2 .

NP-completeness of (k, j)-colorings

Let g k,j be the largest integer g such that there exists a planar graph with girth g that is not (k, j)-colorable. Because of large odd cycles, g 0,0 is not defined. For (k, j) = (0, 0), we have 4 g k,j 10 by the example in Figure 2 and the result that planar graphs with girth at least 11 are (0, 1)-colorable [START_REF] Kim | Improper coloring of sparse graphs with a given girth, I: (0,1)-colorings of triangle-free graphs[END_REF]. We prove this equivalent form of Theorem 3:

Theorem 5.
Let k and j be fixed integers such that (k, j) = (0, 0). It is NP-complete to determine whether a planar graph with girth g k,j is (k, j)-colorable.

the electronic journal of combinatorics 22(1) (2015), #P1.57

Let us define the partial order . Let n 3 (G) be the number of 3 + -vertices in G. For any two graphs G 1 and G 2 , we have G 1 ≺ G 2 if and only if at least one of the following conditions holds:

• |V (G 1 )| < |V (G 2 )| and n 3 (G 1 ) n 3 (G 2 ). • n 3 (G 1 ) < n 3 (G 2 ).
Note that the partial order is well-defined and is a partial linear extension of the subgraph poset. The following lemma is useful. Lemma 6. Let k and j be fixed integers such that (k, j) = (0, 0). There exists a planar graph G k,j with girth g k,j , minimally non-(k, j)-colorable for the subgraph order, such that δ(G k,j ) = 2.

Proof. We have δ(G k,j ) 2, since a non-(k, j)-colorable graph that is minimal for the subgraph order does not contain a 1 --vertex. Supppose that for some pair (k, j), we construct a 2-degenerate non-(k, j)-colorable planar graph with girth g k,j . Then this graph contains a (not necessarily proper) minimally non-(k, j)-colorable subgraph with minimum degree 2. Thus, we can prove the lemma for the following pairs (k, j) by using Claim 2.

• Pairs (k, j) such that g k,j 4: We actually have g k,j = 4 by Claim 2.1.

• Pairs (k, j) such that g k,j

6: Indeed, a planar graph with girth at least 6 is 2degenerate. In particular, Claim 2.3 shows that g k,0 6, so the lemma is proved for all pairs (k, 0).

• Pairs (k, 1) such that 1 k 3: If g k,j 6, then we are in a previous case. Otherwise, we have g k,j = 5 by Claim 2.2.

The remaining pairs satisfy g k,j = 5. There are two types of remaining pairs (k, j):

• Type 1: k 4 and j = 1.

• Type 2: 2 j k.

Consider a planar graph G with girth 5 that is non-(k, j)-colorable and is minimal for the order . Suppose for contradiction that G does not contain a 2-vertex. Also, suppose that G contains a 3-vertex a adjacent to three 4 --vertices a 1 , a 2 , and a 3 . For colorings of type 1, we can extend to G a coloring of G \ {a} by assigning to a the color of improperty at least 4. For colorings of type 2, we consider the graph G obtained from G \ {a} by adding three 2-vertices b 1 , b 2 , and b 3 adjacent to, respectively, a 2 and a 3 , a 1 and a 3 , a 1 and a 2 . Notice that G G, so G admits a coloring c of type 2. We can extend to G the coloring of G \ {a} induced by c as follows. If a 1 , a 2 , and a 3 have the same color, then we assign to a the other color. Otherwise, we assign to a the color that appears at least twice among the colors of b 1 , b 2 , and b 3 . Now, since G does not contain a 2-vertex nor a the electronic journal of combinatorics 22(1) (2015), #P1.57 3-vertex adjacent to three 4 --vertices, we have mad(G) 10 3 . This can be seen using the discharging procedure such that the initial charge of each vertex is its degree and every 5 + -vertex gives 1 3 to each adjacent 3-vertex. The final charge of a 3-vertex is at least 3 + 1 3 = 10 3 , the final charge of a 4-vertex is 4 > 10 3 , and the final charge of a k-vertex with k 5 is at least kk × 1 3 = 2k 3 10 3 . Now, mad(G) 10 3 contradicts the fact that G is a planar graph with girth 5, and this contradiction shows that G contains a 2-vertex.

We are ready to prove Theorem 5. The case of (1, 0)-coloring is proved in a stronger form which takes into account restrictions on both the girth and the maximum degree of the input planar graph [START_REF] Esperet | A complexity dichotomy for the coloring of sparse graphs[END_REF].

Proof of the case (k, 0), k 2. We consider a graph G k,0 as described in Lemma 6, which contains a path uxv where x is a 2-vertex. By minimality, any (k, 0)-coloring of G k,0 \{x} is such that u and v get distinct saturated colors. Let G be the graph obtained from G k,0 \ {x} by adding three 2-vertices x 1 , x 2 , and x 3 to create the path ux 1 x 2 x 3 v. So any (k, 0)-coloring of G is such that x 2 is colored k 1 . To prove the NP-completeness, we reduce the (k, 0)-coloring problem to the (1, 0)-coloring problem. Let I be a planar graph with girth g 1,0 . For every vertex s of I, add (k -1) copies of G such that the vertex x 2 of each copy is adjacent to s, to obtain the graph I . By construction, I is (k, 0)-colorable if and only if I is (1, 0)-colorable. Moreover, I is planar, and since g k,0 g 1,0 , the girth of I is g k,0 .

Proof of the case (1, 1). By Claim 2.2 and [9], g 1,1 is either 5 or 6. There exist two independent proofs [START_REF] Fiala | Graph subcolorings: complexity and algorithms[END_REF][START_REF] Gimbel | Subcolorings and the subchromatic number of a graph[END_REF] that (1, 1)-coloring is NP-complete for triangle-free planar graphs with maximum degree 4. We use a reduction from that problem to prove that (1, 1)-coloring is NP-complete for planar graphs with girth g 1,1 . We consider a graph G 1,1 as described in Lemma 6, which contains a path uxv where x is a 2-vertex. By minimality, any (1, 1)-coloring of G 1,1 \ {x} is such that u and v get distinct saturated colors. Let G be the graph obtained from G 1,1 \ {x} by adding a vertex u adjacent to u and a vertex v adjacent to v. So any (1, 1)-coloring of G is such that u and v get distinct colors and u (resp. v ) has a color distinct from the color of its (unique) neighbor. We construct the graph E a,b from two vertices a and b and two copies of G such that a is adjacent to the vertices u of both copies of G and b is adjacent to the vertices v of both copies of G. There exists a (1, 1)-coloring of E a,b such that a and b have distinct colors and neither a nor b is saturated. There exists a (1, 1)-coloring of E a,b such that a and b have the same color. Moreover, in every (1, 1)-coloring of E a,b such that a and b have the same color, both a and b are saturated.

The reduction is as follows. Let I be a planar graph. For every edge (p, q) of I, replace (p, q) by a copy of E a,b such that a is identified with p and b is identified with q, to obtain the graph I . By the properties of E a,b , I is (1, 1)-colorable if and only if I is (1, 1)-colorable. Moreover, I is planar with girth g 1,1 .

Proof of the case (k, j). We consider a graph G k,j as described in Lemma 6, which contains a path uxv where x the electronic journal of combinatorics 22(1) (2015), #P1.57 is a 2-vertex. By minimality, any (k, j)-coloring of G k,j \ {x} is such that u and v get distinct saturated colors. Let G be the graph obtained from G k,j \ {x} by adding a vertex u adjacent to u and a vertex v adjacent to v. So any (k, j)-coloring of G is such that u and v get distinct colors and u (resp. v ) has a color distinct from the color of its (unique) neighbor. Let t = min(k -1, j). To prove the NP-completeness, we reduce the (k, j)-coloring to the (kt, jt)-coloring. Thus the case (k, k) reduces to the case (1, 1) which is NP-complete, and the case (k, j) with j < k reduces to the case (kj, 0) which is NP-complete. The reduction is as follows. Let I be a planar graph with girth g k-t,j-t . For every vertex s of I, add t copies of G such that the vertices u and v of each copy is adjacent to s, to obtain the graph I . By construction, I is (kt, jt)-colorable if and only if I is (k, j)-colorable. Moreover, I is planar, and since g k,j g k-t,j-t , the girth of I is g k,j .

NP-completeness of (k, j, i)-colorings

In this section, we prove Theorem 4 using a reduction from 3-colorability, i.e. (0, 0, 0)colorability, which is NP-complete for planar graphs [START_REF] Garey | Some simplified NP-complete graph problems[END_REF].

Let E be the graph depicted in Fig 6 . The graph E is obtained from 2k -1 copies of E by identifying the edge ab of all copies. Take 4 copies E 1 , E 2 , E 3 , and E 4 of E and consider a triangle T formed by the vertices y 0 , x 0 , x 1 in one copy of E in E 1 . The graph E is obtained by identifying the edge y 0 x 0 (resp. y 0 x 1 , x 0 x 1 ) of T with the edge ab of E 2 (resp. E 3 , E 4 ). The edge ab of E 1 is then said to be the edge ab of E . Lemma 7.

1. E admits a (0, 0, 0)-coloring.

2. E does not admit a (k, k, 1)-coloring such that a and b have a same color of improperty k.

3. E does not admit a (k, k, 1)-coloring such that a and b have the same color.

Proof.

1. The following (0, 0, 0)-coloring c of E is unique up to permutation of colors: c(a) = c(x i ) = 1 for even i, c(b) = c(y i ) = 2 for even i, and c(x i ) = c(y i ) = 3 for odd i. This coloring can be extended into a (0, 0, 0)-coloring of E and E . x 3k+3+t y 3k+3

Figure 6: The graph E. We take t = 0 if k is odd and t = 1 if k is even, so that 3k + 3 + t is even. We thus have that {c(y 0 ), c(x 0 ), c(x 1 )} ⊂ {k 1 , k 2 }. This implies that at least one edge of the triangle T is monochromatic with a color of improperty k. By the previous item, the coloring c cannot be extended to the copy of E attached to that monochromatic edge. This shows that E does not admit a (k, k, 1)-coloring such that a and b have the same color.

For every fixed integer k, we give a polynomial construction that transforms every planar graph G into a planar graph G such that G is (0, 0, 0)-colorable if G is (0, 0, 0)colorable and G is not (k, k, 1)-colorable otherwise. The graph G is obtained from G by identifying every edge of G with the edge ab of a copy of E . If G is (0, 0, 0)-colorable, then this coloring can be extended into a (0, 0, 0)-coloring of G by Lemma 7.1. If G is not (0, 0, 0)-colorable, then every (k, k, 1)-coloring G contains a monochromatic edge uv, and then the copy of E corresponding to uv (and thus G ) does not admit a (k, k, 1)coloring by Lemma 7.3. The instance graph G in the proof that (0, 0, 0)-coloring is NP-complete [START_REF] Garey | Some simplified NP-complete graph problems[END_REF] is 3-degenerate. Then by construction, G is also 3-degenerate.

the electronic journal of combinatorics 22(1) (2015), #P1.57

2 .

 2 non-(3, 1)-colorable with girth 5, 3. non-(k, 0)-colorable with girth 6, the electronic journal of combinatorics 22(1) (2015), #P1.57 4. non-(2, 0)-colorable with girth 7.

Figure 1 :

 1 Figure 1: A non-(k, 0)-colorable planar graph with girth 6 [4].

Figure 2 :

 2 Figure 2: A non-(k, k)-colorable planar graph with girth 4.

Figure 3 :

 3 Figure 3: A non-(3, 1)-colorable planar graph with girth 5.

Figure 4 :

 4 Figure 4: graphs T x,y,z and S.

Figure 5 :

 5 Figure 5: The graphs H z and J 7 .

2. Let k 1 ,

 1 k 2 , and 1 denote the colors in a potential (k, k, 1)-coloring c of E such that c(a) = c(b) = k 1 . By the pigeon-hole principle, one of the 2k -1 copies of E in E , say E * , is such that a and b are the only vertices with color k 1 . So, one of the vertices x 0 , y 0 , and x 3k+3+t in E * must get color k 2 since they cannot all get color 1. We thus have a vertex v 1 ∈ {a, b} colored k 1 and vertex v 2 ∈ {x 0 , y 0 , x 3k+3+t } colored k 2 in E * which both dominate a path on at least 3k + 3 vertices. This path contains no vertex colored k 1 since it is in E * . Moreover, it contains at most k vertices colored the electronic journal of combinatorics 22(1) (2015), #P1.57

k 2 . 3 = k + 1 vertices colored k 2 .

 232 On the other hand, every set of 3 consecutive vertices in this path contains at least one vertex colored k 2 , so it contains at least 3k+3 This contradiction shows that E does not admit a (k, k, 1)-coloring such that a and b have a same color of improperty k.

3 .

 3 By the previous item and by construction of E , if E admits a (k, k, 1)-coloring c such that c(a) = c(b), then c(a) = c(b) = 1.

* This work was partially supported by the ANR grant EGOS 12-JS02-002-01.