Polytime model checking for times probabilistic computation tree logic (Q1127817)

We consider the model checking problem for timed probabilistic computation tree logic (TPCTL) introduced by H. A. Hansson and D. Jonsson, and studied in a recent book by \textit{H. A. Hansson} ``Time and probability in formal design of distributed systems'' (Elsevier, 1994). The semantics of TPCTL is defined in terms of probabilistic transition systems. It is shown in this book that model checking for TPCTL has exponential time complexity, the latter being measured in terms of the size of formula, the size of transition system and the value of explicit time that appears in the formula. Besides that, some polytime decidable classes are described in the cited book, the proofs being rather voluminous. We show, by a short proof, that this model checking problem is polytime decidable in the general case. The proof is essentially based on results on the complexity of Markov decision processes.