## Tuesday, May 28, 2013

### On-the-fly Construct Büchi Automata for LTL formulae

The previous post introduced the declarative construction, which is exponential. For instance, the LGBA for $p \mathbf{U} q$ has 8 states. However, on-the-fly construction can build Büchi automata for linear size. Surely, distinct automata can express the same language (further, the LTL formula).

### Negative Normal Form

First we write LTL formulas into their NNF equivalence, which is composed by $\vee, \wedge, \mathbf{X}, \mathbf{U}, \mathbf{R}$ only. Negations are pushed down to literals. Here we quote some rules,

• $\neg \mathbf{X} \phi \Rightarrow \mathbf{X} \neg \phi$
• $\neg ( \phi \mathbf{U} \psi ) \Rightarrow (\neg \phi \mathbf{R} \neg \psi)$
• $\neg ( \phi \mathbf{R} \psi ) \Rightarrow (\neg \phi \mathbf{U} \neg \psi)$

### Tableaux Expansion

• $\phi \mathbf{U} \psi \Rightarrow \psi \vee (\phi \wedge \mathbf{X}(\phi \mathbf{U} \psi))$
• $\phi \mathbf{R} \psi \Rightarrow \psi \wedge (\phi \vee \mathbf{X}(\phi \mathbf{R} \psi))$

### Disjunctive Normal Form

With all formulas converted to the following form, each disjunct is a state.

$$\bigvee_i \bigg( \bigwedge_j I_{ij} \wedge \bigwedge_k \mathbf{X}\psi_{ik} \bigg)$$

Note $\bigwedge_j I_{ij}$ represents the labels, and $\bigwedge_k \mathbf{X}\psi_{ik}$ shows the transition. When the $\mathbf{X}$-formula is not present, we write $\mathbf{X} \top$.

### Cover

A cover of a set of LTL formulas $\Psi= \{ \psi_1, \ldots, \psi_k \}$ calculates the set of initial states of Büchi automaton that represents $\bigwedge_i \psi_i$. A state is denoted as $\langle \lambda, \chi, \sigma \rangle$, which are the set of labels, the next formula, the set of subformulas of satisfied in $s$.

$$\mathsf{Cover}(\Psi) := \mathsf{Expand}(\Psi, \langle \emptyset, \emptyset, \emptyset \rangle)$$

### Expand

We quote its definition. Assume $s=\langle \lambda, \chi, \sigma \rangle$, $l$ is a propositional literal, $\mathsf{Expand}(\Psi, s)=$

### Construct $A_\phi$

With the above operations defined, we construct the Büchi Automaton for an LTL formula. $A_\phi = (Q, Q_0 , \Sigma, L, T , FT)$, with $Q_0 = \mathsf{Cover}(\{\phi\})$, $Q$ is the smallest set such that $Q_0 \subseteq Q$, also if $\langle \lambda, \chi, \sigma \rangle \in Q$, then $\mathsf{Cover}(\{\chi\}) \in Q$, the labeling function $L(s) = \{a \in \Sigma | a \models \lambda \}$, transition relation $T = \{(s,s') | s = \langle \lambda, \chi, \sigma \rangle \wedge s' \in \mathsf{Cover}(\{\chi\}) \}$, the fairness conditions $FT = \{F_1, \ldots, F_n\}$, where $F_i = \{s \in Q | \phi_i \mathbf{U} \psi_i \notin \sigma \vee \psi_i \in \sigma \}$.

### Examples

Here we present the Büchi Automata built from the stated method.

Fig 1. NBA of $\mathbf{FG}p$

Fig 2. NBA of $p \mathbf{U} q$

### References

1. R. Sebastiani, Automata-theoretic LTL Model Checking, slides on Formal Methods, 2012
2. Wikipedia, Linear temporal logic to Buchi Automaton, http://en.wikipedia.org/wiki/Linear_temporal_logic_to_Büchi_automaton