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.