Geodesic
Common Knowledge in Well-structured Perfect Recall Systems
Modelirovanie i analiz informacionnyh sistem, Tome 20 (2013) no. 6, pp. 10-21.

Voir la notice de l'article provenant de la source Math-Net.Ru

We investigate a model checking problem for the logic of common knowledge and fixpoints $\mu$PLC$_n$ 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 $\mu$PLC$_n$ is decidable.
Keywords: logic of common knowledge, perfect recall, well-structured systems, model checking. 
@article{MAIS_2013_20_6_a0,
     author = {N. O. Garanina},
     title = {Common {Knowledge} in {Well-structured} {Perfect} {Recall} {Systems}},
     journal = {Modelirovanie i analiz informacionnyh sistem},
     pages = {10--21},
     publisher = {mathdoc},
     volume = {20},
     number = {6},
     year = {2013},
     language = {ru},
     url = {http://geodesic.mathdoc.fr/item/MAIS_2013_20_6_a0/}
}
TY  - JOUR
AU  - N. O. Garanina
TI  - Common Knowledge in Well-structured Perfect Recall Systems
JO  - Modelirovanie i analiz informacionnyh sistem
PY  - 2013
SP  - 10
EP  - 21
VL  - 20
IS  - 6
PB  - mathdoc
UR  - http://geodesic.mathdoc.fr/item/MAIS_2013_20_6_a0/
LA  - ru
ID  - MAIS_2013_20_6_a0
ER  - 
%0 Journal Article
%A N. O. Garanina
%T Common Knowledge in Well-structured Perfect Recall Systems
%J Modelirovanie i analiz informacionnyh sistem
%D 2013
%P 10-21
%V 20
%N 6
%I mathdoc
%U http://geodesic.mathdoc.fr/item/MAIS_2013_20_6_a0/
%G ru
%F MAIS_2013_20_6_a0
N. O. Garanina. Common Knowledge in Well-structured Perfect Recall Systems. Modelirovanie i analiz informacionnyh sistem, Tome 20 (2013) no. 6, pp. 10-21. http://geodesic.mathdoc.fr/item/MAIS_2013_20_6_a0/

[1] P. A. Abdulla, K. Ĉerâns, B. Jonsson, Yih-Kuen Tsay, “Algorithmic analysis of programs with well quasi-ordered domains”, Information and Computation, 160:1–2 (2000), 109–127 | DOI | MR | Zbl

[2] R. H. Bordini, M. Fisher, W. Visser, M. Wooldridge, “Verifying Multi-agent Programs by Model Checking”, Autonomous Agents and Multi-Agent Systems, 12:2 (2006), 239–256 | DOI

[3] M. Cohen, A. Lomuscio, “Non-elementary speed up for model checking synchronous perfect recall”, Proceeding of the 2010 conference on ECAI 2010, IOS Press, Amsterdam, 2010, 1077–1078

[4] E. A. Emerson, “Temporal and Modal Logic”, Handbook of Theoretical Computer Science, v. B, Elsevier; MIT Press, 1990, 995–1072 | MR | Zbl

[5] R. Fagin, J. Y. Halpern, Y. Moses, M. Y. Vardi, Reasoning about Knowledge, MIT Press, 1995 | MR | Zbl

[6] A. Finkel, Ph. Schnoebelen, Well-structured transition systems everywhere!, Theor. Comp. Sci., 256:1–2 (2001), 63–92 | DOI | MR | Zbl

[7] N. O. Garanina, N. A. Kalinina, N. V. Shilov, “Model checking knowledge, actions and fixpoints”, Proc. of Concurrency, Specification and Programming Workshop CS'2004 (Germany, 2004), v. 2, Informatik-Bericht, 170, Humboldt Universitat, Berlin, 351–357

[8] N. O. Garanina, “Exponential Improvement of Time Complexity of Model Checking for Multiagent Systems with Perfect Recall”, Programming and Computer Software, 38:6 (2012), 294–303 | DOI | Zbl

[9] J. Y. Halpern, R. van der Meyden, M. Y. Vardi, “Complete Axiomatizations for Reasoning About Knowledge and Time”, SIAM J. Comp., 33:3 (2004), 674–703 | DOI | MR | Zbl

[10] J. Y. Halpern, L. D. Zuck, “A little knowledge goes a long way: knowledge-based derivations and correctness proofs for a family of protocols”, Journal of the ACM, 39:3 (1992), 449–478 | DOI | MR | Zbl

[11] X. Huang, R. van der Meyden, “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, 215, IOS Press, 2010, 549–554 | Zbl

[12] E. V. Kouzmin, N. V. Shilov, V. A. Sokolov, “Model Checking $\mu$-Calculus in Well-Structured Transition Systems”, Proc. of 11th International Symposium on Temporal Representation and Reasoning, TIME'04, IEEE Press, France, 152–155

[13] D. Kozen, “Results on the Propositional Mu-Calculus”, Theoretical Computer Science, 27:3 (1983), 333–354 | DOI | MR | Zbl

[14] D. Kozen, J. Tiuryn, “Logics of Programs”, Handbook of Theoretical Computer Science, v. B, Elsevier and MIT Press, 1990, 789–840 | MR | Zbl

[15] M. Z. Kwiatkowska, A. Lomuscio, H. Qu, “Parallel Model Checking for Temporal Epistemic Logic”, Proc. of 19th ECAI (Lisbon, Portugal, August 16–20), Frontiers in Artificial Intelligence and Applications, 215, IOS Press, 2010, 543–548 | Zbl

[16] A. Lomuscio, W. Penczek, H. Qu, “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, 659–666 | MR

[17] R. van der Meyden, N. V. Shilov, “Model Checking Knowledge and Time in Systems with Perfect Recall”, Lect. Notes Comput. Sci., 1738, 1999, 432–445 | Zbl

[18] N. V. Shilov, N. O. Garanina, K.-M. Choe, “Update and Abstraction in Model Checking of Knowledge and Branching Time”, Fundamenta Informaticae, 72:1–3 (2006), 347–361 | MR | Zbl

[19] N. V. Shilov, N. O. Garanina, “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, 4378, 2006