Compositional Reasoning for Markov Decision Processes
                        (Extended Abstract)

              Yuxin Deng and Matthew Hennessy

 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.