HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems
From MaRDI portal
Publication:6135762
DOI10.46298/LMCS-19(2:13)2023arXiv2203.07283MaRDI QIDQ6135762FDOQ6135762
Authors: Raven Beutner, Bernd Finkbeiner 
Publication date: 26 August 2023
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Abstract: 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.
Full work available at URL: https://arxiv.org/abs/2203.07283
Recommendations
model checkingmulti-agent systemsnon-interferencealternating-time temporal logichyperpropertiesinformation-flow controlasynchronous hyperpropertiesHyperATL*HyperCTL*HyperLTL
Cites Work
- Solving parity games in practice
- Alternating-time temporal logic
- Relationships between nondeterministic and deterministic tape complexities
- Title not available (Why is that?)
- A calculus of communicating systems
- “Sometimes” and “not never” revisited
- Reasoning about infinite computations
- Knowledge and common knowledge in a distributed environment
- Reasoning about strategies: on the model-checking problem
- Strategy Logic
- Alternation removal in Büchi automata
- On the power of bounded concurrency I
- Cooperation, knowledge, and time: Alternating-time temporal epistemic logic and its applications
- Title not available (Why is that?)
- Secure information flow by self-composition
- Title not available (Why is that?)
- Algorithms for model checking HyperLTL and HyperCTL\(^*\)
- The first-order logic of hyperproperties
- Verifying hyperliveness
- A temporal logic for asynchronous hyperproperties
- ATL Satisfiability is Indeed EXPTIME-complete
- Alternating-time logic with imperfect recall
- Logics for Reasoning About Strategic Abilities in Multi-player Games
- ATL* Satisfiability Is 2EXPTIME-Complete
- Runtime enforcement of hyperproperties
- Unifying hyper and epistemic temporal logics
- Synthesizing reactive systems from hyperproperties
- Title not available (Why is that?)
- Propositional Dynamic Logic for Hyperproperties
- HyperLTL Satisfiability Is Σ₁¹-Complete, HyperCTL* Satisfiability Is Σ₁²-Complete.
- Software Verification of Hyperproperties Beyond k-Safety
Cited In (4)
This page was built for publication: HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems
Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q6135762)
