Do we try to prevent cycles in temporal logic (CTL)?

19 Views Asked by At

When looking at the formulas for the rules in CTL, it is said that we save the states we have already been in a in list/ set. Does that mean that we are trying to preven endless loops? enter image description here For example given the model in the picture if we wanna check for EG, do we way that that $EG q$ holds true for {s0, s3, s0, s3, s0, s3, .....} or just {s0, s3}, it is my understanding that once we visite one state we can't get back to it?