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

868 questions

986 answers

1.4k comments

438 users

0 votes

With Initial State s0                                              With Initial state s7

I am solving 1 local model checking question and I had some issue so I checked the step using tool and I have below query:

In the 1st picture, from 2nd step to 3rd step (Highlighted part), the tool just ignored the RHS of cunjunction i.e (s0, []x1) while in other picture with different initial state for the same formula it checked the RHS. 

Did the tool already checked that path contains loop i.e Termination check and it will stuck in loop so ignored this path ?

in * TF "Emb. Sys. and Rob." by (2.9k points)
edited by

1 Answer

+1 vote
 
Best answer
The tool is not that clever; when checking a conjunction phi&psi, it first checks whether phi holds on that state. If phi holds on the sate (as in the second example), the tool has to check next whether psi holds also on the state.  The result of checking psi is then also the result of checking phi&psi (as in the second example).

However, if phi should not hold on the state (as in the first example), we already know that phi&psi does also not hold, and therefore, there is no need to check psi anymore. We can directly state that phi&psi does also not hold on the state, since phi does not hold there.

If you change the conjunction phi&psi to psi&phi, the tool behaves differently. It does not use a heuristic or so, and just checks the left sub-formula first, and then -- if needed -- the second one.
by (139k points)
selected by
Yes totally clear now.
Thank you
Imprint | Privacy Policy
...