Common Knowledge in Well-structured Perfect Recall Systems
https://doi.org/10.18255/1818-1015-2013-6-10-21
Abstract
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.
About the Author
N. O. Garanina
A.P. Ershov Institute of Informatics Systems RAS, Siberian Branch
Russian Federation
Russian Federation
лаборатория Теоретического программирования, научный сотрудник,
Acad. Lavrentjev pr., 6, Novosibirsk, 630090, Russia
References
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.
Review
For citations:
Garanina N.O. Common Knowledge in Well-structured Perfect Recall Systems. Modeling and Analysis of Information Systems. 2013;20(6):10-21. (In Russ.) https://doi.org/10.18255/1818-1015-2013-6-10-21
Views:
833
Email this article 