Mikołaj Bojańczyk

The goal of this page is proving the following lemma.

Lemma 2. There exists a deterministic Muller automaton such that for every tree  t \in [Q]^\omega, the automaton accepts t if and only if t contains a path with infinitely many accepting edges.

Consider a tree t \in [Q]^\omega, and let n \in \Nat be some depth. Define a node to be important for depth n if it is either: the root, a node at depth n, or a node which is a closest common ancestor of two nodes at depth n. This definition is illustrated below (with solid lines representing accepting edges, and dotted lines representing non-accepting edges):

3-tree-paths

 


 

Definition of the Muller automaton. We now describe the Muller automaton for Lemma 2. After reading the first n letters of an input tree (i.e. after reading the input tree up to depth n), the automaton keeps in its state a tree, where the nodes correspond to nodes of the input tree that are important for depth n, and the edges corresponds to paths in the input tree that connect these nodes. This tree stored by the automaton is a tree with at most |Q| leaves, and therefore it has less than 2|Q| edges. The automaton also keeps track of a colouring of the edges, with each edge being marked as accepting or not, where “accepting” means that the corresponding path in the input tree contains at least one accepting edge. Finally, the automaton remembers for each edge an identifiers from the set \set{1,\ldots,2|Q|-1}, with the identifier policy being described below. A typical memory state looks like this:

summary-identifiers

The big black dots correspond to important nodes for the current depth, black edges are accepting, dotted edges are non-accepting, while the numbers are the identifiers. Note that at any given moment, all identifiers are distinct. It might be the case (which is not true for the picture above), that the identifiers used at a given moment have holes, e.g. identifier 4 is used but not 3.

The initial state of the automaton is a tree which has one node, which is the root and a leaf at the same time, and no edges. We now explain how the state is updated. Suppose the automaton reads a new letter, which looks something like this:

letter

To define the new state, we perform the following four steps.

Step 1. We first append the new letter to the tree in the state of the automaton. In the example of the tree and letter illustrated above, the result looks like this:

summary-extended

Step 2. We then eliminate paths that do die out before reaching the new maximal depth. In the above picture, this means eliminating the path with identifier 4:

summary-extended-pruned

Step 3. We eliminate unary nodes, thus joining several edges into a single edge. This means that a path which only passes through nodes of degree one gets collapsed to a single edge, the identifier for such a path is inherited from the first edge on the path. In the above picture, this means eliminating the unary nodes that are the targets of edges with identifiers 1 and 5:

summary-extended-pruned-unary

Step 4. Finally, if there are edges that do not have identifiers, these edges get assigned arbitrary identifiers that are not currently used. In the above picture, there are two such edges, and the final result looks like this:

summary-extended-pruned-unary-final

This completes the definition of the state update function. We now define the acceptance condition.


 

The acceptance condition. When executing a transition, the automaton described above goes from one tree with edges labelled by identifiers to another tree with edges labelled by identifiers. For each identifier, a transition can have three possible effects, described below:

  1. Delete. An edge can be deleted in  step 2 (it dies out) or in step 3 (it is merged with a path to the left). The identifier of such an edge is said to be deleted in the transition. Since we reuse identifiers, an identifier can still be present after a transition that deletes it, because it has been added again in step 4,  e.g. this happens to identifier 4 in the above example.
  2. Refresh. In step 3, a whole path e_1 e_2 \cdots e_n is folded into its first edge e_1. If the part e_2 \cdots e_n contains at least one accepting edge, then we say that the identifier of edge e_1 is refreshed.
  3. Nothing. An identifier might be neither deleted nor refreshed, e.g. this is the case for identifier 2 in the example.

The following fact describes the key property of the above data structure.

Fact. For every tree in [Q]^\omega, the following are equivalent:
a) the tree contains a path with infinitely many accepting edges;
b) some identifier is deleted finitely often but refreshed infinitely often.

Before proving the above fact, we show how it completes the proof of Lemma 2 at the beginning of this page. We claim that condition b) can be expressed as a Muller condition on transitions. The accepting family of subsets of transitions is

    \[\bigcup_i \Ff_i\]

where i ranges over possible identifiers, and the family \Ff_i contains a set X of transitions if
• some transition in X refreshed identifier i;
• none of the transitions in X delete identifier i.

Identifier i is deleted finitely often but refreshed infinitely often if and only if the set of transitions seen infinitely often belongs to \Ff_i, and therefore, thanks to the fact above, the automaton defined above recognises the language in the statement of Lemma 2. The rest of this page is devoted to proving the fact.


Proof of the fact.  The implication from b) to a) is straightforward. An identifier in the state of the automaton corresponds to a finite path in the input tree. If the identifier is not deleted, then this path stays the same or grows to the right (i.e. something is appended to the path). When the identifier is refreshed, the path grows by at least one accepting state. Therefore, if the identifier is deleted finitely often and refreshed infinitely often, there is some path that keeps on growing with more and more accepting states, and its limit is a path with infinitely many accepting edges.

Let us now focus on the implication from a) to b). Suppose that the tree t contains some infinite path \pi that has infinitely many accepting edges. Call an identifier active in step n if the path described by this identifier in the n-th state of the run corresponds to a prefix of the path \pi. Let I be the set of identifiers that are active in all but finitely many steps, and which are deleted finitely often. This set is nonempty, e.g. the first edge of the path \pi has corresponds always to the same identifier. In particular, there is some step n, such that identifiers from I are not deleted after step n. Let i \in I be the identifier that is last on the path \pi, i.e. all other identifiers in I describe finite paths that are earlier on \pi. It is not difficult to see that the identifier i must be refreshed infinitely often by prefixes of the path \pi.

 

Leave a Reply

Your email address will not be published.