Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision Next revision | Previous revision Next revision Both sides next revision | ||
|
sav08:using_automata_to_decide_ws1s [2010/05/21 01:45] vkuncak |
sav08:using_automata_to_decide_ws1s [2011/04/12 15:09] 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 33: | Line 33: | ||
| w | w | ||
| ______________ | ______________ | ||
| - | patch(w,x,s) | + | patch(w,x,b) |
| Let $w = w_1 \ldots w_n$ where $w_i \in \Sigma$ and $b = b_1 \ldots b_m$ where $b_j \in \Sigma_1$. | Let $w = w_1 \ldots w_n$ where $w_i \in \Sigma$ and $b = b_1 \ldots b_m$ where $b_j \in \Sigma_1$. | ||
| Line 98: | Line 98: | ||
| * 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)$. |
| + | |||
| + | **Example 2:** Compute automaton for formula $\exists Y. (X < Y)$ where $<$ is interpreted treating $X,Y$ as digits of natural numbers. | ||
| ===== References ===== | ===== References ===== | ||