Tableau-based decision procedures for logics of strategic ability in multiagent systems

DOI10.1145/1614431.1614434zbMATH Open1351.68266arXiv0803.2306OpenAlexW2139978539MaRDI QIDQ2946589FDOQ2946589

Authors: Dmitry Shkatov, Valentin Goranko 

Publication date: 17 September 2015

Published in: ACM Transactions on Computational Logic (Search for Journal in Brave)

Abstract: 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.

Full work available at URL: https://arxiv.org/abs/0803.2306

Recommendations

• Deciding \(\mathsf {ATL}^*\) satisfiability by tableaux
• TATL: Implementation of ATL Tableau-Based Decision Procedure
• Optimal Tableaux-Based Decision Procedure for Testing Satisfiability in the Alternating-Time Temporal Logic ATL+
• A tableau-based decision procedure for CTL\(^*\)
• Tableau-based decision procedure for the multiagent epistemic logic with all coalitional operators for common and distributed knowledge

zbMATH Keywords

decision procedurestableauxalternating-time temporal logicLogics for multiagent systems

Mathematics Subject Classification ID

Logic in artificial intelligence (68T27) Agent technology and artificial intelligence (68T42) Decidability of theories and sets of sentences (03B25) Temporal logic (03B44)

Cited In (15)

• Title not available (Why is that?)
• Tableaux-based decision method for single-agent linear time synchronous temporal epistemic logics with interacting time and knowledge
• Alternating-time temporal logic ATL with finitely bounded semantics
• Tableau-based decision procedure for the multiagent epistemic logic with all coalitional operators for common and distributed knowledge
• Title not available (Why is that?)
• Tableau-Based Procedure for Deciding Satisfiability in the Full Coalitional Multiagent Epistemic Logic
• A tableau for bundled strategies
• Complexity of finite-variable fragments of propositional temporal and modal logics of computation
• Ordered resolution for coalition logic
• Tableaux for single-agent epistemic PDL with perfect recall and no miracles
• Logics for Reasoning About Strategic Abilities in Multi-player Games
• Deciding \(\mathsf {ATL}^*\) satisfiability by tableaux
• Synthesizing strategies for homogeneous multi-agent systems with incomplete information
• Undecidability of QLTL and QCTL with two variables and one monadic predicate letter
• Optimal tableau method for constructive satisfiability testing and model synthesis in the alternating-time temporal logic \(\mathrm{ATL}^+\)

This page was built for publication: Tableau-based decision procedures for logics of strategic ability in multiagent systems

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2946589)