Next: State spaces, Previous: LTL formulas, Up: Definitions

`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
tuple^{1}
<S, Q, R, q, F, L>,
where

- S
is the finite
*alphabet*(S = 2^AP in this case), - Q is the finite set of
*states*, - R (a subset of Q x 2^S x 2^F x Q)
is the set of
*transitions*(each of which consists of four components called the*start state*, the*guard*, the*acceptance component*, and the*target state*, respectively), - q
is the
*initial state*, - F = {f1, f2, ..., fn} (for some finite n)
is the set of
*acceptance conditions*(a “nongeneralized” Büchi automaton has exactly one acceptance condition), and - L: Q -> 2^F
is a
*labeling function*that associates each state of the automaton with a set of acceptance conditions.

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:

- Add a new state (associated with an empty set of LTL formulas) into the automaton and add transitions from it to each initial state of the original automaton. Make the new state the (only) initial state of the automaton.
- For each state of the (modified) automaton, construct a conjunction of all propositional constraints (all formulas with no temporal operators) associated with the state and make the conjunction the guard of each transition coming into the state (the acceptance component of each transition remains empty). Then remove the association between states and sets of formulas.
- If Q1, Q2, ..., Qk (subsets of Q) are the sets of states determining acceptance in the original automaton, let fi = Qi for all 1 <= 1 <= k, and let L(q) = {fi | q is a member of fi} for all states q.

[1] 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.