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

- Q is a finite set of states
- I Q is the set of initial states
- F Q is the set of final states
- is a finite input alphabet
- Q Q is the set of transitions

A run of the automaton -or an execution- over an input word is a sequence such that for and .

An automaton can usually have more than only one run and these runs are different. Therefore one can for an automaton define the set as the smallest set of executions of the automaton with the requirement that for all it holds that .

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

- Q is a finite set of states
- I Q is the set of initial states
- F Q is the set of final states
- is an input alphabet
- Q Q is the set of transitions
- is a finite set of properties
- /* 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) iff it is a tuple

- is a finite set of P-states
- I Q is the set of initial states
- F Q is the set of final states
- is an input alphabet
- Q 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) iff it is a tuple

- is a finite set of P-states
- is the initial probability distribution
- 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.

Gerd Doeben-Henisch 2010-03-03