Execution Graph

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 $A$ with $G = \langle V,E,\Sigma,\Xi,l,AP \rangle$ then we can construct an execution graph ExG(G) with $\langle \hat V,\hat E,\Sigma,\Xi, l,AP \rangle$ as follows:

1. $(q_{0},0) \in \hat V$
2. If $(q,n) \in \hat V \& \exists q' \in V \& succ(q) = q' then \{(q',n+1)\m... ...} \& ow \in \Xi^{*} \& \langle q,iw,ow,q'\rangle \in E_{G}\} \subseteq \hat E$
3. Only (1)-(2) define the sets $\hat V$ and $\hat E$

For an example see below figure 5.3.