Raven Beutner ; Bernd Finkbeiner - HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems

lmcs:9209 - Logical Methods in Computer Science, May 31, 2023, Volume 19, Issue 2 - https://doi.org/10.46298/lmcs-19(2:13)2023
HyperATL*: A Logic for Hyperproperties in Multi-Agent SystemsArticle

Authors: Raven Beutner ; Bernd 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.


    Volume: Volume 19, Issue 2
    Published on: May 31, 2023
    Accepted on: April 4, 2023
    Submitted on: March 15, 2022
    Keywords: Computer Science - Logic in Computer Science
    Funding:
      Source : OpenAIRE Graph
    • Logics and Algorithms for a Unified Theory of Hyperproperties; Funder: European Commission; Code: 101055412
    • Output-Sensitive Algorithms for Reactive Synthesis; Funder: European Commission; Code: 683300

    1 Document citing this article

    Consultation statistics

    This page has been seen 1117 times.
    This article's PDF has been downloaded 293 times.