 Propositional temporal logics can be extended with quantifiers over atomic propositions (see Rescher and Urquhart 1971, Chapter XIX). Semantically, these quantify over all valuations of the respective atomic propositions and hence are tantamount to monadic second-order quantifiers. The resulting languages are very expressive, and the respective logics are usually undecidable (often not even recursively axiomatizable). Notable extensions include the logic QPTL, the quantified propositional version of LTL (which is decidable albeit with non-elementary complexity), as well as the extension of CTL* (see French 2001). Complete axiomatic systems and decidability results for the quantified propositional temporal logic QPTL (with and without past operators) have been presented in Kesten and Pnueli (2002) and French and Reynolds (2003).