Institutional Repository
| compositional reasoning for markov decision processes | |
| Deng Yuxin; Hennessy Matthew | |
| 2012 | |
| Conference Name | 4th IPM International Conference on Fundamentals of Software Engineering, FSEN 2011 |
| Source | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
| Pages | 143-157 |
| Conference Date | April 20, 2011 - April 22, 2011 |
| Conference Place | Tehran, Iran |
| Indexed Type | EI |
| ISSN | 0302-9743 |
| ISBN | 9783642293191 |
| Department | (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 |
| English Abstract | 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. |
| Keyword | Markov Processes |
| Language | 英语 |
| Content Type | 会议论文 |
| URI | http://ir.iscas.ac.cn/handle/311060/15683 |
| Collection | 中国科学院软件研究所 |
| Recommended Citation GB/T 7714 | Deng Yuxin,Hennessy Matthew. compositional reasoning for markov decision processes[C],2012:143-157. |
| Files in This Item: | There are no files associated with this item. | |||||
Items in the repository are protected by copyright, with all rights reserved, unless otherwise indicated.
Edit Comment