Concurrency: State Models and Java Programs

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 = < S₁, A₁, Δ₁, q₁ > and Q = < S₂, A₂, Δ₂, q₂ >, such that P ≠ Π and Q ≠ Π, P||Q = < S₁ × S₂, A₁ ∪ A₂, Δ, (q₁, q₂) >,

where Δ is the smallest relation satisfying the rules:

• Let a ∈ Act in

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 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

The set of actions B 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

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 (Q₁ ||…||Q_n) and Q refers to the identifier of a process or composite process.

Parallel Composition || :

lts(Q₁ || Q₂) = lts(Q₁) || lts(Q₂).

Priority High << :

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

Priority Low >> :

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