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.

• 03B44 - Temporal logic
• 03B70 - Logic in computer science
• 68-XX - Computer science
• 68Q60 - Specification and verification (program logics, model checking, etc.)
• 68T27 - Logic in artificial intelligence
• 68T42 - Agent technology and artificial intelligence