Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
sav08:using_automata_to_decide_ws1s [2012/05/15 12:46] vkuncak |
sav08:using_automata_to_decide_ws1s [2012/05/15 12:48] vkuncak |
||
|---|---|---|---|
| Line 14: | Line 14: | ||
| \] | \] | ||
| - | Instead of $e(F)(D,\alpha(w))={\it true}$ we write for short $w \models F$. | + | Instead of $e(F)(D,\alpha(w))={\it true}$ we write for short $w \models F$. So, we design automata so that: |
| + | \[ | ||
| + | w \in L(A(F)) \ \ \ \iff \ \ \ w \models F | ||
| + | \] | ||
| The following lemma follows from the definition of semantic evaluation function 'e' and the shorthand $w \models F$. | The following lemma follows from the definition of semantic evaluation function 'e' and the shorthand $w \models F$. | ||