摘要：The probabilistic bisimilarity distance of Deng et al. has been proposed as arobust quantitative generalization of Segala and Lynch's probabilisticbisimilarity for probabilistic automata. In this paper, we present acharacterization of the bisimilarity distance as the solution of a simplestochastic game. The characterization gives us an algorithm to compute thedistances by applying Condon's simple policy iteration on these games. Thecorrectness of Condon's approach, however, relies on the assumption that thegames are stopping. Our games may be non-stopping in general, yet we are ableto prove termination for this extended class of games. Already other algorithmshave been proposed in the literature to compute these distances, withcomplexity in UP ∩ coUP and PPAD . Despite thetheoretical relevance, these algorithms are inefficient in practice. To thebest of our knowledge, our algorithm is the first practical solution. The characterization of the probabilistic bisimilarity distance mentionedabove 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 thedifference in the maximal (or minimal) probability of two states to satisfyingarbitrary ω--regular properties, expressed, eg., as LTL formulas.
关键词：Computer Science - Formal Languages and Automata Theory; Computer Science - Logic in Computer Science
