Maybe you are confused about the syntax, so I maybe explain that first (but you may also consult https://es.cs.uni-kl.de/tools/teaching/QuartzRef.pdf):
- <>phi holds in a state if that state has a successor state which satisfies phi. Having computes the states Sphi where phi holds, you can compute the states that satisfy <>phi as pre∃(Sphi).
- []phi holds in a state if that state either has no successors or if all of its successor states satisfy phi. Having computes the states Sphi where phi holds, you can compute the states that satisfy []phi as pre∀(Sphi).
- <:>phi holds in a state if that state has a predecessor state which satisfies phi. Having computes the states Sphi where phi holds, you can compute the states that satisfy <:>phi as suc∃(Sphi).
- [:]phi holds in a state if that state either has no predecessors or if all of its predecessor states satisfy phi. Having computes the states Sphi where phi holds, you can compute the states that satisfy [:]phi as suc∀(Sphi).
- if you have computed the states that satisfy phi&psi and as Sphi and Spsi, respectively, then the states that satisfy phi&psi are computes as Sphi ∩ Spsi
- if you have computed the states that satisfy phi∨psi and as Sphi and Spsi respectively, then the states that satisfy phi∨psi are computes as Sphi ∪ Spsi
- if you have computed the states that satisfy ¬phi as Sphi, then the states that satisfy ¬phi are computes as S\Sphi.
Then, just the fix point operators remain. As explained in the slides, µx. is a least fixpoint that we write in ASCII syntax as mu x. and the greatest fix point is written as nu x. . How these are computed, you will find in the lecture slides (it is a fix point computation that requires to repeatedly compute starting with x being either false or true, and then replacing the value of x with the value you got for in the next iteration).
You may also have a look at the model checking tool https://es.cs.uni-kl.de/tools/teaching/ModelChecking.html that can explain such calculations to you.
