2203.07283.pdf (861.13 kB)

HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems

Download (861.13 kB)
journal contribution
posted on 2024-03-26, 09:06 authored by Raven BeutnerRaven Beutner, Bernd FinkbeinerBernd Finkbeiner
Hyperproperties are system properties that relate multiple computation paths in a system and are commonly used to, e.g., define information-flow policies. In this paper, we study a novel class of hyperproperties that allow reasoning about strategic abilities in multi-agent systems. We introduce HyperATL*, an extension of computation tree logic with path variables and strategy quantifiers. Our logic supports quantification over paths in a system - as is possible in hyperlogics such as HyperCTL* - but resolves the paths based on the strategic choices of a coalition of agents. This allows us to capture many previously studied (strategic) security notions in a unifying hyperlogic. Moreover, we show that HyperATL* is particularly useful for specifying asynchronous hyperproperties, i.e., hyperproperties where the execution speed on the different computation paths depends on the choices of a scheduler. We show that finite-state model checking of HyperATL* is decidable and present a model checking algorithm based on alternating automata. We establish that our algorithm is asymptotically optimal by proving matching lower bounds. We have implemented a prototype model checker for a fragment of HyperATL* that can check various security properties in small finite-state systems.


Primary Research Area

  • Reliable Security Guarantees


Logical Methods in Computer Science


Volume 19, Issue 2


Logical Methods in Computer Science e.V.

Open Access Type

  • Gold

Sub Type

  • Article


@article{Beutner:Finkbeiner:2023, title = "HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems", author = "Beutner, Raven" AND "Finkbeiner, Bernd", year = 2023, month = 5, journal = "Logical Methods in Computer Science", publisher = "Logical Methods in Computer Science e.V.", issn = "1860-5974", doi = "10.46298/lmcs-19(2:13)2023" }