Compositional Bisimulation Minimization for Interval Markov Decision Processes.
Lecture Notes in Computer Science(2016)
摘要
Formal verification of PCTL properties of MDPs with convex uncertainties has been recently investigated by Puggelli et al. However, model checking algorithms typically suffer from state space explosion. In this paper, we address probabilistic bisimulation to reduce the size of such an MDP while preserving PCTL properties it satisfies. We give a compositional reasoning over interval models to understand better the ways how large models with interval uncertainties can be composed. Afterwards, we discuss computational complexity of the bisimulation minimization and show that the problem is coNP-complete. Finally, we show that, under a mild condition, bisimulation can be computed in polynomial time.
更多查看译文
关键词
Markov decision process,Interval MDP,Compositionality,Bisimulation,Complexity
AI 理解论文
溯源树
样例
生成溯源树,研究论文发展脉络