Verification of probabilistic systems is an active research field due to its wide range of applications. However, the logics usually employed for these purposes (PCTL, PLTL) lack the expressiveness to assert some common requirements. We present an enrichment of the quantified temporal logic originally proposed by Vardi that addresses this problem by allowing reasoning about any semialgebraic constrain over probabilities of paths on Markov chains. We adapt the usual Model Checking techniques to accommodate the increase in expressiveness and devise a SAT algorithm based on Tarski’s result about real algebraic fields. We also present a reduct of this logic that retains much of the expressiveness while having significantly less demanding SAT and MC algorithms. Finally, capitalizing on the SAT, we present a complete Hilbert calculus for the logics. Joint work with M. Biscaia, P. Baltazar and P. Mateus