Automata, Properties, Execution Graphs

In model checking one uses directed graphs as representations of the behavior of automata. Therefore one needs the concept of an automaton. A simple version of a finite automaton is given below:

Definition: An A is a finite state automaton (FSA) iff A is a tuple

$$\langle Q, I, F, \Sigma, \Delta \rangle$$

with

1. Q is a finite set of states
2. I $\subseteq$ Q is the set of initial states
3. F $\subseteq$ Q is the set of final states
4. $\Sigma$ is a finite input alphabet
5. $\Delta$ $\subseteq$ Q $\times$ $\Sigma^{*}$ $\times$ Q is the set of transitions

A run of the automaton $A$ -or an execution- over an input word $w$ is a sequence $\varrho = \varrho(0)\varrho(1)...\varrho(i)...$ such that $\langle \varrho(i),w(i),\varrho(i+1)\rangle \in \Delta$ for $i \geq 0$ and $\varrho(0) = q_{0}$.

An automaton can usually have more than only one run and these runs are different. Therefore one can for an automaton $A$ define the set $exec(A)$ as the smallest set of executions of the automaton $A$ with the requirement that for all $\varrho, \varrho' \in exec(A)$ it holds that $\varrho \ne \varrho'$.

Definition: An A is a labelled finite state automaton (LFSA) iff it is a tuple

$$\langle Q,I, F, \Sigma, \Delta, l, \Pi \rangle$$

with

1. Q is a finite set of states
2. I $\subseteq$ Q is the set of initial states
3. F $\subseteq$ Q is the set of final states
4. $\Sigma$ is an input alphabet
5. $\Delta$ $\subseteq$ Q $\times$ $\Sigma^{*}$ $\times$ Q is the set of transitions
6. $\Pi \subseteq L_{PROP}$ is a finite set of properties
7. $l: Q \longrightarrow 2^{\Pi}$ /* Associates each state with a finite set of propositions */

An alternative (embedded) definition could be as follows:

Definition: An A is an embedded labelled finite state automaton (FSA$^{\Pi}$) iff it is a tuple

$$\langle Q, I, F, \Sigma, \Delta \rangle$$

with

1. $Q \subseteq 2^{L_{PROP}}$ is a finite set of P-states
2. I $\subseteq$ Q is the set of initial states
3. F $\subseteq$ Q is the set of final states
4. $\Sigma$ is an input alphabet
5. $\Delta$ $\subseteq$ Q $\times$ $\Sigma^{*}$ $\times$ Q is the set of transitions

A finite automaton with a probability distribution induces a Markov Chain.

Definition: An A is a (discrete time) Markov Chain with Embedded Properties (MC$^{\Pi}$) iff it is a tuple

$$\langle Q, \iota_{init}, P \rangle$$

with

1. $Q \subseteq 2^{L_{PROP}}$ is a finite set of P-states
2. $\iota$ is the initial probability distribution
3. $P: Q \times Q \longmapsto [0,1]$ a probabilistic transition function

From these automata one can compute the possible runs and then one can generate the set of all possible runs as a directed graph. This execution graph is then the formal model of all possible states and their possible transitions either deterministically or probabilistic.