Definition of Lambda-specific low bisimulation

kutschke
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 112
Registriert: 16. Apr 2009 10:39

Definition of Lambda-specific low bisimulation

Beitrag von kutschke » 2. Feb 2013 18:51

Hi,
my question concerns slide 66 from the concurrent non-interference slide set. In the definition of lambda-specific low bisimulation, we have the condition

(L1, sigma1, st1) ->i,p (L2,sigma2, st2) => exists ...

My question now is: Does this condition really need to be that strict or can it be weakened by requiring additionally that p > 0?

MatthiasP
Neuling
Neuling
Beiträge: 1
Registriert: 4. Okt 2011 12:52

Re: Definition of Lambda-specific low bisimulation

Beitrag von MatthiasP » 7. Feb 2013 09:21

Is your question whether you could replace the last requirement of the definition with
(L1, sigma1, st1) ->i,p (L2,sigma2, st2) => p>0?

The answer to this question is no. This is not an additional requirement at all, because the judgment (L1, sigma1, st1) ->i,p (L2,sigma2, st2) is only derivable for p>0.

The condition really must be that strict. Abstractly speaking this is necessary, because you want the indistinguishability that the relation models to be invariant under the execution of the programs.
A concrete example why you want this is the relation R={((skip;l:=h),(skip;l:=h))}. If you drop this requirement the relation would satisfy the definition, because l:=h cannot be related to itself and thus, the sum of the probabilities on both sides would be 0. However, the program has an obvious direct information flow and thus should not be self-bisimilar under the lambda-specific strong low bisimulation.

kutschke
BASIC-Programmierer
BASIC-Programmierer
Beiträge: 112
Registriert: 16. Apr 2009 10:39

Re: Definition of Lambda-specific low bisimulation

Beitrag von kutschke » 7. Feb 2013 21:54

Hi, thanks for the answer!
Yes, i forgot that we only can derive (L1, sigma1, st1)->i,p (L2,sigma2,st2) if p>0.

My question was actually if we could replace the last requirement by

(L1,sigma1,st1)->i,p (L2,sigma2,st2) AND p > 0 => exists ...

So, as i understand from your answer, this would actually just be redundant, and not weakening the definition. Thanks, this whole condition p>0 on the derivability was something that i completely missed and that would have caused trouble elsewhere too. Thanks for clearing things up :-)

Antworten

Zurück zu „Archiv“