Polynomial Algorithm of Verication for Subset of PLTL Logic
https://doi.org/10.18255/1818-1015-2012-2-115-137
Abstract
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.
References
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.
Review
For citations:
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
Views:
2303
Email this article 