Augmenting ATL with strategy contexts

DOI10.1016/j.ic.2014.12.020zbMath1332.68140OpenAlexW824553004MaRDI QIDQ897650

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)

Related Items (16)

\(\mathsf{QCTL}\) model-checking with \(\mathsf{QBF}\) solvers ⋮ Model-checking iterated games ⋮ Dependences in Strategy Logic ⋮ Taming strategy logic: non-recurrent fragments ⋮ On the semantics of strategy logic ⋮ Reasoning about Quality and Fuzziness of Strategic Behaviors ⋮ Unnamed Item ⋮ Unnamed Item ⋮ Automated temporal equilibrium analysis: verification and synthesis of multi-player games ⋮ Bisimulations for verifying strategic abilities with an application to the ThreeBallot voting protocol ⋮ Strategic reasoning with a bounded number of resources: the quest for tractability ⋮ Dependences in strategy logic ⋮ Nash equilibria in symmetric graph games with partial observation ⋮ Unnamed Item ⋮ Quantifying Bounds in Strategy Logic ⋮ Verification of multi-agent systems with public actions against strategy logic

Uses Software

• CESAR
• MCMAS
• MCMAS-SLK

Cites Work

• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Games with secure equilibria
• Many-dimensional modal logics: theory and applications
• Complexity Hierarchies beyond Elementary
• Reasoning about Actions Meets Strategic Logics
• Quantified CTL: Expressiveness and Model Checking
• What Makes Atl* Decidable? A Decidable Fragment of Strategy Logic
• On Satisfiability in ATL with Strategy Contexts
• Quantified CTL: Expressiveness and Complexity
• A Temporal Logic for the Interaction of Strategies
• Recurring Dominoes: Making the Highly Undecidable Highly Understandable
• ATL Satisfiability is Indeed EXPTIME-complete
• Alternating-time temporal logic
• Strategy Logic
• ATL with Strategy Contexts and Bounded Memory
• The equational theory of CA₃ is undecidable
• Model-Checking Iterated Games
• Equilibrium points in n -person games

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