Reference:

Stefan Kiefer, Andrzej S. Murawski, Joël Ouaknine, Björn Wachter, and James Worrell. Language equivalence for probabilistic automata. In G. Gopalakrishnan and S. Qadeer, editors, Proceedings of the 23rd International Conference on Computer Aided Verification (CAV), volume 6806 of LNCS, pages 526–540, Snowbird, Utah, USA, 2011. Springer.

Abstract:

In this paper, 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 outcome of which establishes that the randomised algorithm significantly outperforms the deterministic ones in a majority of our test cases. Finally, we also provide fine-grained analytical bounds on the complexity of these algorithms, accounting for the differences in performance.

Suggested BibTeX entry:

@inproceedings{KMOWW:CAV11,
    address = {Snowbird, Utah, USA},
    author = {Stefan Kiefer and Andrzej S. Murawski and Jo\"el Ouaknine and Bj\"{o}rn Wachter and James Worrell},
    booktitle = {Proceedings of the 23rd International Conference on Computer Aided Verification (CAV)},
    editor = {G. Gopalakrishnan and S. Qadeer},
    pages = {526--540},
    publisher = {Springer},
    series = {LNCS},
    title = {Language Equivalence for Probabilistic Automata},
    volume = {6806},
    year = {2011}
}