AGV 1.3 -- The Logic-Automata Connection

Previous chapter: Synthesis

This is a learning note of a course in CISPA, UdS. Taught by Bernd Finkbeiner

Verification or Synthesis

In applications like verification and synthesis, the automata- and game-theoretic machinery is usually “hidden” behind a logical formulation of the problem.

Logics with corresponding Automata

S1S‘s expressiveness exceeds that of LTL, and
S2S‘s expressiveness exceeds that of CTL* (on binary trees)

Logic	Usage	Example
Linear-time temporal logic (LTL)	sets of infinite words	$\square \Diamond \ell_1$
Computation-tree logic (CTL / CTL*)	sets of infinite trees	$\textsf{EF}\ell_1 \wedge \textsf{EF}m_1$
Monadic second-order logic with one successor (S1S)	logic over infinite words	$\forall x . x \in P \rightarrow S(x) \in P$
Monadic second-order logic with two successors (S2S)	logic over infinite binary trees	$\forall x . x \in P \rightarrow S_1(x) \in P \vee S_2(x) \in P$

Explaination

• $\square \Diamond \ell_1$
  $P_0$ is infinitely often at location $\ell_1$.
• $\textsf{EF}\ell_1 \wedge \textsf{EF}m_1$
  There exists a computation path in which $P_0$ reaches location $\ell_1$, and
  there is a (possibly different) computation path in which $P_1$ reaches location $m_1$.
• $\forall x . x \in P \rightarrow S(x) \in P$
  A (given) set of natural numbers $P$ is either empty, or
  consists of all positions starting from some position of the word.
• $\forall x . x \in P \rightarrow S_1(x) \in P \vee S_2(x) \in P$
  A (given) set of nodes $P$ contains from each node $n \in P$ an entire path starting in $n$.

For example, mutual exclusion property can be expressed using linear-time temporal logic (LTL):
$$\square \neg (\ell_1 \wedge m_1)$$

Satisfiability problem

Other than verification and synthesis, another important application of the connection between logic and automata is to decide the satisfiability problem of the various logics.

Example

We want to know if there exist two natural numbers $x$ and $y$ such that $x=y+1$ and $y=x+1$.
This can be expressed as the S1S formula $x=S(y) \wedge y=S(x)$, translate each conjunct into an automaton:

Alphabet: subsets of $\lbrace x,y\rbrace$.

There does not exist a word that is accepted by both automaton. Hence, the formula is unsatisfiable.

---

Next chapter: Büchi automata (Preliminaries)