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.
The traces of a transition system are thus words over the alphabet 2AP.
Trace and Trace Fragment
Let \(\texttt{TS} = (\texttt{S}, \texttt{Act}, \rightarrow,\texttt{I}, \texttt{AP}, \texttt{L})\) be a transition system without terminal states. The trace of the infinite path fragment \(\pi = s_0 s_1 \ldots\) is defined as \(trace(\hat{\pi}) = \texttt{L}(s_0) \texttt{L}(s_1) \ldots\). The trace of the finite path fragment π = s0 s1 … sn is defined as \(trace(\pi) = \texttt{L}(s_0) \texttt{L}(s_1) \ldots \texttt{L}(s_n)\).
The trace of a path fragment is thus the induced finite or infinite word over the alphabet 2AP , i.e., the sequence of sets of atomic propositions that are valid in the states of the path. The set of traces of a set Π of paths is defined in the usual way:
\[ trace(\pi) = \{ trace(\pi) \mid \pi \in \Pi \}. \]
Linear-Time Properties
A linear-time property (LT property) over the set of atomic propositions AP is a subset of (2AP)ω.
- Linear-time properties define the specific execution traces that a transition system should exhibit.
- Informally, they outline the acceptable or intended behavior of the system under analysis.
Satisfaction Relation for LT Properties
Let \(\texttt{P}\) be an \(\texttt{LT}\) property over \(\texttt{AP}\) and \(\texttt{TS} = (texttt{S}, \texttt{Act}, \rightarrow, \texttt{I}, \texttt{AP}, \texttt{L})\) a transition system without terminal states. Then, \(\texttt{TS} = (\texttt{S}, \texttt{Act}, →, \texttt{I}, \texttt{AP}, \texttt{L})\) satisfies \(\texttt{P}\), denoted \(\texttt{TS} \models \texttt{P}\), iff \(\texttt{Traces}(\texttt{TS}) \subseteq \texttt{P}\). State s ∈ S satisfies P, notation $ s \models P$, whenever Traces(s) ⊆ P
Thus, a transition system satisfies the LT property P if all its traces respect P, i.e., if all its behaviors are admissible. A state satisfies P whenever all traces starting in this state fulfill P.