Reasoning About Strategies

DOI10.1145/2631917zbMath1354.68178arXiv1112.6275OpenAlexW2108947407MaRDI QIDQ2946746

Giuseppe Perelli, Aniello Murano, Moshe Y. Vardi, Fabio Mogavero

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/1112.6275

zbMATH Keywords

model checkingbehavioral strategiesstrategy logic

Mathematics Subject Classification ID

Applications of game theory (91A80) Logic in artificial intelligence (68T27) Specification and verification (program logics, model checking, etc.) (68Q60)

Related Items (51)

An abstraction-refinement methodology for reasoning about network games ⋮ The Temporal Logic of Coalitional Goal Assignments in Concurrent Multiplayer Games ⋮ Verification of agent navigation in partially-known environments ⋮ Synthesis with rational environments ⋮ Practical verification of multi-agent systems against \textsc{Slk} specifications ⋮ Graded modalities in strategy logic ⋮ Imperfect information in reactive modules games ⋮ A logic for conditional local strategic reasoning ⋮ From model checking to equilibrium checking: reactive modules for rational verification ⋮ Dependences in Strategy Logic ⋮ Unnamed Item ⋮ Robust worst cases for parity games algorithms ⋮ Taming strategy logic: non-recurrent fragments ⋮ Infinite-duration poorman-bidding games ⋮ On the semantics of strategy logic ⋮ Cooperative concurrent games ⋮ An abstraction-refinement framework for verifying strategic properties in multi-agent systems with imperfect information ⋮ Reasoning about Quality and Fuzziness of Strategic Behaviors ⋮ Reasoning About Substructures and Games ⋮ HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems ⋮ Unnamed Item ⋮ Reasoning about graded strategy quantifiers ⋮ Unnamed Item ⋮ 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 ⋮ Multi-player games with LDL goals over finite traces ⋮ Epistemic GDL: a logic for representing and reasoning about imperfect information games ⋮ Strategic reasoning with a bounded number of resources: the quest for tractability ⋮ Solving parity games via priority promotion ⋮ Strategies, model checking and branching-time properties in Maude ⋮ Intelligence in Strategic Games ⋮ Dependences in strategy logic ⋮ Alternating-time temporal logics with linear past ⋮ Nash equilibria in symmetric graph games with partial observation ⋮ Unnamed Item ⋮ Unnamed Item ⋮ A delayed promotion policy for parity games ⋮ Cycle detection in computation tree logic ⋮ Dynamic resource allocation games ⋮ Knowing-how under uncertainty ⋮ Natural strategic ability ⋮ Unnamed Item ⋮ On composition of bounded-recall plans ⋮ Quantifying Bounds in Strategy Logic ⋮ Multi-valued Verification of Strategic Ability ⋮ Verification of multi-agent systems with public actions against strategy logic ⋮ A game-theoretic approach for the synthesis of complex systems ⋮ A logic with revocable and refinable strategies ⋮ Good-for-Game QPTL: An Alternating Hodges Semantics

Uses Software

• 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
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Unnamed Item
• Doomsday equilibria for omega-regular games
• Simulating alternating tree automata by nondeterministic automata: New results and new proofs of the theorems of Rabin, McNaughton and Safra
• A game of cops and robbers
• Results on the propositional \(\mu\)-calculus
• Strategy logic
• Reasoning about temporal properties of rational play
• The complementation problem for Büchi automata with applications to temporal logic
• Alternating automata on infinite trees
• Borel determinacy
• Module checking
• Automata, logics, and infinite games. A guide to current research
• Pushdown module checking with imperfect information
• Reasoning about Actions Meets Strategic Logics
• Quantified CTL: Expressiveness and Model Checking
• What Makes Atl* Decidable? A Decidable Fragment of Strategy Logic
• A Behavioral Hierarchy of Strategy Logic
• Graded computation tree logic
• Relentful Strategic Reasoning in Alternating-Time Temporal Logic
• A Temporal Logic for the Interaction of Strategies
• Alternating-time temporal logic
• A Generic Constructive Solution for Concurrent Games with Expressive Constraints on Strategies
• ATL* Satisfiability Is 2EXPTIME-Complete
• Strategy Logic
• Enriched MU-Calculi Module Checking
• The Complexity of Enriched Mu-Calculi
• Rational Synthesis
• Graded Computation Tree Logic with Binary Coding
• Coordination Logic
• ATL with Strategy Contexts and Bounded Memory
• “Sometimes” and “not never” revisited
• Formal verification of parallel programs
• A Modal Logic for Coalitional Power in Games
• On the Boundary of Behavioral Strategies
• Substructure Temporal Logic
• Model-Checking Iterated Games
• An automata-theoretic approach to branching-time model checking
• Decidability of Second-Order Theories and Automata on Infinite Trees

This page was built for publication: Reasoning About Strategies