Метод повышения эффективности решения задач вероятностной верификации вычислительных и телекоммуникационных систем

Рассматривается проблема снижения трудоемкости вероятностной верификации при проектировании вычислительных систем. Поставленная цель достигается редукцией вероятностных систем переходов (ВСП), моделирующих проектируемые системы. Верификация ВСП заключается в вычислении истинностных значений формул вероятностной темпоральной логики (PCTL, Probabilistic Computational Tree Logic) в начальных состояниях ВСП. Редукция ВСП выполняется по алгоритму удаления эквивалентных состояний, в результате работы которого получается такая ВСП, у которой все свойства, выражаемые формулами логики PCTL, совпадают со свойствами исходной ВСП.