2 - WMSO

Question 1

NFA to WMSO. Proof + example

Answer 1

Buchi I:
5 step construction:
1) Every letter comes from one single state
2) Run starts in q0
3) Successor state respects transition relation
4) Last letter leads to final state
5) (optional) there is a letter

∃ X0 … Xn | (1)∧(2)∧(3)∧(4)(∧(5) if ε ∉ L)

(1) (0 (qi -a->qj)∨(Xi(x)∧Pa(x)∧Xj(y))
(4) ∀x | last(x) –> (qi -a->qf∉Qf)∨(Xi(x)∧Pa(x))
(5) ∃x | x=x

Proof:
There are X0..Xn so that (1) - (5) hold
iff (?)
there is an accepting run of A on w ∈ L

(?):

Take single initial state from (2)
Find successors with (2)
They are unique with (3)
Accept by (4)

Question 2

WMSO to NFA. Proof + example

Answer 2

Buchi II
- Encode interpretations I:V–>Dw u P(Dw) of free variables into suitable alphabet Σv
- Assign (iductively) to every formula φ(X) (with X free) an NFA Aφ OVER Σv so that:
Sw,I ⊧ φ iff w_I ∈ L

Let φ(V) a formula with free variables V
Alphabet Σv assigns to each variable x,X ∈ V a truth value:
Σv := Σ x {0,1}^V

Identify Sw, I with w_I ∈ Σv* where

• (w_I(k))(x) := I(x) == k (1 or 0)
• (w_I(k))(X) := I(X) ∋ k (1 or 0)

This allows us to encode interpretations I into word w_I over Σv

a.k.a, the alphabet Σv will have true values at the positions where the variables are true, so we can encode sucessors and stuff. For the letters, we then use the alphabet.

1 automaton construction for each formula

SO Existential quantifier: Only project away variable (Guess content of X nondeterministically)

FO Existential quantifier: create automaton that ensures x is guesses precisely one and interect with language. Project it afterwards.

Inductive proof

Question 3

WMSO extencial quantifier projection

Answer 3

Ensures x is quesse precisely one. With the intersection of the automata, we dont need the variable in Σv, therefore we project it away

Question 4

whats the ideia behind the construction NFA -> WMSO?

Answer 4

Encode full runs, with information s about states in second order variables

Question 5

NFA -> sys eq what variable stand for?

Answer 5

Dw for FO and P(Dw) for SO

Question 6

Existential normal form form -> automata -> form with existentials that is eq to initial formula
How do we remove existential quantifiers

Answer 6

Let φ ∈ WMSO. Build Aφ using Buchi II. Build φ’ ∈ ∃WMSO from Aφ using Buchi I.