Tableau-Based Decision Procedures for Logics of Strategic Ability in Multiagent Systems

被引：22

作者：

Goranko, Valentin ^{[1
]}

Shkatov, Dmitry ^{[2
]}

机构：

[1] Tech Univ Denmark, Dept Informat & Math Modeling, DK-2800 Lyngby, Denmark

[2] Univ Witwatersrand, Sch Comp Sci, ZA-2050 Johannesburg, South Africa

来源：

ACM TRANSACTIONS ON COMPUTATIONAL LOGIC | 2009年 / 11卷 / 01期

基金：

新加坡国家研究基金会;

关键词：

Theory; Logics for multiagent systems; alternating-time temporal logic; decision procedures; tableaux; SATISFIABILITY;

D O I：

10.1145/1614431.1614434

中图分类号：

TP301 [理论、方法];

学科分类号：

081202 ;

摘要：

We develop an incremental tableau-based decision procedure for the alternating-time temporal logic ATL and some of its variants. While running within the theoretically established complexity upper bound, we believe that our tableaux are practically more efficient in the average case than other decision procedures for ATL known so far. Besides, the ease of its adaptation to variants of ATL demonstrates the flexibility of the proposed procedure.

引用

页数：51

共 33 条

[1] One-pass tableaux for computation tree logic [J].

Abate, Pietro ;

Gore, Rajeev ;

Widmann, Florian .

LOGIC FOR PROGRAMMING, ARTIFICIAL INTELLIGENCE, AND REASONING, PROCEEDINGS, 2007, 4790 :32-+

[2]

AGOTNES T, 2007, P 11 C THEOR ASP RAT, P15

[3] Alternating-time temporal logic [J].

Alur, R ;

Henzinger, TA ;

Kupferman, O .

38TH ANNUAL SYMPOSIUM ON FOUNDATIONS OF COMPUTER SCIENCE, PROCEEDINGS, 1997, :100-109

[4]

Alur R, 1998, LECT NOTES COMPUT SC, V1536, P23, DOI 10.1007/3-540-49213-5_2

[5] Alternating-time temporal logic [J].

Alur, R ;

Henzinger, TA ;

Kupferman, O .

JOURNAL OF THE ACM, 2002, 49 (05) :672-713

[6]

Alur R, 1998, LECT NOTES COMPUT SC, V1427, P521, DOI 10.1007/BFb0028774

[7]

[Anonymous], B EC RES

[8]

[Anonymous], 1983, Proof Methods for Modal and Intuitionistic Logics

[9]

[Anonymous], LNCS

[10]

[Anonymous], LOGIQUE ANAL

← 1 2 3 4 →