连续时间Markov决策过程互模拟等价及逻辑保持
黄镇谨1
陆阳2
杨娟2
王智文3
1.合肥工业大学计算机与信息学院,安徽合肥230009;广西科技大学计算机与通信工程学院,广西柳州5450062.合肥工业大学计算机与信息学院,安徽合肥,2300093.广西科技大学计算机与通信工程学院,广西柳州,545006
摘要：模型检测中,Markov决策过程可以建模具有不确定性的系统,然而状态空间爆炸问题将会影响系统验证的成败与效率,互模拟等价可以用于系统状态的简约.在强互模拟关系的基础上,给出Markov决策过程模型弱互模拟等价关系的概念,导出了连续时间Markov决策过程及其内嵌离散时间Markov决策过程互模拟等价关系的内在联系;在强互模拟等价关系逻辑特征保持的基础上,给出弱互模拟等价关系下的逻辑保持性质,证明了弱互模拟等价的两个状态,同时满足除下一步算子外的连续随机逻辑公式,从而可以将原模型中的验证问题转换为简约后模型的验证问题,提高验证的效率.
关键词：马尔科夫链马尔科夫决策过程互模拟等价关系逻辑保持
分类号：TP302(计算技术、计算机技术)
论文发表日期：2016-01-01
在线出版日期：2025-08-15（本平台首次上网日期，不代表文献的发表时间）
页数：8( 1031-1038 )
英文信息