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.



Gerd Doeben-Henisch 2010-03-03