Dealing with uncertainty in the context of planning is a natural research subject in Artificial Intelligence. Many of the techniques used capitalize upon the existence of very efficient SAT-solvers for propositional logic. We propose a temporal extension of a probabilistic logic, which on one hand allows us to deal with quantities/probabilities, and on the other hand allows us to simplify the temporal aspect of planning. We present an algorithm for deciding the satisfiability problem for this logic, presenting also a complete Hilbert calculus for it. The algorithm is intended to profit from the fast advances occurring in LTL SAT-solvers. We will then check some of the limitations of our logic regarding specification of properties, discussing some important open problems in Markov chains.