Минимизация вероятностных моделей программ

Рассматривается задача редукции вероятностных систем переходов с целью понижения сложности верификации таких систем. Верификация вероятностной системы переходов заключается в вычислении истинностных значений формул вероятностной темпоральной логики в начальных состояниях вероятностной системы переходов. Введено понятие эквивалентности состояний вероятностной системы переходов и указан алгоритм удаления эквивалентных состояний, в результате работы которого получается вероятностная системы переходов, у которой все свойства, выражаемые формулами вероятностной темпоральной логики, совпадают со свойствами исходной вероятностной системы переходов.