Language Equivalence for Probabilistic Automata
James Worrell Stefan Kiefer Andrzej S. Murawski Joel Ouaknine Björn Wachter
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.
Details
| Book Title |
CAV |
| Note |
to appear in CAV 2011 |
| Year |
2011 |
Links
Related pages
|
People |