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

Appendix

The following is a copy of original copyright notice of slides which this article is quoting.

Copyright notice: some material (text, figures) displayed in these slides is courtesy of M. Benerecetti, A. Cimatti, P. Pandya, M. Pistore, M. Roveri, and S.Tonetta, who detain its copyright. Some exampes displayed in these slides are taken from [Clarke, Grunberg & Peled, “Model Checking”, MIT Press], and their copyright is detained by the authors. All the other material is copyrighted by Roberto Sebastiani. Every commercial use of this material is strictly forbidden by the copyright laws without the authorization of the authors. No copy of these slides can be displayed in public without containing this copyright notice.