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 *LTS*s. This correspondence is defined by the function:

**Equation C.1. **

where *Exp* is the set of *FSP* process expressions, and ℘ the set of *LTS*s. 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

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

Start Free Trial

No credit card required