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

870 questions

988 answers


439 users

0 votes

Hi, I have a question regarding the following example:


I try to do local model checking, first for s4:


Why is s4 |- x1 wrong in this case?

I thought this would be a fixpoint since it's the same as vertex 0 and then it would be true if everything else is true.

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

1 Answer

+1 vote
Best answer
Node 11 closes a loop to node 0. Hence, the function LoopCheck as defined on slide 105 is called. For µ, this is false. For nu, it'd be true.

Basically, the meaning of this closed loop is “state s4 is included if state s4 is included”. Since µ is the least, not the greatest fixpoint, we decide not to include s4.
by (25.2k points)
selected by
Imprint | Privacy Policy