A method of enhancing probabilistic verification efficiency for computer and telecommunication systems

The paper considers the 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 temporal probabilistic computational tree logic (PCTL) in the initial state of the PTS. The paper introduces the concept of equivalence of states of a PTS and represents an algorithm for removing equivalent states. The result of this algorithm is a PTS such that all its properties expressed by formulas of PCTL coincide with those of the original PTS.