Alternating-time temporal logic ATL with finitely bounded semantics

DOI10.1016/J.TCS.2019.05.029MaRDI QIDQ2334601zbMATH OpenOpenAlexWikidataFDO

Authors Antti Kuusisto, Raine Rönnholm, Valentin Goranko

Publication date 7 November 2019

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

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

zbMATH Keywords

alternating-time temporal logicaxiomatizationcompletenessdecidabilityfinitely bounded semanticstableaux

Mathematics Subject Classification ID

Decidability of theories and sets of sentences (03B25) Temporal logic (03B44) Computational difficulty of problems (lower bounds, completeness, difficulty of approximation, etc.) (68Q17) Logic in artificial intelligence (68T27)

Recommendations

• CTL with finitely bounded semantics
• Game-Theoretic Semantics for Alternating-Time Temporal Logic
• Deciding \(\mathsf {ATL}^*\) satisfiability by tableaux
• Complete axiomatization and decidability of alternating-time temporal logic
• Optimal Tableaux-Based Decision Procedure for Testing Satisfiability in the Alternating-Time Temporal Logic ATL+

Cites work

• Alternating-time temporal logic
• ATL Satisfiability is Indeed EXPTIME-complete
• Bounded semantics
• Complete axiomatization and decidability of alternating-time temporal logic
• CTL with finitely bounded semantics
• Finitary winning in \({\omega}\)-regular games
• From Liveness to Promptness
• Game-Theoretic Semantics for Alternating-Time Temporal Logic
• scientific article; zbMATH DE number 1799521 (Why is no real title available?)
• scientific article; zbMATH DE number 3399180 (Why is no real title available?)
• scientific article; zbMATH DE number 3190338 (Why is no real title available?)
• Modal logic
• On promptness in parity games
• Optimal tableau method for constructive satisfiability testing and model synthesis in the alternating-time temporal logic \(\mathrm{ATL}^+\)
• Parity and Streett games with costs
• Promptness in \(\omega \)-regular automata
• Propositional dynamic logic of regular programs
• Tableau-based decision procedures for logics of strategic ability in multiagent systems
• Temporal logics in computer science. Finite-state systems

Cited in

(7)

• Bounded game-theoretic semantics for modal mu-calculus
• Game-theoretic semantics for \(\mathrm{ATL}^+\) with applications to model checking
• Optimal Tableaux-Based Decision Procedure for Testing Satisfiability in the Alternating-Time Temporal Logic ATL+
• ATL with Strategy Contexts and Bounded Memory
• Bounded game-theoretic semantics for modal mu-calculus and some variants
• On some categories of structured sets
• CTL with finitely bounded semantics

This page was built for publication: Alternating-time temporal logic ATL with finitely bounded semantics

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