Using Automata to Decide WS1S
Consider a formula of WS1S. Let be a finite set of all variables in . We construct an automaton in the finite alphabet
for such that the following property holds: for every ,
where is an interpretation of WS1S (mapping variables to finite sets) defined by
Instead of we write for short . So, we design automata so that:
The following lemma follows from the definition of semantic evaluation function 'e' and the shorthand .
Lemma: Let denote formulas, . Then
- iff or
....... ....... 0 ....... bbbbbbbbbbbbbb ....... ....... 0 ....... _______ w ______________ patch(w,x,b)
Let where and where . Let . Define where such that
We define the automaton by recursion on the structure of formula.
Example: Use the rules above to compute (and minimize) the automaton for .
Proof of correctness if by induction. For example, for disjunction we have:
- , so by I.H.
- , so by Lemma above,
To maintain the equivalence above, we need that for every word,
Given a deterministic automaton , we can construct a deterministic automaton accepting in two steps:
- take the same initial state
- for each transition introduce transitions for all
- initially set final states as in the original automaton
- if is a final state and is such that for all , and if , then set also to be final
Example 1: Compute automaton for formula . 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 where is interpreted treating as digits of natural numbers. Also compute the automaton for the formula .
Define less-than relation in MONA and encode this example.
- MONA tool manual (Chapter 3, page 18)