Expansive-Bisimulation for Context-Free Processes - Formal Methods and Hybrid Real-Time Systems - page 475

Definition 1. A binary relation R ⊆S×S is a bisimulation if for all ( α, β ) ∈ R

the following hold:

1. α = if and only if β = ;
2. whenever α

a
−→

a
−→ α ,then β β for some β with ( α ,β )

∈ R ;

a
−→

a
−→ β ,then α α for some α with ( α ,β ) 3. whenever β ∈ R .

Two states α and β are said to be bisimulation equivalent, written α ∼ β ,if

there is a bisimulation R such that ( α, β ) ∈ R .

It is well know that is an equivalence relation between processes. Moreover it

is a congruence with respect to concatenation of sequences of processes.
Note that in general clause 1. of Definition 1 is necessary. Since here we use
the general summation notation Σ to write expressions, and when the index set
is empty, Σ i∈∅ E i is the inactive process which should not be equated with .
Otherwise the congruence property of

∼

∼ would fail. With clause 1. in Definition

1 this cannot happen.
An important notion in the study of bisimulation of context-free processes is
that of self-bisimulation proposed by Caucal [Cau90].

,wedenoteby R → the least
precongruence wrt sequential composition containing R ,denoteby R ↔ the
symmetric closure of R → ,denoteby R ↔ ∗ the reflexive and transitive closure
of R ↔ .

Definition 2. For any binary relation R on S

Definition 3. A binary relation B ⊆S×S is a self-bisimulation if for all

( α, β ) ∈ B , α = just in case β = and moreover the following hold:

a
−→

a
−→

B ↔ ∗ ; α ,then β β for some β with ( α ,β ) 1. whenever α ∈

a
−→

a
−→

B ↔ ∗ .

β ,then α α for some α with ( α ,β )

2. whenever β ∈

Note that for a finite relation, checking if it is a self-bisimulation is in general only
semi-decidable since one needs to check membership of its congruence closure.

Proposition 1. [Cau90] If B is a self-bisimulation then B ↔ ∗ ⊆∼ .

B ↔∗ .Thusif( α, β ) is contained in a self-bisimulation than Obviously B ⊆

α ∼ β .

For the process system , an important finiteness property which

forms the base of our discussion in the paper is that, although the number
of reachable states from an arbitrary state α

S ,Act, −→

can be infinite, the processes
(closed expressions) that can occur in those reachable states must be from a finite
set. Another important finiteness property of

∈S

S ,Act, −→ is finite branching,

which says that for any α ∈S ,theset

a
−→

B ( α )= { β | a ∈ Act, α β }