Zohar Manna introduced temporal logic in order to speak formally about properties of programs which are not expressible in other program logics. The paper presents two closely related propositional probabilistic temporal logics. The syntax is typically temporal while the semantics uses probability theory. Namely a model of \(PTL_ b\) (probabilistic temporal logic for concurrent programs) is a discrete Markov chain for which there is \(\alpha >0\) such that all nonzero transition probabilities are \(\geq \alpha\). A model for \(PTL_ f\) (probabilistic temporal logic for sequential programs) is a finite Markov chain. The authors describe these two calculi in a systematic way. The axiom systems are given, the decision procedures for satisfiability are found, the completeness theorems are proved. The decision procedures are based on tableau methods. They give deterministic exponential time cost for testing satisfiabilty of \(PTL_ b\) and \(PTL_ f\). These parts of the paper which concern decidability procedures are quite nontrivial, use deep facts from Markov chain theory, and give new insight into the theory of probabilistic programs.