0 votes

Below we have two kripke structures where we need to find whether EFGb and EFGa hold respectively. 
I have gone through the solution but they are not clear and kind of conflicting.
Both the property have the same Path and Temporal operator EFG and just differ by the literals. Although the kripke structures are different but still logic of one solution does not apply to another one.
Could you please explain me the logic EFG(phi) which can satisfy both the solutions?

Diagram 1 - 2021-02 Q4.c

Diagram 2 - 2020-02 Q4.c

in * TF "Emb. Sys. and Rob." by (250 points)

1 Answer

+2 votes
Best answer
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.
by (92.2k points)
selected by

Related questions

Imprint | Privacy Policy