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
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:
− 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.