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:

image from book

where Exp is the set of FSP process expressions, and image from book the set of LTSs. The function lts is defined inductively on the structure of FSP process expressions.

C.1 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 image from book States is a finite set of states.

  • A = αP {τ}, where αP image from book L denotes the alphabet of P.

  • Δ image from book 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 image from book, if:

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

  • P = Π, and (q, a, π) Δ.

We use image from book to mean that image from bookP such that image from book, and image from book to mean that image from bookP such that image from book.

We define a set of designated end states ES image from book States such that an LTS P = < S, A, Δ, q > is terminating if there is a state e S and e ES and image from book(e, a, q) Δ for all a A.




Concurrency(c) State Models & Java Programs
Concurrency: State Models and Java Programs
ISBN: 0470093552
EAN: 2147483647
Year: 2004
Pages: 162

flylib.com © 2008-2017.
If you may any questions please contact us: flylib@qtcs.net