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

Bisimulation equivalence relation and logic preservation for continue time Markov decision process

作　　者：黄镇谨[1,2] 陆阳[1] 杨娟[1] 王智文[2] HUANG Zhen-jin;LU Yang;YANG Juan;WANG Zhi-wen(School of Computer and Information, Hefei Univerisity of Technology, Hefei Anhui 230009, China;School of Computer Science and Communication Engineering, Guangxi University of Science and Technology,Liuzhou Guangxi 545006, China)

机构地区：[1]合肥工业大学计算机与信息学院,安徽合肥230009 [2]广西科技大学计算机与通信工程学院,广西柳州545006

出　　处：《控制理论与应用》2016年第8期1031-1038,共8页Control Theory & Applications

基　　金：国家自然科学基金项目(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.

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

分 类 号：O211.62[理学—概率论与数理统计]