On the connections between PCTL and Dynamic Programming
Optimization and Control
2012-02-22 v1 Systems and Control
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.
Cite
@article{arxiv.0910.4738,
title = {On the connections between PCTL and Dynamic Programming},
author = {Federico Ramponi and Debasish Chatterjee and Sean Summers and John Lygeros},
journal= {arXiv preprint arXiv:0910.4738},
year = {2012}
}
Comments
Submitted