An omega automaton is an Finite_state_automaton that recognizes words of infinite length (also called omega words).

In the AutomataTheoreticApproachToModelChecking, an execution of the system to verify is seen as an omega word (the letters of the word are the successive configurations of the system). The whole set of possible executions can be seen as the set of omega words recognized by an omega automaton.

In Spot we use a special kind of omega automaton called TGBA.

OmegaAutomaton (last edited 2004-09-27 14:40:40 by lucifer)

All text is available under the terms of the GNU Free Documentation License, see SpotWikiLicense for details.