Conversion Algorithm: Presburger Formulas To Automata

Conversion algorithm: Presburger formulas to automata: Let us review the conversion algorithm presented thus far, again keeping the example (x y) = 1 in mind, referring to Figure 20.3. The machines we build employ bit-serial conventions, meaning: (i) they begin in a start state where initially it has not seen any inputs (by convention, we assume that x = y = 0). If the formula is satisfied for these

Starting DFA for ∃y.(x y) = 1:

Fig. 20.5. Obtaining the DFA for ∀x.∃y.(x y) = 1 from the DFA in Figure 20.4 through complementation, hiding, determinization, and complementation values of x and y, the start state is also a final state. In this case, since 0 0 = 1, the start state is not a final state. Furthermore, the start state gets labeled as “1.” This is because each state will be labeled by the “imbalance” between the right-hand side and the left-hand side of the equation x y = 1 divided by 2. This quantity is signed negative if the left-hand side is “heavier,” and positive if the left-hand side is “lighter.” The division by 2 happens because as far as the next bit to arrive is concerned, it will treat the imbalance as occurring in a position of half the weight. The general algorithm for handling quantifier-free formulas (matrices) is now described. Quantifications are handled as already illustrated. General equation format: The general equation we are dealing with is

a1x1 a2x2 . . . anxn = b(where a1, . . . , an, b ∈ Z).

Here Z stands for integers (positive and negative numbers). Remember that we allow x1, . . . , xn to range over Nat only.
Example: Our equation is x y = 1. Initial state rule: The initial state is always q0. In our example, the initial state is 0 (we simply express the subscript, omitting the “q” part).
State Transition Equation: Let the set of states be Q. State qc ∈ Q will evolve to state qd ∈ Q upon arrival of bit-tuple θ, written (qc, θ, qd) ∈ δ, provided the following side conditions are true:

• The state transition exists only if the LSB of the equation is satisfied. In other words, a1θ1 a2θ2 . . . anθn = c must be true. If this condition is not satisfied, the transition upon θ goes to the black hole state “BH.” Here, θ = θ1, θ2, . . . , θn. In our example, transition T3 goes to BH because the LSB of the addition 1 1 does not equal the LSB of 1. The same is the reason for T4 going to BH.
• If the above condition holds, then d = (c − a1θ1 − a2θ2 . . . − anθn) div 2.
• Consider T1 for the sake of illustration. The above equation yields 0 which is where this transition goes. Consider T5. The above equation yields -1, and so the transition goes to the BH state, because the arrival of further bits of x and y only makes the left-hand side of the equation heavier (more unbalanced).

In summary, these two equations describe: (i) how to determine whether a state transition exists, and (ii) how to decide which state the transition leads to.