Looping in local model checking

Question

Comments

Hello Professor, Question on point #3:
Is there any example I can solve this on? I want to understand how it looks .


You said :
3. Whether a fixpoint is a least or greatest one does not matter for the choice of initial states, nor does it matter much for the proof tree construction. It matters only if we encounter a loop in which case the greatest fixpoint holds, but the least one does not hold.


Thank you.

Answer 1

You can find examples, and the explanation of the different treatment of mu/nu on the slides 107 ff of the µ-calculus chapter. Also you can easily create examples considering CTL model checking by noting that strong operators like E[x SU y] yield least fixpoints while the corresponding weak ones E[x WU y] yields a greatest fixpoint. Then you can check the difference on a suitable transition system that satisfies the one but not the other formula.