2008/03/15 by Valentin Goranko, Dmitry Shkatov, Goranko, Valentin +1
Computer Science · #Artificial Intelligence (cs.AI) #Constraint Satisfaction and Optimization #F.4.1 #FOS: Computer and information sciences #I.2.11 #I.2.3 #I.2.4 #Logic in Computer Science (cs.LO) #Logic, Reasoning, and Knowledge #Multi-Agent Systems and Negotiation #Multiagent Systems (cs.MA)
paper · pdf · doi:10.48550/arxiv.0803.2306
openalex publication_date 2008/03/15 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
We develop an incremental tableau-based decision procedures for the Alternating-time temporal logic ATL and some of its variants. While running within the theoretically established complexity upper bound, we claim that our tableau is 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.