Efficient algorithms for verification of equivalences for probabilistic processes

Abstract

We present algorithms for automatic verification of equivalences between probabilistic processes. The equivalences we shall verify are testing type equivalences, based on probabilities for probabilistic processes to perform strings of observable events when interacting with different environments (or tests). Our algorithms are based on a recent polynomial-time algorithm for establishing language equivalence of probabilistic automata by Tzeng. We show that the time complexity of our algorithms is polynomial with respect to the number of states in the compared processes.