Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision | ||
|
using_automata_to_decide_presburger_arithmetic [2009/04/29 10:50] vkuncak |
using_automata_to_decide_presburger_arithmetic [2009/04/29 10:55] vkuncak |
||
|---|---|---|---|
| Line 22: | Line 22: | ||
| ===== Automata for Presburger Arithmetic Formulas ===== | ===== Automata for Presburger Arithmetic Formulas ===== | ||
| - | **Automaton for formula:** $x = y + v \land z = y + v\ land v=1$ accepts certain strings in alphabet $\{x,y,z,v\} \to \{0,1\}$. An example word that this automaton accepts: | + | **Automaton for formula:** $x = y + v \land z = y + v$ accepts certain strings in alphabet $\{x,y,z,v\} \to \{0,1\}$. An example string that this automaton accepts can be represented as follows: |
| x: 0 0 1 0 0 | x: 0 0 1 0 0 | ||
| y: 1 1 0 0 0 | y: 1 1 0 0 0 | ||
| z: 0 0 1 0 0 | z: 0 0 1 0 0 | ||
| v: 1 0 0 0 0 | v: 1 0 0 0 0 | ||
| - | If we take the valid formula | + | This string represents the satisfying assignment $\{(x,4),\ (y,3),\ (z,4),\ (v,1)\}$ for the above formula. If we take the valid formula |
| \[ | \[ | ||
| \lnot (x = y + v \land z = y + v\ \land\ v=1)\ \lor\ (x = z) | \lnot (x = y + v \land z = y + v\ \land\ v=1)\ \lor\ (x = z) | ||
| Line 83: | Line 83: | ||
| Therefore, to check if $F$ is satisfiable, we construct $A(F)$ automaton and check whether the graph of $A(F)$ has a reachable accepting state. | Therefore, to check if $F$ is satisfiable, we construct $A(F)$ automaton and check whether the graph of $A(F)$ has a reachable accepting state. | ||
| + | **Example:** Step-by-step construction of automaton for | ||
| + | \[ | ||
| + | \lnot (x = y + v \land z = y + v\ \land\ v=1)\ \lor\ (x = z) | ||
| + | \] | ||