|
Моделирование и анализ информационных систем, 2012, том 19, номер 2, страницы 115–137
(Mi mais224)
|
|
|
|
Полиномиальный алгоритм верификации цепей Маркова для подмножества логики PLTL
П. В. Лебедев Тверской государственный университет
Аннотация:
Описывается полиномиальный алгоритм верификации цепей Маркова, динамические свойства которых описываются формулами некоторого подмножества темпоральной логики PLTL (propositional temporal logic of linear time). Алгоритм позволяет найти вероятность истинности формулы на заданной цепи Маркова, а также множество траекторий, на которых истинна верифицируемая формула.
Ключевые слова:
цепи Маркова, проверка на моделях, темпоральные логики, PLTL, верификация динамических свойств.
Поступила в редакцию: 27.12.2012
Образец цитирования:
П. В. Лебедев, “Полиномиальный алгоритм верификации цепей Маркова для подмножества логики PLTL”, Модел. и анализ информ. систем, 19:2 (2012), 115–137
Образцы ссылок на эту страницу:
https://www.mathnet.ru/rus/mais224 https://www.mathnet.ru/rus/mais/v19/i2/p115
|
Статистика просмотров: |
Страница аннотации: | 206 | PDF полного текста: | 151 | Список литературы: | 36 |
|