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:

Stockholm, Sweden, Proceedings of the HSCC, pp. 253-262, 13th ACM International Conference on Hybrid Systems: Computation and Control (HSCC) presented
Abstract:

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.

Year:

2010
Type of Publication:

(01)Article
Supervisor:



File Download:

Request a copy of this publication.
(Uses JavaScript)
% Autogenerated BibTeX entry
@Article { RamEtal:2010:IFA_3539,
    author={F. Ramponi and D. Chatterjee and S. Summers and J. Lygeros},
    title={{On the Connections Between PCTL and Dynamic Programming}},
    journal={Proceedings of the HSCC},
    year={2010},
    volume={},
    number={},
    pages={253--262},
    month=apr,
    url={http://control.ee.ethz.ch/index.cgi?page=publications;action=details;id=3539}
}
Permanent link