Exact performance equivalence: An equivalence relation for stochastic automata

Stochastic automata are an established formalism to describe and analyse systems according to their qualitative and quantitative behaviour. Equivalence is a basic concept for the analysis, comparison and reduction of untimed automata, whereas equivalence of stochastic automata is less established. This paper introduces a new equivalence relation for stochastic automata denoted as exact performance equivalence. It is shown that this equivalence relation preserves several important qualitative properties and also quantitative results. Exact performance equivalence is a congruence according to the synchronised product of stochastic automata. The smallest exactly equivalent automaton exists for a stochastic automaton and can be generated by a partition refinement algorithm. (C) 1999-Elsevier Science B.V. All rights reserved.