DSpace Repository

Computing Probabilistic Bisimilarity Distances

Computing Probabilistic Bisimilarity Distances

Show full item record

Title: Computing Probabilistic Bisimilarity Distances
Author: Tang, Qiyi
Abstract: Behavioural equivalences like probabilistic bisimilarity rely on the transition probabilities and, as a result, are sensitive to minuscule changes of those probabilities. Such behavioural equivalences are not robust, as first observed by Giacalone, Jou and Smolka. Probabilistic bisimilarity distances, a robust quantitative generalization of probabilistic bisimilarity, capture the similarity of the behaviour of states of a probabilistic model. The smaller the distance, the more alike the states behave. In particular, states are probabilistic bisimilar if and only if the distance between them is zero. In this dissertation, we focus on algorithms to compute probabilistic bisimilarity distances for two probabilistic models: labelled Markov chains and probabilistic automata.

In the late nineties, Desharnais, Gupta, Jagadeesan and Panangaden defined probabilistic bisimilarity distances on the states of a labelled Markov chain. This provided a quantitative generalization of probabilistic bisimilarity, which was introduced by Larsen and Skou a decade earlier. Several algorithms to approximate and compute these probabilistic bisimilarity distances have been put forward. In this dissertation, we correct and generalize some of these policy iteration algorithms. Moreover, we develop several new algorithms which have better performance in practice and can handle much larger systems.

Similarly, Deng, Chothia, Palamidessi and Pang presented probabilistic bisimilarity distances on the states of a probabilistic automaton. This provided a robust quantitative generalization of probabilistic bisimilarity introduced by Segala and Lynch. Although the complexity of computing probabilistic bisimilarity distances for probabilistic automata has already been studied and shown to be in NP coNP and PPAD, we are not aware of any practical algorithms to compute those distances. In this dissertation, we provide several key results that may prove to be useful for the development of algorithms to compute probabilistic bisimilarity distances for probabilistic automata. In particular, we present a polynomial time algorithm that decides distance one. Furthermore, we give an alternative characterization of the probabilistic bisimilarity distances as a basis for a policy iteration algorithm.
Subject: Computer science
Keywords: Probabilistic bisimilarity distances
Bisimulation metric
Probabilistic models
Model checking
Concurrency
Labelled Markov chains
Algorithms
Probabilistic automata
Type: Electronic Thesis or Dissertation
Rights: Author owns copyright, except where explicitly noted. Please contact the author directly with licensing requests.
URI: http://hdl.handle.net/10315/35586
Supervisor: Breugel, Franck van
Degree: PhD - Doctor of Philosophy
Program: Computer Science
Exam date: 2018-08-14
Publish on: 2018-11-21

Files in this item



This item appears in the following Collection(s)