Herein we study the probabilization of Quantified Linear Temporal Logic, which we call PQLTL. PQLTL can reason about any semialgebraic constrain over probabilities of paths of a Markov chain satisfying a QLTL formulae. PQLTL is related with other commonly used probabilistic temporal logics (such as PLTL, PCTL and PCTL*) that were devised only to specify properties for which model checking algorithms are amenable and whose basic results, such as completeness and decidability, were never investigated. In this article, we devise a strong and a weak SAT algorithm for PQLTL. The former relies in [n+2]-EXPSPACE and the latter in [n+1]-EXPSPACE where n is the alternation depth of the quantifiers in the input formula. The weak SAT algorithm for the existential fragment, which has all the expressive power of PQLTL, is in EXPSPACE. Another relevant fragment of PQLTL is the linear closure of PCTL* without nesting of the probability operator. We show that the SAT problem for this fragment is PSPACE complete. Capitalizing in these results, we derive a complete calculus for PQLTL and illustrate it with a toy example.
