Automaton with Properties

If we want to use properties with finite automata then arises the question, how one can handle properties $\Pi$ with finte automata. Strictly speaking there is no place for properties in finite automata. But seen from the point of property checking in the case of execution graphs it is clear that the main goal for the usage of properties is given in the goal to have a tool to enable an automatic proof checker to investigate the possible executions of an automaton with regard to certain specified criteria whether these are occuring in an execution or not. From this point of view we can use the output of a finite automaton as a kind of a protocol showing us all important informations. Thus we can assume that the output function prints the strings encoding the properties, eventually enhanced with additional informations like the actual state. For this we define the Finite Protocol Automaton as follows:

Def.: The automaton $\cal A$ is a Finite Protocol Automaton iff we have the following structure:

$$\langle Q, I, F, \Sigma, \Xi, \Delta, l_{\pi}, l_{q}, \Pi \rangle$$

with

1. $Q$ := Finite set of states
2. $I \subseteq Q$ := Set of initial states
3. $F \subseteq Q$ := Set of final states
4. $\Sigma$ := Finite set of symbols forming the input alphabet
5. $\Xi$ := Finite set of symbols forming the output alphabet
6. $\Pi$ := Finite set of properties as a set of words of some language $L_{\pi}$
7. l$_{\pi}$ : $Q \longrightarrow 2^{\Pi}$ := mapping the states into finite sets of properties
8. l$_{q}$ : $Q \longrightarrow \Xi^{*}$ := mapping the states into words over the output alphabet
9. $\Delta \subseteq Q \times \Sigma^{*} \times Q \times \Xi^{*} \times 2^{\Pi}$ := Relating actual state and input with follow up state and a word encoding the follow up state as well as the set of properties related to the follow up state.

Armed with this definition we can translate the graph $\cal G$ with properties and as well the corresponding execution graph $\cal G'$ as follows:

1. $Q$ = $\{ 1,2,3,4 \}$
2. $I = \{ 1\}$
3. $F = \{ 4\}$
4. $\Sigma$ = $\{ A,B,C \}$.
5. $\Xi$ = $\{ 1,2,3,4 \}$
6. $\Pi$= $\{ start, K=A, K=B \}$.
7. $l_{\pi}: Q$ $\longrightarrow$ 2$^{\Pi}$= $\{ (1,\{ start\}), (2,\{ K=A\}), (3,\{ K=B\}), (1,\{ K=A\}),\}$.
8. $l_{q}: Q$ $\longrightarrow$ $\Xi^{*}$= $\{ (1,1), (2,2), (3,3), (4,4)\}$.
9. $\Delta$ $\subseteq$ $Q \times \Sigma^{*} \times Q \times \Xi^{*} \times 2^{\Pi}$ with $\Delta$ = $\{\langle 1,A,2,2,\{K=A\}\rangle, \langle 1,B,1,1,\{start\}\rangle, \langle ... ...}\rangle, \langle 3,B,1, 1,\{start\}\rangle,\langle 3,C,1, 1,\{start\}\rangle\}$

The definitions for execution, stateSequence, and inputword can be taken as before.

Corresponding to the execution sequence: $\sigma_{\cal A}$ = $\langle (1,B), (1,B), (1,C), (1,A), (2,B), (3,B), (1,A), (2,B), (3,A), (4,\epsilon) \rangle$ we can then construct a protocol based on the output of the automaton as follows (assuming the convention, that the individual properties are printed separated by a comma and one output is enclosed in brackets):

1. (1,start)
2. (1,start)
3. (1,start)
4. (2,K=A)
5. (3,K=B)
6. (1,start)
7. (2,K=A)
8. (3,K=B)
9. (4,K=A)

Because the automaton always will start in state $1$ with property $start$ we can interpolate the first element in the protocol and from this we can deduce the complete protocol. The complete protocol reports not the next states with their properties but the actual states with their properties:

1. (1,start)
2. (1,start)
3. (1,start)
4. (1,start)
5. (2,K=A)
6. (3,K=B)
7. (1,start)
8. (2,K=A)
9. (3,K=B)
10. (4,K=A)

The complete protocol corresponds directly to a possible path in the corresponding execution graph. if one interpretes the word encoding the actual state in the complete protocol then one could specify a CTL-expression like EF $4 \wedge K=A$ asking whether there is an execution path with a state where we have the properties $4 \wedge K=A$. Because a state with such properties must be a final state we can with such a CTL-specification enable an automatic checkler to generate a proof that there is such a path or that there is none.