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


https://doi.org/10.18255/1818-1015-2012-2-115-137

Полный текст:


Аннотация

Описывается полиномиальный алгоритм верификации цепей Маркова, динамические свойства которых описываются формулами некоторого подмножества темпоральной логики PLTL (propositional temporal logic of linear time). Алгоритм позволяет найти вероятность истинности формулы на заданной цепи Маркова, а также множество траекторий, на которых истинна верифицируемая формула.

Об авторе

Павел Валерьевич Лебедев
Тверской государственный университет
Россия
аспирант


Список литературы

1. Baier C., Katoen J.-P., Principles of model checking. The MIT Press. Cambridge, Massachusetts. London, England, 2008.

2. Courcoubetis C., Yannakakis M., The complexity of probabilistic verification // J. ACM. 1995. V. 42, 4. P. 857–907.

3. Dekhtyar M., Dikovsky A., Valiev M. On complexity of verification of interacting agents behavior // Annals of pure and applied logic. 2006. 141. P. 336 – 362.

4. Dekhtyar M., Dikovsky A., Valiev M. Temporal Verification of Probabilistic Multi-Agent Systems. Pillars of Computer Science: Essays Dedicated to Boris (Boaz)Trakhtenbrot on the Occasion of His 85th Birthday // LNCS. 2008. N 4800. P. 256–265.

5. Hansson H., Jonsson B. A logic for reasoning about time and reliability. Formal Aspects of Computing. 1994. P. 512–535.

6. Kwiatkowska Marta. Model checking for probability and time: from theory to practice // Proc. 18th IEEE Symposium on Logic in Computer Science (LICS’03), IEEE Computer Society Press, 2003. P. 351–360.

7. Luka de Alfaro. Formal verification of probabilistic systems. PhD, Stanford Univ., 1997.

8. Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking. МЦНМО, М., 2002.

9. Лебедев П.В. Программа верификации вероятностных многоагентных систем // Труды XII Национальной конференции по искусственному интеллекту с международным участием. Т. 4. М.: Физматлит, 2010. С. 81–88.


Дополнительные файлы

Для цитирования: Лебедев П.В. Полиномиальный алгоритм верификации цепей Маркова для подмножества логики PLTL. Моделирование и анализ информационных систем. 2012;19(2):115-137. https://doi.org/10.18255/1818-1015-2012-2-115-137

For citation: Lebedev P.V. Polynomial Algorithm of Verication for Subset of PLTL Logic. Modeling and Analysis of Information Systems. 2012;19(2):115-137. (In Russ.) https://doi.org/10.18255/1818-1015-2012-2-115-137

Просмотров: 1636

Обратные ссылки

  • Обратные ссылки не определены.


Creative Commons License
Контент доступен под лицензией Creative Commons Attribution 4.0 License.


ISSN 1818-1015 (Print)
ISSN 2313-5417 (Online)