Minimization of probabilistic models of programs

In this paper, we consider a problem of reduction of probabilistic transition systems (PTS) in order to reduce the complexity of model checking of such systems. The problem of model checking of a PTS is to calculate truth values of formulas of the probabilistic temporal logic PCTL in an initial state of the PTS. We introduce a concept of equivalence of states of a PTS, and represent an algorithm for removing equivalent states. A result of this algorithm is a PTS such that all its properties expressed by formulas of PCTL coincide with those of the original PTS.