4. Distance automata

Mikołaj Bojańczyk

zajęcia / courses

The syntax of a distance automaton is the same as for a nondeterministic finite automaton, except that it has a distinguished subset of transitions, called the costly transitions. The cost of a run is defined to be the number of costly transitions that it uses. In this lecture, we prove the following theorem.

Theorem. The following problem is decidable:
• Input. A distance automaton.
• Question. Is the automaton bounded in the following sense: there is some $m \in \Nat$ such that every input word admits an accepting run of cost at most $m$ .

The problem in the above theorem is called the limitedness problem for distance automata. The goal of this lecture is to show how limitedness can be decided using the Büchi-Landweber theorem.

The limitedness game.

Let us fix a distance automaton. For a number $m \in \Nat \cup \set \omega$ , consider the following game, call it the limitedness game with bound $m$ . The game is played in infinitely many rounds $1,2,3,\ldots$ , by two players called Input and Automaton. In each round:
• player Input chooses a letter of the input alphabet;
• player Automaton responds with a set of transitions over this letter.

A set of move of player Automaton in a given round, which is a set of transitions, can be visualised as a bipartite graph, which says how the letter can take a state to a new state, with costly transitions being solid edges and non-costly transitions being dashed edges, like below:

For the definition of the game, it is important that player Automaton does not need to choose all possible transitions over the letter played by player Input, only a subset. After all rounds have been played, the situation looks like this:

The winning condition for player Automaton is the following:

in every column, an accepting state must be reachable from an initial state in the first column; and
every path contains $<m$ solid edges.

In case of $m = \omega$ , the second condition says that every path contains finitely many solid edges.

The following lemma implies the decidability of the limitedness problem.

Lemma. For a distance automaton, the following conditions are equivalent, and furthermore one can decide if they hold:

the automaton is limited;
there is some $m$ such that player Automaton wins the limitedness game with bound $m$ ;
player Automaton wins the limitedness game with bound $\omega$

It remains to prove the lemma. The implications from 2 to 1 and from 2 to 3 are immediate. For the other implications and the decidability part, the key is the observation that for every choice of $m \in \Nat \cup \set{\omega}$ , the limitedness game is a special case of a game with a finite arena and an $\omega$ -regular condition. In particular, one can apply the Büchi-Landweber theorem, yielding that a) the winner can be decided; b) the winner needs finite memory. Condition a) is used to get the decidability in the lemma, while condition b) will be used in the implication from 3 to 2.

Implication from 1 to 2.

We want to prove that if the automaton is limited, then player Automaton has a winning strategy for some finite $m$ , which will turn out to be the same $m$ as in the definition of limitedness. Here is the strategy of player automaton. Define a run $\rho$ of the distance automaton over an input word $w$ to be optimal if it has minimal cost among runs that have the same input word, same source state and same target state. The strategy of player Automaton is as follows: if the input word is $a_1 \cdots a_i$ , then in the $i$ -th round, player Automaton responds with those transitions that participate in some optimal run of cost $<m$ over the word $a_1 \cdots a_i$ . An important observation is that optimal runs are closed under prefixes, and therefore the graph produced by player Automaton in the first $i$ rounds consists of all optimal runs over the first $i$ letters of the input. This guarantees that the strategy is winning.

Implication from 3 to 2.

Suppose that player Automaton wins the limitedness game with bound $\omega$ . We will prove that player Automaton can also win the limitedness game with a finite bound.

By the Büchi-Landweber theorem, if player Automaton can win the game with bound $\omega$ , then he can also win the game with a finite memory strategy. We will show that this finite memory strategy is actually winning for a finite bound.

By unfolding the definition of a finite memory strategy in the limitedness game, there is a deterministic automaton, call it the strategy automaton, over the input alphabet of the original distance automaton, and a function $f$ from the states of the strategy automaton to sets of transitions in the origial distance automaton, such that if in the first $i$ rounds the letters produced by player Input were $a_1 \cdots a_i$ , then the response of player Automaton in the $i$ -th round is obtained by applying $f$ to the state of the strategy automaton after reading $a_1 \cdots a_i$ .

We claim that this same winning strategy produces runs where the cost is at most (number of states in the distance automaton) times (number of states in the automaton for the strategy), thus proving the implication from 3 to 2 in the lemma. To prove the claim, suppose that the strategy produces a run exceeding the above bound. This means that there is some input word $a_1 \cdots a_i$ such that the strategy maps it to a sequence of transitions $\delta_1 \cdots \delta_i$ and there exists a run $\rho$ in $\delta_1 \cdots \delta_i$ which exceeds the above bound. By a pumping argument, there must be some $k < l \le i$ such that:
a) the state of the strategy automaton is the same after $k$ and $l$ steps;
b) the state of the run $\rho$ is the same after $k$ and $l$ steps;
c) there is a costly transition in $\rho$ between steps $k$ and $l$ .
Condition a) implies that if player Input plays the word

$a_1 \cdots a_k (a_{k+1} \cdots a_l)^\omega$

then player Output will respond with the word

$\delta_1 \cdots \delta_k (\delta_{k+1} \cdots \delta_l)^\omega$

Conditions b) and c) imply that the infinite sequence of transitions above will contain a run with infinite cost, thus contradicting the assumption that the strategy is winning.

COMMENTS

Hugo

March 30, 2022

brilliant

zajęcia / courses

4. Distance automata

4. Distance automata

Leave a Reply