Say I have the following transition system:
I've understood how I can tell if □a and ⟡b are valid (□a is invalid because a is not true is S2 and ⟡b is valid there is a state (i.e. S1) in which b is true. Please correct me if I'm wrong). But how do I reason the validity of the following formulas:
□(a -> b)
□⟡(a ^ b)
?