mu-Calculus and Bisimulation Relations

Question

Are those two graphs in the example on slide 29 supposed to be Kripke structures? If so, the states with label a, b, c should be removed on both graphs I think. They are not reachable and don't belong to the Kripke structure according to what we've learned so far (?).

Then, those two graphs are even isomorphic, since only their initial state is left.

To fix this example, I think you should make the states with label b and c initial states as well.

Answer 1

Short answer: No, that slide is correct.

More about that: In general, Kripke structures are allowed to have deadend states, and even initial states may have in general no outgoing transitions. `Allowed' means that we can define the meaning of temporal logic formulas on such structures. In particular, model checking properties of the µ-calculus is no problem on all kinds of Kripke structures, and can even detect such deficiencies.

Why did we then bother you will all of these problems? By personal experience, I can tell you that if these deficiencies are there, something is wrong with the system that you are modeling, and if you would just check LTL properties (which state that on all infinite paths starting in all initial states something holds), you could prove everything on broken structures where there are no infinite paths at all. This way, you may "verify" those LTL properties, but these would just be vacuously satisfied as if you would prove some formula false->phi where phi is some very large formula.

So, while no "sanity checks" have to be made on Kripke structures to perform verification, it is strongly recommended to do so to make sure that the system model is not broken.

Comments

Thanks for the answer. As a feedback then, I think you should be more precise in the exercises (and probably in the exam as well, but I haven't looked at those), on what exactly you expect from us.

Right now, it feels very arbitrary, if deadend or non-reachable states should be submitted / belong to the Kripke structure or not, see e.g. my previous question (https://q2a.cs.uni-kl.de/667/can-deadends-in-kripke-structures-be-initial-states). It's very frustrating to lose time because of this, especially in the last exercise sheet.