# 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 1The 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.

I think language C is wrong as currently written. The existential quantifiers should be universal quantifiers.

Will check right away…rjlipton

Jeremy,

Thanks for finding the “typo”. I really appreciate your seeing the problem. Again thanks.

Dear Dick, there is a problem related to Presburger arithmetic which is worth mentioning. Consider first integer programming. This is a notorious NP complete problem. But in bounded dimension is was proved to be polynomial by Lenstra. Add one quantifier. Now the problem includes the well known Sylvester coins problem. Again in bounded dimension the problem is in P, this was proved by Ravi Kannan. Now add another quantifier. Is the problem still in P for bounded dimension for two quantifiers? for ant bounded number of quantifiers?? This is not known.

Very neat addition. So two is already unknown…rjlipton

Nice…..

You win as the shortest comment yet. Once at a POPL conference a talk when on for 30 minutes. My question was one word “pointers”. Their answer was long since their methods could not handle pointers…

Thanks for kind comment.

rjlipton

LOL

Another interesting open question is the complexity of the existential fragment of Presburger arithmetic extended with the binary “divides” predicate. Lipshitz showed decidability in 1976. (Moreover the tiniest extensions are all undecidable.)

This theory is also related to automata (of sorts), as follows: Consider a one-counter machine in which, in addition to the usual increment, decrement, and zero-test operations, one has transitions of the form “+u”, “+v”, “-w”, for various integer-valued parameters u, v, w. The “parametric reachability problem” for such machines is whether there exist values for the parameters so that, in the resulting concrete one-counter machine, a target final control state is reachable from the initial control state (with initial counter value 0), assuming the counter must always remain non-negative. This problem is in fact equivalent to the satisfiability problem for existential Presburger with divisibility and hence decidable

(see http://web.comlab.ox.ac.uk/people/Joel.Ouaknine/publications/onecounter09.pdf ),

but of unknown complexity.

The singular of “automata” is “automaton”.

Let the deterministic automata that accepts this language be {MM} . …. Translate this blog into different languages. …

rjlipton.wordpress.com/…/finite-state-automata-binary-decision-diagrams-and-presburger-arithmetic/

Musatov

One can get a better bound for the automata-theoretic approach by bounding the size of the automata in the construction. See “Bounds on the automata size for Presburger arithmetic”,

http://portal.acm.org/citation.cfm?doid=1342991.1342995

Regarding Moshe’s comment: recent work shows that one can do more than bound the size of the automata. The time taken to construct an automaton for a Presburger formula can be done in 3EXPTIME, see http://drops.dagstuhl.de/opus/volltexte/2012/3419/pdf/35.pdf

Dick, instead of adding “x is a power of 2″, add the binary predicate div_2(x,y) := “x is a power of 2 and x divides y”. There is an automaton for this predicate. The interesting fact is that (modulo coding) every regular relation is first-order definable in (N,+,div_2). This is the B\”uchi-Elgot-Trakhtenbrot theorem in a FO setting instead of in the standard WMSO setting. In this sense FO(N,+,div_2) is universal for the regular relations.

There is a systematic study of structures (such as (\N,+)) for which the domain and atomic relations are regular (modulo coding). For an overview see http://www.math.ucla.edu/~asl/bsl/1402/1402-001.ps

Could you just take y + 1 – z regarding MM?