x = F(x)and call x a fixed point.
AG phi = phi AX (AG phi);This says: AG phi holds at a state s iff phi holds at state s and AG phi holds at all immediate successor states of s.
EG phi = phi EX (EG phi);This says: EG phi holds at a state s iff phi holds at state s and EG phi holds at at least one immediate successor state of s.
AF phi = phi AX (AF phi);This says: AF phi holds at a state s iff phi holds at state s, or AF phi holds at all immediate successor states of s.
EF phi = phi EX (EF phi);This says: EF phi holds at a state s iff phi holds at state s, or EF phi holds at at least one immediate successor state of s.
A[phi1 U phi2] = phi2 (phi1 AX (A[phi1 U [phi2]));This says: A[phi1 U phi2] holds at a state s iff either phi2 holds at state s, or phi1 holds at state s and A[phi1 U phi2] holds at all immediate successor states of s.
E[phi1 U phi2] = phi2 (phi1 EX (E[phi1 U [phi2]));This says: E[phi1 U phi2] holds at a state s iff either phi2 holds at state s, or phi1 holds at state s and E[phi1 U phi2] holds at at least one immediate successor state of s.
E[phi1 U phi2] = phi2 (phi1 EX (E[phi1 U [phi2]))by unfolding it from left to right, we can compute the set of states that satisfy E[phi1 U phi2] by means of a while-statement. Initially, only the states with a phi2 label get a E[phi1 U phi2] label. Then, we keep adding new such labels to states if they have a phi1 label and some successor state with an "old" E[phi1 U phi2] label. We keep doing this until no new labels are found. One can now prove that this procedure computes the correct set of states according to the satisfaction relation for CTL (exercise). The procedure outlined above computes the least fixed point of the function F(y) = phi2 (phi1 EX (y)).
AG phi = EF ( phi)It requires the greatest fixed point to compute the correct sets for AG and EG. For example, for AG phi, we assume the all states that satisfy phi have been labeled in this manner. Then we initially label ALL states with AG phi, but then we keep DELETING labels from states s which have at least one immediate successor state s' that is not labeled with AG phi. We keep doing this until no further deletions occur. (Exercise: describe the procedure for computing the state set for EG phi).