Note: This content is accessible to all versions of every browser. However, this browser does not seem to support current Web standards, preventing the display of our site's design details.

  

On the connections between PCTL and Dynamic Programming

Author(s):

F. Ramponi, D. Chatterjee, S. Summers, J. Lygeros
Conference/Journal:

vol. AUT09-13, pp. 10, Also available at: http://arxiv.org/abs/0910.4738
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.

Year:

2009
Type of Publication:

(04)Technical Report
Supervisor:

J. Lygeros

File Download:

Request a copy of this publication.
(Uses JavaScript)
% Autogenerated BibTeX entry
@TechReport { RamEtal:2009:IFA_3412,
    author={F. Ramponi and D. Chatterjee and S. Summers and J. Lygeros},
    title={{On the connections between PCTL and Dynamic Programming}},
    institution={},
    year={2009},
    number={},
    address={},
    month=oct,
    url={http://control.ee.ethz.ch/index.cgi?page=publications;action=details;id=3412}
}
Permanent link