For the representations of the set of possible runs of an automaton (see section about automata) one needs the additional concept of unwinding (or: unfolding) of a transition graph which leads to an execution graph. The general definition of an execution graph is as follows (cf. Emerson (1990) [92], P.1012):

If we have a transition graph TrG(G) of an automaton with then we can construct an execution graph ExG(G) with as follows:

- If
- Only (1)-(2) define the sets and

For an example see below figure 5.3.

Gerd Doeben-Henisch 2010-03-03