Model as Execution Graph

Such a transition graph represents the whole potential behavior of the machine. This has to be distinguished from a concrete execution caused by one person A. For exeample can we get the following execution: $\langle (1,B), (1,B), (1,C), (1,A), (2,B), (3,B), (1,A), (2,B), (3,A), (4,\epsilon) \rangle$ or $\langle (1,B), (1,C), (1,A), (2,C), (1,A), (2,B), (3,A), (4,\epsilon) \rangle$ etc. One can every execution interprete as an individual path of another graph called execution graph(cf. figure 3.3).

Figure 3.3: Execution graph related to transition graph G

One constructs an execution graph out of a transition graph G by starting with vertex 1 of G and map this vertex with number 0. Then one takes all the successors of this actual vertex and numbers these with $0+1 = 1$. Then one takes the successors of the level $1$ vertices and numbers these with $0+1+1 = 2$, and so on. In cases of infinite loops would the execution path be infinitely long, but in our toy example one can assume, that every human user will either will 'get through' the door or he/she will give up after finitely many steps.

The execution graph of G gives a more explicit view of the possible executions than the transition graph G itself. A transition graph is more compact and 'hides' some properties of the behavior.

For a possible stakeholder it could be an interesting question to the engineer, whether the engineer could guarantee that there is at least one possible execution in the set of all possible executions which will open the door. A possible answer of the engineer could be: Yes, there is at least one possible path ending up with the sequence of keying in symbol $A$ in state 2, symbol $B$ in state 3, and symbol $B$ in state 4. While such an answer can in our toy example simply be 'read out' from the graph it would not be feasible in applications with several hundreds or thousands or even more than 10000s of possible states. Thus one needs some mechanical proof procedure to allow such checks.