Linear-Time Behavior
To analyze a computer system represented by a transition system 1, either an action-based or a state-based approach can be followed. The state-based approach abstracts from actions; instead, only labels in the state sequences are taken into consideration. In contrast, the action-based view abstracts from states and refers only to the action labels of the transitions.
Paths and State Graph
Let \(\texttt{TS} = (\texttt{S}, \texttt{Act}, \rightarrow, \texttt{I}, \texttt{AP}, \texttt{L})\) be a transition system. The State Graph of TS, notation \(\texttt{G}(\texttt{TS})\), is the Digraph (V, E) with vertices V = S and edges \(E = \{(s, s^\prime) \in \texttt{S} \times \texttt{S} \mid s^\prime \in \texttt{Post}(s)\}\).
- The state graph of TS has a vertex for each state in TS and an edge between vertices s and s^′ whenever s^′ is a direct successor of s in TS for some action α.
Let \(\texttt{Post}^\ast(s)\) denote the states that are reachable in state graph G(TS) from s, then for any \(\texttt{C} \subseteq \texttt{S}\):
\(\texttt{Post}^\ast(C) = \bigcup\limits_{s \in C} \texttt{Post}^\ast(s)\)
Path-Fragment
A finite path fragment \(\hat{\pi}\) of TS is a finite state sequence \(s_0 s_1 \dots s_n\) such that \(s_i \in \texttt{Post}(s_{i-1}), \forall 0 < i \leq n, n \geq 0\). An infinite path fragment π is an infinite state sequence \(s_0 s_1 s_2 \ldots\) such that \(s_i \in \texttt{Post}(s_{i-1}), \forall i > 0\).
Maximal and Initial Path Fragment
A maximal path fragment is either a finite path fragment that ends in a terminal state, or an infinite path fragment. A path fragment is called initial if it starts in an initial state, i.e., if s0 ∈ I.
Path
A path of transition system TS is an initial, maximal path fragment.
Traces
Executions (…) are alternating sequences consisting of states and actions. Actions are mainly used to model the (possibility of) interaction, be it synchronous or asynchronous communication. (…). Thus, rather than having an execution of the form \(s_0 \overset{\alpha_0}{\longrightarrow} s_1 \overset{\alpha_1}{\longrightarrow} s_2 \ldots\) we consider sequences of the form L(s0) L(s1) L(s2) … that register the (set of) atomic propositions that are valid along the execution. Such sequences are called traces.