连续时间Markov决策过程互模拟等价及逻辑保持

摘要：

模型检测中,Markov决策过程可以建模具有不确定性的系统,然而状态空间爆炸问题将会影响系统验证的成败与效率,互模拟等价可以用于系统状态的简约.在强互模拟关系的基础上,给出Markov决策过程模型弱互模拟等价关系的概念,导出了连续时间Markov决策过程及其内嵌离散时间Markov决策过程互模拟等价关系的内在联系;在强互模拟等价关系逻辑特征保持的基础上,给出弱互模拟等价关系下的逻辑保持性质,证明了弱互模拟等价的两个状态,同时满足除下一步算子外的连续随机逻辑公式,从而可以将原模型中的验证问题转换为简约后模型的验证问题,提高验证的效率.

关键词：马尔科夫链、马尔科夫决策过程、互模拟等价关系、逻辑保持

所属期刊栏目：33

分类号：TP302(计算技术、计算机技术)

资助基金：国家自然科学基金项目61462008,61070220;安徽省自然科学基金项目1608085QF149;广西省高校科学技术研究项目LX2014186资助.Supported by National Natural Science Foundation of China61462008,61070220;National Natural Science Foundation of Anhui Province1608085QF149;College and University Scientific and Technology Foundation of Guangxi ProvinceLX2014186

在线出版日期：2016-12-12（万方平台首次上网日期，不代表论文的发表时间）

页数：共8页

页码：1031-1038