Definitions

Overview

A transition system is a reactive system, and a model to describe the behavior of systems

Intuition: a transition system consists of a set of possible states for the system and a set of transitions - or state changes - which the system can effect.

• When a state change is the result of an external event or of an action made by the system, then that transition is labeled with that event or action.
• Particular states or transitions in a transition system can be distinguished.

The state here is the global state, or in other words, ID

Formalism

A transition systems is a tuple $A= \gdef\tuple#1{\langle{#1}\rangle} \tuple{S,~S_0,~T,~\alpha,~\beta}$ where:

• $S$ is a finite or infinite set of states
• $S_0$ is initial location
• $T$ is a finite or infinite set of transitions
• $\alpha$ and $\beta$ are two mapping from T to S which take each transition $t$ in $T$ to the two states $\alpha(t)$ and $\beta(t)$, respectively the source and the target of the transition $t$.

A transition system is finite if $S$ and $T$ are finite.

Path

A path of length $n$, $n>0$, in a transition system $A$ is a sequence of transitions $t_1, t_2, …, t_n$, such that