
arXiv: 1907.01768
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.
Simple policy iteration algorithm, QA75, FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Specification and verification (program logics, model checking, etc.), Probability in computer science (algorithm analysis, random structures, phase transitions, etc.), Logic, Formal Languages and Automata Theory (cs.FL), Temporal logic, Computer Science - Formal Languages and Automata Theory, Formal languages and automata, Simple stochastic games, Behavioural pseudometrics, computer science - logic in computer science, Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.), Probabilistic automata, stochastic games, 000 Computer science, knowledge, general works, BC1-199, 000, probabilistic automata, Behavioural metrics, QA75.5-76.95, 004, Logic in Computer Science (cs.LO), computer science - formal languages and automata theory, Stochastic games, stochastic differential games, Electronic computers. Computer science, Computer Science, behavioural pseudometrics, Stochastic games, ddc: ddc:004
Simple policy iteration algorithm, QA75, FOS: Computer and information sciences, Computer Science - Logic in Computer Science, Specification and verification (program logics, model checking, etc.), Probability in computer science (algorithm analysis, random structures, phase transitions, etc.), Logic, Formal Languages and Automata Theory (cs.FL), Temporal logic, Computer Science - Formal Languages and Automata Theory, Formal languages and automata, Simple stochastic games, Behavioural pseudometrics, computer science - logic in computer science, Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.), Probabilistic automata, stochastic games, 000 Computer science, knowledge, general works, BC1-199, 000, probabilistic automata, Behavioural metrics, QA75.5-76.95, 004, Logic in Computer Science (cs.LO), computer science - formal languages and automata theory, Stochastic games, stochastic differential games, Electronic computers. Computer science, Computer Science, behavioural pseudometrics, Stochastic games, ddc: ddc:004
| selected citations These citations are derived from selected sources. This is an alternative to the "Influence" indicator, which also reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | 1 | |
| popularity This indicator reflects the "current" impact/attention (the "hype") of an article in the research community at large, based on the underlying citation network. | Average | |
| influence This indicator reflects the overall/total impact of an article in the research community at large, based on the underlying citation network (diachronically). | Average | |
| impulse This indicator reflects the initial momentum of an article directly after its publication, based on the underlying citation network. | Average |
