# 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 ,

iff

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
• iff
• iff
   .......
.......  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.

Case :

Case :

Case :

Case :

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,

### Existential Quantification

Case :

To maintain the equivalence above, we need that for every word,

iff

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.