C.3 Composite Processes


C.3 Composite Processes

Before defining the meaning of composition in FSP and of the priority operators on composite processes, we must first describe the meaning of composition and priority in the underlying LTS model.

C.3.1 LTS Composition

The parallel composition P||Q of two LTSs P and Q is defined as follows:

 If P = Π or Q = Π, then P||Q = Π. For P = < S1, A1, Δ1, q1 > and Q = < S2, A2, Δ2, q2 >, such that P  Π and Q  Π, P||Q = < S1 × S2, A1  A2, Δ, (q1, q2) >,

where Δ is the smallest relation satisfying the rules:

  • Let a Act in

    image from book

Parallel composition is both commutative and associative. Consequently, the order in which LTSs are composed is not significant.

In addition:

 P || lts(END) = P, lts(END) || P = P and lts(END) || lts(END) = lts(END).

C.3.2 LTS Priority

The set of actions B image from book Act are high priority in the LTS P B, where P = < S, A, Δ, q >.

P B = < S, A, Δ, q > where Δ is the smallest relation satisfying the rule:

  • Let a, b Act in

    image from book

The set of actions B image from book Act are low priority in the LTS P B, where P = < S, A, Δ, q >.

P B = < S, A, Δ, q > where Δ is the smallest relation satisfying the rule:

  • Let a, b Act in

    image from book

C.3.3 FSP Composition and Priority

Using the definitions for LTS composition and priority, we can now simply define the meaning of composition and priority in FSP. In the following, CE refers to FSP composition expressions of the form (Q1 ||||Qn) and Q refers to the identifier of a process or composite process.

Parallel Composition || :

 lts(Q1 || Q2) = lts(Q1) || lts(Q2).

Priority High << :

 lts(CE<<B) = lts(CE) << B.

Priority Low >> :

 lts(CE >>B) = lts(CE) >> B.




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