Kozen D.C. Theory of Computation

Подождите немного. Документ загружается.

Automata on Inﬁnite Strings and S1S 157

Muller Automata

To correct this inadequacy, we generalize the acceptance condition as fol-

lows. Instead of a set of accept states F ,wedesignateaset of sets of states

F;thatis,F ⊆ 2

. We think of the sets in F as the “good” IO sets. We

deﬁne a run σ to be accepting if IO(σ) ∈ F. The new acceptance condition

is called Muller acceptance, and this type of automaton is called a Muller

automaton [89].

Every B¨uchi automaton is a Muller automaton: take F = {A ⊆ Q |

A ∩ F = ∅}. We show in Lectures 26 and 27 that nondeterministic B¨uchi

automata, nondeterministic Muller automata, and deterministic Muller au-

tomata are all equivalent. For the remainder of this lecture, we assume this

has been done. We use the equivalence between deterministic and nonde-

terministic Muller automata to eliminate existential quantiﬁers in S1S.

Encoding S1S with Automata

B¨uchi showed that S1S was decidable by reducing it to the emptiness prob-

lem for nondeterministic B¨uchi automata [23, 24]. In fact, S1S and nonde-

terministic B¨uchi automata are equivalent in expressive power.

To make sense of this statement, let us represent a set A ⊆ ω by its

characteristic string, the inﬁnite string over {0, 1} with a 1 in position i iﬀ

i ∈ A. For example, the characteristic strings of the sets {multiples of 3}

and {primes} are

100100100100100100100···,

001101010001010001010···,

respectively. We represent an element a ∈ ω as we would the singleton {a}.

For example, we would represent the number 4 as the string

000010000000000000000···.

For a tuple a

,... ,a

,... ,A

∈ ω

× (2

)

, the characteristic

string is a string over the alphabet {0, 1}

m+n

. Think of the string as divided

into m + n tracks, each of which contains the characteristic string of one

of the a

or A

. For example, the characteristic string of the 5-tuple

3, 5, {even numbers}, {multiples of 3}, {primes}

would be

0001000000000000000000000000

0000010000000000000000000000

1010101010101010101010101010 ··· .

1001001001001001001001001001

0011010100010100010100010000

158 Lecture 25

Theorem 25.3 (i) Let ϕ(x, X) be a formula of S1S with free individual variables among

x = x

,... ,x

and free set variables among X = X

,... ,X

.There

exists a Muller automaton M

over alphabet {0, 1}

m+n

such that

L(M

)={(a, A) | ϕ(a, A) is true},

where

a = a

,... ,a

and A = A

,... ,A

(ii) For any nondeterministic B¨uchi automaton M over the alphabet

{0, 1}, there is a formula ϕ

(X) of S1S such that ϕ

(A) is true

iﬀ M accepts the characteristic string of A.

Proof. We only prove (i), leaving (ii) as an exercise.

To prove (i), we proceed by induction on the structure of the given

formula ϕ. Any atomic formula is of the form

ss ···s



 

x ∈ X

for some ﬁxed k ≥ 0. A deterministic B¨uchi automaton can be built to

read the tracks corresponding to x and X only, checking that the track

corresponding to x has a unique 1, say in position i, and that the track

corresponding to X has a 1 in position i + k. Here is the automaton for

k =3:

sssss

- - - -









(0, –) (0, –)

(1, 0) (0, –) (0, –) (0, 1)

In the label (b, c), b and c represent the input bits on the tracks correspond-

ing to x and X, respectively, and − indicates that the transition is enabled

under either bit. Transitions not shown can be assumed to go to a dead

state.

For a formula of the form

(x, X) ∧ ϕ

(x, X), (25.1)

assume that we have already constructed deterministic Muller automata

=(Q

, Σ,δ

, F

)forϕ

, i ∈{1, 2}. To get an automaton for (25.1),

we do a product construction. Let

=(Q

, Σ,δ

, F

where

def

= Q

× Q

def

=(s

((q

),a)

def

=(δ

,a),δ

,a)),

def

= {A ⊆ Q

| π

(A) ∈ F

and π

(A) ∈ F

Automata on Inﬁnite Strings and S1S 159

where π

and π

are the appropriate projections:

(A)

def

= {p ∈ Q

|∃q ∈ Q

(p, q) ∈ A}

(A)

def

= {q ∈ Q

|∃p ∈ Q

(p, q) ∈ A}.

For a formula of the form

¬ϕ(

x, X),

assume we have constructed a deterministic Muller automaton

M =(Q, Σ,δ,s,F)

for ϕ. To get an automaton for the negation, take the complement of F in

The constructions for ∨, →,and↔ are obtained by composing the

constructions above.

For a formula of the form

∃X

ϕ(x, X

,... ,X

assume we have constructed the deterministic Muller automaton M

(we

show how to do this in Lectures 26 and 27). Build a new automaton M

that on input a

,... ,a

,... ,A

nondeterministically guesses A

and

simulates M

on a

,... ,a

,... ,A

The construction for a formula of the form

∃x

ϕ(x

,... ,x

, X)

is similar, except that the automaton only guesses strings of the form 0

∗

;

that is, strings containing a single 1.

For universal quantiﬁers ∀,weusethefactthat∃xϕis equivalent to

¬∀x ¬ϕ and compose the constructions for ¬ and ∃ above.

Continuing inductively in this fashion, we can obtain a nondeterministic

B¨uchi automaton M

such that L(M

) is nonempty iﬀ the sentence ϕ is

true. For B¨uchi automata, nonemptiness can be tested by checking if there

is an accessible loop containing a state of F . 2

In Lectures 26 and 27 we discuss the relationship between B¨uchi and

Muller automata and give an eﬃcient determinization construction due to

Safra.

Undecidability of the Dyadic Theory

The monadic second-order theory of successor, which is decidable, allows

second-order quantiﬁcation only over sets (monadic predicates, unary re-

160 Lecture 25

lations). The dyadic theory, which allows quantiﬁcation over dyadic pred-

icates (binary relations), is undecidable. To show this we encode the Post

correspondence problem (PCP), a well-known undecidable problem.

An instance of the PCP consists of a pair of monoid homomorphisms

f,g :Σ

∗

→ Γ

∗

, where Σ and Γ are ﬁnite alphabets. Recall that a monoid

homomorphism is a map that satisﬁes f (xy)=f(x)f(y)andf(ε)=ε.

A solution of the instance is a string x ∈ Σ

∗

such that f(x)=g(x). Of

course, there is always the trivial solution ε; the interesting question is

whether there exists a nonnull solution. This problem is undecidable, and

we use this fact to show the undecidability of dyadic second-order theory

of successor. See [61, §9.4] for more details and a proof of undecidability

of PCP (or, if you are in a do-it-yourself mood, try Miscellaneous Exercise

96).

Let f,g be an instance of PCP with Γ = {0, 1}. We encode the problem

as a formula of dyadic S1S as follows. Let z ∈{0, 1}

∗

. Considering subsets

A ⊆ ω as inﬁnite-length strings A ∈{0, 1}

,letψ

(A, i) be the predicate,

“z is the substring of A of length |z | beginning at position i.” This predicate

is easily expressible in our language: for example,

10011

(A, i)=i ∈ A ∧ s(i) ∈ A ∧ s

(i) ∈ A ∧ s

(i) ∈ A ∧ s

(i) ∈ A.

Now let R be a dyadic predicate (binary relation) variable, and consider

the formula

ϕ(A, R)

def

= R(0, 0) ∧∀i ∀j



a∈Σ

(R(i, j) ∧ ψ

f(a)

(A, i) ∧ ψ

g(a)

(A, j)

→ R(s

|f (a) |

(i), s

|g(a) |

(j))).

If this formula is true of A, R,thenR(i, j) holds for any pair of numbers

i, j such that for some x ∈ Σ

∗

, the preﬁx of A of length i is f(x)andthe

preﬁx of A of length j is g(x); in other words,

{(|f (x)|, |g(x)|) | f(x),g(x) are preﬁxes of A}⊆R. (25.2)

Note that for each A, the intersection of all relations R satisfying ϕ(A, R)

is also a relation satisfying ϕ(A, R), and is the smallest such. For that

relation, equality holds in (25.2). Then there is a solution iﬀ the sentence

∃A ∀Rϕ(A, R) →∃i>0 R(i, i)

is true.

Lecture 26

Determinization of ω-Automata

Rabin Automata

Last time we deﬁned B¨uchi and Muller automata. Recall that in B¨uchi

acceptance, we specify a subset F ⊆ Q and call a run accepting if IO(σ) ∩

F = ∅. In Muller acceptance, we specify a set F ⊆ 2

and call a run

accepting if IO(σ) ∈ F.EveryB¨uchi automaton is a Muller automaton:

take F = {A ⊆ Q | A ∩ F = ∅}.

A third type that lies somewhere in between is Rabin automata.In

the Rabin acceptance condition, we specify a ﬁnite set of pairs (G

1 ≤ i ≤ k,whereG

and R

are subsets of Q. Think of a green light ﬂashing

every time the machine enters a state in G

and a red light ﬂashing every

time the machine enters a state in R

. A run is deﬁned to be accepting if

for some i,theith green light ﬂashes inﬁnitely often and the ith red light

ﬂashes only ﬁnitely often. Formally, a run σ is accepting if there exists an

i such that IO(σ) ∩ G

= ∅ and IO(σ) ∩ R

= ∅.

Every B¨uchi automaton is a Rabin automaton: take k =1,G

= F ,

and R

= ∅. In turn, every Rabin automaton is a Muller automaton: take

F = {A ⊆ Q |



(A ∩ G

= ∅ ∧ A ∩ R

= ∅)}.

162 Lecture 26

In this lecture and the next we show that nondeterministic and deter-

ministic Rabin automata, nondeterministic and deterministic Muller au-

tomata, and nondeterministic B¨uchi automata are all equivalent. As men-

tioned last time, deterministic B¨uchi automata are strictly weaker (Home-

work 8, Exercise 1).

We show the equivalence of all these automata by means of the inclu-

sions in the following diagram, where the arrows mean “can be simulated

by.”



nondeterministic Muller





nondeterministic Rabin deterministic Muller





deterministic Rabin

nondeterministic B¨uchi

Inclusions B and E are immediate. Inclusions C and D are straightforward

and have already been argued above.

For inclusion F, let M be a nondeterministic Muller automaton with

acceptance set F. Design a nondeterministic B¨uchi automaton N (a Rabin

automaton with a single green light) that operates as follows. On any input

x, N simulates the computation of M on x, guessing some run σ of M

nondeterministically. At some point, N nondeterministically guesses that

all states of M not in IO(σ) have already been seen for the last time. It

also guesses the IO set A and veriﬁes that A ∈ F. For the remainder of the

computation, it veriﬁes that A is indeed IO(σ). It checks that from that

point on,

• every state of σ is in A,and

• σ hits every state in A inﬁnitely often.

To do this, it continues to simulate M, marking each state that M ever

enters. If at any point M enters a state not in A, N just rejects. As soon

as all the states of A become marked, N ﬂashes its green light, erases all

the marks, and begins the process anew.

The most diﬃcult of the six inclusions is A. This was ﬁrst shown by

McNaughton in 1966 [84], but his construction was doubly exponential. A

more eﬃcient singly exponential construction was given by Safra in 1988

[107].

In order to motivate the construction, we start with an incorrect con-

struction and show why it does not work. Our attempt to rectify the sit-

Determinization of ω-Automata 163

uation leads us to a second incorrect construction that errs too far in the

opposite direction. Finally we give a correct construction.

First construction (incorrect) Let M =(Q, Σ, ∆,s,F) be a nondetermin-

istic B¨uchi automaton with n states. Recall that a nondeterministic tran-

sition function is of type ∆ : Q × Σ → 2

. Intuitively, if the machine is in

state p and sees input symbol a, then it can move to any state in ∆(p, a).

The function ∆ extends uniquely to

∆:2

× Σ

∗

→ 2

by induction as follows: for x ∈ Σ

∗

and a ∈ Σ,

∆(A, ε)

def

= A

∆(A, xa)

def



q∈∆(A,x)

∆(q, a).

It follows that

∆(p, a)=

∆({p},a)

∆(A, xy)=

∆(

∆(A, x),y).

Build a deterministic Rabin automaton N that keeps track of all the states

M could possibly be in. It starts with a single token on the start state

of M . In each step, there is a set of tokens occupying the states of N,

which mark all states M could possibly be in at that point according to

the nondeterministic choices M has made so far. On each input symbol,

N moves the tokens on M in all possible ways according to the transition

relation of M.ThusN is deterministic.

Now N must somehow decide if there is a run of M that hits a state

in F inﬁnitely often. Let us make N ﬂash a green light every time one of

the tokens on M occupies a state of F .ThusN is actually a deterministic

B¨uchi automaton.

Formally, take

N =(2

, Σ,

∆, {s},G),

where

∆ is deﬁned above, and

def

= {A ⊆ Q | A ∩ F = ∅}.

It is true that L(M) ⊆ L(N ), because if there is an accepting run of

M (that is, a run that hits F inﬁnitely often), then in N’s simulation, a

state of F is occupied by a token inﬁnitely often, therefore N ﬂashes green

inﬁnitely often, hence N accepts. Unfortunately, the reverse inclusion does

not hold. Here is a counterexample:

0, 1

ssg





164 Lecture 26

(The short arrow indicates the start state and a circle indicates an accept

state.) This automaton accepts no strings, because there is only one inﬁnite

run, and that run has IO set {s}, which does not contain a ﬁnal state.

However, the construction above gives the automaton

ssg











where the state on the left represents the set {s} and the state on the right

represents the set {s, t}. This automaton accepts the set of strings with

inﬁnitely many zeros.

Second construction (also incorrect) The problem with the previous con-

struction was that it is possible for M to hit F at inﬁnitely many time

instants, even though none of those hits occur on the same run. To remedy

this, we modify the construction to make sure that when such a situation

arises, we can always reconstruct an inﬁnite run of M that hits F inﬁnitely

often.

We describe N in terms of blue and white tokens on the states of M .It

starts with a single blue token on the start state of M . On each input sym-

bol, it moves the tokens according to the transition rules of M , preserving

colors; except that if a blue and white token both occupy a state M,then

the blue token is removed, and if a blue token occupies a state of F ,then

it is replaced by a white token. Whenever all the tokens become white, N

ﬂashes green and replaces all the white tokens with blue tokens. Again, N

is a deterministic B¨uchi automaton.

Formally, the set of states of N is 2

× 2

, where a state (B,W)ofN

represents the set of states B of M occupied by blue tokens and the set of

states W of M occupied by white tokens. Deﬁne

N =(2

× 2

, Σ,δ,({s}, ∅),G)

with

δ :2

× 2

× Σ → 2

× 2

δ((B,W),a)

def

=(B



where



def

∆(W, a) ∪ (F ∩

∆(B,a))



def

∆(B,a) − W



if B = ∅,and



def

∆(W, a) ∩ F



def

∆(W, a) − F

Determinization of ω-Automata 165

if B = ∅;and

def

= {(∅,W) | W ⊆ Q}.

The idea here is that at any green ﬂash, any token occupying any state

must have gotten there via a path through a state of F since the last green

ﬂash, because that is the only way the token could have become white. If

there are inﬁnitely many green ﬂashes, we can reconstruct an accepting run

of M (one whose IO set intersects F inﬁnitely often). We do this with the

aid of K¨onig’s lemma:

Lemma 26.1 (K¨onig’s lemma) Every inﬁnite ﬁnite-degree tree has an inﬁnite path.

Proof. If the root has inﬁnitely many descendants but only ﬁnitely many

children, then some child must have inﬁnitely many descendants. Move

down to that child and repeat the argument. In this way we can trace an

inﬁnite path down through the tree. 2

K¨onig’s lemma is false without the degree restriction. A tree consisting

of a root with countably many childen is an inﬁnite tree, all of whose paths

are ﬁnite.









Xsssssssss

··· ·

Now suppose that N ﬂashes green inﬁnitely often on input x.Atevery

green ﬂash, every state occupied by a token is accessible from a state at

the previous green ﬂash by a path segment that goes through a state of F .

Let these path segments be the edges of an inﬁnite tree whose nodes are

labeled with pairs (q, t), where t is a time instant at which N ﬂashes green

and q is a state of M occupied by a token at time t. By the construction,

every node labeled (q,t + 1) has a parent labeled (p, t), thus we have an

inﬁnite tree of ﬁnite degree. By K¨onig’s lemma, there exists an inﬁnite path

in this tree, which represents an inﬁnite run intersecting F inﬁnitely often.

The problem here is that we have erred too far in the other direction.

It is true that if N ﬂashes green inﬁnitely often on input x, then there is

an accepting run of M on x,soL(N) ⊆ L(M ), but not vice versa.

Unfortunately, it is not necessarily the case that L(M) ⊆ L(N). Here

is a counterexample:











*

166 Lecture 26

This automaton accepts a

, but the construction above gives





which does not. Here the state on the left represents the pair ({s}, ∅)and

the state on the right represents the pair ({u}, {t}).

Thus the ﬁrst construction gives a deterministic automaton that accepts

too many strings and the second too few. Next time we give a construction

due to Safra [107] that achieves a happy compromise.