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

TL;DR

A novel class of hyperproperties that allow reasoning about strategic abilities in multi-agent systems and 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.

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.

Figures (10)

• Figure 1: Hierarchy of expressiveness of temporal logics. An arrow $A \to B$ indicates that $A$ is a (syntactic) fragment of $B$. Logics in the blue, dashed area can express hyperproperties. Logics in the red, dotted area can express strategic properties in multi-agent systems. Logics that are interpreted on multi-agent systems (ATL, ATL$^*$, and HyperATL$^*$) can also be applied to transition systems (the standard model for the remaining logics) by interpreting transition systems as 1-agent systems (see Remark ); the reverse does not hold, i.e., logics that are interpreted on transitions systems cannot reason about strategic abilities in multi-agent systems.
• Figure 2: Example program that violates (synchronous) observational determinism.
• Figure 3: Automaton construction for boolean and temporal operators. Here, $\mathcal{A}_{\psi_i} = (Q_i, q_{0, i}, \Sigma_{\psi_i}, \rho_i, c_i)$ for $i \in \{1, 2\}$ are inductively constructed alternating automata for sub-formulas $\psi_1$ and $\psi_2$. We assume that $Q_1$ and $Q_2$ are disjoint sets of states and $q_\mathit{init}$ is a fresh state. For two colorings $c_1 : Q_1 \to \mathbb{N}$ and $c_2 : Q_2 \to \mathbb{N}$, $c_1 \cupdot c_2 : Q_1 \cupdot Q_2 \to \mathbb{N}$ denotes the combined coloring. We write $[q \mapsto n]$ for the function $\{q\} \to \mathbb{N}$ that maps $q$ to $n$.
• Figure 4: Construction of a $\mathcal{G}$-equivalent automaton for $\varphi = \exists \pi \mathpunct{.} \psi$. Here, $\mathcal{A}_\psi^{\mathit{ndet}} = (Q, q_0, \Sigma_\psi, \rho, c)$ with $\rho : Q \times \Sigma_\psi \to 2^Q$ is a non-deterministic automaton that is equivalent to the inductively constructed automaton $\mathcal{A}_\psi$ for $\psi$.
• Figure 5: Construction of a $\mathcal{G}$-equivalent automaton for $\varphi = \llangle A \rrangle \pi \mathpunct{.} \psi$. Here, $\mathcal{A}^\mathit{det}_\psi = (Q, q_0, \Sigma_\psi, \rho, c)$ with $\rho : Q \times \Sigma_\psi \to Q$ is a deterministic automaton that is equivalent to the inductive constructed alternating automaton $\mathcal{A}_\psi$ for $\psi$.

Theorems & Definitions (45)

• proof
• proof
• Remark 2.1
• proof
• Definition 2.2
• proof
• Theorem 2.3: MiyanoH84DrusinskyH94
• Theorem 2.4
• Remark 3.1
• proof