A.2 Generalized automata

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.

A.2.1 Formal definition of generalized automata

Formally, a generalized Büchi automaton can be represented as a tuple¹ <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.

A.2.2 Transition label encoding

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.

A.2.3 Converting between equivalent definitions

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:

1. 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.
2. 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.
3. 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.