The language of words that satisfy an LTL formula \(\varphi \)  over \(AP\)  can be fully captured through [1]} a Nondeterministic Büchi automaton (NBA) \(\mathcal {A}_{\varphi } \) , defined as \(\mathcal {A}_{\varphi }=(Q, \,2^{AP},\, \delta ,\, Q_0,\, {F})\) ,
where \(Q\)  is a set of states; \(2^{AP}\)  is the set of all allowed alphabets; \(\delta \subseteq Q\times 2^{AP} \times {Q}\)  is a transition relation; \(Q_0, \, {F}\subseteq Q\)  are the set of initial and accepting states, respectively.
The process of constructing \(\mathcal {A}_{\varphi }\)  can be done in time and space \(2^{\mathcal {O}(|\varphi |)}\) , where \(|\varphi |\)  is the length of \(\varphi \)  [1]}. There are fast translation tools [3]}, [4]} to obtain \(\mathcal {A}_{\varphi }\)  given \(\varphi \) .
