Common knowledge in well-structured perfect recall systems

被引：1

作者：

Garanina N.O. ^{[1
]}

机构：

[1] Ershov Institute of Informatic Systems, Siberian Branch, Russian Academy of Sciences, pr. Akad. Lavrent’eva 6, Novosibirsk

来源：

Automatic Control and Computer Sciences | 2014年 / 48卷 / 07期

基金：

俄罗斯基础研究基金会;

关键词：

logic of common knowledge; model checking; multiagent perfect recall systems; well-structured systems;

D O I：

10.3103/S0146411614070086

中图分类号：

学科分类号：

摘要：

In this paper, a model checking problem for the μPLCn logic of common knowledge and fixpoints in well-structured multiagent systems with perfect recall is investigated. It is shown that a synchronous perfect recall environment generated by a well-structured environment and provided with a special PRS order forms a well-structured environment. This implies that the model checking problem for the disjunctive fragment of μPLCn is decidable. © 2014, Allerton Press, Inc.

引用

页码：381 / 388

页数：7

共 17 条

[1]

Abdulla P.A., Cerans K., Johnson B., Tsay Y.-K., Algorithmic analysis of programs with well quasiordered domains, Inform. Compt., 160, pp. 109-127, (2000)

[2]

Bordini R.H., Fisher M., Visser W., Wooldridge M., Verifying multi-agent programs by model checking, Autonom. Agents and Multi-Agent Syst., 12, pp. 239-256, (2006)

[3]

Cohen M., Lomuscio A., Non-elementary speed up for model checking synchronous perfect recall, Proc. 2010 Conf. on ECAI 2010, pp. 1077-1078, (2010)

[4]

Emerson E.A., Temporal and modal logic, Handbook of Theoretical Computer Science, pp. 995-1072, (1990)

[5]

Fagin R., Halpern J.Y., Moses Y., Vardi M.Y., Reasoning about Knowledge, (1995)

[6]

Finkel A., Schnoebelen P., Well-structured transition systems everywhere!, Theor. Comp. Sci., 256, pp. 63-92, (2001)

[7]

Garanina N.O., Kalinina N.A., Shilov N.V., Model checking knowledge, actions and fixpoints, Proc. Concurrency, Specification and Programming Workshop CS&P, pp. 351-357, (2004)

[8]

Garanina N.O., Exponential improvement of time complexity of model checking for multiagent systems with perfect recall, Program. Compt. Software, 38, pp. 294-303, (2012)

[9]

Halpern J.Y., van der Meyden R., Vardi M.Y., Complete axiomatizations for reasoning about knowledge and time, SIAM J. Compt., 33, pp. 674-703, (2004)

[10]

Halpern J.Y., Zuck L.D., A little knowledge goes a long way: knowledge-based derivations and correctness proofs for a family of protocols, J. ACM, pp. 449-478, (1992)

← 1 2 →