compositional reasoning for markov decision processes

ISCAS OpenIR

	compositional reasoning for markov decision processes
	Deng Yuxin; Hennessy Matthew
	2012
会议名称	4th IPM International Conference on Fundamentals of Software Engineering, FSEN 2011
会议录名称	Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
页码	143-157
会议日期	April 20, 2011 - April 22, 2011
会议地点	Tehran, Iran
收录类别	EI
ISSN	0302-9743
ISBN	9783642293191
部门归属	(1) Dept. Comp. Sci. and Eng. MOE-Microsoft Key Lab. for Intell. Comp. and Syst. Shanghai Jiao Tong University China; (2) State Key Lab. of Comp. Sci. Inst. of Software Chinese Academy of Sciences China; (3) Trinity College Dublin Ireland
摘要	Markov decision processes (MDPs) have long been used to model qualitative aspects of systems in the presence of uncertainty. However, much of the literature on MDPs takes a monolithic approach, by modelling a system as a particular MDP; properties of the system are then inferred by analysis of that particular MDP. In this paper we develop compositional methods for reasoning about the qualitative behaviour of MDPs. We consider a class of labelled MDPs called weighted MDPs from a process algebraic point of view. For these we define a coinductive simulation-based behavioural preorder which is compositional in the sense that it is preserved by structural operators for constructing MDPs from components. For finitary convergent processes, which are finite-state and finitely branching systems without divergence, we provide two characterisations of the behavioural preorder. The first uses a novel qualitative probabilistic logic, while the second is in terms of a novel form of testing, in which benefits are accrued during the execution of tests. © 2012 Springer-Verlag.; Markov decision processes (MDPs) have long been used to model qualitative aspects of systems in the presence of uncertainty. However, much of the literature on MDPs takes a monolithic approach, by modelling a system as a particular MDP; properties of the system are then inferred by analysis of that particular MDP. In this paper we develop compositional methods for reasoning about the qualitative behaviour of MDPs. We consider a class of labelled MDPs called weighted MDPs from a process algebraic point of view. For these we define a coinductive simulation-based behavioural preorder which is compositional in the sense that it is preserved by structural operators for constructing MDPs from components. For finitary convergent processes, which are finite-state and finitely branching systems without divergence, we provide two characterisations of the behavioural preorder. The first uses a novel qualitative probabilistic logic, while the second is in terms of a novel form of testing, in which benefits are accrued during the execution of tests. © 2012 Springer-Verlag.
关键词	Markov Processes
语种	英语
内容类型	会议论文
URI标识	http://ir.iscas.ac.cn/handle/311060/15683
专题	中国科学院软件研究所
推荐引用方式 GB/T 7714	Deng Yuxin,Hennessy Matthew. compositional reasoning for markov decision processes[C],2012:143-157.