Probabilistic Model Checking of Labelled Markov Processes via Finite Approximate Bisimulations

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 ap-plication 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 the-ory, propose a simple technique to compute an approximate probabilistic bisimulation of a given LMP, where the resulting abstraction is charac-terised as a finite-state labelled Markov chain (LMC). This construction enables the application of automated quantitative verification and pol-icy 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.