info@tmpaconf.org
En | Ru


Андрей Миронов, Сергей Френкель, ИПИ РАН, Москва

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

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

Ключевые слова: верификация; вероятностные системы; вероятностная темпоральная логика; редукция вероятностных моделей