# Mew Calculus - CTL manipulation without using mew calculus formula

+1 vote
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 ?

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.

by (166k points)
selected by