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

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

模型检测中,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.