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: | Article |
| Language: | English |
| Published: |
Logical Methods in Computer Science e.V.
2021-02-01
|
| Series: | Logical Methods in Computer Science |
| Subjects: | |
| Online Access: | https://lmcs.episciences.org/5994/pdf |
| _version_ | 1827322749932011520 |
|---|---|
| author | Giorgio Bacci Giovanni Bacci Kim G. Larsen Radu Mardare Qiyi Tang Franck van Breugel |
| author_facet | Giorgio Bacci Giovanni Bacci Kim G. Larsen Radu Mardare Qiyi Tang Franck van Breugel |
| author_sort | Giorgio Bacci |
| collection | DOAJ |
| 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 $\textbf{UP} \cap \textbf{coUP}$ 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\'emoli. As an additional contribution, in this paper we show that M\'emoli'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 $\omega$-regular properties, expressed, eg., as LTL formulas. |
| first_indexed | 2024-04-25T01:34:51Z |
| format | Article |
| id | doaj.art-c6f32619ae8444a09335d630eb19c76a |
| institution | Directory Open Access Journal |
| issn | 1860-5974 |
| language | English |
| last_indexed | 2024-04-25T01:34:51Z |
| publishDate | 2021-02-01 |
| publisher | Logical Methods in Computer Science e.V. |
| record_format | Article |
| series | Logical Methods in Computer Science |
| spelling | doaj.art-c6f32619ae8444a09335d630eb19c76a2024-03-08T10:33:16ZengLogical Methods in Computer Science e.V.Logical Methods in Computer Science1860-59742021-02-01Volume 17, Issue 110.23638/LMCS-17(1:9)20215994Computing Probabilistic Bisimilarity Distances for Probabilistic AutomataGiorgio BacciGiovanni BacciKim G. LarsenRadu MardareQiyi TangFranck van BreugelThe 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 $\textbf{UP} \cap \textbf{coUP}$ 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\'emoli. As an additional contribution, in this paper we show that M\'emoli'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 $\omega$-regular properties, expressed, eg., as LTL formulas.https://lmcs.episciences.org/5994/pdfcomputer science - formal languages and automata theorycomputer science - logic in computer science |
| spellingShingle | Giorgio Bacci Giovanni Bacci Kim G. Larsen Radu Mardare Qiyi Tang Franck van Breugel Computing Probabilistic Bisimilarity Distances for Probabilistic Automata Logical Methods in Computer Science computer science - formal languages and automata theory computer science - logic in computer science |
| 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 |
| topic | computer science - formal languages and automata theory computer science - logic in computer science |
| url | https://lmcs.episciences.org/5994/pdf |
| work_keys_str_mv | AT giorgiobacci computingprobabilisticbisimilaritydistancesforprobabilisticautomata AT giovannibacci computingprobabilisticbisimilaritydistancesforprobabilisticautomata AT kimglarsen computingprobabilisticbisimilaritydistancesforprobabilisticautomata AT radumardare computingprobabilisticbisimilaritydistancesforprobabilisticautomata AT qiyitang computingprobabilisticbisimilaritydistancesforprobabilisticautomata AT franckvanbreugel computingprobabilisticbisimilaritydistancesforprobabilisticautomata |