Introducing Properties

The basic idea to do this is to enlarge the execution graph representation with additional properties $\Pi$ which represent critical aspects of the system (cf. figure 3.4). Furthermore one would need a language $\cal L$ to speak about these properties, and we would need an automaton $\cal A$ which can automatically prove whether a description (specification) given as an $\cal L$-expression is true in the given execution graph $\cal G'$ of the transition graph $\cal G$. One can imagine the following enhancement of the transition graph $\cal G$:

Figure 3.4: Transition graph with properties

From the point of view of the planned automatic proof system are the properties only strings out of the set of properties $\Pi$ which usually have either the format of 'names' like start or the format of predicates like K = A ('=' is the 2-position predicate and 'K' and 'A' are the arguments). If a vertex has a property $\pi_{i}$ of the set $\Pi$ then this property is understood to be true. If a possible property $\pi_{i}$ of the set $\Pi$ is not in a state then it is assumed that the property is false. The definition of the graph has to be changed accordingly:

$$\langle V,E,\Sigma, l, \Pi \rangle$$

with $V$ as a set of vertices, $E$ as a set of edges, $\Sigma$ as an input alphabet, which is used for the Symbols attached to the edges as labels, $\Pi$ as a set of properties and $l$ as a labeling function which maps the vertices into the set $\Pi$. For our toy exampe we get:

1. $V$ = $\{ 1,2,3,4 \}$
2. $E$ $\subseteq$ $V \times \Sigma \times V$ with $E$ = $\{\langle 1,A,2\rangle, \langle 1,B,1\rangle,\langle 1,C,1\rangle, \langle 2,A... ...C,1\rangle, \langle 3,A,4\rangle, \langle 3,B,1\rangle,\langle 3,C,1\rangle\}$
3. $\Sigma$ = $\{ A,B,C \}$.
4. $l: V$ $\longrightarrow$ 2$^{\Pi}$= $\{ (1,\{ start\}), (2,\{ K=A\}), (3,\{ K=B\}), (1,\{ K=A\}),\}$.
5. $\Pi$= $\{ start, K=A, K=B \}$.

With these additional informations the execution graph $\cal G'$ will also be enhanced and we can now look to the different pathes of the execution graph enlighted by questions like those of the stakeholder, 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. These would mean that there exist a path $\sigma$ in the execution graph $\cal G'$ whose last three vertices have the properties $K=A, K=B, K=A$.