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:48] vkuncak |
using_automata_to_decide_presburger_arithmetic [2009/04/29 10:50] vkuncak |
||
|---|---|---|---|
| Line 23: | Line 23: | ||
| **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\ land v=1$ accepts certain strings in alphabet $\{x,y,z,v\} \to \{0,1\}$. An example word that this automaton accepts: | ||
| - | 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 | If we take the valid formula | ||
| \[ | \[ | ||