Galina Jirásková
email: jiraskov@saske.sk

Tomáš Masopust
email: masopust@math.cas.cz

On Properties and State Complexity of Deterministic State-Partition Automata

Keywords: Regular languages, finite automata, descriptional complexity, projections, state-partition automata

A deterministic automaton accepting a regular language L is a state-partition automaton with respect to a projection P if the state set of the deterministic automaton accepting the projected language P (L), obtained by the standard subset construction, forms a partition of the state set of the automaton. In this paper, we study fundamental properties of state-partition automata. We provide a construction of the minimal state-partition automaton for a regular language and a projection, discuss closure properties of state-partition automata under the standard constructions of deterministic automata for regular operations, and show that almost all of them fail to preserve the property of being a statepartition automaton. Finally, we define the notion of a state-partition complexity, and prove the tight bound on the state-partition complexity of regular languages represented by incomplete deterministic automata.

Introduction

A deterministic finite automaton G accepting a regular language L is a statepartition automaton with respect to a projection P if the state set of the deterministic automaton accepting the projected language P (L), obtained by the standard subset construction [START_REF] Hopcroft | Introduction to automata theory, languages, and computation[END_REF][START_REF] Yu | Regular languages[END_REF], forms a partition of the state set of the automaton G. This means that the projection of a string uniquely specifies the state of the projected automaton. Therefore, all projected strings of a language with the same observation, that is, with the same projections, lead to the same state of the projected automaton. This property immediately implies that the size of the minimal state-partition automaton is not smaller than the size of the minimal deterministic automaton accepting the projected language.

From the practical point of view, state-partition automata are of interest in engineering and computer science, especially in applications where the user, supervisor, or controller has only a partial observation of the whole behavior of a system, which is modeled by a projection. From the theoretical point of view, state-partition automata have found applications as a proof formalism for systems with partial observations. Namely, they have been successfully used to simplify constructions and proofs, and are useful in applications of natural projections to obtain or describe an abstraction of a system. Note that projections are sometimes generalized to so-called causal reporter maps, see [START_REF] Wong | Hierarchical control of discrete-event systems[END_REF][START_REF] Zhong | On the consistency of hierarchical supervision in discrete-event systems[END_REF]. We refer the reader to [START_REF] Cho | On supremal languages of classes of sublanguages that arise in supervisor synthesis problems with partial observation[END_REF][START_REF] Cho | Supremal and maximal sublanguages arising in supervisor synthesis problems with partial observations[END_REF][START_REF] Komenda | Supremal normal sublanguages of large distributed discrete-event systems[END_REF][START_REF] Komenda | Modular control of discrete-event systems with coalgebra[END_REF] for applications of state-partition automata in supervisory control of discrete-event systems. Note that state-partition automata are related to the Schützenberger covering. More specifically, the construction of a state-partition automaton is close to the Schützenberger construct [START_REF] Sakarovitch | A construction on finite automata that has remained hidden[END_REF].

A system represented by a state-partition automaton with respect to a projection that describes an abstraction or a partial observation has a projected automaton that is not larger than the original automaton. This is the most important property from the application point of view. Notice that, up to now, there is only one well-known condition ensuring that a projected automaton is smaller than the original automaton, an observer property, cf. [START_REF] Wong | On the complexity of projections of discrete-event systems[END_REF]. The study of state-partition automata is thus a further step to the understanding and characterization of the class of automata useful for practical applications in, e.g., coordination or hierarchical supervisory control of discrete-event systems [START_REF] Boutin | Hierarchical control with partial observations: Sufficient conditions[END_REF][START_REF] Komenda | Synthesis of controllable and normal sublanguages for discrete-event systems using a coordinator[END_REF][START_REF] Komenda | Supervisory control synthesis of discrete-event systems using a coordination scheme[END_REF][START_REF] Schmidt | Maximally permissive hierarchical control of decentralized discrete event systems[END_REF][START_REF] Schmidt | Nonblocking hierarchical control of decentralized discrete event systems[END_REF].

In this paper, we discuss fundamental properties of state-partition automata. In Section 3, we recall the known result proving that every regular language has a state-partition automaton with respect to a given projection. A procedure to construct this automaton is also known, see [START_REF] Cho | On supremal languages of classes of sublanguages that arise in supervisor synthesis problems with partial observation[END_REF]. We repeat the construction here and use it to obtain the minimal state-partition automaton for a given language and a projection. The last result of this section describes a regular language and two projections with respect to which the language has no state-partition automaton. This negative result indicates that state-partition automata are useful for systems with either a partial observation or abstraction, but not with the combination of both.

Then, in Section 4, we study the closure properties of state-partition automata under the standard constructions of deterministic automata for the operations of complement, union, intersection, concatenation, Kleene star, reversal, cyclic shift, and left and right quotients. We show that almost all of them fail to preserve the property of being a state-partition automaton. Only two of the considered operations preserve this property, namely, the construction of a deterministic automaton for the right quotient of two regular languages, and the construction of a deterministic automaton for the complement of regular languages represented by complete deterministic automata.

Finally, in the last section of this paper, we introduce and study the statepartition complexity of regular languages with respect to a projection, defined as the smallest number of states in any state-partition automaton (with respect to the projection) accepting the language. The first result of this section shows that a language represented by a minimal incomplete deterministic automaton with n states has state-partition complexity at most 3n • 2 n-3 . The second result then proves the tightness of this upper bound using a language defined over a three-letter alphabet and a projection on binary strings.

Preliminaries and Definitions

In this paper, we assume that the reader is familiar with the basic notions and concepts of formal languages and automata theory, and we refer the reader to [START_REF] Hopcroft | Introduction to automata theory, languages, and computation[END_REF][START_REF]Handbook of Formal Languages[END_REF][START_REF] Salomaa | Formal languages[END_REF] for all details and unexplained notions.

For a finite non-empty set Σ, called an alphabet, the set Σ * represents the free monoid generated by Σ. A string over Σ is any element of Σ * , and the unit of Σ * is the empty string denoted by ε. A language over Σ is any subset of Σ * . For a string w in Σ * , let |w| denote the length of w, and for a symbol a in Σ, let |w| a denote the number of occurrences of the symbol a in w. If w = xyz, for strings x, y, z, w in Σ * , then x is a prefix of w, and y is a factor of w.

A deterministic finite automaton (a DFA, for short) is a quintuple G = (Q, Σ, δ, s, F ), where Q is a finite non-empty set of states, Σ is an input alphabet, δ : Q × Σ → Q is a partial transition function, s ∈ Q is the initial (or start) state, and F ⊆ Q is the set of final states. Note that we consider incomplete deterministic finite automata that are also called generators in the literature, cf. [START_REF] Cassandras | Introduction to discrete event systems[END_REF][START_REF] Wonham | Supervisory control of discrete-event systems[END_REF]. That is why we prefer to use G to denote an incomplete deterministic automaton. The transition function can be naturally extended to the domain Q × Σ * by induction. The language accepted by the automaton G is the set of strings L(G) = {w ∈ Σ * | δ(s, w) ∈ F }. A state q of G is called reachable if q = δ(s, w) for a string w in Σ * , and it is called useful, or co-reachable, if δ(q, w) ∈ F for a string w.

A nondeterministic finite automaton (an NFA, for short) is a quintuple N = (Q, Σ, δ, S, F ), where Q, Σ, and F are as in a DFA, S ⊆ Q is the set of initial states, and δ : Q × (Σ ∪ {ε}) → 2 Q is the nondeterministic transition function that can be extended to the domain 2 Q ×Σ * by induction. The language accepted by the NFA N is defined as the set L(N ) = {w ∈ Σ * | δ(S, w) ∩ F = ∅}. Notice that our NFAs may have ε-transitions and multiple initial states. However, ε-transitions and multiple initial states can be eliminated by a standard technique [START_REF] Hopcroft | Introduction to automata theory, languages, and computation[END_REF].

Two automata are equivalent if they accept the same language. Every NFA N = (Q, Σ, δ, S, F ) without ε-transitions can be converted to an equivalent DFA det(N ) = (2 Q , Σ, δ d , s d , F d ) by an algorithm known as the "subset construction" [START_REF] Rabin | Finite automata and their decision problems[END_REF], where we have

δ d (R, a) = δ(R, a) for each R in 2 Q and a in Σ, s d = S, and
F d = {R ∈ 2 Q | R ∩ F = ∅}.
We call the deterministic automaton det(N ) the subset automaton corresponding to the automaton N . Notice that the state set of the subset automaton is the set of all subsets of Q, even though some of them may be unreachable from the initial state s d .

Let Σ be an alphabet and Σ o ⊆ Σ. A homomorphism P from Σ * to Σ * o is called a (natural) projection if it is defined by P (a) = a for each a in Σ o and P (a) = ε for each a in Σ \ Σ o . The inverse image of P is a mapping

P -1 from Σ * o to 2 Σ * defined by P -1 (w) = {u ∈ Σ * | P (u) = w}. Let G = (Q, Σ, δ, s, F
) be a DFA accepting a language L and P be the projection from

Σ * to Σ * o with Σ o ⊆ Σ.
From the DFA G, we construct an NFA N G accepting the language P (L) by replacing all transitions labeled by symbols from Σ \ Σ o with ε-transitions, and by eliminating these ε-transitions. Then the projected automaton for the language P (L) is the deterministic automaton

P (G) = (Q , Σ o , δ , s , F )
that forms the reachable part of the subset automaton det(N G ). Thus, Q is the set of all states of 2 Q reachable from the initial state s . Notice that we do not eliminate states, from which no final state is reachable. This is due to applications in supervisory control, where this problem is known as the problem of nonblockingness [START_REF] Cassandras | Introduction to discrete event systems[END_REF].

A DFA G = (Q, Σ, δ, s, F ) is a state-partition automaton (an SPA, for short) with respect to a projection

P from Σ * to Σ * o with Σ o ⊆ Σ if the states of the projected automaton P (G) = (Q , Σ o , δ , s , F ) are pairwise disjoint as sets.
Note that if all states of G are reachable, then the state set of the projected automaton P (G) defines a partition of the state set of G.

For an automaton A (deterministic or nondeterministic), let sc(A) denote the number of states of the automaton A.

We immediately have the following result.

Lemma 1. Let G be a DFA over an alphabet Σ that has no unreachable states. Let P be a projection from

Σ * to Σ * o with Σ o ⊆ Σ.
If G is a state-partition automaton with respect to P , then sc(P (G)) ≤ sc(G). Now we define a parallel composition of two incomplete deterministic automata, which is basically the intersection of two automata defined over two different alphabets. Therefore, it is first necessary to unify their alphabets by adding the missing symbols.

For two deterministic finite automata

G 1 = (Q 1 , Σ 1 , δ 1 , s 1 , F 1 ) and G 2 = (Q 2 , Σ 2 , δ 2 , s 2 , F 2 ), we define the parallel composition of G 1 and G 2 , denoted by G 1 G 2 , as the reachable part of the DFA (Q 1 × Q 2 , Σ 1 ∪ Σ 2 , δ, (s 1 , s 2 ), F 1 × F 2 ), where δ((p, q), a) =            (δ 1 (p, a), δ 2 (q, a)), if δ 1 (p, a) is defined in G 1 and δ 2 (q, a) is defined in G 2 ; (δ 1 (p, a), q), if δ 1 (p, a) is defined in G 1 and a / ∈ Σ 2 ; (p, δ 2 (q, a)), if a / ∈ Σ 1 and δ 2 (q, a) is defined in G 2 ; undefined, otherwise.
From the language point of view, it can be shown that

L(G 1 G 2 ) = P -1 1 (L(G 1 )) ∩ P -1 2 (L(G 2 ))
,

where P i is the projection from (Σ 1 ∪ Σ 2 ) * to Σ * i for i = 1, 2.
Let us briefly recall definitions of the operations of reversal, cyclic shift, and left and right quotients for languages over an alphabet Σ. The reversal of a string w over Σ is defined by ε R = ε and (va) R = av R for a symbol a in Σ and a string v in Σ * . The reversal of a language L is the language

L R = {w R ∈ Σ * | w ∈ L}.
The cyclic shift of a language L is defined as the language L shif t = {uv ∈ Σ * | vu ∈ L}. The left and right quotients of a language L by a language K are the languages K\L = {x ∈ Σ * | there exists w ∈ K such that wx ∈ L} and L/K = {x ∈ Σ * | there exists w ∈ K such that xw ∈ L}, respectively. By L c we denote the complement of a language L, that is, the language Σ * \ L.

Minimal State-Partition Automata

The fundamental question is whether every regular language can be accepted by a state-partition automaton with respect to a given projection. If this is the case, can we construct such a state-partition automaton efficiently? The answer to this question is known, and we repeat it in the following theorem. Although a proof has been given in [START_REF] Cho | On supremal languages of classes of sublanguages that arise in supervisor synthesis problems with partial observation[END_REF], we prefer to recall it here since some fundamental observations play a role later in the paper.

Theorem 1 ( [START_REF] Cho | On supremal languages of classes of sublanguages that arise in supervisor synthesis problems with partial observation[END_REF][START_REF] Cho | Supremal and maximal sublanguages arising in supervisor synthesis problems with partial observations[END_REF]). Let P be a projection from Σ * to Σ * o with Σ o ⊆ Σ. Let L be a language over the alphabet Σ, and let G be a DFA accepting the language L. Then the automaton P (G) G is a state-partition automaton with respect to the projection P that accepts the language L.

Proof. Let G = (Q, Σ, δ, s, F ) be a DFA accepting the language L, and let P (G) = (Q , Σ o , δ , s , F ) be the corresponding projected automaton. By definition of the parallel composition and the comment below the definition, we have that

L(P (G) G) = P -1 (P (L(G))) ∩ L(G) = L(G) .
Hence, the automaton P (G) G accepts the language L. Let w be a string over the alphabet Σ o . Then the state of the projected automaton P (P (G) G) reached from the initial state by the string w is (δ (s , w), q) | q ∈ δ(s, P -1 (w)) . Since δ(s, P -1 (w)) = δ (s , w), by definition of the transition function of the automaton P (G), the state reachable from its initial state by the string w in the DFA

P (P (G) G) is, in fact, {(δ (s , w), q) | q ∈ δ (s , w)} .
It then follows that the states of the projected automaton P (P (G) G) reachable by two different strings are either the same or disjoint.

Next we prove that the state-partition automaton constructed from a minimal DFA using the construction of the previous theorem is the minimal statepartition automaton with respect to the number of states. To prove this, we need the notion of isomorphic automata, and the result proved in the following lemma.

Let

G 1 = (Q 1 , Σ, δ 1 , s 1 , F 1 ) and G 2 = (Q 2 , Σ, δ 2 , s 2 , F 2 ) be two DFAs. Let f be a mapping from Q 1 to Q 2 such that • f (δ 1 (q, a)) = δ 2 (f (q), a) for each q in Q 1 and a in Σ, • f (s 1 ) = s 2 , and • q ∈ F 1 if and only if f (q) ∈ F 2 .
The mapping f is called a homomorphism from G 1 to G 2 . If f is a bijection, then it is called an isomorphism, and G 1 and G 2 are said to be isomorphic.

The next lemma shows that the parallel composition of automata P (G) and G is isomorphic to G for a state-partition automaton G.

Lemma 2. Let G be an SPA with respect to a projection P from Σ * to Σ * o , in which all states are reachable. Then the DFA P (G) G is isomorphic to G.

Proof. Let G = (Q, Σ, δ, s, F ) be a state-partition automaton with respect to the projection P , and let P (G) = (Q , Σ o , δ , s , F ) be the corresponding projected automaton. Define a mapping f :

Q × Q → Q by f (X, q) = q.
Then it holds that δ(q, a) = δ(f (X, q), a), and f is an isomorphism from P (G) G to G.

The following result constructs the minimal state-partition automaton for a given regular language and a projection.

Theorem 2. Let L be a regular language over an alphabet Σ, and let G be the minimal DFA accepting the language L. Let P be a projection from Σ * to Σ * o . Then the DFA P (G) G is the minimal state-partition automaton with respect to the projection P that accepts the language L.

Proof. Let G = (Q, Σ, δ, s, F ) be the minimal DFA accepting the language L, and let G 2 = (Q 2 , Σ, δ 2 , s 2 , F 2 ) be a state-partition automaton with respect to the projection P that also accepts the language L. We may assume that all states of the DFA G 2 are reachable and useful; otherwise, we can remove unreachable and useless states from G 2 and obtain a smaller state-partition automaton.

Define a mapping f : Q 2 → Q as follows. For a state q in Q 2 that is reachable in the automaton G 2 from the initial state s 2 by a string w, set f (q) = δ(s, w), that is, f (q) is a state in Q that is reachable in the automaton G from the initial state s by the string w. Notice that f is well-defined since if a state in Q 2 is reached by two different strings u and v, then states δ(s, u) and δ(s, v) must be equivalent in the automaton G, and since G is minimal, we must have δ(s, u) = δ(s, v).

Next, we have f (δ 2 (q, a)) = δ(f (q), a) for each state q in Q 2 and symbol a in Σ, f (s 2 ) = s, and q ∈ F 2 if and only if f (q) ∈ F . Hence f is a homomorphism from G 2 to G. Now, extend the mapping f to a mapping from the state set of the automaton P (G 2 ) G 2 to the state set of the automaton P (G) G by setting f (X, q) = (f (X), f (q)) .

Then f is surjective. Since the automaton G 2 is a state-partition automaton with respect to the projection P , we have, using Lemma 2, that

sc(P (G) G) ≤ sc(P (G 2 ) G 2 ) = sc(G 2 ) .
This completes the proof.

Corollary 1. Let L be a regular language over an alphabet Σ, and let P be a projection from Σ * . Then the minimal state-partition automaton accepting the language L is unique up to isomorphism.

It is natural to ask whether an automaton can be a state-partition automaton with respect to more than one projection. This property would be useful in applications, where both an abstraction and a partial observation are combined, cf. [START_REF] Boutin | Hierarchical control with partial observations: Sufficient conditions[END_REF]. Unfortunately, the following result shows that this does not hold true in general [8]. Lemma 3. There exist a language L and projections P and P such that no DFA accepting the language L is a state-partition automaton with respect to both projections P and P .

Proof. Let Σ = {a, b}. Let P and P be projections from Σ * onto {a} * and {b} * , respectively. Consider the language L = (ab) * . Assume that G = (Q, Σ, δ, s, F ) is a state-partition automaton for both projections P and P accepting the language L. Notice that the DFA G does not have any loop, that is, no state of G goes to itself on any symbol, because otherwise the automaton G would accept a string that does not belong to the language L.

Let w be a string of the language L of length at least |Q|. Then at least one state appears twice in the computation of the automaton G on the string w. Let p be the first such state. Then w = xyz, where x is the shortest prefix of w such that the initial state s goes to state p by x, and y is the shortest non-empty factor of w by which p goes to itself. Since the automaton G has no loops, the length of y is at least two. Therefore, y = cy d, where c, d ∈ {a, b}. In addition, c = d because xyyz = xcy dcy dz belongs to the language L. Let q be the state of the automaton G that is reached from the state p on reading the string cy . Fig. 1 illustrates the computation of G on the string w. Since x is the shortest prefix of w that moves G to state p, and y is the shortest non-empty factor of w by which p goes to itself, we have p = q.

In case d = b, we consider the projected automaton

P (G) = (Q , {a}, δ , s , F ) .
Let X = δ (s , P (x)) and Y = δ (X, P (ay )) be two states of the automaton P (G). Then p ∈ X and p, q ∈ Y . Notice that X = δ(s, P -1 (P (x))). Since c = a and w ∈ L, we have x = (ab) k for a non-negative integer k. Therefore, P -1 (P (x)) = P -1 (a k ).

Assume that there exists a string u in P -1 (a k ) that moves the automaton G from the initial state s to the state q. Then the string udz is accepted by the automaton G. Since d = b, we must have u = (ab) k-1 a. However, then the state q would be the first state in the computation on the string w that appears at least twice in it, which contradicts the choice of the state p. It follows that q / ∈ X, and, therefore, X = Y . Hence, the automaton G is not a state-partition automaton with respect to the projection P .

The case d = a is similar.

Closure Properties

Since every regular language has a state-partition automaton with respect to a given projection, the class of languages accepted by state-partition automata is closed under all regular operations. In the following, we consider the closure properties of state-partition automata under the standard constructions of deterministic automata for regular operations as described in the literature [START_REF] Hopcroft | Introduction to automata theory, languages, and computation[END_REF][START_REF] Salomaa | Formal languages[END_REF][START_REF] Sipser | Introduction to the theory of computation[END_REF][START_REF] Yu | Regular languages[END_REF]. Hence, we investigate the following question: Given state-partition automata with respect to a projection, is the deterministic automaton resulting from the standard construction for a regular operation a state-partition automaton with respect to the same projection?

We prove that almost all standard constructions, except for the complement of complete state-partition automata and right quotient, fail to preserve the property of being a state-partition automaton. Theorem 3. State-partition automata are not closed under the operations of complement, intersection, union, concatenation, star, reversal, cyclic shift, and left quotient.

Proof. We briefly recall the standard construction of a deterministic automaton for each operation under consideration. Let us emphasize that we do not minimize the resulting deterministic automata.

Complement: To get a deterministic automaton for complement from a possibly incomplete DFA G, add the dead state, if necessary, and interchange the final and non-final states. We prove that state-partition automata are not closed under this operation.

Consider the two-state DFA G in Fig. 2 (left). The DFA accepts the language ab * . Let P be the projection from {a, b} * to {a} * . Then G is a state-partition automaton with respect to the projection P since the projected automaton P (G) is deterministic. However, the complement of G, the DFA G c shown in Fig. 2 (right), is not a state-partition automaton with respect to the projection P because we have to add the dead state, 3, which then appears in two different reachable sets of the projected automaton P (G c ), namely, in {1, 3} reached by ε and in {2, 3} reached by a. However, as the next theorem shows, the resulting DFA is a state-partition automaton if the given DFA is complete.

Intersection and union: To get the deterministic automaton for intersection and union, we apply the standard cross-product construction.

Consider two automata G 1 and G 2 shown in Fig. 3, and their cross-product automaton G 1 × G 2 depicted in Fig. 3. In the case of intersection, the only final state is state 3, while in the case of union, the final states are states 3 and 4. Let P be the projection from {a, b} * to {a} * . Both G 1 and G 2 are state-partition automata with respect to the projection P . However, the automaton G 1 × G 2 is not since the sets {2, 3} and {3, 4} are reachable in the projected automaton P (G 1 × G 2 ) by strings a and aa, respectively.

Concatenation: Recall that an NFA for concatenation of two DFAs G 1 and G 2 is obtained from G 1 and G 2 by adding ε-transitions from final states of G 1 to the initial state of G 2 , and by setting the initial state to be the initial state of G 1 , and final states to be final states of G 2 . The corresponding subset automaton restricted to its reachable states provides the resulting DFA for concatenation. Now, let G be the DFA shown in Fig. 4 (left). Let P be the projection from {a, b} * to {b} * . The projected automaton P (G) is a one-state automaton and, therefore, the DFA G is a state-partition automaton with respect to the projection P . The DFA G • G for concatenation is depicted in Fig. 4 (right), and states {1, 2, 3} and {1, 2, 3, 4} are reachable in the projected automaton P (G • G) by strings ε and b, respectively. Hence, the DFA G • G for concatenation is not a state-partition automaton for the projection P . Consider the DFA G in Fig. 5 (left), and the projection P from {a, b, c} * to {a, b} * . The automaton G is a state-partition automaton with respect to the projection P since the projected automaton P (G) is deterministic. However, the deterministic automaton G * for star, shown in Fig. 5 (right), is not a statepartition automaton with respect to the projection P because the sets {3} and {3, 4} are reachable in the projected automaton P (G * ) by strings ab and aba, respectively. Reversal: We can get an NFA for reversal from a DFA G by swapping the roles of initial and final states, and by reversing all transitions. After the application of the subset construction, we obtain a DFA for reversal.

Consider the DFA G in Fig. 6 (left), and the projection P from {a, b, c} * to {a, c} * . The DFA G is a state-partition automaton with respect to P since the states of the projected automaton P (G) are {2, 3} and {1}. On the other hand, the DFA G R in Fig. 6 (right) is not a state-partition automaton with respect to the projection P because the sets {2} and {2, 3} are reachable in the projected automaton P (G R ) by strings a and ac, respectively.

Cyclic shift: For the construction of an NFA for cyclic shift, we refer to [START_REF] Jirásková | State complexity of cyclic shift[END_REF]. Fig. 7 (middle) shows an NFA for the cyclic shift of the language accepted by the DFA G of Fig. 7 (left). Let P be the projection from {a, b} * to {b} * . Then G is a state-partition automaton with respect to the projection P since the projected automaton P (G) has just one state {1, 2}. However, the automaton G shif t in Fig. 7 (right) is not a state-partition automaton with respect to the projection The following theorem demonstrates that if the structure of the automaton is not changed after an operation, then the automaton remains state-partition with respect to the same projection. Proof. Let G be a complete state-partition automaton. Construct a deterministic automaton G c for the complement of L(G) from the DFA G by interchanging final and non-final states. The result now follows from the fact that the states of the projected automaton P (G c ) are the same as the states of the projected automaton P (G) since the structure of the automaton G c is the same as the structure of the automaton G. Now, consider the right quotient of a language L(G) by a language K; here, the DFA G may be incomplete. Construct an automaton for the right quotient L(G)/K from the automaton G by replacing the set of final states with the set of states of G from which a string of the language K is accepted. Again, the structure of the automaton remains the same; we only change the set of final states.

State-Partition Complexity

Let L be a regular language over an alphabet Σ, and let P be a projection from Σ * to Σ * o . We define the state-partition complexity of the language L, denoted by spc(L), as the smallest number of states in any automaton accepting the language L that is a state-partition automaton with respect to the projection P . By Theorem 2, the state-partition complexity of the language L is the number of states of the DFA P (G) G, where G is the minimal incomplete DFA accepting the language L. Now, we give the upper bound on the state-partition complexity of regular languages, and prove that this bound is tight. We omit the proof due to space constraints.

Theorem 5. Let L be a language over an alphabet Σ accepted by the minimal incomplete DFA G with n states. Let P be a projection from Σ * to Σ * o . Then spc(L) ≤ 3n • 2 n-3 .

Finally, we prove that the bound proved in the previous theorem is tight. Theorem 6. For every integer n ≥ 3, there exists a regular language L accepted by the minimal incomplete DFA G with n states such that spc(L) = 3n • 2 n-3 .

Proof. Consider the language L accepted by the DFA G depicted in Fig. 9 and the projection P from {a, b, c} * to {a, b} * . We need to prove that all subsets of the state set {0, 1, . . . , n -1}, except for the sets that contain n -1 and do not contain 0, are states of the automaton P (G). Notice that if X is reachable in P (G) by a string u over {a, b} and q ∈ X, then state q is reachable in the automaton G by a string w in P -1 (u). This means that (X, q) is a reachable state in the automaton P (G) G since (X, q) = δ(s, P -1 (P (w)), δ(s, w) . First, we construct an NFA accepting the language P (L) as shown in Fig. 10. Let us show that all subsets of the state set {0, 1, . . . , n -1} containing state 0, as well as all non-empty subsets of the set {1, 2, . . . , n -2} are reachable.

The proof is by induction on the size of subsets. Each set {i}, where i ≤ n -2, is reached from {0} by the string a i . Let 2 ≤ k ≤ n. Assume that each subset of size k -1, satisfying the above mentioned conditions, is reachable. Let X = {i 1 , i 2 , . . . , i k }, where 0 ≤ i 1 < i 2 < • • • < i k ≤ n -1, be a subset of size k. Consider two cases:

(i ) i 1 = 0. Take Y = {i j -i 2 -1 | 3 ≤ j ≤ k} ∪ {n -2}. Then Y is of size k -1 and it does not contain state n -1. Therefore, it is reachable by the induction hypothesis. The subset Y goes to X on the string aab i2-1 since we have

Y a → {0, n -1} ∪ {i j -i 2 | 3 ≤ j ≤ k} a → {0, 1} ∪ {i j -i 2 + 1 | 3 ≤ j ≤ k} b i 2 -1
---→ X.

(ii ) i 1 ≥ 1. Then i k ≤ n -2. Take Y = {0} ∪ {i j -i 1 | 2 ≤ j ≤ k}. Then the subset Y is of size k and contains state 0. Therefore, it is reachable as shown in case (i ). The subset Y goes to X on the string a i1 .

This proves the reachability of all 3 • 2 n-2 -1 subsets of the automaton P (G).

The number of all reachable pairs (X, q) with q ∈ X of the automaton P (G) G is

Fig. 1 .

 1 Fig. 1. The computation of G on the string w = xcy dz.

Fig. 2 .

 2 Fig. 2. SPA G (left), and DFA G c for the complement of the language L(G) (right); projection P : {a, b} * → {a} * .

Fig. 3 .

 3 Fig. 3. SPAs G1 (left) and G2 (middle), and their cross-product G1 × G2 (right); projection P : {a, b} * → {a} * .

Fig. 4 .

 4 Fig. 4. SPA G (left) and DFA G • G for concatenation of the languages L(G) • L(G) (right); projection P : {a, b} * → {b} * .

Fig. 5 .

 5 Fig. 5. SPA G (left), and DFA G * for the star of the language L(G) (right); projection P : {a, b, c} * → {a, b} * .

Fig. 6 .

 6 Fig. 6. SPA G (left), and DFA G R for the reversal of the language L(G) (right); projection P : {a, b, c} * → {a, c} * .

Fig. 7 .

 7 Fig. 7. SPA G (left), NFA for shift(L(G)) (middle), and DFA G shif t (right); projection P : {a, b} * → {b} * .

Theorem 4 .

 4 State-partition automata are closed under the operations of right quotient and complement of complete state-partition automata.

Fig. 8 .

 8 Fig. 8. SPA G (left) and DFA a\G for the left quotient by the string a (right); projection P : {a, b} * → {b} * .

Fig. 9 .

 9 Fig. 9. The minimal incomplete DFA G meeting the upper bound 3n • 2 n-3 .

i

  = 3n•2 n-3 , which proves the theorem.

Fig. 10 .

 10 Fig. 10. An NFA for language P (L(G)), where G is shown in Fig. 9.

Acknowledgements. We wish to thank Jan Komenda, Klaus Schmidt, and Jan H. van Schuppen for a discussion on state-partition automata.

Research supported by the Slovak Research and Development Agency under contract APVV-0035-10 "Algorithms, Automata, and Discrete Data Structures". Research supported by the GA ČR grant no. P202/11/P028 and by RVO: 67985840.

Conclusions and Discussion

We investigated deterministic state-partition automata with respect to a given projection. The state set of such an automaton is partitioned into disjoint subsets that are reachable in the projected automaton. Using a result from the literature that every regular language has a state-partition automaton with respect to a given projection, we provided the construction of the minimal state-partition automaton for a regular language and a projection. We also described a regular language and two projections such that no automaton accepting this language is a state-partition automaton with respect to both projections.

Next, we studied closure properties of state-partition automata under the standard constructions of deterministic automata for the operations of complement, union, intersection, concatenation, star, reversal, cyclic shift, and left and right quotients. We showed that except for the right quotient and complement of complete deterministic automata, all other constructions fail to preserve the property of being a state-partition automaton.

Finally, we defined the notion of the state-partition complexity of a regular language as the smallest number of states of any state-partition automaton with respect to a given projection accepting the language. We proved that the tight bound on the state-partition complexity of a language represented by an incomplete deterministic automaton with n states is 3n • 2 n-3 . To prove the tightness of this bound, we used a language defined over the ternary alphabet {a, b, c} and the projection from {a, b, c} * to {a, b} * . Note that it follows from the results of [START_REF] Jirásková | On a structural property in the state complexity of projected regular languages[END_REF] that this bound cannot be reached using a smaller alphabet or a projection to a singleton.

State-partition complexity of regular operations may be investigated in the future. We only know that state-partition complexity of a language and its complement differs by one in the case of complete deterministic automata, and by 3n if the automata are incomplete. Defining nondeterministic state-partition automata and investigating their properties may also be of interest.


Marijke H L Bodlaender

Cor A J Hurkens

Vincent J J Kusters

Frank Staals

Gerhard J Woeginger

Hans Zantema

Cinderella versus the wicked Stepmother

We investigate a combinatorial two-player game, in which one player wants to keep the behavior of an underlying water-bucket system stable whereas the other player wants to cause overflows. This game is motivated by data management applications in wireless sensor networks. We construct optimal strategies and characterize optimal bucket sizes for many instances of this game.

Introduction

Motivated by a data management application in wireless sensor networks, Bender & al [START_REF] Bender | The minimum-backlog problem[END_REF] study the minimum-backlog problem which is a two-player game on an undirected graph. The vertices of the graph contain buckets (which model bu↵ers) that can store water (which models data). In every time step the adversary distributes exactly one liter of water over the buckets. The player then moves from his current vertex to an adjacent one and empties the corresponding bucket. The player's objective is to minimize the maximum amount of water in any bucket at any time, or in other words, to prevent the buckets from overflowing while using the smallest possible bucket size. Bodlaender & al [START_REF] Bodlaender | The Cinderella game on holes and anti-holes[END_REF] discuss another variant where in every time step the player can empty a subset of buckets standing in an arbitrary independent set in the graph. Polishchuk & Suomela [START_REF] Polishchuk | Optimal backlog in the plane[END_REF] investigate the variant of the minimum-backlog problem where the underlying metric space is not a graph but the Euclidean plane. Chrobak & al [START_REF] Chrobak | The bu↵er minimization problem for multiprocessor scheduling with conflicts[END_REF] discuss related scenarios in undirected graphs where data/water arrives continuously over time and where the player can (continuously) empty an entire independent set of buckets/bu↵ers; if the player spends t time units on a bucket set, then the contents of each such bucket is decreased by t. Note that in [START_REF] Bender | The minimum-backlog problem[END_REF] the graph structure constrains the route taken by the player, whereas in [START_REF] Chrobak | The bu↵er minimization problem for multiprocessor scheduling with conflicts[END_REF] the graph structure constrains the sets of buckets that the player can empty simultaneously.

In the current paper we will concentrate on discrete scenarios where data/water arrives in rounds and where in every round the player can empty certain subsets of the buckets. One of the simplest cases of our game is as follows [START_REF] Woeginger | Combinatorics problem C5. Problem Shortlist of the 50th International Mathematical Olympiad[END_REF][START_REF] Hurkens | How Cinderella won the bucket game (and lived happily ever after)[END_REF].

"Five empty buckets of capacity b stand in the corners of a regular pentagon. Cinderella and her wicked Stepmother play a game that goes through a sequence of rounds: at the beginning of every round, the Stepmother takes one liter of water from the nearby river, and distributes it arbitrarily over the five buckets.

Then Cinderella chooses a pair of neighboring buckets, empties them into the river, and puts them back into the pentagon. Then the next round begins. The Stepmother's goal is to make one of these buckets overflow. Cinderella's goal is to prevent this. For which bucket sizes b can the Stepmother eventually enforce a bucket overflow? And for which bucket sizes can Cinderella keep the game running forever?"

We study a general bucket game BG(n, c) for integers n and c with 1  c  n 1, where there are n 2 buckets standing in a circle. Throughout we will use the term Cinderella to denote the player and the wicked Stepmother to denote the adversary. In every round the Stepmother first distributes one liter over the n buckets, and then Cinderella empties an arbitrary group of c consecutive buckets. The Stepmother wants to reach a bucket overflow, and Cinderella wants to avoid this. Clearly the above Cinderella puzzle coincides with BG [START_REF] Dutertre | Yices -A high-performance SMT solver[END_REF][START_REF] Bodlaender | The Cinderella game on holes and anti-holes[END_REF]. We define F 0 (n, c) as the infimum of all bucket sizes for which Cinderella can keep the game running forever, and we furthermore introduce the quantity F (n, c) = F 0 (n, c) 1. If Cinderella consistently avoids overflows for buckets of size F 0 (n, c), then at the end of every round she will only leave buckets with contents F (n, c) or less.

Summary of results

. Table 1 lists the values F (n, c) for all games with n  12 buckets. For every single entry in this table with n  10 we have proofs that were constructed by humans (and that are presented in this paper) as well as computerized proofs (that have been done with the SMT solver YICES [START_REF] Dutertre | Yices -A high-performance SMT solver[END_REF]). For some of the entries in the lines n = 11 and n = 12, we only have computer proofs.

The entries in the table might seem somewhat chaotic at first sight. But taking a second look, the reader perhaps notices that the topmost numbers 1, 1/2, 1/3, . . ., 1/11 in the columns are the reciprocals of the positive integers. This indeed is a (fairly shallow) mathematical fact which we present in Section 3, and which says that F (c + 1, c) = 1/c for all c 1. Next let us discuss the values F (c + 2, c) immediately below the topmost numbers, which are 3/2, 1, 5/9, 1/2, 7/20, 1/3, 9/35, 1/4, 11/54, 1/5. We note that the values in the even positions again are the reciprocals of integers. Indeed Section 2 shows that the function values F (n, c) only depend on the ratio n/c, which for even c = 2s implies F (2s + 2, 2s) = F (s + 1, s) = 1/s. Section 3 shows that the remaining values in the odd positions satisfy F (c + 2, c) = (2c + 4)/(c 2 + 3c). By stepping further down in the columns, we meet the values

F (c + 3, c) which read 11/6, 1, 1, 17/30, 1/2, 1/2, 69/196, 1/3, 1/3.
The values F (3s + 3, 3s) = F (s + 1, s) = 1/s are of course once again the reciprocals of the integers. Section 3 shows that also the values F (3s+2, 3s 1) = 1/s are such reciprocals, and it fully explains the (more complicated) structure of the remaining values F (3s + 1, 3s 2). Moving further down in Table 1, we eventually hit an area that entirely consists of 1-entries. The uppermost 1-entry in every column is F (2c, c) = F (2, 1) = 1, and these entries form the so-called half-diagonal of the table (the diagonal where c is half of n). This half-diagonal is a natural separation line, and it turns out that the combinatorics of the games below the half-diagonal behaves quite di↵erently from the combinatorics of the games above the half-diagonal. Going even further down, we see that the lowermost 1-entry in every column is F (3c 1, c) = 1. In other words F (n, c) = 1 holds whenever 2c  n  3c 1, and this is a mathematical theorem which we establish in Section 5. This theorem actually is our main result, and its proof is long and involved and uses quite delicate invariants.

n\c 1 2 3 4 5 6 7 8 9 1 0 2 1 - - - - - - - - - 3 3/2 1 /2 - - - - - - - - 4 11/6 1 1 /3 - - - - - - - 5
What else is going on below the half-diagonal? The first column lists the harmonic numbers H k = 1+ 1 2 + 1 3 + . . . + 1 k . The second column (below the halfdiagonal) seems to list again the harmonic numbers, but this time with every term occurring twice. And also the third column (below the half-diagonal) seems to list the harmonic numbers, with every term occurring thrice. And so on. We settle the behavior of the first column in Section 5, and we furthermore derive some partial results on the other columns. Many questions remain open.

Also the global structure of Table 1 shows many interesting properties. Of course, the values in every row form a non-increasing sequence (since c increases and Cinderella becomes more powerful), and for similar reasons the values in every column form a non-decreasing sequence. In fact an even stronger property holds true (see Section 2): the function F (n, c) is non-decreasing in the ratio n/c. Here is one application of this fact: from F (3, 2) = F (8, 5) = 1/2 and from 3/2 < 11/7 < 8/5 we immediately deduce F (11, 7) = 1/2.

Organization of the paper. Section 2 states simple observations, summarizes the notation, and explains the general setup of our proofs. Section 3 deals with the games above the half-diagonal, and Section 5 deals with the games below the half-diagonal. Section 6 gives some conclusions.

Preliminaries, notations, and conventions

The n buckets in any fixed game BG(n, c) are ordered along the circle and denoted 1, 2, . . . , n. The numbering of buckets is always taken modulo n, so that k and n + k denote the same bucket. We use d(i, j) = min{|i j|, n |i j|} to denote the distance between buckets i and j along the circle. If d(i, j) c, then Cinderella can not simultaneously empty i and j within a single round. A subset S of buckets is called independent, if it does not contain two adjacent buckets. The family I consists of all independent bucket subsets.

The contents of the buckets at a particular moment in time are often summarized in a vector x = (x 1 , . . . , x n ) where x i denotes the current contents of bucket i. For a subset S of the buckets, we use x(S) = P i2S x i . To keep the notation simple, we write x(i, j) short for x({i, j}) and x(i, j, k) short for x({i, j, k}), and we use x i and x(i) interchangeably.

The following two lemmas imply that function F (n, c) only depends on the ratio n/c, and that it is non-decreasing in this ratio. Proof. Consider an arbitrary strategy for the Stepmother for BG(n, c). The Stepmother can emulate this strategy in BG( n, c) by using the buckets , 2 , . . . , n . This yields F ( n, c) F (n, c). Vice versa, Cinderella can carry over strategies from BG(n, c) to BG( n, c). She cuts the circle into n intervals with buckets, treats every interval as a super-bucket, and uses her strategy for BG(n, c) on the super-buckets. This yields

F ( n, c)  F (n, c). ⇤ Lemma 2. (Monotonicity lemma) F (n 1 , c 1 )  F (n 2 , c 2 ) whenever n 1 /c 1  n 2 /c 2 . Proof. This follows from F (n 1 , c 1 ) = F (n 1 n 2 , c 1 n 2 )  F (n 1 n 2 , c 2 n 1 ) = F (n 2 , c 2 ). ⇤
By the definition of F 0 (n, c), Cinderella wins the game BG(n, c) if the bucket size is strictly larger than F 0 (n, c), and the Stepmother wins the game if the bucket size is strictly smaller than F 0 (n, c). What happens at the threshold F 0 (n, c)? Lemma 3. If BG(n, c) is played with buckets of size F 0 (n, c), then Cinderella can keep the game running forever.

Proof. Let G(n, c, R) denote the maximum amount of water that the Stepmother can accumulate in some bucket within the first R rounds of game BG(n, c); it can be proved by an inductive argument that this maximum indeed exists. Now suppose that the Stepmother could enforce an overflow for buckets of size F 0 (n, c). Then she can enforce this overflow after a finite number R of rounds, which means G(n, c, R) > F 0 (n, c). But then within R rounds the Stepmother could as well enforce overflows for any bucket size between F 0 (n, c) and G(n, c, R), which conflicts with the definition of F 0 (n, c). ⇤ Lower bounds from balancing Stepmothers. Our lower bound arguments for F (n, c) use a special adversary which we call balancing Stepmother. A balancing Stepmother balances the water levels in certain buckets, and works in two phases. During the first phase, the Stepmother always distributes her liter in such a way that all n buckets are filled to the same level. This common filling level is 1/n in the first round, and in later rounds increases and converges to 1/c. The first phase ends, when the common filling level exceeds 1/c " (where " is a tiny positive real number that can be made arbitrarily close to 0). The set of n c buckets that are filled to level L 1 ⇡ 1/c at the end of the last round of the first phase is denoted by S 1 .

In the second phase, we will usually ignore the dependence of our bounds on ", so that the presentation remains simple and our formulas stay clean. The second phase goes through n c 1 further rounds. At the beginning of the r-th one of these rounds (r = 1, . . . , n c 1), there are (n c) r +1 buckets filled to the same level L r that Cinderella could not empty in the preceding round; these buckets form the set S r . The balancing Stepmother then picks an appropriate set T r ◆ S r of buckets, such that in the current round Cinderella must leave at least (n c) r buckets in T r untouched. All buckets in T r are then filled to the same level L r+1 = (|S r | L r + 1)/|T r |. At the end of the last round n c 1, there remains a single non-empty bucket whose contents L n c 1 forms the resulting lower bound.

Upper bounds from invariants. Our upper bound arguments for F (n, c) are based on appropriate systems of invariants that (i) can be maintained by Cinderella, and that (ii) imply that every bucket contents remains below F (n, c). A typical invariant system bounds the contents of every bucket by x i < F (n, c), and furthermore bounds the overall contents of certain groups of buckets. All invariants are trivially satisfied at the beginning of the first round when all buckets are empty. In our proofs we usually assume inductively that these invariants are satisfied at the beginning of some fixed round (just before the Stepmother moves), and then show that Cinderella can re-establish them at the end of the round. In doing this, we always let x i denote the contents of bucket i at the beginning of the round, and we always let y i denote the contents of bucket i after the Stepmother has moved.

Above the half-diagonal

By definition the games BG(n, c) above the half-diagonal satisfy n < 2c. It is not hard to see that all these games satisfy F (n, c) < 1 (as at the end of her move, Cinderella can keep the total amount of water in the system below n/c 1). We fully understand the games BG(c + 1, c), BG(c + 2, c), and BG(c + 3, c). The proofs of Theorems 2, 3 and 4 are to be found in the subsections below. It is easily verified that these theorems (together with monotonicity) imply all entries for n  10 above the half-diagonal of Table 1.

We think that also all values F (c + 4, c) are within reach and could be fully characterized, if one invests su cient time and energy. We actually determined many values F (n, c) above the half-diagonal with the help of computer programs. For instance we know that F (13, 9) = 37/105 and F (17, 13) = 1961/7605, and it took us hours of computation time to establish F (16, 11) = 252/715. We see many patterns and regularities in the data, but we can not find a unifying conjecture that would systematically cover all possible cases; certain divisibility properties seem to kick in and totally mess up the structure. Our data suggests the following conjecture (which is fairly weak and only covers a small part of the unknown area).

Conjecture 1. F (n, c) = 1/2 holds for all n and c with 3/2  n/c < 5/3.

The proof of Theorem 2

Since monotonicity settles the cases with even c, we only discuss the games where c is odd (and n = c + 2).

(Upper bound) At the end of every round, Cinderella leaves two non-empty buckets (say buckets 1 and 2) whose loads x 1 and x 2 satisfy the following two invariants:

x(1, 2) < 2/c (1a)

x 1 , x 2 < L 2 := (2c + 4)/(c 2 + 3c) (1b)
Then the Stepmother moves and yields bucket contents y 1 , . . . , y c+2 . Cinderella maintains the invariants by leaving a pair j, j + 1 of neighboring buckets with smallest total contents. Since the Stepmother only adds a single liter, invariant (1a) implies

c+2 X i=1 y i < (c + 2)/c. ( 2
)
By averaging we get y(j, j + 1)  (2 P y i )/(c + 2) < 2/c, which ensures invariant (1a). Next, suppose for the sake of contradiction that y j L 2 . Partition the remaining c + 1 buckets (except bucket j) into (c + 1)/2 pairs of neighboring buckets. The total contents of every such pair is at least y(j, j + 1) L 2 , which implies

P c+2 i=1 y i 1 2 (c + 3) L 2 = (c + 2)/c
, and thus contradicts (2). Hence y j < L 2 , and an analogous argument yields y j+1 < L 2 .

(Lower bound) The first phase of the balancing Stepmother ends with two buckets (say 1 and 2) of contents very close to 1/c. In the second phase, the Stepmother chooses set T 1 to contain buckets 1 and 2 together with all buckets with even numbers; note that |T 1 | = (c+3)/2. Then all buckets in T 1 are brought to level at least (2/c + 1)/|T 1 | = L 2 . Since Cinderella cannot simultaneously empty all buckets in T 1 , we get F (c + 2, c) L 2 .

The proof of Theorem 3.(i) and (ii)

Monotonicity and Theorem 1 yield the lower bound F (3s + 2, 3s 1) F (3s + 3, 3s) = F (s + 1, s) = 1/s. Hence we will concentrate on the upper bound for the game with n = 3s + 2 buckets and c = 3s 1.

At the end of some fixed round Cinderella leaves three adjacent buckets, say the buckets 3, 4, 5. She always maintains the following two invariants.

x 4 < 1/s (3a) x(3, 5) < 1/s (3b)
The Stepmother adds one liter to the system and brings the contents to y 1 , y 2 , . . . , y 3s+2 . A triple is a group of three consecutive buckets i, i + 1, i + 2 in the circle. A triple is called good, if y(i, i + 1, i + 2) < 1/s. By emptying all buckets outside a good triple, Cinderella can maintain the invariants. Hence we assume from now on that there is no good triple.

We denote by W the total amount of water in all buckets except bucket 4. Invariant (3b) implies W < 1 + 1/s. Since there are no good triples, we have y(1, 2, 3) 1/s and y(5, 6, 7) 1/s. By subtracting these two inequalities from

W < 1 + 1/s, we get 3s+2 X i=8 y i < 1 1/s. ( 4
)
Next suppose for the sake of contradiction that y 3i+2 1/s holds for some i with 2  i  s. Then the 3i 6 buckets 8, 9, . . . , 3i + 1 and the 3s 3i buckets 3i + 3, 3i + 4, . . . , 3s + 2 can be divided into s 2 non-good triples. Therefore the overall amount of water in these s 2 triples together with y 3i+2 would be at least (s 1)/s, which contradicts (4). This contradiction implies y 3i+2 < 1/s for 2  i  s. Furthermore we assume y(3i + 1, 3i + 3) 1/s, since otherwise Cinderella could easily maintain the invariants by emptying all buckets except the triple 3i + 1, 3i + 2, 3i + 3. Summing these s 1 inequalities for 2  i  s yields

s X i=2 y 3i+1 + s X i=2 y 3i+3 1 1/s. ( 5
)
If y(6, 8) 1/s, then (5) yields that the Stepmother has added her entire liter to the buckets outside the triple 3, 4, 5, and Cinderella can maintain all invariants by reverting the system to the preceding state. Hence we assume from now on y(6, 8) < 1/s, and a symmetric argument yields y(3s + 2, 2) < 1/s. If y 7 < 1/s or y 1 < 1/s, then Cinderella maintains the invariants by emptying everything except the triple 6, 7, 8, respectively by emptying everything except the triple 3s + 2, 1, 2. Hence we assume from now y 7 1/s and y 1 1/s.

Finally note that the 3s 5 buckets 8, 9, 10, . . . , 3s + 2 contain s 2 pairwise disjoint triples, each of which is non-good and has total contents at least 1/s. Together with y 1 1/s and y 7 1/s this shows that the Stepmother must have added her entire liter to the buckets 7, 8, 9, 10, . . . , 3s + 2, and 1. By emptying these buckets, Cinderella reverts the system to the preceding state and maintains all invariants.

The proof of Theorem 3.(iii)

We discuss the game with n = 3s + 4 and c = 3s + 1. For s 1, we introduce three parameters L 1 , L 2 , L 3 by

L 1 = 1 3s + 1 L 2 =
3s + 4 (2s + 3)(3s + 1)

L 3 = (s + 1)(6s + 11) (s + 2)(2s + 3)(3s + 1)
Note that these three parameters satisfy

L 2 = 3L 1 + 1 2s + 3 and L 3 = 2L 2 + 1 s + 2 . ( 6
)
Furthermore, we have

L 1  L 2  L 3  2L 2  3L 1 , (7)
and finally there is the useful inequality

3L 1 + 1  (s + 1) L 3 + 2L 2 . (8)
(Upper bound) At the end of some fixed round Cinderella leaves three nonempty buckets, say buckets 1, 2, 3. She maintains the following three invariants.

x i < L 3 for 1  i  3 (9a)
x(i, j) < 2L 2 for 1  i < j  3 (9b)

x(1, 2, 3) < 3L 1 (9c)

Then the Stepmother moves, and raises the bucket contents to y 1 , y 2 , . . . , y 3s+4 . By invariant (9c) the overall amount of water in the system is bounded by

3s+4 X j=1 y j < 3L 1 + 1. (10)
A bucket i with y i L 3 is called large. A triple is a group of three consecutive buckets i, i + 1, i + 2 in the circle. A triple is called good, if (i) none of its buckets is large and (ii)

y(i, i + 1, i + 2) < 2L 2 .
If Cinderella empties all buckets outside a good triple, she automatically maintains the invariants. Hence we assume from now on that there is no good triple.

Lemma 4. If there is no good triple, then there also are no large buckets.

Proof. We distinguish several cases on the number `of large buckets. The overall amount of water in the system is at least `L3 , and below 3L 1 + 1 by (10). By using ( 8) and ( 7) this yields

`L3 < 3L 1 + 1  (s + 1) L 3 + 2L 2  (s + 3) L 3 .
Therefore ` s + 2. If `= s + 2 and at most two of the buckets 1, 2, 3 are large, then (9b) implies that the overall amount W of water in the large buckets satisfies

(s + 2)L 3  W < 2L 2 + 1,
which contradicts [START_REF] Hurkens | How Cinderella won the bucket game (and lived happily ever after)[END_REF]. If `= s + 2 and all three buckets 1, 2, 3 are large, then these s + 2 large buckets divide the 2s + 2 non-large buckets into at most s nonempty intervals along the circle. One of these intervals contains at least three non-large buckets, and hence a non-good triple whose total contents is at least 2L 2 . Then the overall amount W of water in the large buckets plus the water in this non-good triple satisfies

(s + 2)L 3 + 2L 2  W < 3L 1 + 1,
which contradicts [START_REF] Woeginger | Combinatorics problem C5. Problem Shortlist of the 50th International Mathematical Olympiad[END_REF]. In the remaining cases we have ` s + 1.

If ` 1, the large buckets divide the 3s + 4 `non-large buckets into ìntervals along the circle. If an interval consists of k non-large buckets, we can find bk/3c pairwise disjoint triples in this interval. It can be seen that altogether we find at least s + 2 `pairwise disjoint triples in all `intervals. Each of these triples is non-good and has total contents at least 2L 2 . By applying (10) the total contents W of all buckets satisfies

`L3 + 2L 2 (s + 2 `)  W < 3L 1 + 1.
Since L 3 2L 2  0, the expression in the left hand side is decreasing in `. Together with ` s + 1 this yields (s + 1) L 3 + 2L 2 < 3L 1 + 1, which contradicts [START_REF] Woeginger | Combinatorics problem C5. Problem Shortlist of the 50th International Mathematical Olympiad[END_REF]. This leaves `= 0 as the only possible case. u t By the lemma there is no large bucket, and we see that all buckets a priori satisfy invariant (9a). Consider a fixed bucket i, and divide the remaining 3s + 3 buckets into s + 1 non-good triples. Then

y i + (s + 1) • 2L 2  3s+4 X j=1 y j < 3L 1 + 1 = (2s + 3) L 2 ,
which implies y i < L 2 . Hence any pair of buckets satisfies invariant (9b). By averaging, there exists a triple of buckets whose total contents is

y j + y j+1 + y j+2 < 3 • 3L 1 + 1 3s + 4 = 3L 1 .
Cinderella empties all buckets except this triple, and thereby also fulfills invariant (9c).

(Lower bound) The first phase of the balancing Stepmother ends with three buckets (say buckets 1, 2, 3) having contents very close to L 1 . The second phase goes through two further rounds.

In the first of these rounds, the Stepmother selects the set T 1 to contain all buckets except the buckets 3i + 1 with i = 1, . . . , s + 1. Then T 1 contains 2s + 3 buckets which the Stepmother all brings to contents L 2 . Cinderella leaves a set S 2 of two buckets with contents L 2 ; these two buckets are either adjacent (say 1 and 2) or separated by a single other bucket (say buckets 3s + 4 and 2).

In the second round, the Stepmother selects the set T 2 to contain the two buckets in set S 2 together with the buckets 3i + 2 with i = 1, . . . , s. Then T 2 consists of s + 2 buckets which the Stepmother all brings to contents L 3 . Cinderella must leave one bucket with contents L 3 at the end of the round. [START_REF] Dietz | Two algorithms for maintaining order in a list[END_REF] The proof of Theorem 4 (Upper bound) Assume that in the game BG(9, 5), Cinderella leaves a bucket configuration that satisfies the following four invariants.

x i < 299/525 ⇡ 0.569 for 1  i  9 (11a)

x(S) < 124/175 ⇡ 0.708 for all S with |S| = 2 (11b)

x(S) < 27/35 ⇡ 0.771 for all S with |S| = 3 (11c)

x(S) < 4/5 = 0.800 for all S with |S| = 4 (11d)

The Stepmother moves and raises the bucket contents from x 1 , . . . , x 9 to y 1 , . . . , y 9 . Note that P 9 i=1 y i < 9/5 by (11d). A quadruple is a set of four consecutive buckets in the circle. A quadruple is called good, if its four buckets satisfy (11a)-(11d). If there is a good quadruple, then Cinderella can maintain the invariants by emptying all buckets outside the quadruple. Lemma 5. If y j 299/525 for some j, then Cinderella can maintain the invariants.

Proof. A bucket j with y j 299/525 =: L is called large. If the Stepmother leaves three large buckets i, j, k, then x(i, j, k) y(i, j, k) 1 3L 1 = 124/175. This implies that x i , x j , x k all are non-zero, since otherwise two of these buckets would have violated (11b). Hence i, j, k all belong to the quadruple that Cinderella did not touch in the preceding round. If Cinderella empties this quadruple (together with some fifth bucket), the remaining volume of water decreases to 9/5 3L < 124/175, and all invariants are maintained.

If the Stepmother leaves two large buckets i and j, then Cinderella empties these large buckets (together with three other buckets). The remaining volume of water decreases to 9/5 2L < 124/175, and all invariants are maintained.

Finally assume that the Stepmother leaves a single large bucket, which without loss of generality is bucket 1. Then y(2, 3, 4, 5) + y(6, 7, 8, 9)  9/5 L < 2 • 124/175, which implies that one of the quadruples 2, 3, 4, 5 and 6, 7, 8, 9 must be good. u t Lemma 6. If y j 62/175 for some j, then Cinderella can maintain the invariants.

Proof. By the preceding lemma we assume y i < 299/525 for all i. We assume furthermore that bucket 1 with y 1 62/175 is the fullest bucket, and that the quadruples 2, 3, 4, 5 and 6, 7, 8, 9 both are non-good (so that the total contents of either quadruple is at least 124/175). If the quadruple 2, 3, 4, 5 violates (11c) or (11d), then we would get the contradiction . Now (11c) implies that T contains all the four buckets that Cinderella did not touch in the preceding round. By emptying this quadruple (together with some fifth bucket), the remaining volume of water goes below 124/175 and all invariants are maintained. u t By the above lemmas we assume from now on y i < 62/175 for all i, so that invariants (11a) and (11b) become harmless. Consider an arbitrary bucket k, and consider the partition of the remaining eight buckets into two quadruples T 1 and T 2 , so that

y k < 9/5 y(T 1 ) y(T 2 ). (12)
We may assume that both quadruples T 1 and T 2 are non-good. Then the lower bounds y(T 1 ), y(T 2 ) 27/35 and (12) together yield y k < 9/35. Since k was an arbitrary bucket, this means that every bucket triple satisfies (11c), which also makes invariant (11c) harmless. Since T 1 and T 2 are non-good, we now conclude y(T 1 ), y(T 2 ) 4/5. But then (12) yields y k < 1/5 for all k, and any move of Cinderella will maintain all invariants. This completes the proof.

(Lower bound) The first phase of the balancing Stepmother ends with four consecutive buckets (say buckets 1, 2, 3, 4) having contents very close to 1/5. The second phase goes through three further rounds.

In the first of these rounds, the Stepmother uses set T 1 = {1, 2, 3, 4, 6, 7, 8} with all buckets except 5 and 9. The Stepmother brings every bucket in T 1 to contents 9/35. Cinderella leaves a set of four buckets, at least three of which are in T 1 . These three buckets are either adjacent (say 2, 3, 4 in this first case) or separated by a single empty bucket (say 3, 4, 6 in the second case).

In the second round the Stepmother selects the set T 2 to contain five buckets; in the first case she uses T 2 = {2, 3, 4, 7, 8} and in the second case T 2 = {3, 4, 6, 7, 8}. The Stepmother brings every bucket in T 2 to contents 62/175. Cinderella leaves a set of four buckets, at least two of which are in T 2 . We rename the buckets so that 1 and b 2 {2, 3, 4} keep their contents 62/175.

In the third round the Stepmother uses T 3 = {1, b, 6}, and fills these three buckets up to level 299/525. Cinderella must leave at least one such bucket with contents 299/525 at the end of the round. have no idea how to settle Conjecture 2. In fact, we cannot even settle the special case F (13, 2) = 137/60. The games BG(n, 2) with odd n  11 can be handled by certain types of invariant systems that we understand very well; all these systems are built around subsets of pairwise non-adjacent buckets that follow a certain pattern. With the help of YICES we can prove that the most natural generalization of this pattern to BG(13, 2) will not work out, since there exist situations where Cinderella cannot maintain the corresponding invariants.

Final remarks

We have settled all bucket games BG(n, c) with n  12. Some of our smaller results started to grow together, and eventually resulted in general theorems that cover large families of games (as for instance the families in Theorem 3 and Theorem 7). There remain many open questions, and in particular there remains our tantalizing Conjecture 2.

All our lower bounds have been derived by a suitable balancing Stepmother strategy (sometimes in combination with monotonicity). For many games, we performed extensive computer experiments and used backtracking algorithms (written in Haskell) to detect the strongest balancing Stepmothers; this boils down to checking a huge but finite number of cases. For some of the considered games it was far from clear how to choose the right system of invariants, and several attempts were required before finding the right choice. For experimenting with such invariants it was convenient to use an SMT solver (Satisfiability Modulo Theories) which checks the satisfiability of any Boolean formula on linear inequalities. Note that this goes far beyond linear programming, as in linear programming the set of constraints is the conjunction of a set of linear inequalities, whereas in SMT any combination of disjunctions and conjunctions is allowed. Now I is an invariant system for Cinderella if the formula

I ^ X i y i = 1 + X i x i ! ^ î y i x i ! ^_ j ¬I j
is unsatisfiable. Here the formula I j (1  j  n) is obtained from I as follows. For i = j + 1, . . . , j + c every occurrence of x i is replaced by 0, and for the remaining indices i every occurrence of x i is replaced by y i . Our approach was to check this by the SMT solver YICES for several candidates for I. If this formula is unsatisfiable, we have proved the invariance and thereby derived an upper bound on F (n, c); if it is satisfiable then YICES provides the corresponding values of x i and y i that can be interpreted as a counterexample for the invariance. Internally, YICES works with rational numbers in unbounded precision, and typically the proof trees consist of thousands of indigestible case distinctions, but are found within at most a few seconds.

Lemma 1 .

 1 F ( n, c) = F (n, c) for all integers 1.

Theorem 1 .Theorem 3 .

 13 F (c + 1, c) = 1/c holds for all c 1.Proof. (Upper bound) As invariant, Cinderella always leaves a single bucket untouched whose contents is below 1/c. The Stepmother adds one liter to the system and increases the total amount of water to less than (c + 1)/c. By averaging, one of the c + 1 buckets has contents below 1/c, and that's the bucket that Cinderella does not touch in her move.(Lower bound) In her first phase, the balancing Stepmother brings the contents of all buckets arbitrarily close to 1/c. ⇤ Theorem 2. F (c + 2, c) = (2c + 4)/(c 2 + 3c) holds for all odd c 1, and F (c + 2, c) = 2/c holds for all even c 2. The values F (c + 3, c) behave as follows for c 1.

  (i) F (3s + 2, 3s 1) = 1/s (ii) F (3s + 3, 3s) = 1/s (iii) F (3s + 4, 3s + 1) = (s + 1)(6s + 11) (s + 2)(2s + 3)(3s + 1) Theorem 4. F (9, 5) = 299/525.

y 1 +

 1 y(2, 3, 4, 5) + y(6, 7, 8, 9) 62/175 + 27/35 + 124/175 > 9/5. Hence the quadruple 2, 3, 4, 5 contains two buckets b 1 , b 2 that violate (11b) with y(b 1 , b 2 ) 124/175. Symmetric arguments show that the quadruple 6, 7, 8, 9 contains two buckets b 3 , b 4 with y(b 3 , b 4 ) 124/175. Let T = {1, b 1 , b 2 , b 3 , b 4 } and note x(T ) y(T ) 1 27/35

Question 1 .Conjecture 3 .

 13 Does every value F (n, c) result from an adversary argument with a balancing Stepmother (in combination with monotonicity)?A positive answer to Question 1 would also imply the truth of the following conjecture. The function F (n, c) only takes rational values, and is Turingcomputable.

Table 1 .

 1 Summary of the values F (n, c) for n  12 buckets. For the entries with n  10, we even have proofs constructed by humans.

		25/12	1	5/9	1/4	-	-	-	-	-	-
	6	137/60	3/2	1	1/2	1/5	-	-	-	-	-
	7	49/20	3/2	1	17/30 7/20	1/6	-	-	-	-
	8 363/140	11/6	1	1	1/2	1/3	1/7	-	-	-
	9 761/280	11/6	3/2	1 299/525 1/2	9/35 1/8 -	-
	10 7129/2520	25/12	3/2	1	1	5/9 69/196 1/4 1/9	-
	11 7381/2520	25/12	3/2	1	1	77/135 1/2 1/3 11/54 1/10
	12 83711/27720 137/60 11/6	3/2	1	1	5/9 1/2 1/3	1/5

Below the half-diagonal

By definition the games BG(n, c) below the half-diagonal satisfy n 2c. For these games the harmonic sums H k = 1 + 1 2 + 1 3 + 1 4 + . . . + 1 k seem to play a major role. The following theorem has been observed before by Dietz & Sleator [START_REF] Dietz | Two algorithms for maintaining order in a list[END_REF] and Chrobak & al. [3].

Theorem 5. F (n, 1) = H n 1 holds for all n 2. Proof. (Upper bound) Let x i denote the contents of bucket i at the beginning of some round. We argue that Cinderella can maintain the following invariants.

for all bucket sets T (13)

The Stepmother raises the bucket contents to y 1 , . . . , y n , and we assume that y n y i for all i. Then for any bucket set T ✓ {1, . . . , n 1} we have

Therefore Cinderella can maintain the invariants by emptying the fullest bucket n. By applying (13) to a single bucket set T = {i}, we get that all buckets satisfy x i < H n 1 .

(Lower bound) In the first phase, the balancing Stepmother brings the filling level of all buckets very close to 1. The first phase terminates with a set S 1 of n 1 buckets with contents L 1 ⇡ 1. In the second phase, the Stepmother always chooses T r := S r as the set of the n r currently fullest buckets (which Cinderella could not empty in the preceding round), and fills all of them to level L r+1 = 1 + H n 1 H n r 1 . Then at the end of round n 2 Cinderella has left a bucket of contents H n 1 . ⇤ Theorem 6. (i) F (7, 2) = 3/2 and (ii) F (9, 2) = 11/6. Theorem 7. F (n, c) = 1 holds for all n and c with 2  n/c < 3.

The proof of Theorem 6 and the (long and technical) proof of Theorem 7 can be found in the full version of this paper. Note that the theorems in this section together with the monotonicity property imply all entries for n  10 below the half-diagonal of Table 1. Furthermore Theorem 7 covers the cases with bn/cc = 2 for the following clean and natural conjecture. If true, then this conjecture (in combination with Theorem 5) would determine all values of F (n, c) below the half-diagonal. Note that the monotonicity Lemma 2 yields F (n, c) F (bn/cc , 1), and that therefore the hard part of the conjecture is to come up with the right systems of invariants. Unfortunately, we