Sciweavers

Share
HYBRID
2010
Springer

On the connections between PCTL and dynamic programming

10 years 11 days ago
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
Federico Ramponi, Debasish Chatterjee, Sean Summer
Added 28 May 2010
Updated 28 May 2010
Type Conference
Year 2010
Where HYBRID
Authors Federico Ramponi, Debasish Chatterjee, Sean Summers, John Lygeros
Comments (0)
books