The Relative Completeness of a Version of CTL*
We show the relative completeness of a version of CTL* over possibly infinite states. It is based on a fair discrete system, which is with strong and weak fairness. Validity of a CTL* formula is reduced to the validity of an assertion by eliminating the temporal operators and path quantifiers inductively. The idea is to represent the predicate describing that "a fair path begins with the current state" in the underlying assertion language using fixpoint operators.