The paper presents a sound and (relatively) complete deductive proof system for the verification of CTL* properties over possibly infinite-state reactive systems. The proof system is based on a set of proof rules for the verification of basic CTL* formulas, namely CTL* formulas with no embedded path quantifiers. We first present proof rules for some of the most useful basic CTL* formulas, then present a methodology for transforming an arbitrary basic formula into one of these special cases. Finally, we present a rule for decomposing the proof of a general (non-basic) CTL* formula into proofs of basic CTL* formulas.
13th International Conference on Concurrency Theory