Example
	• Next mark all the states in which AF C1 is true, etc. – The algorithm tracks states visited using depth-first search – Slight variations for AF, AG, EF, EG, etc. • At termination, (not T1) OR AF C1 is true everywhere – Hence the temporal property is true for the state machine