Compositional reasoning for weighted Markov decision processes
Citation:
Deng, Y., Hennessy, M., Compositional reasoning for weighted Markov decision processes, Science of Computer Programming, 2013Download Item:
1-s2.0-S0167642313000440-main.pdf (Published (author's copy) - Peer Reviewed) 698.5Kb
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. 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. ? 2013 Elsevier B.V. All rights reserved.
Sponsor
Grant Number
Science Foundation Ireland (SFI)
SFI06IN.11898
Author's Homepage:
http://people.tcd.ie/mcbhenneDescription:
PUBLISHED
Author: HENNESSY, MATTHEW
Type of material:
Journal ArticleSeries/Report no:
Science of Computer ProgrammingAvailability:
Full text availableDOI:
http://dx.doi.org/10.1016/j.scico.2013.02.009Licences: