Decision procedures and expressiveness in the temporal logic of branching time

In this paper we consider the Computation Tree Logic (CTL) proposed in [CE] which extends the Unified Branching Time Logic (UB) of [BMP] by adding an until operator. We establish that CTL has the small property by showing that any satisfiable CTL formulae is satisfiable in a small finite model obtained from a small “pseudo-model” resulting from the Fischer Ladner quotient construction. We then give an exponential time algorithm for deciding satisfiability in CTL, and extend the axiomatization of UB given in [BMP] to a complete axiomatization for CTL. Lastly, we study the relative expressive power of a family of temporal logics obtained by extending or restricting the syntax of UB and CTL.