This is an old revision of the document!
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
\[
\Sigma = \Sigma_1^V
\]
for such that the following property holds: for every
,
iff
where is an interpretation of WS1S (mapping variables
to finite sets) defined by
\[
\alpha(a_0 \ldots a_n)(v) = \{ i \mid 0 \le i \le n \land a_i(v) = 1 \}
\]
Instead of we write for short
. So, we design automata so that:
\[
w \in L(A(F)) \ \ \ \iff \ \ \ w \models F
\]
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
\[
p_i(v) = \left\{ \begin{array}{ll}
w_i(v), & \textsf{ if } v \neq x \land i \le n
0, & \textsf{ if } v \neq x \land i > n
b_i, & \textsf{ if } v=x \land i \le m
0, & \textsf{ if } v=x \land i > m
\right.
\]
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,
\[
w \in L(A(\exists x.F))
\] iff \[
\exists s \in \Sigma_1^*.\ patch(w,x,s) \in L(A(F))
\]
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.
References
- MONA tool manual (Chapter 3, page 18)