Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision | Next revision Both sides next revision | ||
using_automata_to_decide_presburger_arithmetic [2009/04/29 10:51] vkuncak |
using_automata_to_decide_presburger_arithmetic [2009/04/29 10:53] 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 string 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 |