| 引用本文: | 黄镇谨,陆阳,杨娟,王智文.连续时间Markov决策过程互模拟等价及逻辑保持[J].控制理论与应用,2016,33(8):1031~1038.[点击复制] |
| HUANG Zhen-jin,LU Yang,YANG Juan,WANG Zhi-wen.Bisimulation equivalence relation and logic preservation for continue time Markov decision process[J].Control Theory and Technology,2016,33(8):1031~1038.[点击复制] |
|
| 连续时间Markov决策过程互模拟等价及逻辑保持 |
| Bisimulation equivalence relation and logic preservation for continue time Markov decision process |
| 摘要点击 3399 全文点击 1748 投稿时间：2015-10-14 修订日期：2016-04-22 |
| 查看全文 查看/发表评论 下载PDF阅读器 |
| DOI编号 10.7641/CTA.2016.50812 |
| 2016,33(8):1031-1038 |
| 中文关键词 马尔科夫链 马尔科夫决策过程 互模拟等价关系 逻辑保持 |
| 英文关键词 Markov chains Markov decision process bisimulation equivalence relation logic preservation |
| 基金项目 国家自然科学基金项目(61462008, 61070220), 安徽省自然科学基金项目(1608085QF149), 广西省高校科学技术研究项目(LX2014186)资助. |
|
| 中文摘要 |
| 模型检测中, Markov决策过程可以建模具有不确定性的系统, 然而状态空间爆炸问题将会影响系统验证的
成败与效率, 互模拟等价可以用于系统状态的简约. 在强互模拟关系的基础上, 给出Markov决策过程模型弱互模拟
等价关系的概念, 导出了连续时间Markov决策过程及其内嵌离散时间Markov决策过程互模拟等价关系的内在联
系; 在强互模拟等价关系逻辑特征保持的基础上, 给出弱互模拟等价关系下的逻辑保持性质, 证明了弱互模拟等价
的两个状态, 同时满足除下一步算子外的连续随机逻辑公式, 从而可以将原模型中的验证问题转换为简约后模型的
验证问题, 提高验证的效率. |
| 英文摘要 |
| Markov decision process can be employed to model complex systems with nondeterministic choice in model
checking. However, whether system verification can be performed successfully and effectively is influenced by the emergence
of state space explosion. Bisimulation equivalence can be views as a feasible states reduction approach. Based on
the concept of strong bisimulation, the definition of weak bisimulation on Markov decision process are proposed, then the
inherent link of bisimulation equivalence between continue time markov decision process and its embedded discrete time
decision process is derived. Meanwhile, based on Logic characterization preservation of strong bisimulation, the relation
between the weak bisimulation equivalence and the continue stochastic logic equivalence for continue time Markov decision
process is proved, which shows that weak bisimulation coincides with logical equivalence excepted the next-step
operator. |
|
|
|
|
|