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)
Please cite the source for reprints, feel free to verify the sources cited in the article, and point out any errors or lack of clarity of expression. You can comment in the comments section below or email to GreenMeeple@yahoo.com