maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2012-2-115-137mais-23Research ArticleОригинальные статьиArticlesПолиномиальный алгоритм верификации цепей Маркова для подмножества логики PLTLPolynomial Algorithm of Verication for Subset of PLTL LogicЛебедевПавел ВалерьевичLebedevP. V.

аспирант

аспирант

pavelvlebedev@gmail.comТверской государственный университетРоссияТверской государственный университетRussian Federation201225022015192115137Copyright © Лебедев П.В., 20152015Лебедев П.В.Lebedev P.V.Данная работа распространяется под лицензией Creative Commons Attribution 4.0.This work is licensed under a Creative Commons Attribution 4.0 License.https://www.mais-journal.ru/jour/article/view/23

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

In this article a polynomial algorithm is described of verification of dynamic properties of Markov chains described by formulas of a subset of temporal logic PLTL (propositional temporal logic of linear time). The algorithm allows to find probability of the validity of the formula on the Markov chain, and also set of trajectories on which the verified formula is true.

цепи Марковапроверка на моделяхтемпоральные логикиPLTLверификация динамических свойствMarkov chainsPLTLtemporal logicsverification of dynamic propertiesРФФИReferencesBaier C., Katoen J.-P., Principles of model checking. The MIT Press. Cambridge, Massachusetts. London, England, 2008.Baier C., Katoen J.-P., Principles of model checking. The MIT Press. Cambridge, Massachusetts. London, England, 2008.Courcoubetis C., Yannakakis M., The complexity of probabilistic verification // J. ACM. 1995. V. 42, 4. P. 857–907.Courcoubetis C., Yannakakis M., The complexity of probabilistic verification // J. ACM. 1995. V. 42, 4. P. 857–907.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.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.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.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.Hansson H., Jonsson B. A logic for reasoning about time and reliability. Formal Aspects of Computing. 1994. P. 512–535.Hansson H., Jonsson B. A logic for reasoning about time and reliability. Formal Aspects of Computing. 1994. P. 512–535.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.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.Luka de Alfaro. Formal verification of probabilistic systems. PhD, Stanford Univ., 1997.Luka de Alfaro. Formal verification of probabilistic systems. PhD, Stanford Univ., 1997.Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking. МЦНМО, М., 2002.Кларк Э.М., Грамберг О., Пелед Д. Верификация моделей программ: Model Checking. МЦНМО, М., 2002.Лебедев П.В. Программа верификации вероятностных многоагентных систем // Труды XII Национальной конференции по искусственному интеллекту с международным участием. Т. 4. М.: Физматлит, 2010. С. 81–88.Лебедев П.В. Программа верификации вероятностных многоагентных систем // Труды XII Национальной конференции по искусственному интеллекту с международным участием. Т. 4. М.: Физматлит, 2010. С. 81–88.

The authors declare that there are no conflicts of interest present.