Algorithms for computing pseudometrics on probalistic models
|
Supervisor |
|
|
Suitable for |
Abstract
Pseudometrics on labelled Markov chains or labelled Markov decision processes have been introduced in literature. They generalise the notion of probabilistic bisimilarity by assigning a similarity distance to pairs of states of the model under consideration. The smaller the distance, the more alike are the states, with states having distance zero if and only if they are probabilistic bisimilar. The pseudometrics have found applications in, e.g., systems biology, planning, and security. Theoretical algorithms based on linear programming have been proposed to compute such a distance. However, they perform poorly in practice. This project aims to develop more practical algorithms, based on value iteration, and incorporate the notion of “on-the-fly” analysis. It is expected that the algorithms will be implemented as an extension of PRISM and, ideally, also applied to some real case studies.
Prerequisites: Some familiarity of basic probability theory and probalistic models