Computing probabilistic bisimilarity distances for probabilistic automata

Giorgio Bacci, Giovanni Bacci, Kim G. Larsen, Radu Mardare, Qiyi Tang, Franck van Breugel

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

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 ∩ 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.

LanguageEnglish
Title of host publication30th International Conference on Concurrency Theory, CONCUR 2019
EditorsWan Fokkink, Rob van Glabbeek
Place of PublicationDagstuhl, Germany
Number of pages17
Volume140
ISBN (Electronic)9783959771214
DOIs
Publication statusPublished - 1 Aug 2019
Event30th International Conference on Concurrency Theory, CONCUR 2019 - Amsterdam, Netherlands
Duration: 27 Aug 201930 Aug 2019

Conference

Conference30th International Conference on Concurrency Theory, CONCUR 2019
CountryNetherlands
CityAmsterdam
Period27/08/1930/08/19

Keywords

  • behavioural metrics
  • probabilistic automata
  • simple policy iteration algorithm
  • simple stochastic games

Cite this

Bacci, G., Bacci, G., Larsen, K. G., Mardare, R., Tang, Q., & van Breugel, F. (2019). Computing probabilistic bisimilarity distances for probabilistic automata. In W. Fokkink, & R. van Glabbeek (Eds.), 30th International Conference on Concurrency Theory, CONCUR 2019 (Vol. 140). [9] Dagstuhl, Germany. https://doi.org/10.4230/LIPIcs.CONCUR.2019.9
Bacci, Giorgio ; Bacci, Giovanni ; Larsen, Kim G. ; Mardare, Radu ; Tang, Qiyi ; van Breugel, Franck. / Computing probabilistic bisimilarity distances for probabilistic automata. 30th International Conference on Concurrency Theory, CONCUR 2019. editor / Wan Fokkink ; Rob van Glabbeek. Vol. 140 Dagstuhl, Germany, 2019.
@inproceedings{fb43c59692c247a8ad7111b30b4bf455,
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 ∩ 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.",
keywords = "behavioural metrics, probabilistic automata, simple policy iteration algorithm, simple stochastic games",
author = "Giorgio Bacci and Giovanni Bacci and Larsen, {Kim G.} and Radu Mardare and Qiyi Tang and {van Breugel}, Franck",
year = "2019",
month = "8",
day = "1",
doi = "10.4230/LIPIcs.CONCUR.2019.9",
language = "English",
volume = "140",
editor = "Wan Fokkink and {van Glabbeek}, Rob",
booktitle = "30th International Conference on Concurrency Theory, CONCUR 2019",

}

Bacci, G, Bacci, G, Larsen, KG, Mardare, R, Tang, Q & van Breugel, F 2019, Computing probabilistic bisimilarity distances for probabilistic automata. in W Fokkink & R van Glabbeek (eds), 30th International Conference on Concurrency Theory, CONCUR 2019. vol. 140, 9, Dagstuhl, Germany, 30th International Conference on Concurrency Theory, CONCUR 2019, Amsterdam, Netherlands, 27/08/19. https://doi.org/10.4230/LIPIcs.CONCUR.2019.9

Computing probabilistic bisimilarity distances for probabilistic automata. / Bacci, Giorgio; Bacci, Giovanni; Larsen, Kim G.; Mardare, Radu; Tang, Qiyi; van Breugel, Franck.

30th International Conference on Concurrency Theory, CONCUR 2019. ed. / Wan Fokkink; Rob van Glabbeek. Vol. 140 Dagstuhl, Germany, 2019. 9.

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

TY - GEN

T1 - Computing probabilistic bisimilarity distances for probabilistic automata

AU - Bacci, Giorgio

AU - Bacci, Giovanni

AU - Larsen, Kim G.

AU - Mardare, Radu

AU - Tang, Qiyi

AU - van Breugel, Franck

PY - 2019/8/1

Y1 - 2019/8/1

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 ∩ 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 ∩ 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.

KW - behavioural metrics

KW - probabilistic automata

KW - simple policy iteration algorithm

KW - simple stochastic games

UR - http://www.scopus.com/inward/record.url?scp=85071636423&partnerID=8YFLogxK

UR - https://event.cwi.nl/concur2019/

U2 - 10.4230/LIPIcs.CONCUR.2019.9

DO - 10.4230/LIPIcs.CONCUR.2019.9

M3 - Conference contribution book

VL - 140

BT - 30th International Conference on Concurrency Theory, CONCUR 2019

A2 - Fokkink, Wan

A2 - van Glabbeek, Rob

CY - Dagstuhl, Germany

ER -

Bacci G, Bacci G, Larsen KG, Mardare R, Tang Q, van Breugel F. Computing probabilistic bisimilarity distances for probabilistic automata. In Fokkink W, van Glabbeek R, editors, 30th International Conference on Concurrency Theory, CONCUR 2019. Vol. 140. Dagstuhl, Germany. 2019. 9 https://doi.org/10.4230/LIPIcs.CONCUR.2019.9