Definition. Traces and behaviours [ltp-0002]

Liam O'Connor

Let the set of all possible states be $\Sigma$ . Note that we do not require that $\Sigma$ is finite. Then, $\Sigma ^\ast$ is the set of finite sequences of states. We denote the empty sequence as $\varepsilon$ . The concatenation of two sequences $t$ and $u$ is written $tu$ .

The set of all behaviours — infinite sequences of states — is $\Sigma ^\omega$ . We define $\sigma {}t = \sigma$ when the sequence $\sigma$ is infinite. We say that $t$ is a prefix of $u$ (or $u$ is an extension of $t$ ) iff there exists some $w$ such that $tw = u$ .

We shall model terminating systems, which have finite behaviours, as behaviours that infinitely repeat their final state.