Mew Calculus - CTL manipulation without using mew calculus formula

Question

Dear Prof. and Team,

S4= EFE[ b SB a]

[b SB a] means, left side needs to hold. So as b holds, we are choosing the states containing b , i.e 1,3,5,7

But here how is X0, X1,X2 values calculated and finally the value of EFE[b SB a] too ?

https://drive.google.com/open?id=1NJL-UsQF1KEkjOYdv5pMkxGjxbArjGez

https://drive.google.com/open?id=1fUu_stBXVutkSB5UYvHVSVOhj4rYRDon

https://drive.google.com/open?id=1t6_pS6_MVRW5oQhbkFPmmYpeEwTrNj0g

Answer 1

You are wondering how the states satisfying E[b SB a] are computed. To that end, you first have to check the fixpoint formulation of this CTL formula which is µZ.(!a & (phioo & b | <>Z)). It is based on the recursion E[b SB a] = !a & (b | EXE[b SB a]) where phioo means states having infinite outgoing paths.

Every state of the structure has an outgoing transition, so all states have an outgoing infinite path, and phi00 = {s0;s1;s2;s3;s4;s5;s6;s7}. Now, let's first compute the states of E[b SB a] by µ-calculus by our model checker:

computing states of E[b SB a], i.e., µZ.(!a & (phioo & b | <>Z))

        〖a〗= {s0;s2;s4;s6}
        〖!a〗= {s1;s3;s5;s7}
        〖b〗= {s0;s1;s3;s5;s7}
        〖phioo & b〗=〖b〗= {s0;s1;s3;s5;s7}
    step 0 : Z = {} (this is X0 in the example solution)
        〖Z〗= {}
        〖<>Z〗 = {}
        〖phioo & b | <>Z〗 = {s0;s1;s3;s5;s7}
        〖!a & (phioo & b | <>Z)〗 = {s1;s3;s5;s7}
    step 1 : Z = {s1;s3;s5;s7} (this is X1 in the example solution)
        〖Z〗= {s1;s3;s5;s7}
        〖<>Z〗 = {s0;s1;s2;s3;s4;s5;s7}
        〖phioo & b | <>Z〗 = {s0;s1;s2;s3;s4;s5;s7}
        〖!a & (phioo & b | <>Z)〗 = {s1;s3;s5;s7}
fixpoint reached -->〖Z〗= {s1;s3;s5;s7} (this is X2 in the example solution)

Now, I understand you want to do that less formal, and more comprehensively, which is great! 

So, E[b SB a] means all states having an outgoing path where b holds before a holds, and b must eventually hold. In particular, this is true in the states where b&!a holds (just b as you said it not sufficient!), i.e., {s1;s3;s5;s7}. These states are found by the model checker in step 0. 

From these states, we work `backwards', i.e., add existential predecessors that satisfy !a&!b as long as new ones are added. This is done in step 1: Existential predecessors of {s1;s3;s5;s7} are {s0;s1;s2;s3;s4;s5;s7} but none of them satisfies !a&!b, so no new states are added and we already got our fixpoint as {s1;s3;s5;s7}.

Remarks: 

1. The fixpoint calculation in µ-calculus is a bit different, since it starts with Z={}, but the next step is where you would really want to start. 
2.  µZ.(!a & (phioo & b | <>Z)) can be rewritten to µZ.(!a & b & phioo | !a & !b & <>Z)) so that you can see that we start with !a & b & phioo and continue adding existential  predecessors that satisfy !a & !b.