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.
Cite as: Machi, H., Tomita, K. and Hosono, C. (2005). The Relative Completeness of a Version of CTL*. In Proc. Eleventh Computing: The Australasian Theory Symposium (CATS2005), Newcastle, Australia. CRPIT, 41. Atkinson, M. and Dehne, F., Eds. ACS. 81-85.
(from crpit.com)
(local if available)