English (United Kingdom)

https://curated-unify.zendy.io/wp-json/zendy-region/v1/featured_content/oa?rat=en

https://curated-unify.zendy.io/wp-json/zendy-region/v1/highlighted_journal/

Global: Zendy Plus annual

Presents the access of premium content as premium feature

Premium Content

Presents the keyphrase highlighting as premium feature

Keyphrase Highlighting

Presents the summarisation as premium feature

Summarisation

Insights

Presents the pdf analysis as premium feature

PDF Analysis

Presents the zaia usage as premium feature

ZAIA

Global: Zendy Plus monthly

Global: Zendy Tools annual

Global: Zendy Tools monthly

Global: Zendy Free Plan

Alternating-time temporal logic (ATL$^*$) is a well-established framework forformal reasoning about multi-agent systems. However, while ATL$^*$ can reasonabout the strategic ability of agents (e.g., some coalition $A$ can ensure thata goal is reached eventually), we cannot compare multiple strategicinteractions, nor can we require multiple agents to follow the same strategy.For example, we cannot state that coalition $A$ can reach a goal sooner (ormore often) than some other coalition $A'$. In this paper, we proposeHyperATLS$^*_S$, an extension of ATL$^*$ in which we can (1) compare theoutcome of multiple strategic interactions w.r.t. a hyperproperty, i.e., aproperty that refers to multiple paths at the same time, and (2) enforce thatsome agents share the same strategy. We show that HyperATL$^*_S$ is a richspecification language that captures important AI-related properties that wereout of reach of existing logics. We prove that model checking of HyperATL$^*_S$on concurrent game structures is decidable. We implement our model-checkingalgorithm in a tool we call HyMASMC and evaluate it on a range of benchmarks.

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