Definition: An A is a finite automaton (FA) iff A is a tuple

- Q is a finite set of states
- I Q is the set of initial states
- F Q is the set of final states
- is a finite input alphabet
- Q Q is the set of transitions

A run of the automaton -or an execution- over an input word is a sequence such that for and .

An automaton usually can have more than only one run and these runs are different. Therefore one can for an automaton define the set as the smallest set of executions of the automaton with the requirement that for all it holds that .

Gerd Doeben-Henisch 2010-03-03