[next] [prev] [prev-tail] [tail] [up]

2.6 Decidable Properties for Finite-Memory Programs

The emptiness problem, the equivalence problem, the halting problem, and other decision problems for finite-memory programs or, equivalently, for finite-state transducers are defined in a similar manner as for the general class of programs.

For instance, the equivalence problem for finite-state transducers asks for any given pair of finite-state transducers whether or not the transducers compute the same relation.

Similarly, the halting problem for finite-state transducers asks for any given pair (M, x), of a finite-state transducer M and of an input x for M, whether or not M has only halting computations on x.

In this section, some properties of finite-state transducers are shown to be decidable. The proofs are constructive in nature and they therefore imply effective algorithms for determining the properties in discourse. The first theorem is interesting mainly for its applications (see Example 2.1.2). It is concerned with the problem of determining whether an arbitrarily given finite-state automaton accepts no input.

Theorem 2.6.1 The emptiness problem is decidable for finite-state automata.

Proof Consider any finite-state automaton M. M accepts some input if and only if there is a path in its transition diagram from the node that corresponds to the initial state to a node that corresponds to an accepting state. The existence of such a path can be determined by the following algorithm.

Step 1: Mark in the transition diagram the node that corresponds to the initial state of M.
Step 2: Repeatedly mark those unmarked nodes in the transition diagram that are reachable by an edge from a marked node. Terminate the process when no additional nodes can be marked.
Step 3: If the transition diagram contains a marked node that corresponds to an accepting state, then determine that L(M) is not empty. Otherwise, determine that L(M) is empty.

By definition, a program has only halting computations on inputs that it accepts. On the other hand, on each input that it does not accept, the program may have some computations that never terminate.

An important general determination about programs is whether they halt on all inputs. The proof of the following theorem indicates how, in the case of finite-memory programs, the uniform halting problem can be reduced to the emptiness problem.

Theorem 2.6.2 The uniform halting problem is decidable for finite-state automata.

Proof Consider any finite-state automaton M = <Q, , , q₀, F>. With no loss of generality, assume that the symbol c is not in , and that Q has n states. In addition, assume that every state from which M can reach an accepting state by reading nothing is also an accepting state. Let A be a finite-state automaton obtained from M by replacing each transition rule of the form (q, , p) with a transition rule of the form (q, c, p). Let B be a finite-state automaton that accepts the language { x | x is in ( {c})*, and cⁿ is a substring of x }.

M has a nonhalting computation on a given input if and only if the following two conditions hold.

The input is not accepted by M.
On the given input M can reach a state that can be repeated without reading any input symbol.

Consequently, M has a nonhalting computation if and only if A accepts some input that has cⁿ as a substring.

By the proof of Theorem 2.5.2, a finite-state automaton C can be constructed to accept the complementation of L(A). By that same proof, a finite-state automaton D can also be constructed to accept the intersection of L(B) and L(C).

By construction, D is a finite-state automaton that accepts exactly those inputs that have cⁿ as a substring and that are not accepted by A. That is, D accepts no input if and only if M halts on all inputs. The theorem thus follows from Theorem 2.6.1.

For finite-memory programs that need not halt on all inputs, the proof of the following result implies an algorithm to decide whether or not they halt on specifically given inputs.

Theorem 2.6.3 The halting problem is decidable for finite-state automata.

Proof Consider any finite-state automaton M and any input a₁ a_n for M. As in the proof of Theorem 2.3.1, one can derive for each i = 1, . . . , n the set A_{a₁ a_i} of all the states that can be reached by consuming a₁ a_i. Then M is determined to halt on a₁ a_n if and only if either of the following two conditions hold.

A_{a₁ a_n} contains an accepting state.
For no integer i such that 1 i n the set A_{a₁ a_i} contains a state that can be reached from itself by a sequence of one or more moves on transition rules.

There are many other properties that are decidable for finite-memory programs. This section concludes with the following theorem.

Theorem 2.6.4 The equivalence problem is decidable for finite-state automata.

Proof Two finite-state automata M₁ and M₂ are equivalent if and only if the relation (L(M₁) $/~\$ ) ( $/~\$ L(M₂)) = Ų holds, where denotes the complementation of L(M_i) for i = 1, 2. The result then follows from the proof of Theorem 2.5.2 and from Theorem 2.6.1.

The result in Theorem 2.6.4 can be shown to hold also for deterministic finite-state transducers (see Corollary 3.6.1). However, for the general class of finite-state transducers the equivalence problem can be shown to be undecidable (see Corollary 4.7.1).

[next] [prev] [prev-tail] [front] [up]