Compositional Reasoning for Weighted Markov Decision Processes
(Extended Abstract)
Yuxin Deng and Matthew Hennessy
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.
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 quantitative probabilistic logic, while the second is in terms of a novel form of testing, in
which benefits are accrued during the execution of tests.