Полиномиальный алгоритм верификации цепей Маркова для подмножества логики 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
Просмотров: 2212
Послать статью по эл. почте 