Probabilistic model checking of labelled markov processes via finite approximate bisimulations

Alessandro Abate, Marta Kwiatkowska, Gethin Norman, David Parker

Research output: Chapter in Book/Report/Conference proceedingConference contribution

14 Citations (Scopus)


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.

Original languageEnglish
Title of host publicationHorizons of the Mind. A Tribute to Prakash Panangaden
Subtitle of host publicationEssays Dedicated to Prakash Panangaden on the Occasion of His 60th Birthday
EditorsFranck van Breugel, Elham Kashefi, Catuscia Palamidessi, Jan Rutten
Number of pages19
Volume8464 LNCS
ISBN (Electronic) 9783319068800
ISBN (Print)9783319068794
Publication statusPublished - 2014
EventPrakashFest Conference - Oxford, United Kingdom
Duration: 19 May 201422 May 2014

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume8464 LNCS
ISSN (Print)03029743
ISSN (Electronic)16113349


ConferencePrakashFest Conference
Country/TerritoryUnited Kingdom

ASJC Scopus subject areas

  • Computer Science(all)
  • Theoretical Computer Science


Dive into the research topics of 'Probabilistic model checking of labelled markov processes via finite approximate bisimulations'. Together they form a unique fingerprint.

Cite this