马尔可夫过程上无限时域规范的刻画与计算
最优化与控制
2014-07-23 v4 计算机科学中的逻辑
系统与控制
概率论
摘要
本工作致力于对一般离散时间马尔可夫过程上的规范进行形式化验证，重点在于无限时域属性。这些属性在一种称为 PCTL 的模态逻辑中表述，可以通过定义在过程状态空间上的值函数来表达。主要目标是理解模型的结构特征（主要是吸收集的存在）如何影响相应 Bellman 方程解的唯一性。此外，本文表明，对这些结构特征的研究导致了计算感兴趣规范的新计算技术：重点在于推导具有相关显式收敛速率和形式误差界的近似技术。
引用
@article{arxiv.1211.4346,
title = {Characterization and computation of infinite horizon specifications over Markov processes},
author = {Ilya Tkachev and Alessandro Abate},
journal= {arXiv preprint arXiv:1211.4346},
year = {2014}
}