In the first example (2021-02), EFGb is to be checked. EFGb is equivalent to the CTL formula EF EG b, so that we first determine the states where EG b holds. That means to check which states have an outgoing infinite path where always b holds. These are the states {s0;s2;s3;s5;s6}. Next, we have to check the EF operator which means we now have to determine the states that have an outgoing path that reaches one of the states in {s0;s2;s3;s5;s6} which are the states {s0;s1;s2;s3;s4;s5;s6}, i.e., all states except for s7.

In the second case, we apply the same reasoning and get {s2;s3;s6} as the states that satisfy EG a, and EF EG a holds in states {s0;s1;s2;s3;s4;s5;s6}, i.e., all states except for s7.