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

1.1k questions

1.3k answers

1.7k comments

556 users

0 votes

I had attached the question and the solution of local model checking from a past paper. Doesn't local model checking fail as there is a mu and loop?

Could you please explain this answer

in * TF "Emb. Sys. and Rob." by (200 points)
If image is unclear,  it is 2019\08\27 paper, Problem 4 a)

1 Answer

0 votes
The local model checking tree has a loop on nodes 4->5->6->7->8->9->4 where nodes 4 and 7 contain fixpoint formulas with a greatest fixpoint. The outermost fixpoint of the loop does therefore not cover a least fixpoint formula (in that case it would be false), but a greatest one, so it is true.

Don't be confused; the mentioned greatest fixpoint is contained in a least fixpoint that is found in nodes 1 and 15. The nodes 1 and 15 expose the greatest fixpoints in nodes 4 and 7, but neither node 1 nor node 15 is on the mentioned loop.
by (170k points)
Is there a order of precedence that needs to be followed while splitting the equation?
Well, we have to follow the syntax tree to decompose the formula, and this determines an ordering.
Imprint | Privacy Policy
...