On the connections between PCTL and dynamic programming

Probabilistic Computation Tree Logic (PCTL) is a wellknown 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. Categories and Subject Descriptors I.6.4 [Simulation and modeling]: Model Validation and Analysis General Terms Theory Keywords PCTL, dynamic programming, Markov processes, integral equation

• Type: Conference
• Year: 2010
• Where: HYBRID
• Authors: Federico Ramponi, Debasish Chatterjee, Sean Summers, John Lygeros
• Keywords: Dynamic Programming, HYBRID 2010, Hybrid Systems, Markov Chains, finite-state Markov Chains