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

Hyperproperties are system properties that relate multiple computation pathsin 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 reasoningabout strategic abilities in multi-agent systems. We introduce HyperATL*, anextension of computation tree logic with path variables and strategyquantifiers. Our logic supports quantification over paths in a system - as ispossible in hyperlogics such as HyperCTL* - but resolves the paths based on thestrategic choices of a coalition of agents. This allows us to capture manypreviously studied (strategic) security notions in a unifying hyperlogic.Moreover, we show that HyperATL* is particularly useful for specifyingasynchronous hyperproperties, i.e., hyperproperties where the execution speedon the different computation paths depends on the choices of a scheduler. Weshow that finite-state model checking of HyperATL* is decidable and present amodel checking algorithm based on alternating automata. We establish that ouralgorithm is asymptotically optimal by proving matching lower bounds. We haveimplemented a prototype model checker for a fragment of HyperATL* that cancheck various security properties in small finite-state systems