Polytime model checking for timed probabilistic computation tree logic

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 H. A. Hansson [Han94]. The semantics of TPCTL is defined in terms of probabilistic transition systems. It is shown in [Han94] 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, [Han94] describes some polytime decidable classes, 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.