期刊
THEORETICAL COMPUTER SCIENCE
卷 515, 期 -, 页码 1-18出版社
ELSEVIER
DOI: 10.1016/j.tcs.2013.09.032
关键词
Discrete-time Markov processes; PCTL model checking; Infinite-horizon properties; Bellman equations; Absorbing sets
This work is devoted to the formal verification of specifications over general discrete-time Markov processes, with an emphasis on infinite-horizon properties. These properties, formulated in a modal logic known as PCTL, can be expressed through value functions defined over the state space of the process. The main goal is to understand how structural features of the model (primarily the presence of absorbing sets) influence the uniqueness of the solutions of corresponding Bellman equations. Furthermore, this contribution shows that the investigation of these structural features leads to new computational techniques to calculate the specifications of interest: the emphasis is to derive approximation techniques with associated explicit convergence rates and formal error bounds. (C) 2013 Elsevier B.V. All rights reserved.
作者
我是这篇论文的作者
点击您的名字以认领此论文并将其添加到您的个人资料中。
推荐
暂无数据