Differences
This shows you the differences between two versions of the page.
Both sides previous revision Previous revision Next revision | Previous revision | ||
sav08:using_automata_to_decide_ws1s [2010/05/21 01:45] vkuncak |
sav08:using_automata_to_decide_ws1s [2012/05/15 15:38] vkuncak |
||
---|---|---|---|
Line 1: | Line 1: | ||
====== Using Automata to Decide WS1S ====== | ====== Using Automata to Decide WS1S ====== | ||
- | Consider a formula $F$ of [[weak_monadic_logic_of_one_successor|WS1S]] without quantifiers. Let $V$ be a finite set of all variables in $F$. We construct an automaton $A(F)$ in the finite alphabet | + | Consider a formula $F$ of [[weak_monadic_logic_of_one_successor|WS1S]]. Let $V$ be a finite set of all variables in $F$. We construct an automaton $A(F)$ in the finite alphabet |
\[ | \[ | ||
\Sigma = \Sigma_1^V | \Sigma = \Sigma_1^V | ||
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$. | ||
**Lemma**: Let $F,F_i$ denote formulas, $w \in \Sigma^*$. Then | **Lemma**: Let $F,F_i$ denote formulas, $w \in \Sigma^*$. Then | ||
- | * $w \models (F_1 \lor F_2)$ iff $w \models F_1$ and $w \models F_2$ | + | * $w \models (F_1 \lor F_2)$ iff $w \models F_1$ or $w \models F_2$ |
* $w \models \lnot F$ iff $\lnot (w \models F)$ | * $w \models \lnot F$ iff $\lnot (w \models F)$ | ||
* $w \models \exists x.F$ iff $\exists b. patch(w,x,b) \models F$ | * $w \models \exists x.F$ iff $\exists b. patch(w,x,b) \models F$ | ||
Line 98: | Line 101: | ||
* if $q$ is a final state and $zero_x \in \Sigma$ is such that $zero_x(v)=0$ for all $x \neq v$, and if $\delta(q',zero_x)=q$, then set $q'$ also to be final | * if $q$ is a final state and $zero_x \in \Sigma$ is such that $zero_x(v)=0$ for all $x \neq v$, and if $\delta(q',zero_x)=q$, then set $q'$ also to be final | ||
- | **Example:** Compute automaton for formula $\exists X. \lnot (X \subseteq Y)$. | + | **Example 1:** Compute automaton for formula $\exists X. \lnot (X \subseteq Y)$. MONA syntax: |
+ | var2 Y; | ||
+ | ex2 X: ~(X sub Y); | ||
+ | Command to produce dot file: | ||
+ | mona -gw $1 | dot -Tps > output.ps | ||
+ | |||
+ | **Example 2:** Compute automaton for formula $\exists Y. (X < Y)$ where $<$ is interpreted treating $X,Y$ as digits of natural numbers. Also compute the automaton for the formula $\exists X. (X < Y)$. | ||
+ | |||
+ | Define less-than relation in MONA and encode this example. | ||
===== References ===== | ===== References ===== |