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

DOI10.1145/1614431.1614434zbMATH Open1351.68266OpenAlexW2139978539MaRDI QIDQ2946589FDOQ2946589

Authors Dmitry Shkatov, Valentin Goranko

Publication date 17 September 2015

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

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

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)

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.

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

Cited in

(15)

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

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)