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 | ||
|
tree_automata [2010/05/25 15:32] vkuncak |
tree_automata [2010/05/27 18:10] vkuncak |
||
|---|---|---|---|
| Line 60: | Line 60: | ||
| Projection. | Projection. | ||
| + | |||
| ===== Weak Monadic Logic of Two Successors (WS2S) ===== | ===== Weak Monadic Logic of Two Successors (WS2S) ===== | ||
| Line 81: | Line 82: | ||
| where $succ0$ takes a tree node and finds its left child: | where $succ0$ takes a tree node and finds its left child: | ||
| \[ | \[ | ||
| - | \alpha(succ) = \{ (\{w\},\{w0\}) \mid w \in \Sigma^* \} | + | \alpha(succ0) = \{ (\{w\},\{w0\}) \mid w \in \Sigma^* \} |
| \] | \] | ||
| and where $succ1$ takes a tree node and finds its right child: | and where $succ1$ takes a tree node and finds its right child: | ||
| \[ | \[ | ||
| - | \alpha(succ) = \{ (\{w\},\{w1\}) \mid w \in \Sigma^* \} | + | \alpha(succ1) = \{ (\{w\},\{w1\}) \mid w \in \Sigma^* \} |
| \] | \] | ||
| The meaning of formulas is then given by standard [[sav08:First-order logic semantics]]. | The meaning of formulas is then given by standard [[sav08:First-order logic semantics]]. | ||
| + | |||
| ===== Deciding WS2S ===== | ===== Deciding WS2S ===== | ||
| A construction is similar to one for WS1S and is possible thanks to closure properties of finite automata. | A construction is similar to one for WS1S and is possible thanks to closure properties of finite automata. | ||
| + | |||
| + | Examples: | ||
| + | * subset | ||
| + | * successor | ||
| ===== Verification of Trees ===== | ===== Verification of Trees ===== | ||