The goal of this page is proving the following lemma.
Lemma 1. There exists a deterministic transducer
which outputs only trees and is invariant with respect to the universal Büchi language, i.e. if the input contains a path with infinitely many accepting edges, then so does the output and vice versa.
Consider a -dag. To make notation easier, we assume that there is a root, i.e. a vertex from which all others are reachable. This assumption can be made without loss of generality, because one can easily write a transducer which transforms every
-dag into one that has a root, and which is invariant with respect to the universal Büchi automaton.
Profiles. For a path in a
-dag, define its profile to be the word of same length over the alphabet “accepting” and “non-accepting” which is obtained by replacing each edge with its appropriate type. We consider order profiles lexicographically, with “accepting” is smaller than “non-accepting”. Call a finite path
in
optimal if it has lexicographically least profile among paths in
that have the same source and target.
Claim 1. There is a transducer
such that if the input is , then
is a tree with the same reachable vertices as in
, and such that every path from the root in
is an optimal path in
.
Proof. We use the following congruence property of optimal paths: if and
are optimal paths such that the target of
is equal to the source of
, then also their composition
is optimal. A corollary is that if we choose for every vertex in the input graph
an outgoing edge that participates in some optimal path, then the putting all of these edges together will yield a tree as in the statement of the claim. To produce such edges, after reading the first
letters, the automaton keeps in its memory the lexicographic ordering on the profiles of optimal paths lead from the root to nodes at depth
.
To complete the proof of Lemma 1, we show the following claim.
Claim 2. Let be the transducer from Claim 1. If the input to
contains a path with infinitely many accepting edges, then so does the output.
Assume that the input to the transducers contains a path with infinitely many accepting edges. Define a sequence
of finite paths in
as follows by induction. We want to preserve the invariant that each path in the sequence
can be extended to an an accepting path in the graph
. We begin with
being the edge-less path that begins and ends in the root of the tree
. This path
satisfies the invariant, by the assumption that the input
contains a path with infinitely many accepting edges. Suppose that
has been defined. By the invariant, we can extend
to an infinite path in the graph
, and therefore we can extend
to a finite path that contains at least one more accepting edge. Define
to be the unique path in the tree
which has the same source and target as the new path that extends
with at at leat one accepting edge.
Define to be the profile of the path
. We claim that the sequence of profile
has a well defined limit
This because is lexicographically smaller or equal to some extension of
. Therefore, if we take some
, then the sequence
gets lexicographically smaller and smaller, and thus it must stabilise (a few first terms in the sequence might be undefined). The stable value of the above sequence is the first letters of the limit
. Furthermore, the limit
must contain the letter “accepting” infinitely often. Toward a contradiction, suppose that
has the letter “accepting” finitely often, i.e. there is some
such that after
, only the letter “non-accepting” appears in
. Choose
so that
have profile consistent with
on the first
letters. By construction, the profile
has an accepting letter on some position after
, and this property remains true for all subsequent profiles
and therefore is also true in the limit, contradicting our assumption that
has only “non-accepting” letters after position
.
Consider the set of finite paths in the tree which have profile that is a prefix of
. This set of paths forms a tree (because it is prefix-closed). This tree has bounded degree (assuming the parent of a path is obtained by removing the last edge) and it contain paths of arbitrary finite length (suitable prefixes of the paths
). Therefore, by the Köning lemma, this tree contains an infinite path. The profile of this path
, and therefore contains infinitely many accepting edges.
Leave a Reply