Created: 2012/11/21 16:47:39+0000

Automata are used to represent the state space of an Event-B machine. It is represented as a graph where some states are said to be accepting. Every transition followed in the execution of an Event-B machine adds to a word. Every word in the language of the automata describes a possible execution path. An accepted word must go though an accepting state infinitely often.

B??chi Automata are the simplest type of finite automata that accept an infinite word. This is important because if the automata is infinite it is impossible to fully enumerate and cannot be model checked. An infinite word must be accepted as the execution of an Event-B machine may not terminate.