Compositional reasoning for weighted Markov decision processes |
| |
Authors: | Yuxin Deng Matthew Hennessy |
| |
Affiliation: | 1. Shanghai Jiao Tong University, China;2. Trinity College Dublin, Ireland |
| |
Abstract: | Weighted Markov decision processes (MDPs) have long been used to model quantitative aspects of systems in the presence of uncertainty. However, much of the literature on such 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 contrast in this paper we develop compositional methods for reasoning about weighted MDPs, as a possible basis for compositional reasoning about their quantitative behaviour. In particular we approach these systems 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 weighted MDPs from components. |
| |
Keywords: | Markov decision processes Simulation Testing preorder Modal logic Compositionality |
本文献已被 ScienceDirect 等数据库收录! |