maisМоделирование и анализ информационных системModeling and Analysis of Information Systems1818-10152313-5417Yaroslavl State University10.18255/1818-1015-2013-6-10-21mais-154Research ArticleОригинальные статьиArticlesОбщие знания в хорошо структурированных системах с абсолютной памятьюCommon Knowledge in Well-structured Perfect Recall SystemsГаранинаНаталья ОлеговнаGaraninaN. O.

лаборатория Теоретического программирования, научный сотрудник,

630090, Россия, г. Новосибирск, проспект Лаврентьева, 6

лаборатория Теоретического программирования, научный сотрудник,

Acad. Lavrentjev pr., 6, Novosibirsk, 630090, Russia

garanina@iis.nsk.suИнститут систем информатики им. А.П. Ершова СО РАНРоссияA.P. Ershov Institute of Informatics Systems RAS, Siberian BranchRussian Federation2013201220132061021Copyright © Гаранина Н.О., 20132013Гаранина Н.О.Garanina N.O.Данная работа распространяется под лицензией 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/154

В данной работе исследуется задача проверки моделей для логики общих знаний и неподвижных точек µPLCn в хорошо структурированных мультиагентных системах с абсолютной памятью. Показано, что среда с абсолютной памятью, порожденная хорошо структурированной средой и снабженная специальным PRS-порядком, образует хорошо структурированную среду. Из этого следует, что проверка моделей для дизъюнктивного фрагмента µPLCn разрешима.

We investigate a model checking problem for the logic of common knowledge and fixpoints µPLCn in well-structured multiagent systems with perfect recall. In this paper we show that a perfect recall synchronous environment over a well-structured environment forms a well-structured environment provided with a special PRS-order. This implies that the model checking problem for the disjunctive fragment of µPLCn is decidable.

логика общих знаниймультиагентные системы с абсолютной памятьюхорошо структурированные системыпроверка моделейlogic of common knowledgeperfect recallwell-structured systemsmodel checkingРФФИ, Президиум РАНReferencesAbdulla P.A., Cerˆans K., Jonsson B., and Tsay Yih-Kuen. Algorithmic analysis of programs with well quasi-ordered domains // Information and Computation. 2000. V. 160(1–2). P. 109–127.Abdulla P.A., Cerˆans K., Jonsson B., and Tsay Yih-Kuen. Algorithmic analysis of programs with well quasi-ordered domains // Information and Computation. 2000. V. 160(1–2). P. 109–127.Bordini R.H., Fisher M., Visser W., Wooldridge M. Verifying Multi-agent Programs by Model Checking // Autonomous Agents and Multi-Agent Systems. 2006. 12(2). P. 239–256.Bordini R.H., Fisher M., Visser W., Wooldridge M. Verifying Multi-agent Programs by Model Checking // Autonomous Agents and Multi-Agent Systems. 2006. 12(2). P. 239–256.Cohen M., Lomuscio A. Non-elementary speed up for model checking synchronous perfect recall // Proceeding of the 2010 conference on ECAI 2010. Amsterdam, IOS Press, 2010. P. 1077-1078.Cohen M., Lomuscio A. Non-elementary speed up for model checking synchronous perfect recall // Proceeding of the 2010 conference on ECAI 2010. Amsterdam, IOS Press, 2010. P. 1077-1078.Emerson E.A. Temporal and Modal Logic // Handbook of Theoretical Computer Science. V. B. Elsevier and MIT Press, 1990. P. 995–1072.Emerson E.A. Temporal and Modal Logic // Handbook of Theoretical Computer Science. V. B. Elsevier and MIT Press, 1990. P. 995–1072.Fagin R., Halpern J.Y., Moses Y., Vardi M.Y. Reasoning about Knowledge. MIT Press, 1995.Fagin R., Halpern J.Y., Moses Y., Vardi M.Y. Reasoning about Knowledge. MIT Press, 1995.Finkel A., Schnoebelen Ph. Well-structured transition systems everywhere! // Theor. Comp. Sci. 2001. V. 256(1–2). P. 63–92.Finkel A., Schnoebelen Ph. Well-structured transition systems everywhere! // Theor. Comp. Sci. 2001. V. 256(1–2). P. 63–92.Garanina N.O., Kalinina N.A. and Shilov N.V. Model checking knowledge, actions and fixpoints // Proc. of Concurrency, Specification and Programming Workshop CS&P’2004, Germany, 2004. Humboldt Universitat, Berlin, Informatik-Bericht Nr. 170, V. 2. P. 351–357.Garanina N.O., Kalinina N.A. and Shilov N.V. Model checking knowledge, actions and fixpoints // Proc. of Concurrency, Specification and Programming Workshop CS&P’2004, Germany, 2004. Humboldt Universitat, Berlin, Informatik-Bericht Nr. 170, V. 2. P. 351–357.Garanina N.O. Exponential Improvement of Time Complexity of Model Checking for Multiagent Systems with Perfect Recall // Programming and Computer Software. 2012. Vol. 38, No 6. P. 294–303.Garanina N.O. Exponential Improvement of Time Complexity of Model Checking for Multiagent Systems with Perfect Recall // Programming and Computer Software. 2012. Vol. 38, No 6. P. 294–303.Halpern J.Y., van der Meyden R., Vardi M.Y. Complete Axiomatizations for Reasoning About Knowledge and Time // SIAM J. Comp. 2004. 33(3). P. 674–703.Halpern J.Y., van der Meyden R., Vardi M.Y. Complete Axiomatizations for Reasoning About Knowledge and Time // SIAM J. Comp. 2004. 33(3). P. 674–703.Halpern J.Y. and Zuck L.D. A little knowledge goes a long way: knowledge-based derivations and correctness proofs for a family of protocols // Journal of the ACM. 1992. 39(3). P. 449–478.Halpern J.Y. and Zuck L.D. A little knowledge goes a long way: knowledge-based derivations and correctness proofs for a family of protocols // Journal of the ACM. 1992. 39(3). P. 449–478.Huang X., van der Meyden R. The Complexity of Epistemic Model Checking: Clock Semantics and Branching Time // Proc. of 19th ECAI. Lisbon, Portugal, August 16–20, Frontiers in Artificial Intelligence and Applications. V. 215. IOS Press, 2010. P. 549–554.Huang X., van der Meyden R. The Complexity of Epistemic Model Checking: Clock Semantics and Branching Time // Proc. of 19th ECAI. Lisbon, Portugal, August 16–20, Frontiers in Artificial Intelligence and Applications. V. 215. IOS Press, 2010. P. 549–554.Kouzmin E.V., Shilov N.V., Sokolov V.A. Model Checking µ-Calculus in Well-Structured Transition Systems // Proc. of 11th International Symposium on Temporal Representation and Reasoning (TIME’04). France, IEEE Press. P. 152–155.Kouzmin E.V., Shilov N.V., Sokolov V.A. Model Checking µ-Calculus in Well-Structured Transition Systems // Proc. of 11th International Symposium on Temporal Representation and Reasoning (TIME’04). France, IEEE Press. P. 152–155.Kozen D. Results on the Propositional Mu-Calculus // Theoretical Computer Science. 1983. V. 27, No 3. P. 333–354.Kozen D. Results on the Propositional Mu-Calculus // Theoretical Computer Science. 1983. V. 27, No 3. P. 333–354.Kozen D., Tiuryn J. Logics of Programs // Handbook of Theoretical Computer Science. V. B. Elsevier and MIT Press, 1990. P. 789–840.Kozen D., Tiuryn J. Logics of Programs // Handbook of Theoretical Computer Science. V. B. Elsevier and MIT Press, 1990. P. 789–840.Kwiatkowska M.Z., Lomuscio A., Qu H. Parallel Model Checking for Temporal Epistemic Logic // Proc. of 19th ECAI. Lisbon, Portugal, August 16-20, Frontiers in Artificial Intelligence and Applications. V. 215. IOS Press, 2010. P. 543–548.Kwiatkowska M.Z., Lomuscio A., Qu H. Parallel Model Checking for Temporal Epistemic Logic // Proc. of 19th ECAI. Lisbon, Portugal, August 16-20, Frontiers in Artificial Intelligence and Applications. V. 215. IOS Press, 2010. P. 543–548.Lomuscio A., Penczek W., Qu H. Partial order reductions for model checking temporal epistemic logics over interleaved multi-agent systems // Proc. of 9th AAMAS, Toronto, Canada, May 10-14, 2010. V. 1. IFAAMAS, 2010. P. 659–666.Lomuscio A., Penczek W., Qu H. Partial order reductions for model checking temporal epistemic logics over interleaved multi-agent systems // Proc. of 9th AAMAS, Toronto, Canada, May 10-14, 2010. V. 1. IFAAMAS, 2010. P. 659–666.van der Meyden R., Shilov N.V. Model Checking Knowledge and Time in Systems with Perfect Recall // Lect. Notes Comput. Sci. 1999. V. 1738. P. 432–445.van der Meyden R., Shilov N.V. Model Checking Knowledge and Time in Systems with Perfect Recall // Lect. Notes Comput. Sci. 1999. V. 1738. P. 432–445.Shilov N.V., Garanina N.O., and Choe K.-M. Update and Abstraction in Model Checking of Knowledge and Branching Time // Fundamenta Informaticae. 2006. V. 72. No 1–3. P. 347–361.Shilov N.V., Garanina N.O., and Choe K.-M. Update and Abstraction in Model Checking of Knowledge and Branching Time // Fundamenta Informaticae. 2006. V. 72. No 1–3. P. 347–361.Shilov N.V., Garanina N. O. Well-structured Model Checking of Multiagent Systems // Proceedings of 6th International Conference on Perspectives of System Informatics, Novosibirsk, Russia, June 27-30, 2006 // Lecture Notes in Computer Science. 2006. V. 4378.Shilov N.V., Garanina N. O. Well-structured Model Checking of Multiagent Systems // Proceedings of 6th International Conference on Perspectives of System Informatics, Novosibirsk, Russia, June 27-30, 2006 // Lecture Notes in Computer Science. 2006. V. 4378.

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