On the connections between PCTL and dynamic programming

Probabilistic Computation Tree Logic (PCTL) is a well-known modal logic which has become a standard for expressing temporal properties of finite-state Markov chains in the context of automated model checking. In this paper, we consider PCTL for noncountable-space Markov chains, and we show that there is a substantial affinity between certain of its operators and problems of Dynamic Programming. We prove some basic properties of the solutions to the latter. We also provide two examples and demonstrate how recovery strategies in practical applications, which are naturally stated as reach-avoid problems, can be viewed as particular cases of PCTL formulas.