Decision procedures and expressiveness in the temporal logic of branching time

We consider the computation tree logic (CTL) proposed in (Sci. Comput. Programming 2 (1982), 241-260) which extends the unified branching time logic (UB) of ("Proc. Ann. ACM Sympos. Principles of Programming Languages, 1981," pp. 164-176) by adding an until operator. It is established that CTL has the small model property by showing that any satisfiable CTL formulae is satisfiable in a small finite model obtained from the small "pseudomodel" resulting from the Fischer-Ladner quotient construction. Then an exponential time algorithm is given for deciding satisfiability in CTL, and the axiomatization of UB given in ibid. is extended to a complete axiomatization for CTL. Finally, the relative expressive power of a family of temporal logics obtained by extending or restricting the syntax of UB and CTL is studied. © 1985.