## Monday, May 27, 2013

### Translate LTL formulae into Büchi Automata

LTL formulae are translated in Labelled Generalized Büchi Automata (LGBA), where labels are moved into states. See a previous post (link).

### $\omega$-automaton, $\omega$-word, $\omega$-language

An $\omega$-automaton is an automaton which accepts infinite inputs. Büchi Automata are a typical example. An $\omega$-word is an accepting run on an $\omega$-automaton, the set of all $\omega$-words accepted (defined) by an $\omega$-automaton is called an $\omega$-language.

The alphabet of a language is denoted as $\Sigma$, the set of all $\omega$-words composed by symbols in $\Sigma$ is denoted as $\Sigma^{\omega}$. A language recognizable (accepted) by an automaton $A$ is written $L(A)$. Usually we only work in automata that have $L(A) \subset \Sigma^{\omega}$.

### $\omega$-regular

Recall that regular languages can be recognized by NFAs/DFAs (equivalent). It can also be generated by regular grammar (left linear or right linear, but not mixed).

A language is called $\omega$-regular when it is represented as $$\bigcup_{i=1}^n U_i(V_i)^{\omega}$$

we require that $U_i$, $V_i$ be regular languages. $L$ is $\omega$-regular iff it can be recognized by Nondeterministic Büchi Automata. The $\omega$-regular languages are closed under complementation (useful for constructing $A_{\neg\phi}$).

### Closures

The closure of an LTL formula is intended to calculate its components (including their negations). For instance, a closure set of $p\mathbf{U}q$ is $$\{p, q, p\mathbf{U}q, \mathbf{X}(p\mathbf{U}q), \neg p, \neg q, \neg (p\mathbf{U}q), \neg (\mathbf{X}(p\mathbf{U}q))\}$$

### Atoms

An atom $A$ is called a maximal consistent subset of the closure set. First we remove negations. In order to be consistent (agree on assignments), we should have $p,q \in A$ when we have $p \wedge q \in A$. Similarly, when we have $p\mathbf{U}q \in A$, we require either $q \in A$ or $\{p \in A, \mathbf{X}(p\mathbf{U}q)\} \subset A$.

### LTL to LGBA

$A_{\phi} = (Q, Q_0, \Sigma, L, T, FT)$, respectively, the set of states Q is the the set of all atoms of $\phi$, the set of initial states $Q_0$ are the atoms where $\phi$ is included, $\Sigma$ is the power set of all free variables in $\phi$, namely the alphabet, labeling function $L$ maps a state to the set of free variables appeared in that state, transition relation is built from $\mathbf{X}$-formulas, say $(\mathbf{X}\psi, \psi) \in T$, $FT$ is a set of fair conditions $\{F_1, \ldots, F_n \}$, where $$F_i = \{ s \text{ is an atom} | \psi \mathbf{U} \phi \in s \vee \phi \in s \}$$

The above is on the condition that $\psi \mathbf{U} \phi$ appears positively in $\phi$. (see Polarity)

### Example

One can calculate the atoms of $p \mathbf{U} q$ and other parameters by the stated method, thus its Büchi automaton.

Fig 1. $A_{p \mathbf{U} q}$ constructed by definition

### On-the-fly Construction

The above construction is called declarative construction, though an alternative is present, considering its volume, it is to be introduced in another post.

### References

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