Here you can ask questions and find or give answers to organizational, academic and other questions about studying computer science.

915 questions

1k answers

1.4k comments

441 users

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 (142k points)
selected by

Related questions

0 votes
1 answer
asked Sep 1, 2022 in * TF "Emb. Sys. and Rob." by learner (350 points)
0 votes
1 answer
0 votes
1 answer
asked Aug 30, 2022 in * TF "Emb. Sys. and Rob." by ss (160 points)
0 votes
1 answer
asked Aug 24, 2022 in * TF "Emb. Sys. and Rob." by ln (1k points)
0 votes
1 answer
asked Aug 24, 2022 in * TF "Emb. Sys. and Rob." by CS_E (2.9k points)
Imprint | Privacy Policy
...