C.4 Common Operators

C.4 Common Operators

To define the FSP re-labeling, hiding and interface operators, which can be applied to processes and composite processes, we first describe the meaning of re-labeling and hiding in the underlying LTS model.

C.4.1 Re-Labeling

Re-labeling applies a relation over action labels R L × L, to an LTS P = < S, A, Δ, q > such that:

where

• B₁ = {a ∈ A|a′.(a, a′) ∈ R},

• B₂ = {a′|a ∈ A.(a, a′) ∈ R},

• Δ₁ = {(p, a, p′) ∈ Δ|a ∈ B₁}, and

• Δ₂ = {(p, a′, p′)|(p, a, p′) ∈ Δ₁ (a, a′) ∈ R}.

C.4.2 Hiding

The set of actions B Act are hidden in the LTS P\B, where P = < S, A, Δ, q >.

If P = Π then P\B = Π otherwise

P\B =< S, (A–B) ∪ {τ}, Δ, q >

where Δ is the smallest relation satisfying the rule:

• Let a ∈ Act in

  

C.4.3 FSP Re-Labeling, Hiding and Interface

Re-labeling /:

 lts(E/ R) = lts(E)/R. lts((Q1 || ... || Qn)/ R) = lts(Q1)/R || ... || lts(Qn)/R 

Hiding\:

 lts(E\B) = lts(E)\B.

Interface @:

 lts(E@ I) = lts(E)\B where B = α(lts(E)) – I.