COMPUTING PROBABILISTIC BISIMILARITY DISTANCES FOR PROBABILISTIC AUTOMATA

被引:3
|
作者
Bacci, Giorgio [1 ]
Bacci, Giovanni [1 ]
Larsen, Kim G. [1 ]
Mardare, Radu [2 ]
Tang, Qiyi [3 ]
van Breugel, Franck [4 ]
机构
[1] Aalborg Univ, Dept Comp Sci, Aalborg, Denmark
[2] Univ Strathclyde, Dept Comp & Informat Sci, Glasgow, Lanark, Scotland
[3] Univ Oxford, Dept Comp Sci, Oxford, England
[4] York Univ, Dept Elect Engn & Comp Sci, DisCoVeri Grp, Toronto, ON, Canada
基金
加拿大自然科学与工程研究理事会;
关键词
probabilistic automata; behavioural pseudometrics; stochastic games; COMPLEXITY; METRICS; GAMES;
D O I
10.23638/LMCS-17(1:9)2021
中图分类号
TP301 [理论、方法];
学科分类号
081202 ;
摘要
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 UP boolean AND 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. The characterization of the probabilistic bisimilarity distance mentioned above crucially uses a dual presentation of the Hausdorff distance due to Memoli. As an additional contribution, in this paper we show that Memoli'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 w-regular properties, expressed, eg., as LTL formulas.
引用
收藏
页码:9:1 / 9:36
页数:36
相关论文
共 50 条
  • [1] Computing Bisimilarity Metrics for Probabilistic Timed Automata
    Lanotte, Ruggero
    Tini, Simone
    [J]. INTEGRATED FORMAL METHODS, IFM 2019, 2019, 11918 : 303 - 321
  • [2] Deciding probabilistic bisimilarity distance one for probabilistic automata
    Tang, Qiyi
    van Breugel, Franck
    [J]. JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 2020, 111 : 57 - 84
  • [3] On the Complexity of Computing Probabilistic Bisimilarity
    Chen, Di
    van Breugel, Franck
    Worrell, James
    [J]. FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATIONAL STRUCTURES, FOSSACS 2012, 2012, 7213 : 437 - 451
  • [4] Explainability of Probabilistic Bisimilarity Distances for Labelled Markov Chains
    Rady, Amgad
    van Breugel, Franck
    [J]. FOUNDATIONS OF SOFTWARE SCIENCE AND COMPUTATION STRUCTURES, FOSSACS 2023, 2023, 13992 : 285 - 307
  • [5] GAME CHARACTERIZATION OF PROBABILISTIC BISIMILARITY, AND APPLICATIONS TO PUSHDOWN AUTOMATA
    Forejt, Vojtech
    Jancar, Petr
    Kiefer, Stefan
    Worrell, James
    [J]. LOGICAL METHODS IN COMPUTER SCIENCE, 2018, 14 (04) : 1 - 25
  • [6] Probabilistic automata for computing with words
    Cao, Yongzhi
    Xia, Lirong
    Ying, Mingsheng
    [J]. JOURNAL OF COMPUTER AND SYSTEM SCIENCES, 2013, 79 (01) : 152 - 172
  • [7] Computing with Probabilistic Cellular Automata
    Schuele, Martin
    Ott, Thomas
    Stoop, Ruedi
    [J]. ARTIFICIAL NEURAL NETWORKS - ICANN 2009, PT II, 2009, 5769 : 525 - +
  • [8] Computing Probabilistic Queries in the Presence of Uncertainty via Probabilistic Automata
    Andronikos, Theodore
    Singh, Alexander
    Giannakis, Konstantinos
    Sioutas, Spyros
    [J]. ALGORITHMIC ASPECTS OF CLOUD COMPUTING, ALGOCLOUD 2017, 2018, 10739 : 106 - 120
  • [9] On the computation of some standard distances between probabilistic automata
    Cortes, Corinna
    Mohri, Mehryar
    Rastogi, Ashish
    [J]. IMPLEMENTATION AND APPLICATION OF AUTOMATA, 2006, 4094 : 137 - 149
  • [10] Probabilistic bisimilarity as testing equivalence
    Deng, Yuxin
    Feng, Yuan
    [J]. INFORMATION AND COMPUTATION, 2017, 257 : 58 - 64