Finite State Automata, Binary Decision Diagrams and Presburger Arithmetic

On the power of finite state automata

Mike Sipser is a complexity theorist who has done important research into questions surrounding the P=NP question. He is on my short list of people who might one day make a breakthrough on P=NP, partly because of the “rumor” that he does “think” about this famous problem. Partly because he is very strong problem solver. (An observation: if you do not think about a problem ever, it is really hard to solve it.) At conferences people talk about P=NP and for years the answer to the question: “but who is really thinking about P=NP?” was Mike. I hope so.

Mike is also the author of one of the best books on classic complexity theory. Well written, nice coverage, and some terrific extras that make for a great textbook. Actually one of his exercises is today’s subject. I feel that I had something to do with that exercise. I have the pleasure of knowing Mike since he was a graduate student at Berkeley. I believe I can say that I have taught some of what Mike knows–he took my complexity class at Berkeley. I certainly did not teach him all he knows. But I will take credit for teaching him something.

When I say finite automata you probably do not think “powerful”. Everything about them is easy. Their languages are closed under just about any reasonable operation. Most questions about them are decidable, and they cannot recognize even as simple a language as But they are very powerful when used properly. In future posts I will expand on this theme and show how understanding them better could be the key to solving open questions in theory. More on that in the future.

Today I want to show that we can use finite state automata to prove that Presburger arithmetic is decidable. Presburger arithmetic is the first-order theory of the natural numbers with addition. It consists of all the true sentences about the natural numbers that only involve addition. Mojzesz Presburger, a student of the famous logician Alfred Tarski, showed in his master thesis of 1928 that there was a decision procedure for his theory. While Presburger’s proof was not that difficult, afterall it used a method pioneered by his advisor, the result is of great significance today. It is believed, by many, that he should have gotten a Ph.D. for it, but Tarski apparently did not think it was enough.

Presburger Arithmetic

Presburger arithmetic is, as I said already, the first order theory of addition. Sentences in this theory can be placed into the following form by standard methods of logic:

where the quantifiers range over the natural numbers. The formula can be assumed to consist of boolean combinations of equations: note the formula has no quantifers. Each equation can involve variables and only the operation of addition. Thus,

is a legal equation. For example, the theory can define the order relation by

The following true sentence says that there are an infinite number of natural numbers:

It really says that for any there is a that is strictly larger than . The problem that Presburger solved is given a sentence from his theory determine whether or not it is true. He did this by using what is called quantifer elimination, we will present a completely different proof that uses finite state automata.

The Decision Procedure

The proof depends on the following critical insight: finite state automata can do addition. What exactly do I mean by this? Let’s try to write down a language that represents “addition”: a natural approach is the following,

where are strings that encode numbers in the usual way. Thus, stands for the number

The trouble with this language is that no finite state automata can recognize it. The issue, of course, is that the automata cannot “remember” the value of exactly after it reads the symbol .

The key is to select a clever representation so that a finite automata can recognize the language. To do this let’s consider the following language:

where is defined to be the string

Note, if one string is longer than another then just use ‘s to pad them out to the same length. Then,

Lemma 1 The language is accepted by a finite state automata.

The reason this can be done is the automata now only has to remember the value of the “carry” from the last triple of bits. This is bounded independent of the length of the numbers. Using clever representations is what Binary Decision Diagrams (BDD’s)–invented by Randy Bryant–are all about. BDDs use clever representations–just like we do. Bryant’s work has revolutionized the world of digital logic, and I will definitely devote a post to this in the future.

However, lets get back to the proof that Presburger arithmetic is decidable. As usual call a set recognized by some finite state automata regular. All of our finite state automata will be deterministic. Consider, again, the example sentence :

I will show you how to check this sentence. The general case will follow in the same manner.

The plan is this. Let be the following language:

We will show that it is regular. Then, we will consider the language

We will again show that this language is regular. Finally, consider the language

this will also be shown to be regular. Finally, we will check that this set is empty. The key point is that if is empty, then the sentence must be true. Note, the last step is easy, since deciding if a finite state automata accepts any string is doable in polynomial time (in the number of states).

It remains only to show why are all regular. Why is regular? The answer is that we make critical use of the power of nondeterminism. We know that the following language is regular:

Let the deterministic automata that accepts this language be . We will construct a new nondeterministic finite state automata for by simulating . Note, gets as input , but gets as input . So how does simulate , since it does not have ? The answer is that just guesses values for the missing ‘s. It accepts provided the guesses are correct; otherwise, it rejects. The machine shows that is regular. Of course that means that the language has a deterministic finite state automata.

The same trick handles the other set . The set is just the complement of and is even easier: recall that regular sets are closed under complements. Note, this uses that the finite state automata for is deterministic. This a is critical point: The machine that we get for the set is nondeterministic, so we must convert it to a deterministic finite state automata to satisfy our “induction”. This follows by the famous power set construction. However, the price that we pay is that for each quantifier we increase the number of states by an exponential.

Open Questions

The decision procedure we outlined here has both good and bad features. On the positive side, I think its simple and shows the power of finite automata in a way that you may not have known. Also it can prove more. For example, suppose we add to the theory of addition the predicate “ is a power of ”. Then, the new theory is still decidable. The point is that checking whether or not a binary number is a power of two can easily be done by a finite automata. Indeed we can add any predicate that can be checked by a finite automata in our representation. A more complex example is “disjointness”: two numbers and are disjoint if for each , either or is .

On the negative side the procedure we have outlined is not very efficient. Not even close. It uses the power set construct over and over. Thus, the running time is a stack of two’s: to the to a number of times that is dependent on the number of quantifiers. This is a much worse running time than the best known upper bound. I mention in passing that Mike Fischer and Michael Rabin (1974) proved that is a lower bound on the running time. I will get back to this beautiful and important result in the future.

There are two types of interesting open questions. The first concerns extensions to Presburger arithmetic. What happens if we add to Presburger predicates like “ is a prime”. Does this still have a decidable theory? The conventional wisdom is no, since the theory can easily encode the twin-prime conjecture: are the an infinite number of so that and are both prime. I believe that it remains open whether adding this predicate makes Presburger undecidable. See this for a fuller discussion. There are other extensions that would also be interesting. It is known that if one adds too powerful a new predicate, then Presburger becomes undecidable.

The second class of questions concern sub-theories of Presburger arithmetic. In modern compiler theory there are often questions about linear expressions that one needs to check. Often they can be expressed in Presburger arithmetic, but they use only a small part of the theory. Thus, an open question is to find fragments of Presburger arithmetic that have efficient decision procedures. This is an active area, but I not say anymore about it today.