CISPA
Browse
29679-Article Text-33733-1-2-20240324.pdf (215.59 kB)

On Alternating-Time Temporal Logic, Hyperproperties, and Strategy Sharing

Download (215.59 kB)
conference contribution
posted on 2024-04-11, 07:55 authored by Raven BeutnerRaven Beutner, Bernd FinkbeinerBernd Finkbeiner
Alternating-time temporal logic (ATL*) is a well-established framework for formal reasoning about multi-agent systems. However, while ATL* can reason about the strategic ability of agents (e.g., some coalition A can ensure that a goal is reached eventually), we cannot compare multiple strategic interactions, nor can we require multiple agents to follow the same strategy. For example, we cannot state that coalition A can reach a goal sooner (or more often) than some other coalition A'. In this paper, we propose HyperATL*_S, an extension of ATL* in which we can (1) compare the outcome of multiple strategic interactions w.r.t. a hyperproperty, i.e., a property that refers to multiple paths at the same time, and (2) enforce that some agents share the same strategy. We show that HyperATL*_S is a rich specification language that captures important AI-related properties that were out of reach of existing logics. We prove that model checking of HyperATL*_S on concurrent game structures is decidable. We implement our model-checking algorithm in a tool we call HyMASMC and evaluate it on a range of benchmarks.

History

Editor

Wooldridge MJ ; Dy JG ; Natarajan S

Primary Research Area

  • Reliable Security Guarantees

Name of Conference

National Conference of the American Association for Artificial Intelligence (AAAI)

Journal

Proceedings of the AAAI Conference on Artificial Intelligence

Volume

38

Page Range

17317-17326

Publisher

Association for the Advancement of Artificial Intelligence (AAAI)

Open Access Type

  • Green

BibTeX

@inproceedings{Beutner:Finkbeiner:2024, title = "On Alternating-Time Temporal Logic, Hyperproperties, and Strategy Sharing", author = "Beutner, Raven" AND "Finkbeiner, Bernd", editor = "Wooldridge, Michael J" AND "Dy, Jennifer G" AND "Natarajan, Sriraam", year = 2024, month = 3, journal = "Proceedings of the AAAI Conference on Artificial Intelligence", number = "16", pages = "17317--17326", publisher = "Association for the Advancement of Artificial Intelligence (AAAI)", issn = "2159-5399", doi = "10.1609/aaai.v38i16.29679" }