# Transition systems

## Definition of transition system

Based on [C. Baier, J.-P. Katoen: Principles of model checking, Ch. 1](https://mitpress.mit.edu/9780262026499/principles-of-model-checking/).

:::info
**Definition (Transition system).**
A *transition system* $\mathcal T$ is a tuple $(S, \mathrm{Act}, \to, I, \mathrm{AP}, \lambda)$ where:
* $S$ is a set of *states*,
* $\Phi$ is a set of *actions*,
* $\to \subseteq S \times \Phi \times S$ is a *transition relation*,
* $I \subseteq S$ is a set of *initial states*,
* $A$ is a set of *atomic propositions*, and
* $\lambda : S \to 2^A$ is a *labeling* function.

A transition system $\mathcal T$ is called *finite* if all $S$, $\Phi$, and $A$ are finite.
:::

As a prominent example we obtain [Deterministic finite automata (DFAs)](/B12ryxVpRZWjGOlXU93-Yw) (or [Nondeterministic finite automa (NFAs)](/dDaFPm6hRUCpxr9OTEVJUw); see the examples at [Introduction to automata theory](/dF2SKHuSThWcmtb55siHNA) for an intuitive picture.

The transition relation captures the process of a system changing from a state $s \in S$ to a state $s' \in S$ via an action $\alpha \in \Sigma$. Instead of $(s,\alpha,s') \in \to$ we write:
$$ s \stackrel{\alpha}{\to} s' $$
This transition is in general **nondeterministic**, i.e., we might have multiple transitions $s \stackrel{\alpha}{\to} s'$ and $s \stackrel{\alpha}{\to} s''$, or undefined transitions for some $s$ and $\alpha$.

:::info
**Descriptions of the power set.**
For a set $A$ the set $2^A$ is an alternative description of the *power set* of $\mathcal P(A)$. The notation $2^A$ stands for the set of functions $A \to 2$, where $2 = \{\mathbb T, \mathbb F\} = \{0,1\}$ is the set of boolean truth values $\mathbb F$ and $\mathbb T$. One can show that this set of functions $A \to \{0,1\}$ is in one-to-one correspondence with $\mathcal P(A)$:
A subset $S \subseteq A$ corresponds to the **indicator function** $\chi_S : A \to \{0,1\}$ defined by:
$$ \chi_S(a) := \begin{cases}
1 & a \in S \\
0 & a \notin S \\
\end{cases}$$
Conversely, any function $f : A \to \{0,1\}$ gives rise to a subset $A_f \subseteq A$ defined by:
$$ A_f := f^{-1}(1) = \{a \in A \; | \; f(a) = 1\} $$
One can show that these assignments are mutually inverse.

In all, this justifies an identification
$$\mathcal P(A) = \{\text{subsets} \, S \subseteq A\} \cong \{\mathrm{functions} \,\, f : A \to 2\} = 2^A$$
:::

With this view of the power set, the labeling function $L$ yields the set $\lambda(s) \in 2^A$ of all propositions, i.e. logical formulas, that are true at state $s$.

Given that the elements of $A$ are logical propositions, the set $2^A$ can be also be understood as $\{0,1\}$-assignments *aka* **valuations** $\sigma : A \to \{0,1\}$ of the logical formulas in $A$. If $\varphi \in A$ is such a formula we say "the state $s$ satisfies the atomic proposition $\varphi$," written

$$s \models \varphi$$ iff $$\lambda(s) \models \varphi,$$
meaning that the valuation $\lambda(s) : A \to \{0,1\}$ satisfies $\varphi$, i.e. $\lambda(s) \models \varphi$.

We will often take the view of $\lambda(s)$ as a **subset** of $A$ (see above) consisting exactly of those atoms $p$ in $A$ that get assigned the boolean value of truth $1 = \mathbb T$.

In the most basic case, the atomic propositions are the ones from [propositional logic](). You can read up on the syntax and semantics of propositional logic in [Open Logic Project, Chapter 7](https://builds.openlogicproject.org/open-logic-complete.pdf).

## Paths and traces

:::info
**Definition (Path fragment).** A **path fragment** in a transition system $\mathcal T = (S, \mathrm{Act}, \to, I, \mathrm{AP}, L)$ is either of the two:
1. a finite sequence $s_0 \stackrel{\alpha_0}{\longrightarrow} s_1 \stackrel{\alpha_1}{\longrightarrow} s_2 \to \ldots \to s_n$ where $s_i \in S$ are arbitrary states
2. an infinite sequence $s_0 \stackrel{\alpha_0}{\longrightarrow} s_1 \stackrel{\alpha_1}{\longrightarrow} s_2 \to \ldots$ where $s_i \in S$ are arbitrary states.

We call a path fragment **initial** if it starts in an initial state.

We call a path fragment **maximal** if it is either infinite or ends in a terminal state.

We denote the set $\mathrm{Paths}(s)$ the set of maximal path fragments starting at $s$. We denote the set $\mathrm{Paths}_{\mathrm{fin}(s)}$ the set of maximal path fragments starting at $s$.
:::

:::info
**Definition (Path).** A **path** in a transition system $\mathcal T = (S, \mathrm{Act}, \to, I, \mathrm{AP}, L)$ is either of the two:
1. a finite sequence $s_0 \stackrel{\alpha_0}{\longrightarrow} s_1 \stackrel{\alpha_1}{\longrightarrow} s_2 \to \ldots \to t$, where $s_0 \in I$ and $t \in S$ is *terminal* in the sense that there is no transition from $t \to s$ for any $s \in S$
2. an infinite sequence $s_0 \stackrel{\alpha_0}{\longrightarrow} s_1 \stackrel{\alpha_1}{\longrightarrow} s_2 \to \ldots$, where $s_0 \in I$.

One also says that a path is an **initial and maximal path fragment**.
:::

But instead of just looking paths, capturing transitions $s_0 \stackrel{\alpha_0}{\longrightarrow} s_{1} \stackrel{\alpha_1}{\longrightarrow} s_{2} \to \ldots$ we want to keep track of the sequence $\lambda(s_0) \lambda(s_1) \lambda(s_2) \ldots$ keeping track of the set of atomic propositions that are true along the path. Such sequences are called traces.

:::info
**Definition (Trace).**
1. The **trace of a finite path fragment** $\rho := s_0 \stackrel{\alpha_0}{\longrightarrow} s_1 \stackrel{\alpha_1}{\longrightarrow} s_2 \longrightarrow \ldots \longrightarrow s_n$ is given by $\mathrm{trace}(\rho) := \lambda(s_0) \lambda(s_1) \ldots \lambda(s_n)$.
2. The **trace of an infinite path fragment** $\rho := s_0 \stackrel{\alpha_0}{\longrightarrow} s_1 \stackrel{\alpha_1}{\longrightarrow} s_2 \longrightarrow \ldots$is given by $\mathrm{trace}(\rho) := \lambda(s_0) \lambda(s_1) \ldots$

If $s$ is a state a **trace of s** is a trace of any path fragments starting at $s$. We denote the set of traces of $s$ as $\mathrm{Traces}(s)$.

From this, we define the set of traces of $\mathcal T$ as:
$\mathrm{Traces}(\mathcal T) = \bigcup_{s \in I}\mathrm{Traces}(s)$
:::