HyperATL*: A Logic for Hyperproperties in Multi-Agent Systems
From MaRDI portal
Publication:6135762
DOI10.46298/lmcs-19(2:13)2023arXiv2203.07283MaRDI QIDQ6135762
Raven Beutner, Bernd Finkbeiner
Publication date: 26 August 2023
Published in: Logical Methods in Computer Science (Search for Journal in Brave)
Full work available at URL: https://arxiv.org/abs/2203.07283
model checkingmulti-agent systemsnon-interferencealternating-time temporal logichyperpropertiesinformation-flow controlasynchronous hyperpropertiesHyperATL*HyperCTL*HyperLTL
Cites Work
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- Unnamed Item
- A temporal logic for asynchronous hyperproperties
- A calculus of communicating systems
- Reasoning about infinite computations
- Cooperation, knowledge, and time: Alternating-time temporal epistemic logic and its applications
- Algorithms for model checking HyperLTL and HyperCTL\(^*\)
- Runtime enforcement of hyperproperties
- Relationships between nondeterministic and deterministic tape complexities
- Logics for Reasoning About Strategic Abilities in Multi-player Games
- Reasoning About Strategies
- Unifying Hyper and Epistemic Temporal Logics
- Secure information flow by self-composition
- ATL Satisfiability is Indeed EXPTIME-complete
- Alternating-time temporal logic
- Knowledge and common knowledge in a distributed environment
- ATL* Satisfiability Is 2EXPTIME-Complete
- Strategy Logic
- Alternation Removal in Büchi Automata
- Solving Parity Games in Practice
- “Sometimes” and “not never” revisited
- On the power of bounded concurrency I
- The First-Order Logic of Hyperproperties
- Propositional Dynamic Logic for Hyperproperties
- Synthesizing reactive systems from hyperproperties
- Verifying hyperliveness
- HyperLTL Satisfiability Is Σ₁¹-Complete, HyperCTL* Satisfiability Is Σ₁²-Complete.
