Concurrency: State Models and Java Programs

Appendix C. FSP Semantics

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:

Equation C.1. 

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.

Labeled Transition System (LTS)

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

• P′ = < S, A, Δ, q′ >, where q′ ≠ π and (q, a, q′) ∈ Δ, or

• P′ = П, and (q, ...