Complete axiomatization and decidability of alternating-time temporal logic

DOI10.1016/j.tcs.2005.07.043zbMath1089.03013OpenAlexW2160254449MaRDI QIDQ2368988

Govert van Drimmelen, Valentin F. Goranko

Publication date: 28 April 2006

Published in: Theoretical Computer Science (Search for Journal in Brave)

Full work available at URL: https://doi.org/10.1016/j.tcs.2005.07.043

zbMATH Keywords

SatisfiabilityOpen systemsAlternating tree automataAlternating-time temporal logicComplete axiomatizationConcurrent game structures

Mathematics Subject Classification ID

Applications of game theory (91A80) Automata and formal grammars in connection with logical questions (03D05) Specification and verification (program logics, model checking, etc.) (68Q60) Decidability of theories and sets of sentences (03B25) Temporal logic (03B44)

Related Items

Differential Game Logic ⋮ Optimal Tableau Method for Constructive Satisfiability Testing and Model Synthesis in the Alternating-Time Temporal Logic ATL ⁺ ⋮ Specification and Verification of Multi-Agent Systems ⋮ A complete coalition logic of temporal knowledge for multi-agent systems ⋮ An alternating-time temporal logic with knowledge, perfect recall and past: axiomatisation and model-checking ⋮ The Temporal Logic of Coalitional Goal Assignments in Concurrent Multiplayer Games ⋮ Ordered Resolution for Coalition Logic ⋮ Undecidability of QLTL and QCTL with two variables and one monadic predicate letter ⋮ Complexity of finite-variable fragments of propositional temporal and modal logics of computation ⋮ Data-informed knowledge and strategies ⋮ Dependences in Strategy Logic ⋮ Completeness of a branching-time logic with possible choices ⋮ THE LOGIC OF JOINT ABILITY IN TWO-PLAYER TACIT GAMES ⋮ Formal modelling and verification of probabilistic resource bounded agents ⋮ Together we know how to achieve: an epistemic logic of know-how ⋮ A first-order coalition logic for BDI-agents ⋮ Deductive verification of alternating systems ⋮ Intelligence in Strategic Games ⋮ Dependences in strategy logic ⋮ Action and knowledge in alternating-time temporal logic ⋮ Model-Checking Strategic Ability and Knowledge of the Past of Communicating Coalitions ⋮ Game Quantification Patterns ⋮ Knowing-how under uncertainty ⋮ Natural strategic ability ⋮ A logic of strategic ability under bounded memory ⋮ On composition of bounded-recall plans ⋮ Embedding Coalition Logic in the Minimal Normal Multimodal Logic with Intersection ⋮ From oughts to goals: a logic for Enkrasia ⋮ Alternating-Time Temporal Announcement Logic ⋮ Alternating-time temporal logic ATL with finitely bounded semantics ⋮ Unnamed Item ⋮ Representing and reasoning about game strategies ⋮ A logic with revocable and refinable strategies

Cites Work

• Unnamed Item
• Unnamed Item
• Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra
• Computer science today. Recent trends and developments
• Comparing semantics of logics for multi-agent systems
• ATL Satisfiability is Indeed EXPTIME-complete
• Alternating-time temporal logic
• A Modal Logic for Coalitional Power in Games
• An automata-theoretic approach to branching-time model checking
• Rudiments of \(\mu\)-calculus

This page was built for publication: Complete axiomatization and decidability of alternating-time temporal logic