maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State Universitymais-1050Research ArticleОригинальные статьиArticlesО сложности верификации недетерминированных вероятностных мультиагентных системOn complexity of veri¯cation of nondeterministic probabilistic multiagent systemsВалиевМ. К.ValievM. K.valiev@keldysh.ruДехтярьМ. И.DekhtyarM. I.Michael.Dekhtyar@tversu.ruИнститут прикладной математики им. М.В. Келдыша РАНRussian FederationТверской государственный университетRussian Federation2010201220101744151Copyright © Валиев М.К., Дехтярь М.И., 20102010Валиев М.К., Дехтярь М.И.Valiev M.K., Dekhtyar M.I.Данная работа распространяется под лицензией 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/1050

Рассматриваются вероятностные системы взаимодействующих недетерминированных интеллектуальных агентов. Состояниями агентов в таких системах являются вероятностные базы данных (фактов), а их действия управляются вероятностными логическими программами. Кроме того, каналы взаимодействий между агентами также являются вероятностными. Показано, как таким системам за полиномиальное время могут быть сопоставлены моделирующие их конечные Марковские процессы принятия решений. Это позволяет перенести известные результаты о верификации динамических свойств конечных Марковских процессов на вероятностные мультиагентные системы рассматриваемого типа.

Probabilistic systems of interacting nondeterministic intelligent agents are consid- ered. States of the agents in these systems are some probabilistic databases, and the activity of the agents is controlled by some probabilistic logic programs. Moreover, com- munication channels between agents are also probabilistic. We show how such systems can be polynomially transformed to ¯nite state Markov decision processes. This allows one to transfer the known results on verifying temporal properties of the ¯nite state Markov processes to the probabilistic multi-agent systems of considered type.

вероятностные мультиагентные системыМарковские цепи и процессы принятия решенийтемпоральные логикиверификация динамических свойствprobabilistic multi-agent systemsMarkov chains and decision processestemporal logicsveri¯cation of dynamic propertiesReferencesDe Alfaro L. Formal verification of probabilistic systems. PhD Thesis, Stanford Univ., 1998.De Alfaro L. Formal verification of probabilistic systems. PhD Thesis, Stanford Univ., 1998.Baier C., Katoen J. Principles of Model Checking. MIT Press, 2008.Baier C., Katoen J. Principles of Model Checking. MIT Press, 2008.Barringer, H., Fisher, M., Gabbay, D., Gough, G., and Owens R. METATEM: An Introduction // Formal Aspects of Computing. 1995. 7. P. 533-549.Barringer, H., Fisher, M., Gabbay, D., Gough, G., and Owens R. METATEM: An Introduction // Formal Aspects of Computing. 1995. 7. P. 533-549.Bordini R., FisherM., Pardavila C., and Wooldridge M. Model checking AgentSpeak. AAMAS. 2003. P. 409-416.Bordini R., FisherM., Pardavila C., and Wooldridge M. Model checking AgentSpeak. AAMAS. 2003. P. 409-416.Benerecetti, M., Guinchiglia, F., and Serafini L. Model checking multiagent systems. Technical Report # 9708-07. Instituto Trentino di Cultura, 1998.Benerecetti, M., Guinchiglia, F., and Serafini L. Model checking multiagent systems. Technical Report # 9708-07. Instituto Trentino di Cultura, 1998.Clarke E.M., Grumberg O., and Peled D. Model checking, MIT Press, 2000.Clarke E.M., Grumberg O., and Peled D. Model checking, MIT Press, 2000.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 A., Dekhtyar M.I. The Theory of Interval Probabilistic Logic Programs // Annals of Mathematics and Artificial Intelligence. 2009. 55, N 3-4. P. 355-388.Dekhtyar A., Dekhtyar M.I. The Theory of Interval Probabilistic Logic Programs // Annals of Mathematics and Artificial Intelligence. 2009. 55, N 3-4. P. 355-388.Dekhtyar M., Dikovsky A., and Valiev M. On feasible cases of checking multi-agent Systems Behavior // Theoretical Computer Science, Elsevier Science. 2003. V. 303, N 1. P. 63-81.Dekhtyar M., Dikovsky A., and Valiev M. On feasible cases of checking multi-agent Systems Behavior // Theoretical Computer Science, Elsevier Science. 2003. V. 303, N 1. P. 63-81.Dekhtyar M.I., Dikovsky A.Ja., Valiev M.K. On complexity of verification of interacting agent's behavior // Annals of Pure and Applied Logic. 2006. 141. P. 336- 362.Dekhtyar M.I., Dikovsky A.Ja., Valiev M.K. On complexity of verification of interacting agent's behavior // Annals of Pure and Applied Logic. 2006. 141. P. 336- 362.Dekhtyar M,I., Dikovsky A.Ja., Valiev M.K. 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. V. 4800. Springer- Verlag, Berlin, 2008. P. 256-265.Dekhtyar M,I., Dikovsky A.Ja., Valiev M.K. 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. V. 4800. Springer- Verlag, Berlin, 2008. P. 256-265.Dix J., Nanni M., and Subrahmanian V. S. Probabilistic agent reasoning // ACM Transactions of Computational Logic. 2000. 1(2). P. 201-245.Dix J., Nanni M., and Subrahmanian V. S. Probabilistic agent reasoning // ACM Transactions of Computational Logic. 2000. 1(2). P. 201-245.Hansson H., Jonsson B. A logic for reasning about time and reliability // Formal Aspects of Computing. 1994. 6(5). P. 512-535.Hansson H., Jonsson B. A logic for reasning about time and reliability // Formal Aspects of Computing. 1994. 6(5). P. 512-535.Kwiatkowska M. Model Checking for probability and time: from theory to practice // Proc. 18th IEEE Symposium on Logic in Computer Science. 2003. P. 351-360.Kwiatkowska M. Model Checking for probability and time: from theory to practice // Proc. 18th IEEE Symposium on Logic in Computer Science. 2003. P. 351-360.Ng R., Subrahmanian V.S. Probabilistic Logic Programming // Information and Computation. 1993. 101, N 2. P. 150-201.Ng R., Subrahmanian V.S. Probabilistic Logic Programming // Information and Computation. 1993. 101, N 2. P. 150-201.Rao A.S., Georgeff M.P. Modelling rational agents within a BDI architecture // Proc. 2nd Intern. Conf on Principles of Knowledge Representation and Reasoning, Morgan Kaufman Publisyers, 1991.Rao A.S., Georgeff M.P. Modelling rational agents within a BDI architecture // Proc. 2nd Intern. Conf on Principles of Knowledge Representation and Reasoning, Morgan Kaufman Publisyers, 1991.Subrahmanian V. S., Bonatti P., Dix J., et al. Heterogeneous agent systems, MIT LPess, 2000.Subrahmanian V. S., Bonatti P., Dix J., et al. Heterogeneous agent systems, MIT LPess, 2000.van der Hoek W., Wooldridge M. Tractable multiagent planning for epistemic goals. AAMAS'02, Bologna, Italy, 2002.van der Hoek W., Wooldridge M. Tractable multiagent planning for epistemic goals. AAMAS'02, Bologna, Italy, 2002.Vardi M.Y. Automatic verification of probabilistic concurrent finite state programs // Proceedings of 26th IEEE Symposium on Foundations of Computer Science. IEEE, New York. P. 327-338.Vardi M.Y. Automatic verification of probabilistic concurrent finite state programs // Proceedings of 26th IEEE Symposium on Foundations of Computer Science. IEEE, New York. P. 327-338.Wooldridge M., Dunne P.E. The computational complexity of agent verification. Lecture Notes in AI, 2002.Wooldridge M., Dunne P.E. The computational complexity of agent verification. Lecture Notes in AI, 2002.Wooldridge M., Jennings N. Intelligent agents. Theory and Practice // The Knowledge Engineering Review. 1995. 10(2).Wooldridge M., Jennings N. Intelligent agents. Theory and Practice // The Knowledge Engineering Review. 1995. 10(2).Валиев М.К., Дехтярь М.И. Вероятностные мультиагентные системы: семантика и верификация // Вестник Тверского госуниверситета. 2008. № 35(98). С. 9-22.Валиев М.К., Дехтярь М.И. Вероятностные мультиагентные системы: семантика и верификация // Вестник Тверского госуниверситета. 2008. № 35(98). С. 9-22.Валиев М.К., Дехтярь М.И. Сложность верификации мультиагентных систем с вероятностными состояниями и программами // Труды V Международной научно-практической конференции «Интегрированные модели и мягкие вычисления в искусственном интеллекте». Т. 1. М.: Физматлит, 2009. С. 198-206Валиев М.К., Дехтярь М.И. Сложность верификации мультиагентных систем с вероятностными состояниями и программами // Труды V Международной научно-практической конференции «Интегрированные модели и мягкие вычисления в искусственном интеллекте». Т. 1. М.: Физматлит, 2009. С. 198-206Тарасов В.Б. От многоагентных систем к интеллектуальным организациям. Эдиториал УРСС. М., 2002.Тарасов В.Б. От многоагентных систем к интеллектуальным организациям. Эдиториал УРСС. М., 2002.

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