lbtt uses internally finite-state automata on infinite words (Büchi automata) over the alphabet 2^AP (where AP is a finite set of atomic propositions) with one initial state, labels on transitions and zero or more acceptance conditions.
Formally, a generalized Büchi automaton can be represented as a tuple1 <S, Q, R, q, F, L>, where
A run of a Büchi automaton on an infinite sequence <x(0), x(1), x(2), ...> over the alphabet 2^AP is an infinite sequence of pairs of states and transitions <(q(0),t(0)), (q(1),t(1)), (q(2),t(2)) ...> (where each q(i) is a state in Q and each t(i) is a transition in R) such that q(0) = q and for all i >= 0, t(i) = <q(i), X(i), Y(i), q(i+1)> in R such that x(i) belongs to X(i). (Because the relation R is not necessarily a function from Q x 2^S x 2^F to Q, the automaton may have many runs on the same input.)
A run <(q(0),t(0)), (q(1),t(1)), (q(2),t(2)), ...> (where t(i) = < q(i), X(i), Y(i), q(i+1) > for all i) is accepting if and only if additionally, for each acceptance condition f in F, f is in L(q(i)) or f is in Y(i) for infinitely many i.
The automaton accepts an infinite sequence <x(0), x(1), x(2), ...> over the alphabet 2^AP if and only if the automaton has at least one accepting run on this sequence.
When working with automata on words over the alphabet 2^AP, the guards of transitions can be expressed as propositional formulas by identifying a set of symbols from this alphabet with the set of models of a propositional formula. A transition can then be seen as a rule “if in state q(i) and the next input symbol x(i) is a model of the propositional formula guarding the transition, the automaton can move to state q(i+1)”. In the context of Büchi automata constructed from LTL formulas, this often allows for a compact representation for the transitions.
Many LTL-to-Büchi translation algorithms presented in the literature (for example, [GPVW95]) are based on a slightly different definition for generalized Büchi automata, where the automata can have several initial states, acceptance is determined using a family of sets of states, and the guards of transitions are replaced with an additional state labeling that associates a set of LTL formulas with each state. These automata can easily be described using the above definition through the following steps:
 This definition differs from those commonly found in the literature by specifying the acceptance conditions in terms of a separate set that is independent of the other components of the automaton, together with an explicit labeling function for the states. This is to allow the definition to correspond more accurately to the automata that can be described in input files.