Strong Low Bisimulation on Configurations and Strong Low Bisimulation on Programs

[AlexanderF]

hello,

in Exercise 9.2
there are no strong low bisimulations on programs for:

a) ii) ([skip], [l1 := 0])
iii) ([l1 := 0||l1 := 1], [l1 :=1||l1 := 0])
b) i) ([S], [S]) where S = (l2 := 0; if l2 = 0 then l1 := 0 else l1 := h1 fi)


But do I see right that there are actually strong low bisimulations on configurations in these cases, i.e. for:

-(([skip], sigma), ([l1 := 0], sigma')) for each low-equal sigma, sigma' with sigma(l1)=0(=sigma'(l1))

e.g. R:= symmetric closure of
{(([skip], sigma), ([l1 := 0], sigma')),
(([], sigma), ([], sigma'))}

-(([l1:=0||l1:=1], sigma), ([l1:=1||l1:=0], sigma')) for each low-equal sigma, sigma'

e.g. R := symmetric closure of
{(([l1:=0||l1:=1], sigma), ([l1:=1||l1:=0], sigma')),
(([l1:=1], sigma[l1/0]), ([l1:=1], sigma'[l1/0])),
(([l1:=0], sigma[l1/1]), ([l1:=0], sigma'[l1/1])),
(([], sigma[l1/1]), ([], sigma'[l1/1])),
(([], sigma[l1/0]), ([], sigma'[l1/0]))}

-((S, sigma), (S, sigma')) for each for each low-equal sigma, sigma'
(where again S = (l2 := 0; if l2 = 0 then l1 := 1 else l1 := h1 fi))

e.g. R:= symmetric closure of
{(([S], sigma), ([S], sigma')),
(([if l2=0 ...], sigma[l2/0]), ([if l2=0 ...], sigma'[l2/0])),
(([l1:=0], sigma[l2/0]), ([l1:=0], sigma'[l2/0])),
(([], sigma[l2/0][l1/0]), ([], sigma'[l2/0][l1/0]))}


the differences between strong low bisimulations on configurations and strong low bisimulations on programs,
I think are,
-that in strong low bisimulations on configurations the states are part of the places of the transitions system,
whereas in the strong low bisimulations on programs they are not (resulting in an different result for 9.2 b) i) ) and
-that in the definition of strong low bisimulations on programs the right hand program L1' needs to execute the same thread (i) as the left hand program L1 (whenever L1 R L1'),
whereas this is not required in the definition of strong low bisimulations on configurations
(leading to the different result for 9.2 a) iii) ).


So I conclude that:
- forall low-equal sigma, sigma', (L, sigma) "strongly low bisimilar on configurations" to (L', sigma'),
does not imply
- L "strongly low bisimilar on programs" to L',

is this correct?


best regards,
Alexander

[ximl]

Hi Alexander,

I did not read in detail all your arguments about the example
programs, but it is correct that for each of the examples
a strong low bisimulation on configurations can be constructed
such that the pairing of the two programs with some pair/
all pairs of low equal states is in the bisimulation relation.

It is also correct that

- \forall \sigma, \sigma'. \sigma "low equals" \sigma' =>
<L, \sigma> "strongly low bisimilar on config. to" <L', \sigma'>
does not imply
- L "strongly low bisimilar on programs to" L'

With our definitions, "strong low bisimulation on configurations"
takes a global perspective, and comes with the assumption that
the states cannot be modified by the environment of a multi-threaded
program. On the other hand, "strong low bisimulation on programs"
takes a local perspective, and comes with the assumption that
the states might be modified by the environment of a thread.

Note that, in general, it is still possible to obtain strong low
bisimulation on programs from a suitable definition of strong
low bisimulation on configurations, using a product construction.

Best regards,
Ximeng