Probabilistic model checking of labelled markov processes via finite approximate bisimulations
Research output: Chapter in Book/Report/Conference proceeding › Conference contribution
Authors
Colleges, School and Institutes
External organisations
- Department of Computer Science
- School of Computing Science
- University of Oxford
- University of Glasgow
Abstract
This paper concerns labelled Markov processes (LMPs), probabilistic models over uncountable state spaces originally introduced by Prakash Panangaden and colleagues. Motivated by the practical application of the LMP framework, we study its formal semantics and the relationship to similar models formulated in control theory. We consider notions of (exact and approximate) probabilistic bisimulation over LMPs and, drawing on methods from both formal verification and control theory, propose a simple technique to compute an approximate probabilistic bisimulation of a given LMP, where the resulting abstraction is characterised as a finite-state labelled Markov chain (LMC). This construction enables the application of automated quantitative verification and policy synthesis techniques over the obtained abstract model, which can be used to perform approximate analysis of the concrete LMP. We illustrate this process through a case study of a multi-room heating system that employs the probabilistic model checker PRISM.
Details
Original language | English |
---|---|
Title of host publication | Horizons of the Mind. A Tribute to Prakash Panangaden |
Subtitle of host publication | Essays Dedicated to Prakash Panangaden on the Occasion of His 60th Birthday |
Editors | Franck van Breugel, Elham Kashefi, Catuscia Palamidessi, Jan Rutten |
Publication status | Published - 2014 |
Event | PrakashFest Conference - Oxford, United Kingdom Duration: 19 May 2014 → 22 May 2014 |
Publication series
Name | Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) |
---|---|
Volume | 8464 LNCS |
ISSN (Print) | 03029743 |
ISSN (Electronic) | 16113349 |
Conference
Conference | PrakashFest Conference |
---|---|
Country | United Kingdom |
City | Oxford |
Period | 19/05/14 → 22/05/14 |