The semantics of basic FSP are defined in terms of Labeled Transition Systems (LTSs). In the body of the book, we have depicted the LTS that corresponds to an FSP process as a graph. In the following, we formally define what an LTS is and then describe the correspondence between FSP process expressions and LTSs. This correspondence is defined by the function:
where Exp is the set of FSP process expressions, and the set of LTSs. The function lts is defined inductively on the structure of FSP process expressions.
Let States be the universal set of states including π a designated error state, L be the universal set of labels, and Act = L ∪ {τ}, where τ is used to denote an internal action that cannot be observed by the environment of an LTS.
A finite LTS P is a quadruple < S, A, Δ, q > where:
S States is a finite set of states.
A = αP ∪ {τ}, where αP L denotes the alphabet of P.
Δ S – {π} × A × S, denotes a transition relation that maps from a state and an action onto another state.
q ∈ S indicates the initial state of P.
The only LTS that is allowed to have the error state π as its initial state is < {π}, Act, {}, π>, named Π. The alphabet of this process αΠ = L.
An LTS P = < S, A, Δ, q > transits with action a ∈ A into an LTS P′, denoted as , if:
P′ = < S, A, Δ, q′ >, where q′ ≠ π and (q, a, q′) ∈ Δ, or
P′ = Π, and (q, a, π) ∈ Δ.
We use to mean that P′ such that , and to mean that P′ such that .
We define a set of designated end states ES States such that an LTS P = < S, A, Δ, q > is terminating if there is a state e ∈ S and e ∈ ES and (e, a, q) ∈ Δ for all a ∈ A.