Compositional Reasoning for Markov Decision Processes
Item Type:Conference Paper
Citation:Yuxin Deng and Matthew Hennessy., Compositional Reasoning for Markov Decision Processes, To be presented at Fundamentals of Software Engineering, Tehran, Iran, April, 2011
Compositional.pdf (Published (author's copy) - Peer Reviewed) 177.4Kb
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.
Author: HENNESSY, MATTHEW
Type of material:Conference Paper
Availability:Full text available