Concurrency: State Models and Java Programs

C.6 Semantic Equivalences

Minimization of the LTS corresponding to an FSP process definition results in a semantically equivalent LTS. The equivalence relations used in performing minimization are defined in the following sections.

C.6.1 Strong Equivalence

Strong semantic equivalence equates LTSs that have identical behavior when the occurrence of all their actions can be observed, including that of the silent action τ.

Let be the universal set of LTSs. Strong semantic equivalence “~” is the union of all relations satisfying that (P, Q) ∈ R implies:

1. αP = αQ;

2. ∀a ∈ Act:

   • implies and (P′, Q′) ∈ R.

   • implies P′, and (P′, Q′) ∈ R.

3. P = Π iff Q = Π.

The LTSA tool performs minimization using strong equivalence if an LTS contains no silent actions (τ). For an LTS P, without τ-actions:

• minimized(P) ~ P.

C.6.2 Weak Equivalence

Weak semantic equivalence equates systems that exhibit the same behavior to an external observer who cannot detect the occurrence of τ-actions.

Let denote , where τ* means a sequence of zero or more τs. Then weak (or observational) semantic equivalence “≈” is the union of all relations satisfying that (P, Q) ∈ R implies:

1. αP = αQ;

2. ∀ a ∈ L ∪ {ε}, where L = Act – {τ}, and ε is the empty sequence:

   • implies Q′, and (P′, Q′) ∈ R.

   • implies P′, and (P′, Q′) ∈ R.

3. P = Π iff Q = Π.

The LTSA tool performs minimization using weak equivalence if an LTS contains silent actions (τ). For an LTS P, with τ-actions:

• minimized(P) ≈P.

Both strong and weak equivalence are congruences with respect to the composition, re-labeling, and hiding operators. This means that strongly or weakly equivalent components may substitute one another in any system constructed with these operators, without affecting the behavior of the system with respect to strong or weak equivalence, respectively.