I've been reading on omega automata(automata on infinite words) and stumbled upon a definition involving logic which caught me off guard.
For example, on Buchi automata the definition I originally saw was :
An omega automaton $M = (Q,\Sigma,\delta,I,F)$ is called a Buchi automaton if for every $w : \mathbb{N} \rightarrow \Sigma$ there exists a run $r$ so that $inf(r) \cap F \neq \emptyset$ where $inf$ is a function
$$inf(\sigma) = \left\{ w \in \Sigma ~: \exists^{\infty} n \in \mathbb{N} : \sigma(w) = s \right\}$$ where $\sigma : \mathbb{N} \rightarrow \Sigma$ is the function describing each letter of a word. These definitions are seen at 1 and 2.
However what I found here and here involve a new definition where the transition function is defined as $\delta : Q \times \Sigma \rightarrow B^{+}(Q)$ instead of $Q \times\Sigma \rightarrow P(Q)$.
$B^{+}(Q)$ is said to be a positive boolean formula. This thesis pretty much explains everything but I have not taken a course in Math Logic and can't understand why he involves formulas in the definitions. He also then defines the behaviour of the automatons using quantifiers, eg.
Muller automata. A path $\pi$ is accepting if $Inf(\pi) \in \mathcal{F}$. This is equivalent to saying that there exists $F \in \mathcal{F}$ such that $Inf(\pi) = F$. In the logical setting, this condition should be written as
where $Acc$ is an appropriate formula. Thus $Acc$ can be written as $\bigvee_{F \in \mathcal{F}} \varphi_F$, where $F$ exactly satisfies an appropriate formula $\varphi_F$. For this, it suffices to take $$ \varphi_F = \bigwedge_{q \in F}q \wedge \bigwedge_{q \in Q-F} \neg q $$ a formula which exactly defines $F$ (see Definition 1.1 of the thesis for a formal definition). Indeed, the unique truth assignment $v:Q \to \{True, False\}$ that makes $\varphi_F$ true is given by $$ v(q) = \begin{cases} True &\text{if }q \in F \\ False &\text{if }q \notin F \end{cases} $$ Altogether, you get the acceptance condition $$ Acc = \bigvee_{F \in \mathcal{F}} \bigl(\bigwedge_{q \in F}q \wedge \bigwedge_{q \in Q-F} \neg q \bigr) $$ For instance, if you take $Q = \{q_1, q_2, q_3\}$, $\mathcal{F} = \{F_1, F_2\}$, where $F_1 = \{q_1, q_2\}$ and $F_2= \{q_1, q_3\}$, the formula will be $(q_1 \wedge q_2 \wedge \neg q_3) \vee (q_1 \wedge q_3 \wedge \neg q_2)$.
Rabin's conditions can be represented by a logical formula in a similar way.