On the connections between PCTL and Dynamic Programming

TL;DR

This paper extends PCTL to noncountable-state Markov chains and reveals its connections to Dynamic Programming, illustrating how practical reach-avoid problems relate to PCTL formulas.

Contribution

It introduces a PCTL definition for noncountable-state Markov chains and links certain operators to Dynamic Programming, with practical examples.

Findings

PCTL can be extended to noncountable-state Markov chains.

Certain PCTL operators are closely related to Dynamic Programming problems.

Reach-avoid strategies can be formulated as PCTL formulas.

Abstract

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 give a definition of 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. After proving some uniqueness properties of the solutions to the latter, we conclude the paper with two examples to show that some recovery strategies in practical applications, which are naturally stated as reach-avoid problems, can be actually viewed as particular cases of PCTL formulas.