Source: https://www.mais-journal.ru/jour/article/view/154
Timestamp: 2019-04-23 05:55:39+00:00

Document:
В данной работе исследуется задача проверки моделей для логики общих знаний и неподвижных точек µPLCn в хорошо структурированных мультиагентных системах с абсолютной памятью. Показано, что среда с абсолютной памятью, порожденная хорошо структурированной средой и снабженная специальным PRS-порядком, образует хорошо структурированную среду. Из этого следует, что проверка моделей для дизъюнктивного фрагмента µPLCn разрешима.
1. 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.
2. 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.
3. 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.
4. Emerson E.A. Temporal and Modal Logic // Handbook of Theoretical Computer Science. V. B. Elsevier and MIT Press, 1990. P. 995–1072.
5. Fagin R., Halpern J.Y., Moses Y., Vardi M.Y. Reasoning about Knowledge. MIT Press, 1995.
6. Finkel A., Schnoebelen Ph. Well-structured transition systems everywhere! // Theor. Comp. Sci. 2001. V. 256(1–2). P. 63–92.
7. 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.
8. 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.
9. 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.
10. 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.
11. 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.
12. 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.
13. Kozen D. Results on the Propositional Mu-Calculus // Theoretical Computer Science. 1983. V. 27, No 3. P. 333–354.
14. Kozen D., Tiuryn J. Logics of Programs // Handbook of Theoretical Computer Science. V. B. Elsevier and MIT Press, 1990. P. 789–840.
15. 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.
16. 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.
17. 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.
18. 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.
19. 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.

References: V. 
 V. 
 V. 
 V. 
 V. 
 V. 
 V. 
 V. 
 V. 
 V. 
 V. 
 V.