Next: The lbtt-translate utility, Previous: Format for LTL formulas, Up: Interfacing with lbtt

`lbtt` expects the Büchi automata generated by each LTL-to-Büchi
translator implementation to be in the format specified below. The format
encodes a generalized Büchi automaton (a Büchi automaton with zero or
more acceptance conditions) with a single initial state and labels (guards) on
transitions. For the full formal definition and examples on how
to reduce other definitions into the one used by `lbtt`, see
Definitions.

The output file generated by the translator should contain an `automaton`
described using the following grammar
(as before, quoted characters denote the characters themselves, `sp`
denotes any nonempty string of white space, lines containing a // are
comments that are not part of the grammar, and ``\n`' corresponds to the
newline character).

automaton::=num-statesspcond-specifierstate-listnum-states::= [0---9]+cond-specifier::= [0---9]+[st]*state-list::=state-listspstate| // empty

The automaton description begins with a nonnegative number that gives the
number of states in the automaton. If the number of
states is 0, the automaton will not accept any input. If the number is
positive, it should be followed by a `cond-specifier` that determines the
number
and placement of acceptance conditions in the automaton. If the number of
acceptance conditions is 0, the automaton accepts an input word if and only if
it has a run on that word according to the definition given in the
Appendix (see Definitions).

The placement of acceptance conditions is specified by concatenating a
string formed from the symbols ``s`' and ``t`' to the number of
acceptance conditions (with no white space in between). The interpretation of
this string is as follows:

- If the string is empty or does not include the symbol `
`t`', the acceptance conditions of the automaton are placed exclusively on its states. (This alternative corresponds to the definition supported by`lbtt`1.0.x.) - If the string is nonempty but does not include the symbol `
`s`', the automaton has acceptance conditions exclusively on its transitions. - Otherwise, the automaton has acceptance conditions on both states and transitions.

The `cond-specifier` is followed by a list of the descriptions of states in
the automaton. The format of this list is affected by the choice of the
placement of the acceptance conditions.
More precisely, the choice affects the interpretation of the
`cond-list` nonterminal symbol in the following fragment of the grammar: we
indicate this by prefixing the nonterminal with either “<s>” or
“<t>” to denote that the list (together with its terminating ``-1`')
should be
omitted in automata that do not associate acceptance conditions with states or
transitions, respectively.

state::=state-idspinitial?<s>cond-listtransition-liststate-id::= [0---9]+initial?::= `0' | `1'cond-list::=spacceptance-condition-idcond-list|sp`-1'acceptance-condition-id::= [0---9]+transition-list::=sptransitiontransition-list|sp`-1'transition::=state-id<t>cond-listspguard-formula`\n'guard-formula::= `t' // ``true'' | `f' // ``false'' | `p'[0---9]+ // atomic proposition | `!'spguard-formula// negation | `&'spguard-formulaspguard-formula// conjunction | `|'spguard-formulaspguard-formula// disjunction | `i'spguard-formulaspguard-formula// implication | `e'spguard-formulaspguard-formula// equivalence | `^'spguard-formulaspguard-formula// exclusive or

The description of each state begins with a numeric state identifier, which can
be any nonnegative integer. The state identifier should be followed by a number
telling whether the state is initial (``1`' if yes). The automaton should
have exactly one initial state. If the automaton has acceptance conditions
associated with its states, this number should then be followed by a list of
acceptance condition identifiers separated by white space. This list should be
terminated with ``-1`'.

The state description should be followed by the list of transitions starting
from the state (terminated again by ``-1`'). Each transition consists of a
state identifier (the target state of the transition), a list of acceptance
condition identifiers (if the automaton has acceptance conditions on
transitions), and a propositional formula ^{1} that encodes
the symbols of the alphabet
2^AP
(where `AP` is a finite set of atomic propositions) on which the
automaton is allowed to take the transition. The propositional formula should
be terminated with a newline.

The state and acceptance condition identifiers need not be successive, and the
states or acceptance conditions can be listed in any order. The only
restrictions are that the identifiers of different states and acceptance
conditions should be unique and that the total number of different identifiers
should equal `num-states` or `num-conds`,
respectively. (The same identifiers can be shared between states and acceptance
conditions, however.)

Note that the output file should always contain a valid automaton description
if the LTL-to-Büchi translation was successful, even in the case that the
resulting automaton is empty (`lbtt` interprets a missing automaton
description file as an error).

The following examples illustrate the file format. The first example
gives the description of an automaton with acceptance conditions on
states. Note that in this case the ``s`' is optional for describing the
placement of acceptance conditions; therefore, the automaton files used with
`lbtt` 1.0.x are upwards compatible with newer versions of the tool
(provided that each guard of a transition is terminated by a newline).

6 2s // an automaton with six states and two acc. conditions on states 0 1 -1 // state 0: initial state, no acceptance conditions 2 p1 // transition to state 2, guard `p1' 5 p2 // transition to state 5, guard `p2' 15 p3 // transition to state 15, guard `p3' -1 // end of state 0 2 0 1 -1 // state 2: non-initial state, acceptance condition 1 2 p1 // transition to state 2, guard `p1' 5 p2 // transition to state 5, guard `p2' 15 p3 // transition to state 15, guard `p3' -1 // end of state 2 5 0 0 -1 // state 5: non-initial state, acceptance condition 0 5 p2 // transition to state 5, guard `p2' 8 & p1 p2 // transition to state 8, guard `p1 /\ p2' 12 & p1 p3 // transition to state 12, guard `p1 /\ p3' 15 p3 // transition to state 15, guard `p3' -1 // end of state 5 8 0 0 -1 // state 8: non-initial state, acceptance condition 0 5 p2 // transition to state 5, guard `p2' 8 & p1 p2 // transition to state 8, guard `p1 /\ p2' 12 & p1 p3 // transition to state 12, guard `p1 /\ p3' 15 p3 // transition to state 15, guard `p3' -1 // end of state 8 15 0 1 0 -1 // state 15: non-initial state, acceptance conditions 1 and 0 2 p1 // transition to state 2, guard `p1' 5 p2 // transition to state 5, guard `p2' 15 p3 // transition to state 15, guard `p3' -1 // end of state 15 12 0 1 0 -1 // state 12: non-initial state, acceptance conditions 1 and 0 2 p1 // transition to state 2, guard `p1' 5 p2 // transition to state 5, guard `p2' 15 p3 // transition to state 15, guard `p3' -1 // end of state 12

The following example illustrates an automaton in which acceptance conditions are placed on transitions.

4 3t // four states, three acceptance conditions on transitions 5 0 // state 5: non-initial state 84 0 -1 p1 // transition to state 84, condition 0, guard `p1' 27 0 -1 & p1 ! p2 // tr. to state 27, condition 0, guard `p1 /\ ! p2' 5 -1 t // transition to state 5, no conditions, guard `true' -1 // end of state 5 84 1 // state 84: initial state 5 1 -1 t // transition to state 5, condition 1, guard `true' 27 0 -1 p1 // transition to state 27, condition 0, guard `p1' -1 // end of state 84 49 0 // state 49: non-initial state 5 -1 t // transition to state 5, no conditions, guard `true' 49 1 4 -1 & p1 ! p2 // tr. to state 49, conds. 1 and 4, guard `p1 /\ ! p2' 84 -1 p1 // transition to state 84, no conditions, guard `p1' -1 // end of state 49 27 0 // state 27: non-initial state 49 -1 & p1 p3 // transition to state 49, no conds., guard `p1 /\ p3' -1 // end of state 27

Automata with acceptance conditions on both states and transitions can be
specified using a combination of the above two formats, that is, by using
``st`' as the acceptance condition placement specifier and including a list
of acceptance conditions both after the value determining the initialness of a
state, and after the identifier of the target state of each transition.

[1] Although not described
formally in the grammar, the guard formulas can be specified in any
of the formats `lbtt` supports in its formula input files
(see ``--formulafile`' command line option). Note that
the formula always needs to be terminated with a newline, though.