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