Decision procedures and expressiveness in the temporal logic of branching time (Q2265816)

\textit{E. A. Emerson} and \textit{E. M. Clarke} [Sci. Comput. Program. 2, 241- 266 (1982; Zbl 0514.68032)] have proposed the computation tree logic (CTL), which is the unified branching time logic (UB) of \textit{M. Ben- Ari}, \textit{Z. Manna} and \textit{A. Pnueli} [8th ACM Symp. on Principles of Programming Languages, 164-176 (1981)] augmented with an until operator. This paper gives an exponential decision procedure for deciding satisfiability in CTL with the small model theorem and its complete axiomatization. The relative expressive power of temporal logics obtained by extending or restricting the syntax of UB and CTL is also studied.