Computing Probabilistic Bisimilarity Distances for Probabilistic Automata

Research output: Contribution to journalConference article in JournalResearchpeer-review

Abstract

The probabilistic bisimilarity distance of Deng et al. has been proposed as a robust quantitative generalization of Segala and Lynch's probabilistic bisimilarity for probabilistic automata. In this paper, we present a novel characterization of the bisimilarity distance as the solution of a simple stochastic game. The characterization gives us an algorithm to compute the distances by applying Condon's simple policy iteration on these games. The correctness of Condon's approach, however, relies on the assumption that the games are stopping. Our games may be non-stopping in general, yet we are able to prove termination for this extended class of games. Already other algorithms have been proposed in the literature to compute these distances, with complexity in UP cap coUP and PPAD. Despite the theoretical relevance, these algorithms are inefficient in practice. To the best of our knowledge, our algorithm is the first practical solution. In the proofs of all the above-mentioned results, an alternative presentation of the Hausdorff distance due to Mémoli plays a central rôle.
Original languageEnglish
JournalLeibniz International Proceedings in Informatics
Volume140
Pages (from-to)1
Number of pages17
ISSN1868-8969
DOIs
Publication statusPublished - 2019
Event30th International Conference on Concurrency Theory - Amsterdam, Netherlands
Duration: 26 Aug 201931 Aug 2019
Conference number: 30
https://event.cwi.nl/concur2019/

Conference

Conference30th International Conference on Concurrency Theory
Number30
CountryNetherlands
CityAmsterdam
Period26/08/201931/08/2019
Internet address

Cite this

@inproceedings{027298ddf55c4787aec8379ff4fbd07a,
title = "Computing Probabilistic Bisimilarity Distances for Probabilistic Automata",
abstract = "The probabilistic bisimilarity distance of Deng et al. has been proposed as a robust quantitative generalization of Segala and Lynch's probabilistic bisimilarity for probabilistic automata. In this paper, we present a novel characterization of the bisimilarity distance as the solution of a simple stochastic game. The characterization gives us an algorithm to compute the distances by applying Condon's simple policy iteration on these games. The correctness of Condon's approach, however, relies on the assumption that the games are stopping. Our games may be non-stopping in general, yet we are able to prove termination for this extended class of games. Already other algorithms have been proposed in the literature to compute these distances, with complexity in UP cap coUP and PPAD. Despite the theoretical relevance, these algorithms are inefficient in practice. To the best of our knowledge, our algorithm is the first practical solution. In the proofs of all the above-mentioned results, an alternative presentation of the Hausdorff distance due to M{\'e}moli plays a central r{\^o}le.",
author = "Giorgio Bacci and Giovanni Bacci and Larsen, {Kim Guldstrand} and Radu Mardare and Qiyi Tang and {van Breugel}, Franck",
year = "2019",
doi = "10.4230/LIPIcs.CONCUR.2019.9",
language = "English",
volume = "140",
pages = "1",
journal = "Leibniz International Proceedings in Informatics",
issn = "1868-8969",
publisher = "Schloss Dagstuhl - Leibniz-Zentrum fuer Informatik GmbH",

}

Computing Probabilistic Bisimilarity Distances for Probabilistic Automata. / Bacci, Giorgio; Bacci, Giovanni; Larsen, Kim Guldstrand; Mardare, Radu; Tang, Qiyi; van Breugel, Franck.

In: Leibniz International Proceedings in Informatics, Vol. 140, 2019, p. 1.

Research output: Contribution to journalConference article in JournalResearchpeer-review

TY - GEN

T1 - Computing Probabilistic Bisimilarity Distances for Probabilistic Automata

AU - Bacci, Giorgio

AU - Bacci, Giovanni

AU - Larsen, Kim Guldstrand

AU - Mardare, Radu

AU - Tang, Qiyi

AU - van Breugel, Franck

PY - 2019

Y1 - 2019

N2 - The probabilistic bisimilarity distance of Deng et al. has been proposed as a robust quantitative generalization of Segala and Lynch's probabilistic bisimilarity for probabilistic automata. In this paper, we present a novel characterization of the bisimilarity distance as the solution of a simple stochastic game. The characterization gives us an algorithm to compute the distances by applying Condon's simple policy iteration on these games. The correctness of Condon's approach, however, relies on the assumption that the games are stopping. Our games may be non-stopping in general, yet we are able to prove termination for this extended class of games. Already other algorithms have been proposed in the literature to compute these distances, with complexity in UP cap coUP and PPAD. Despite the theoretical relevance, these algorithms are inefficient in practice. To the best of our knowledge, our algorithm is the first practical solution. In the proofs of all the above-mentioned results, an alternative presentation of the Hausdorff distance due to Mémoli plays a central rôle.

AB - The probabilistic bisimilarity distance of Deng et al. has been proposed as a robust quantitative generalization of Segala and Lynch's probabilistic bisimilarity for probabilistic automata. In this paper, we present a novel characterization of the bisimilarity distance as the solution of a simple stochastic game. The characterization gives us an algorithm to compute the distances by applying Condon's simple policy iteration on these games. The correctness of Condon's approach, however, relies on the assumption that the games are stopping. Our games may be non-stopping in general, yet we are able to prove termination for this extended class of games. Already other algorithms have been proposed in the literature to compute these distances, with complexity in UP cap coUP and PPAD. Despite the theoretical relevance, these algorithms are inefficient in practice. To the best of our knowledge, our algorithm is the first practical solution. In the proofs of all the above-mentioned results, an alternative presentation of the Hausdorff distance due to Mémoli plays a central rôle.

U2 - 10.4230/LIPIcs.CONCUR.2019.9

DO - 10.4230/LIPIcs.CONCUR.2019.9

M3 - Conference article in Journal

VL - 140

SP - 1

JO - Leibniz International Proceedings in Informatics

JF - Leibniz International Proceedings in Informatics

SN - 1868-8969

ER -