MSO Logic & Automata
# MSO Logic
## Syntax
The Syntax of MSO Logic is given by;
~~~
ð ::= Lab(a,x)
| Suc(x,y)
| x â X
| False
| ÂŽ ð
| ð âĐ ð
| âx. ð
| âX. ð
~~~
Note that it's decidable and the law of excluded middle (LEM) holds.
Since LEM holds, the conversion which is true in classical logic is true.
For examples, see the following equations;
* $\forall x. \varphi == \lnot\exists x. \lnot \varphi$
* $\varphi_1 \lor \varphi_2 == \lnot(\lnot\varphi_1\land\lnot\varphi_2)$
* $\varphi_1 \Rightarrow \varphi_2 == \lnot \varphi_1 \lor \varphi_2$
## Semantics
Given a word $w$, and variable assignments $v$ ,
( i.e.
$ w = a_1 a_2 a_3 \cdots a_n $ and,
$ v $ is a fuction from variables $ \{ x,y,z, ... \} $ to the location in the word $ \{1,2,3, .., n \} $ )
the semantics of MSO Logic is defined as follows;
~~~
w,v ⧠Lab(a,x) ( w[v(x)] = 'a' )
w,v ⧠Suc(x,y) ( v(x) + 1 = v(y) )
w,v ⧠x â X ( v(x) â v(X) )
w,v ⧠Ž ð ( w,v ⧠ð is false )
w,v ⧠ð1 âĐ ð2 ( Both w,v ⧠ð1 and w,v ⧠ð2 is true )
w,v ⧠âx. ð ( There exists i â {1,..,n} , w, v[xâĶi] ⧠ð holds )
w,v ⧠âX. ð ( There exists S â {1,..,n} , w, v[XâĶS] ⧠ð holds )
~~~
# MSO-Automata Conversion
The domain of the conversion is MSO Logic formalae $\varphi$ and the codomain is an Automaton $A=(Q,ÎĢÃ2^{|fv(\varphi)|},Î,i,T)$ where $fv(\varphi)$ is free variable occuring in $\varphi$.
## $lab_a(x)$
the converted automata of $lab_a(x)$ is given as follows;
( the alphabet (a,1) means that a â ÎĢ and the position of the variable $x$ in $2^{|fv(\varphi)|}$ is 1. )
**********************************************************
* *
* *
* *
* *
* *
* *
* * * *
* .---. .---. *
* + + + + *
* \ / \ / *
* \ v \ v *
* .--. (a,1) .--. *
* -->| +---------->| |--> *
* '--' '--' *
* *
* *
* *
* *
* *
**********************************************************
## $suc(x,y)$
the converted automata of $suc(x,y)$ is given as follows;
( the alphabet (*,1,0) means that any alphabe in $\Sigma$ is OK. and the position of the variable $x$ in $2^{|fv(\varphi)|}$ is 1 and the position of $y$ is 0 . )
**********************************************************
* *
* *
* *
* *
* *
* *
* * * * *
* .---. .---. .---. *
* + + + + + + *
* \ / \ / \ / *
* \ v \ v \ v *
* .--. (*,1,0) .--. (*,0,1) .--. *
* -->| +---------->| +---------->| +--> *
* '--' '--' '--' *
* *
* *
* *
* *
* *
**********************************************************
## $x â X$
**********************************************************
* *
* *
* *
* *
* *
* *
* * * *
* .---. .---. *
* + + + + *
* \ / \ / *
* \ v \ v *
* .--. (*,1,1) .--. *
* -->| +---------->| |--> *
* '--' '--' *
* *
* *
* *
* *
* *
**********************************************************
## $ð1 âĐ ð2$
Given 2 converted automata $A_1$ and $A_2$ from $\varphi_1$ and $\varphi_2$,
the the automaton of $\varphi_1 \land \varphi_2$ is given by the "intersection" of the two automata.
## $ÂŽ ð$
Given the converted automata $A$ of $\varphi$, the automaton of $\lnot\varphi$ is given by the "complement" of $A$.
## $âx. ð$
Given the converted automata $A$ of $\varphi$, the automaton of $âx. \varphi$ is given by,
1. checking the free variable $x$ part of $A$, in order to assure that the part is '1' only once. In order to do that, we take intersection of $A$ and the following automata.
2. And then, eleminating the free variable $x$ part of the alphabet because $x$ is no longer free variable in $âx. \varphi$ .
**********************************************************
* *
* *
* * * *
* .---. .---. *
* + + + + *
* \ / \ / *
* \ v \ v *
* .--. (*,1) .--. *
* -->| +---------->| |--> *
* '--' '--' *
* *
* *
**********************************************************
## $âX. ð$
Given the converted automata $A$ of $\varphi$, the automaton of $âx. \varphi$ is given by,
eleminating the free variable $x$ part of the alphabet because the variable $x$ is no longer a free variable in $âx. \varphi$ .
# Appendix : Automata theory
Here we had better explain automata theory because given an automaton $A$, neither "intersection" of 2 automata nor "complement" of an automaton is defined but they are assumed in this post.
However, it'll be explaind in next time. And you can find these basic definitions of automata conversions in the world wide web.
e.g. see this site: https://www.inf.ed.ac.uk/teaching/courses/inf2a/slides/2014_inf2a_L04_slides.pdf.
The noting point of automata theory is, given a nondeterministic finite automata, we can always create a deterministic finite automata from it. The construction from NFA to DFA is called "subset construction", an important terminology in automata theory.
Other important ones are "trim", "(co)accessible", and so on.
Here we will explain in the next time, and just give topics.
## DFA
## NFA
## intersection
## union
## complement
## subset construction
## trim