Compositional Reasoning for Markov Decision Processes
Citation:
Yuxin Deng and Matthew Hennessy., Compositional Reasoning for Markov Decision Processes, To be presented at Fundamentals of Software Engineering, Tehran, Iran, April, 2011Download Item:
Compositional.pdf (Published (author's copy) - Peer Reviewed) 177.4Kb
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.
Author's Homepage:
http://people.tcd.ie/mcbhenneDescription:
PUBLISHEDLicences: