• 主题
高级搜索  >
历史搜索 清空历史
首页> 外文会议>2011 Eighth International Conference on Quantitative Evaluation of Systems >Model Checking MDPs with a Unique Compact Invariant Set of Distributions
【24h】

Model Checking MDPs with a Unique Compact Invariant Set of Distributions

机译：具有唯一的紧凑不变分布集的模型检查MDP

获取原文
页面导航
  • 摘要
  • 著录项
  • 相似文献
  • 相关主题

摘要

The semantics of Markov Decision Processes (MDPs), when viewed as transformers of probability distributions, can described as a labeled transition system over the probability distributions over the states of the MDP. The MDP can be seen as defining a set of executions, where each execution is a sequence of probability distributions. Reasoning about sequences of distributions allows one to express properties not expressible in logics like PCTL, examples include expressing bounds on transient rewards and expected values of random variables, as well as comparing the probability of being in one set of states at a given time with another set of states. With respect to such a semantics, the problem of checking that the MDP never reaches a bad distribution is undecidable~cite{qest10}. In this paper, we identify a special class of MDPs called emph{semi-regular} MDPs that have a unique non-empty, compact, invariant set of distributions, for which we show that checking any $omega$-regular property is decidable. Our decidability result also implies that for semi-regular probabilistic finite automata with isolated cut-points, the emptiness problem is decidable.
机译：当被视为概率分布的转换器时，马尔可夫决策过程（MDP）的语义可以描述为MDP状态上概率分布上的标记过渡系统。可以将MDP视为定义了一组执行，其中每个执行都是一系列概率分布。关于分布序列的推理使一个人​​可以表达在诸如PCTL之类的逻辑中无法表达的属性，示例包括表达瞬态奖励的边界和随机变量的期望值，以及将给定时间处于一组状态的概率与另一组状态进行比较状态集。关于这种语义，检查MDP永远不会达到不良分布的问题是无法确定的{qest10}。在本文中，我们确定了称为Emph {semi-regular} MDP的一类特殊的MDP，它们具有唯一的非空，紧凑，不变的分布集，对于这些MDP，我们证明检查$ omega $ -regular属性是可以确定的。我们的可判定性结果还暗示，对于具有孤立切点的半规则概率有限自动机，空性问题是可判定的。

著录项

相似文献

  • 外文文献
  • 中文文献
  • 专利
获取原文

客服邮箱：kefu@zhangqiaokeyan.com

京公网安备：11010802029741号 ICP备案号：京ICP备15016152号-6 六维联合信息科技 (北京) 有限公司©版权所有

  • 客服微信

  • 服务号