Dfa For Presburger Arithmetic

In Automaton/Logic Connection, Symbolic Techniques, we took our first step towards presenting another perspective of computation, namely one based on mathematical logic. Specifically, in Automaton/Logic Connection, Symbolic Techniques, we demonstrated that

Boolean propositions (expressed through Boolean formulas) can be represented using binary decision diagrams (BDDs).
Each BDD b representing a Boolean formula f is a minimized DFA that recognizes the finite language of bit-strings that satisfy f.
We introduced the notion of state transition systems, which can be used to represent the behavior of many real-world systems such as synchronous hardware and even recreational games.
We showed that the allowed moves of transition systems can be encoded using Boolean formulas, based on the convention of using two classes of Boolean variables capturing the current and the next state values. Such formulas can, then, be encoded using BDDs.
We showed how to compute the set of all states reached by a transition system through logical manipulations performed on two BDDs, one representing the “present state” and another representing the “machine” (or transition system). Essentially, given these BDDs, one conjoins them and projects out the present state variables through existential quantification to obtain the next state. The present and next states are pooled, thus forming the set of all visited states. When this pool stops growing, we essentially reach a fixed-point amounting to the set of all reachable states.

We connected these ideas to the real world by demonstrating how to encode the familiar game of tic-tac-toe using BDDs, as well as computing all possible draw configurations in one fell swoop. In Basic Notions in Logic including SAT, we examined the power of machines to decide the validity of first-order logic sentences, and proved that Turing machines cannot be programmed to algorithmically carry out this decision. In Complexity Theory and NP-Completeness, we showed that
Turing machines can decide Boolean logic, but the apparent complexity is exponential (the NPC class). DFA for Presburger Arithmetic through Model Checking: Algorithms will again pursue the automaton/logic connection, but in the context of verifying reactive systems.
This section illustrates another instance of automaton-logic connection. In contrast to the undecidability of full first-order logic, there is a fragment of first-order logic called Presburger arithmetic that is decidable. A widely used decision procedure for Presburger arithmetic consists of building a DFA for the satisfying instances of Presburger formulas. In this connection, an interesting contrast with Automaton/Logic Connection is the following. BDDs are essentially DFA whose languages are a finite set of finite strings,1 with each string specifying assignments to the Boolean variables of the BDD. In contrast, the languages of the Presburger DFA built in this chapter are finite or infinite sets of finite but unbounded strings. Each string encodes the assignments to the quantified individual variables of a Presburger formula.
In this chapter we present the following results:

We define the syntax of Presburger arithmetic formulas.
We introduce, largely through examples,2 a technique by which DFA can be made to accept bit-serial presentations of tuples of natural numbers.
Using this method, we present a conversion algorithm from a given Presburger formula f to a DFA d such that the satisfying assignments for the free variables of f correspond to the language of d.
We further demonstrate that logical operations and automaton operations have a natural strong correspondence. In particular, we sketch the following results:

− The DFA for the conjunction of two Presburger formulas f1 and f2 may be obtained by first obtaining the DFA d1 and d2 for the individual formulas and then performing a DFA product construction for intersection. Similar results are obtained for disjunction and negation.
− Existential quantification can be modeled by hiding the quantified symbol from the interface of the corresponding automaton. The result may be an NFA that can then be determinized.