Language Equivalence for Probabilistic Automata

Abstract

We propose a new randomised algorithm for deciding language equivalence for probabilistic automata. This algorithm is based on polynomial identity testing and thus returns an answer with an error probability that can be made arbitrarily small. We implemented our algorithm, as well as deterministic algorithms of Tzeng and Doyen et al., optimised for running time whilst adequately handling issues of numerical stability. We conducted extensive benchmarking experiments, including the verification of randomised anonymity protocols, the out- come of which establishes that the randomised algorithm significantly outperforms the deterministic ones in a majority of our test cases. Fi- nally, we also provide fine-grained analytical bounds on the complexity of these algorithms, accounting for the differences in performance.