I am programmer with a grip on automata, but not on logic.

I read in papers that the two are very tightly related. Deterministic Finite Automata (DFA), Tree Automata and Visibly Pushdown Automata are all related to Monadic Second Order Logic (MSO). Although, I understand the automata and people (in papers) have tried to explain the relation to MSO to me, they always assume a strong background in logic and an understanding of MSO.

When I look at books and courses on logic, they mostly only handle first order logic, which seems pretty simple and consisting of only a few concepts: variables, or, and, not, implies, for all, exists, etc.

Can someone explain or point me to a resource that can explain:

  1. What is second order logic in contrast to first order logic?
  2. What is monadic vs non monadic logic?
  3. Why is it important for a second order logic to be monadic to be decidable OR why is this the wrong question?
  4. Why is monadic second order logic decidable?
  5. The relation to at least DFAs?

If it is a resource it would be nice if it assumes that I am a programmer and not a logician. This means that I would like to understand how I would implement it as code, because until then math feels like magic to me ;)

Thank you for any help you can give me. I would really appreciate it.

  • $\begingroup$ "Why is it important for a second order logic to be monadic to be decidable OR why is this the wrong question?" if you allow the quantification over a binary predicate e.g. $\exists M[...M(x,y)...]$ then you immediately grab the power of First Order Logic with a single binary predicate which is already undecidable (even without functions of arity > 0, and without equality) [Kalmar, Suranyi, 1950] $\endgroup$
    – Vor
    Commented Oct 25, 2017 at 16:08

1 Answer 1

  1. What is second order logic in contrast to first order logic?
  2. What is monadic vs non monadic logic?

Monadic second-order logic is first-order logic plus quantification over sets. So, as well as being able to say that there exists a domain element with some property ($\exists x\dots$), you can also say that there exists a set of domain elements with some property. So, for example, we can define 3-colourability of graphs by saying

\begin{align*} \exists R\,\exists G\,\exists B\, \big[&\forall x\,\big(x\in R\lor x\in G\lor x\in B\big)\\ &\land \neg\exists x\,\big((x\in R\land x\in G) \lor (x\in G\land x\in B) \lor (x\in B\land x\in R)\big)\\ &\land \forall x\,\forall y\,\big(E(x,y)\rightarrow \neg \big((x\in R\land y\in R)\lor (x\in G\land y\in G)\\ &\qquad\qquad\qquad\qquad\qquad\quad\lor (x\in B\land y\in B)\big)\big)\big]\,. \end{align*}

In words, there are colours red, green and blue such that

  • every vertex has a colour
  • and no vertex has two colours
  • and, if there's an edge between two vertices, those two vertices don't have the same colour.

General second-order logic allows not just quantification over sets but also over arbitrary relations over the domain. Recall that a relation is a set of $k$-tuples over the domain, for some $k$. Sets are just unary relations: $k=1$ and a $1$-tuple is just an element of the domain.

  1. Why is it important for a second order logic to be monadic to be decidable OR why is this the wrong question?

  2. Why is monadic second order logic decidable?

Honestly, I don't remember the decidability issues. A key point is that full second-order logic lets you quantify into existence a linear order of the domain

\begin{align*} \exists R\,\forall x\,\forall y\,\forall z\,\big[&(R(x,y)\lor R(y,x)\big)\\ &\big((R(x,y)\land R(y,x))\rightarrow x=y\big)\\ &\big((R(x,y)\land R(y,z))\rightarrow R(x,z)\big)\big]\,. \end{align*}

That is, there exists a binary relation that is total, antisymmetric and transitive, i.e., is a linear order on the domain $D$. That implicitly gives you a linear order on $D^n$ for any $n$, and you can use relations on $D^n$ for large enough $n$ to simulate a Turing machine tape. But, with monadic SO, you can't do any of these things.

(I guess that, if your domain is infinite, you probably need to specify in addition that the linear order is discrete and has a minimal element; then you know that it has an initial segment that's isomorphic to the natural numbers, and that should be enough.)

On finite inputs, the existential fragment of SO – formulas of the form $\exists R_1\dots \exists R_k\,\varphi$, where the $R_i$ are relation symbols and $\varphi$ is first-order – defines exactly NP. Full second-order logic defines exactly the polynomial hierarchy. This is exactly because of the ability to encode Turing machines and the fact that quantifying a fixed collection of relations gives you a polynomial amount of stuff to play with.

  1. The relation to at least DFAs?

We can represent strings over some finite alphabet $\Sigma$ by relational structures. The vocabulary has a binary relation symbol $\leq$ that will be interpreted as a linear order, and a unany relation symbol $R_a$ for each character $a\in\Sigma$. Each element of the domain is a character in the string, the linear order tells you what order the characters appear in and the relations $R_a$ tell you what character appears in each position.

Now, suppose we have a DFA with $k$ states and let's assume we're dealing with finite strings, for now. We can write a formula that's broadly similar to the three-colourability formula above that says that our DFA accepts the string coded by its input. It says that there are sets (of domain elements, i.e., positions in the string) $Q_1, \dots, Q_k$, such that $Q_i$ will be the set of positions in the string at which the automaton is in state $i$. So assert that:

  • each position $j$ is in exactly one of $Q_1, \dots, Q_k$;
  • the first position is in $Q_1$ (assuming this is the start state);
  • if the $j$th position is in $Q_i$ then the $(j+1)$th position is in whatever state the automaton's transition function says it should be;
  • the final position is in an accepting state.

If this formula is true, the automaton must accept the string; if it's false, the automaton must reject. For NFAs, we just say that each position is in at least one state and the final state is in at least one accepting state. For infinite inputs, we can code, e.g., the Büchi condition by saying "for all positions $j$ in the input, if $j$ is in an accepting state, there's some $j'>j$ such that $j'$ is also in an accepting state.

Right now, I don't recall the proof of the converse (that everything definable in MSO can be recognized by an appropriate automaton). If I have time, I'll look that up and post a sketch.

Conversely, we can represent the meaning of MSO formulas by finite state automata inductively, following the construction of the automata. To do this we augment the alphabet of the automaton, by adding components that indicate the value of the free position variables $i$ and set variables $X$. If we read a string along the automaton we find exactly a single $1$ to indicate a certain postion $i$, and the positions in a set $X$ are marked likewise.

The basic formulas are $R_a(i)$ for "position $i$ has symbol $a$", $i\in X$ for "$i$ is an element of $X$" and $i<j$ for "position $i$ is before position $j$". These formulas can be represented by the following simple finite state automata (over the augmented alphabet suited for the formula):

basic automata

More complicated formulas are constructed using the Boolean connectives $\lor, \lnot$ and the existential quantifiers $\exists i, \exists X$. The intended meaning of these operators are easily translated to languages as the language operators union $\cup$, complement ${}^c$ and projection, which is the operation that removes the corresponding component from the augmented alphabet. For union we have to pay some attention to the augmented alphabets in case the two parts of the formula do not agree on the set of free variables. Projection is simple, but it will change a deterministic automaton into a nondeterministic one.

  • $\begingroup$ Added my suggestion for the converse. Pending approval by @DavidRicherby $\endgroup$ Commented Oct 25, 2017 at 19:11
  • $\begingroup$ Thank you for a great response. I am still processing all of this and working through it, looking up terms, thinking how I would implement this, etc. In the mean time I think number 3 was the wrong question. Maybe it should rather have been why is the relation between automata and logic so important, that it is mentioned in so many articles? $\endgroup$ Commented Oct 28, 2017 at 10:14
  • $\begingroup$ Thank you for the excellent answer! $\endgroup$
    – Klas. S
    Commented Feb 26, 2020 at 19:26
  • $\begingroup$ Great answer! This helped me a lot to understand more on this topic, thank you! I'm having some trouble understanding the automata added by @HendrikJan. What exactly is the meaning of $\binom{a}{0}$? I've intrepreted it as $a$ in position $i$, since I thought that the first trace describes $i$ and the second one $j$. I'm generally having some issue to comprehend how these automata work, but am I right with my assumption on $i,j$? $\endgroup$
    – Algebruh
    Commented Mar 20, 2021 at 17:04
  • $\begingroup$ The special symbols like $a \choose 0$ code both the presence of symbol $a$ at any position in the string, but also the boolean value indication either the position of a certain variable $i$, or the positions of the elements a set $X$. $\endgroup$ Commented Mar 21, 2021 at 12:29

Your Answer

By clicking “Post Your Answer”, you agree to our terms of service and acknowledge you have read our privacy policy.

Not the answer you're looking for? Browse other questions tagged or ask your own question.