LARA

Using Automata to Decide WS1S

Consider a formula $F$ of WS1S. Let $V$ be a finite set of all variables in $F$. We construct an automaton $A(F)$ in the finite alphabet

\begin{equation*} \Sigma = \Sigma_1^V \end{equation*}

for $\Sigma_1 = \{0,1\}$ such that the following property holds: for every $w \in \Sigma^*$,

$w \in L(A(F))$ iff $e(F)(D,\alpha(w))={\it true} \ \ \ \ \ \ (*)$

where $\alpha(w)$ is an interpretation of WS1S (mapping variables $V$ to finite sets) defined by

\begin{equation*} \alpha(a_0 \ldots a_n)(v) = \{ i \mid 0 \le i \le n \land a_i(v) = 1 \} \end{equation*}

Instead of $e(F)(D,\alpha(w))={\it true}$ we write for short $w \models F$. So, we design automata so that:

\begin{equation*} w \in L(A(F)) \ \ \ \iff \ \ \ w \models F \end{equation*}

The following lemma follows from the definition of semantic evaluation function 'e' and the shorthand $w \models F$.

Lemma: Let $F,F_i$ denote formulas, $w \in \Sigma^*$. Then

  • $w \models (F_1 \lor F_2)$ iff $w \models F_1$ or $w \models F_2$
  • $w \models \lnot F$ iff $\lnot (w \models F)$
  • $w \models \exists x.F$ iff $\exists b. patch(w,x,b) \models F$
   .......   
   .......  0
   .......
   bbbbbbbbbbbbbb
   .......   
   .......  0
   .......
   _______
      w
   ______________
    patch(w,x,b)

Let $w = w_1 \ldots w_n$ where $w_i \in \Sigma$ and $b = b_1 \ldots b_m$ where $b_j \in \Sigma_1$. Let $N=\max(n,m)$. Define $patch(w,x,b) = p_1 \ldots p_N$ where $p_i \in \Sigma$ such that

\begin{equation*} 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. \end{equation*}

We define the automaton by recursion on the structure of formula.

Case $A(x \subseteq y)$:

Case $A(succ(x,y))$:

Case $A(F_1 \lor F_2)$:

Case $A(\lnot F)$:

Example: Use the rules above to compute (and minimize) the automaton for $\lnot ((\lnot (X \subseteq Y)) \land (\lnot (Y \subseteq X)))$.

Proof of correctness if by induction. For example, for disjunction we have:

  • $w \in L(A(F_1 \lor F_2))$
  • $w \in L(A(F_1) \sqcup A(F_2)))$
  • $w \in L(A(F_1)) \lor w \in L(A(F_2))$, so by I.H.
  • $w \models F_1\ \lor\ w \models F_2$, so by Lemma above,
  • $w \models (F_1 \lor F)$

Existential Quantification

Case $A(\exists x.F)$:

To maintain the equivalence $(*)$ above, we need that for every word,

\begin{equation*} w \in L(A(\exists x.F)) \end{equation*}

iff

\begin{equation*} \exists s \in \Sigma_1^*.\ patch(w,x,s) \in L(A(F)) \end{equation*}

Given a deterministic automaton $A(F)$, we can construct a deterministic automaton accepting $\{ w \mid \exists s \in \Sigma_1^*.\ patch(w,x,s) \in L(A(F)) \}$ in two steps:

  • take the same initial state
  • for each transition $\delta(q,w)$ introduce transitions $\delta(q,w[x:=b])$ for all $b \in \Sigma_1$
  • initially set final states as in the original automaton
  • if $q$ is a final state and $zero_x \in \Sigma$ is such that $zero_x(v)=0$ for all $x \neq v$, and if $\delta(q',zero_x)=q$, then set $q'$ also to be final

Example 1: Compute automaton for formula $\exists X. \lnot (X \subseteq Y)$. 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 $\exists Y. (X < Y)$ where $<$ is interpreted treating $X,Y$ as digits of natural numbers. Also compute the automaton for the formula $\exists X. (X < Y)$.

Define less-than relation in MONA and encode this example.

References