Semantics of Modal Operators (exercise sheet 6 question 2)

Question

for part e and g I have no idea how to solve. Could you please help me?

Answer 1

“true” is the tautology. The formula that is always satisfied, no matter which evaluation you consider. This means that you are asked to compute those states whose all next (e)) / previous (g)) neighbor states satisfy the property of just being any arbitrary state.

Answer 2

I am no organizer of the course and only a student, but my approach was the following:

I remembered these symbols from the 05_Solution pdf on slide 4, they are just other meanings of expressing successors and predecessors with their extended universal oder existing attribute. If the parameter true is given, I think a valid set of states is given there, so I treated it like this. If false is given, I treated it as the empty set.

With this in mind I got the solution, I hope this is helping you.

Comments

Thanks a lot for your help :)
It was very useful.

Answer 3

Please have a look at slides 21-24 of Chapter 05, i.e., the µ-calculus. These operators are explained there in detail, and the above exercise just asks for the cornercases, i.e., when the formula where the modal operator is applied to is either false or true. That is simple if you remember those values for the predecessor and successor states that we already discussed.