Computing probabilistic bisimilarity distances for probabilistic automata
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 characterization of the bisimilarity distance as the solution of a simple sto...
| Main Authors: | , , , , |
|---|---|
| Format: | Journal article |
| Language: | English |
| Published: |
Logical Methods in Computer Science
2021
|
| _version_ | 1826256955623079936 |
|---|---|
| author | Bacci, G Bacci, G Larsen, KG Mardare, R Tang, Q van Breugel, F |
| author_facet | Bacci, G Bacci, G Larsen, KG Mardare, R Tang, Q van Breugel, F |
| author_sort | Bacci, G |
| collection | OXFORD |
| description | 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 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 𝐔𝐏∩𝐜𝐨𝐔𝐏 and \textbf{PPAD}. Despite the theoretical relevance, these algorithms are inefficient in practice. To the best of our knowledge, our algorithm is the first practical solution. The characterization of the probabilistic bisimilarity distance mentioned above crucially uses a dual presentation of the Hausdorff distance due to Mémoli. As an additional contribution, in this paper we show that Mémoli's result can be used also to prove that the bisimilarity distance bounds the difference in the maximal (or minimal) probability of two states to satisfying arbitrary 𝜔-regular properties, expressed, eg., as LTL formulas. |
| first_indexed | 2024-03-06T18:10:29Z |
| format | Journal article |
| id | oxford-uuid:02d6cecb-6af5-4803-82f4-e005011cfed6 |
| institution | University of Oxford |
| language | English |
| last_indexed | 2024-03-06T18:10:29Z |
| publishDate | 2021 |
| publisher | Logical Methods in Computer Science |
| record_format | dspace |
| spelling | oxford-uuid:02d6cecb-6af5-4803-82f4-e005011cfed62022-03-26T08:43:01ZComputing probabilistic bisimilarity distances for probabilistic automataJournal articlehttp://purl.org/coar/resource_type/c_dcae04bcuuid:02d6cecb-6af5-4803-82f4-e005011cfed6EnglishSymplectic ElementsLogical Methods in Computer Science2021Bacci, GBacci, GLarsen, KGMardare, RTang, Qvan Breugel, FThe 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 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 𝐔𝐏∩𝐜𝐨𝐔𝐏 and \textbf{PPAD}. Despite the theoretical relevance, these algorithms are inefficient in practice. To the best of our knowledge, our algorithm is the first practical solution. The characterization of the probabilistic bisimilarity distance mentioned above crucially uses a dual presentation of the Hausdorff distance due to Mémoli. As an additional contribution, in this paper we show that Mémoli's result can be used also to prove that the bisimilarity distance bounds the difference in the maximal (or minimal) probability of two states to satisfying arbitrary 𝜔-regular properties, expressed, eg., as LTL formulas. |
| spellingShingle | Bacci, G Bacci, G Larsen, KG Mardare, R Tang, Q van Breugel, F Computing probabilistic bisimilarity distances for probabilistic automata |
| title | Computing probabilistic bisimilarity distances for probabilistic automata |
| title_full | Computing probabilistic bisimilarity distances for probabilistic automata |
| title_fullStr | Computing probabilistic bisimilarity distances for probabilistic automata |
| title_full_unstemmed | Computing probabilistic bisimilarity distances for probabilistic automata |
| title_short | Computing probabilistic bisimilarity distances for probabilistic automata |
| title_sort | computing probabilistic bisimilarity distances for probabilistic automata |
| work_keys_str_mv | AT baccig computingprobabilisticbisimilaritydistancesforprobabilisticautomata AT baccig computingprobabilisticbisimilaritydistancesforprobabilisticautomata AT larsenkg computingprobabilisticbisimilaritydistancesforprobabilisticautomata AT mardarer computingprobabilisticbisimilaritydistancesforprobabilisticautomata AT tangq computingprobabilisticbisimilaritydistancesforprobabilisticautomata AT vanbreugelf computingprobabilisticbisimilaritydistancesforprobabilisticautomata |