Differences
This shows you the differences between two versions of the page.
| Both sides previous revision Previous revision | Next revision Both sides next revision | ||
|
tree_automata [2010/05/25 15:32] vkuncak |
tree_automata [2010/05/25 15:33] vkuncak |
||
|---|---|---|---|
| Line 89: | Line 89: | ||
| 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 ===== | ||