Augmenting ATL with strategy contexts

DOI10.1016/J.IC.2014.12.020zbMATH Open1332.68140OpenAlexW824553004MaRDI QIDQ897650FDOQ897650

Authors François Laroussinie, Nicolas Markey

Publication date 7 December 2015

Published in Information and Computation (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1016/j.ic.2014.12.020

zbMATH Keywords

model checkingsatisfiabilitytemporal logicsgames for synthesis

Mathematics Subject Classification ID

Specification and verification (program logics, model checking, etc.) (68Q60) Temporal logic (03B44)

Recommendations

• ATL with strategy contexts: expressiveness and model checking
• ATL with Strategy Contexts and Bounded Memory
• Satisfiability of \textsf{ATL} with strategy contexts
• On satisfiability in ATL with strategy contexts
• Temporal logics for games

Cites work

• scientific article; zbMATH DE number 3870578 (Why is no real title available?)
• scientific article; zbMATH DE number 3757688 (Why is no real title available?)
• scientific article; zbMATH DE number 1989659 (Why is no real title available?)
• scientific article; zbMATH DE number 2084388 (Why is no real title available?)
• scientific article; zbMATH DE number 1825622 (Why is no real title available?)
• scientific article; zbMATH DE number 2209335 (Why is no real title available?)
• A Temporal Logic for the Interaction of Strategies
• ATL Satisfiability is Indeed EXPTIME-complete
• ATL with Strategy Contexts and Bounded Memory
• ATL with strategy contexts: expressiveness and model checking
• Alternating-time temporal logic
• Complexity hierarchies beyond elementary
• Equilibrium points in n -person games
• Games with secure equilibria
• Many-dimensional modal logics: theory and applications
• Model-checking iterated games
• On satisfiability in ATL with strategy contexts
• Quantified CTL: expressiveness and complexity
• Quantified CTL: expressiveness and model checking (extended abstract)
• Reasoning about actions meets strategic logics
• Reasoning about strategies
• Recurring Dominoes: Making the Highly Undecidable Highly Understandable
• Satisfiability of \textsf{ATL} with strategy contexts
• Strategy Logic
• The equational theory of CA₃ is undecidable
• Towards an updatable strategy logic
• What makes \textsc{Atl}* decidable? A decidable fragment of strategy logic

Cited in

(24)

• Epistemic ATL with perfect recall, past and strategy contexts
• On the semantics of strategy logic
• Reasoning about Quality and Fuzziness of Strategic Behaviors
• Automated temporal equilibrium analysis: verification and synthesis of multi-player games
• ATL with strategy contexts: expressiveness and model checking
• Dependences in strategy logic
• Robust alternating-time temporal logic
• \(\mathsf{QCTL}\) model-checking with \(\mathsf{QBF}\) solvers
• On satisfiability in ATL with strategy contexts
• Verification of multi-agent systems with public actions against strategy logic
• Satisfiability of \textsf{ATL} with strategy contexts
• Dependences in strategy logic
• Bisimulations for verifying strategic abilities with an application to the ThreeBallot voting protocol
• Model-checking iterated games
• Strategic reasoning with a bounded number of resources: the quest for tractability
• ATL with Strategy Contexts and Bounded Memory
• Taming strategy logic: non-recurrent fragments
• Nash equilibria in symmetric graph games with partial observation
• Quantifying Bounds in Strategy Logic
• scientific article; zbMATH DE number 7438567 (Why is no real title available?)
• scientific article; zbMATH DE number 7577569 (Why is no real title available?)
• Temporal logics for games
• On the complexity of \(\mathsf{ATL}\) and \(\mathsf{ATL}^*\) module checking
• scientific article; zbMATH DE number 7361818 (Why is no real title available?)

Describes a project that uses

Uses Software

• CESAR
• MCMAS
• MCMAS-SLK

This page was built for publication: Augmenting ATL with strategy contexts

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