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.
Research supported by EPSRC grant EP/G069158. The first author is supported by a postdoctoral fellowship of the German Academic Exchange Service (DAAD).
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
Baier, C., Bertrand, N., Größer, M.: Proceedings Eleventh International Workshop on Descriptional Complexity of Formal Systems. In: DCFS. EPTCS, vol. 3, pp. 3–16 (2009)
Blondel, V.D., Canterini, V.: Undecidable problems for probabilistic automata of fixed dimension. Theoretical Computer Science 36(3), 231–245 (2003)
Blum, M., Chandra, A., Wegman, M.: Equivalence of free boolean graphs can be decided probabilistically in polynomial time. Inf. Process. Lett. 10(2), 80–82 (1980)
Chatterjee, K., Doyen, L., Henzinger, T.A.: Probabilistic weighted automata. In: Bravetti, M., Zavattaro, G. (eds.) CONCUR 2009. LNCS, vol. 5710, pp. 244–258. Springer, Heidelberg (2009)
Christoff, L., Christoff, I.: Efficient algorithms for verification of equivalences for probabilistic processes. In: Larsen, K.G., Skou, A. (eds.) CAV 1991. LNCS, vol. 575, pp. 310–321. Springer, Heidelberg (1992)
Condon, A., Lipton, R.: On the complexity of space bounded interactive proofs (extended abstract). In: Proceedings of FOCS, pp. 462–467 (1989)
Cortes, C., Mohri, M., Rastogi, A.: On the computation of some standard distances between probabilistic automata. In: Ibarra, O.H., Yen, H.-C. (eds.) CIAA 2006. LNCS, vol. 4094, pp. 137–149. Springer, Heidelberg (2006)
Danos, V., Harmer, R.: Probabilistic game semantics. ACM Transactions on Computational Logic 3(3), 359–382 (2002)
DeMillo, R., Lipton, R.: A probabilistic remark on algebraic program testing. Inf. Process. Lett. 7(4), 193–195 (1978)
Doyen, L., Henzinger, T., Raskin, J.-F.: Equivalence of labeled Markov chains. International Journal of Foundations of Computer Science 19(3), 549–563 (2008)
Herman, T.: Probabilistic self-stabilization. Inf. Process. Lett. 35(2), 63–67 (1990)
Legay, A., Murawski, A.S., Ouaknine, J., Worrell, J.B.: On automated verification of probabilistic programs. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 173–187. Springer, Heidelberg (2008)
Lynch, N.A., Segala, R., Vaandrager, F.W.: Compositionality for Probabilistic Automata. In: Amadio, R.M., Lugiez, D. (eds.) CONCUR 2003. LNCS, vol. 2761, pp. 208–221. Springer, Heidelberg (2003)
Murawski, A.S., Ouaknine, J.: On probabilistic program equivalence and refinement. In: Abadi, M., de Alfaro, L. (eds.) CONCUR 2005. LNCS, vol. 3653, pp. 156–170. Springer, Heidelberg (2005)
Paz, A.: Introduction to Probabilistic Automata. Academic Press, London (1971)
Rabin, M.O.: Probabilistic automata. Information and Control 6(3), 230–245 (1963)
Schützenberger, M.-P.: On the definition of a family of automata. Inf. and Control 4, 245–270 (1961)
Schwartz, J.: Fast probabilistic algorithms for verification of polynomial identities. J. ACM 27(4), 701–717 (1980)
Segala, R.: Modeling and verification of randomized distributed real -time systems. Technical report, MIT, Cambridge MA, USA (1996)
Trefethen, L.N., Bau, D.: Numerical Linear Algebra. SIAM, Philadelphia (1997)
Tzeng, W.: A polynomial-time algorithm for the equivalence of probabilistic automata. SIAM Journal on Computing 21(2), 216–227 (1992)
Zippel, R.: Probabilistic algorithms for sparse polynomials. In: Ng, K.W. (ed.) EUROSAM 1979 and ISSAC 1979. LNCS, vol. 72, pp. 216–226. Springer, Heidelberg (1979)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2011 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Kiefer, S., Murawski, A.S., Ouaknine, J., Wachter, B., Worrell, J. (2011). Language Equivalence for Probabilistic Automata. In: Gopalakrishnan, G., Qadeer, S. (eds) Computer Aided Verification. CAV 2011. Lecture Notes in Computer Science, vol 6806. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-22110-1_42
Download citation
DOI: https://doi.org/10.1007/978-3-642-22110-1_42
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-22109-5
Online ISBN: 978-3-642-22110-1
eBook Packages: Computer ScienceComputer Science (R0)