O'Reilly logo

Concurrency: State Models and Java Programs by Jeff Kramer, Jeff Magee

Stay ahead with the world's most comprehensive technology and business learning platform.

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, tutorials, and more.

Start Free Trial

No credit card required

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. 

FSP Semantics

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:

  • SStates is a finite set of states.

  • A = αP ∪ {τ}, where αPL denotes the alphabet of P.

  • Δ ⊆ S −{π} × A × S, denotes a transition relation that maps from a state and an action onto another state.

  • qS 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 aA into an LTS P′, denoted as

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

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

With Safari, you learn the way you learn best. Get unlimited access to videos, live online training, learning paths, books, interactive tutorials, and more.

Start Free Trial

No credit card required