## What is "Locally Respects", Unwinding

momoto
Nichts ist wie es scheint
Beiträge: 23
Registriert: 14. Feb 2008 21:43

### What is "Locally Respects", Unwinding

Hi,

can someone try to explain me the term "Locally Respects". I just don't get it:

e.g. Exersice 8(Solution)/8.1/d claims that:
do(S1,l) ist untermenge von S2
Why? - do(S1,l)=S4 not S2
do(S2,l) ist untermenge von S1
Why? - do(S2,I)=S3 not S1

Any help is appreciated!

Sebastian Hartte
Sonntagsinformatiker
Beiträge: 236
Registriert: 15. Apr 2004 17:57

### Re: What is "Locally Respects", Unwinding

*edit* Oh I think I see why you are so confused about the solution: S1 is a set, s1 is the state!
momoto hat geschrieben:do(S1,l) ist untermenge von S2
Why? - do(S1,l)=S4 not S2
In the solution 8.1 d) two sets are defined:

S1 := {s1, s2, s5} (This is one equivalence class of ~L)
S2 := {s3, s4, s6} (This is the other equivalence class of ~L)

Then, do(SET, a) is defined intuitively as the set of all states that
you reach by executing "a" in any state contained SET.

So, do(S1, l) = { do(s1, l) } U { do(s2, l) } U { do(s5, l) } = {s4} U {s3} U {s6} = {s4, s3, s6}
do(S2, l) = { do(s3, l) } U { do(s4, l) } U { do(s6, l) } = {s2} U {s1} U {s5} = {s2, s1, s5}

Since {s4, s3, s6} and {s2, s1, s5} are equivalence classes of ~L, step consistency is shown for ~L. (And still has to be shown for ~H, which I won't show here)

Regarding the solution for exercise 8.1 e), which shows how locally respects is proven:

In my intuition you have to show, that even if an invisible action (here: h1 or h2) is taken, you "stay" in the same
equivalence class of ~L. To show this you just check for both equivalence classes of ~L (defined above as S1 and S2),
that for both "invisible" actions (h1 and h2) the result of the do function as defined above is a subset of the same
equivalence class.

In detail:
do(S1, h1) = { do(s1, h1) = s2 } U { do(s2, h1) = s5 } U { do(s5, h1) = s1 } = { s2, s5, s1 } (which is obviously a subset of S1)
do(S1, h2) = { do(s1, h2) = s1 } U { do(s2, h2) = s2 } U { do(s5, h2) = s5 } = { s1, s2, s5 } (which is obviously a subset of S1)
do(S2, h1) = { do(s3, h1) = s3 } U { do(s4, h1) = s4 } U { do(s6, h1) = s6 } = { s3, s4, s6 } (which is obviously a subset of S2)
do(S2, h2) = { do(s3, h2) = s4 } U { do(s4, h2) = s6 } U { do(s6, h2) = s3 } = { s4, s6, s3 } (which is obviously a subset of S2)

As you can see, if s is a state in S1 and you take a "high" action, the resulting state is again in S1. (Which just means the
new state is again in Relation ~L to the original state). The same holds for states in S2.

Since anything may interfere with H (as specified in the flow policy: H ~> H, L ~> H) you wont have to show this for ~H as well. (This is done in the solution for exercise 8.1 e) as well)

I hope this helped. And i also hope this is correct

momoto
Nichts ist wie es scheint
Beiträge: 23
Registriert: 14. Feb 2008 21:43

### Re: What is "Locally Respects", Unwinding

Many many Thanks! I think I get it now.
You saved my life.