Logo
ScienceStack
Table of Contents
Fetching ...
Sign In

On Alternating-Time Temporal Logic, Hyperproperties, and Strategy Sharing

Raven Beutner, Bernd Finkbeiner

TL;DR

This paper proposes HyperATL*_S, an extension of ATL* in which it is proved that model checking of HyperATL*_S on concurrent game structures is decidable and shows that HyperATL*_S is a rich specification language that captures important AI-related properties that were out of reach of existing logics.

Abstract

Alternating-time temporal logic (ATL$^*$) is a well-established framework for formal reasoning about multi-agent systems. However, while ATL$^*$ can reason about the strategic ability of agents (e.g., some coalition $A$ can ensure that a goal is reached eventually), we cannot compare multiple strategic interactions, nor can we require multiple agents to follow the same strategy. For example, we cannot state that coalition $A$ can reach a goal sooner (or more often) than some other coalition $A'$. In this paper, we propose HyperATLS$^*_S$, an extension of ATL$^*$ in which we can (1) compare the outcome of multiple strategic interactions w.r.t. a hyperproperty, i.e., a property that refers to multiple paths at the same time, and (2) enforce that some agents share the same strategy. We show that HyperATL$^*_S$ is a rich specification language that captures important AI-related properties that were out of reach of existing logics. We prove that model checking of HyperATL$^*_S$ on concurrent game structures is decidable. We implement our model-checking algorithm in a tool we call HyMASMC and evaluate it on a range of benchmarks.

On Alternating-Time Temporal Logic, Hyperproperties, and Strategy Sharing

TL;DR

This paper proposes HyperATL*_S, an extension of ATL* in which it is proved that model checking of HyperATL*_S on concurrent game structures is decidable and shows that HyperATL*_S is a rich specification language that captures important AI-related properties that were out of reach of existing logics.

Abstract

Alternating-time temporal logic (ATL) is a well-established framework for formal reasoning about multi-agent systems. However, while ATL can reason about the strategic ability of agents (e.g., some coalition can ensure that a goal is reached eventually), we cannot compare multiple strategic interactions, nor can we require multiple agents to follow the same strategy. For example, we cannot state that coalition can reach a goal sooner (or more often) than some other coalition . In this paper, we propose HyperATLS, an extension of ATL in which we can (1) compare the outcome of multiple strategic interactions w.r.t. a hyperproperty, i.e., a property that refers to multiple paths at the same time, and (2) enforce that some agents share the same strategy. We show that HyperATL is a rich specification language that captures important AI-related properties that were out of reach of existing logics. We prove that model checking of HyperATL on concurrent game structures is decidable. We implement our model-checking algorithm in a tool we call HyMASMC and evaluate it on a range of benchmarks.
Paper Structure (40 sections, 12 theorems, 32 equations, 4 figures, 2 tables, 1 algorithm)

This paper contains 40 sections, 12 theorems, 32 equations, 4 figures, 2 tables, 1 algorithm.

Table of Contents

  1. Introduction
  2. Hyperproperties.
  3. Strategy Sharing and HyperATL$^*_S$.
  4. Model Checking.
  5. Implementation.
  6. Supplementary Material.
  7. Related Work
  8. Preliminaries
  9. ATL$^*$.
  10. HyperATL$^*_S$
  11. Syntax.
  12. Semantics.
  13. HyperATL$^*_S$ and ATL$^*$.
  14. Model Checking of HyperATL$^*_S$
  15. Alternating Automata
  16. ...and 25 more sections

Key Result

Proposition 1

For every ATL$^*$ formula $\varphi$, there exists an effectively computable HyperATL$^*_S$ formula $\varphi'$ such that for every CGS $\mathcal{G}$, $\mathcal{G} \models_{\text{ATL$^*${}}} \varphi$ iff $\mathcal{G} \models \varphi'$.

Figures (4)

  • Figure 1: A simple CGS with $\mathit{Agts} = \{\mathit{sched}, \mathit{W1}, \mathit{W2}\}$. Each edge has the form $(a_1, a_2, a_3)$ where $a_1, a_2$, and $a_3$ are the actions of $\mathit{sched}$, $\mathit{W1}$, and $\mathit{W2}$, respectively. We write "$\_$" for an arbitrary action.
  • Figure 2: Example APA over alphabet $\Sigma = \{a, b, c\}$.
  • Figure 3: Illustration of our model-checking algorithm on \ref{['ex:cgs']}. In \ref{['fig:sub:apa-dpa']}, we depict a DPA over alphabet $\{\pi, \pi'\} \to \{s_0, s_1, s_2\}$ for the body $(\neg \mathit{w}_{\pi'}) \mathop{\mathrm{\normalfont\textsf{U}}}\nolimits (\neg \mathit{w}_{\pi'} \land \mathit{w}_{\pi} )$. In \ref{['fig:sub:apa-apa']}, we sketch the APA over alphabet $\{\pi\} \to \{s_0, s_1, s_2\}$ constructed using \ref{['theo:construction']} that is $(\mathcal{G}, s_0)$-equivalent to subformula $\llbracket \mathit{sched}, \mathit{W1} \rrbracket \, \pi'\mathpunct{.} (\neg \mathit{w}_{\pi'}) \mathop{\mathrm{\normalfont\textsf{U}}}\nolimits (\neg \mathit{w}_{\pi'} \land \mathit{w}_{\pi})$. In \ref{['fig:sub:apa-res-dpa']}, we depict a DPA that is equivalent to the APA in \ref{['fig:sub:apa-apa']}. Lastly, in \ref{['fig:running-cont-final']}, we sketch the APA (over singleton alphabet $\emptyset \to \{s_0, s_1, s_2\}$) constructed using \ref{['theo:construction']} that is $(\mathcal{G}, s_0)$-equivalent to $\@undefined \mathit{sched}, \mathit{W1}, \mathit{W2} \@undefined \, \pi \mathpunct{.}\llbracket \mathit{sched}, \mathit{W1} \rrbracket \, \pi'\mathpunct{.} (\neg \mathit{w}_{\pi'}) \mathop{\mathrm{\normalfont\textsf{U}}}\nolimits (\neg \mathit{w}_{\pi'} \land \mathit{w}_{\pi})$.
  • Figure 4: In \ref{['fig:apa-re']}, we depict the APA from \ref{['ex:apa']}. In \ref{['fig:apa-run']}, we sketch a run tree of this APA on the infinite word $b^\omega$.

Theorems & Definitions (27)

  • Example 1
  • Definition 1: AlurHK02
  • Example 2: Running Example
  • Proposition 1
  • Definition 2
  • Example 3
  • Proposition 2: MiyanoH84
  • Definition 3
  • Theorem 1
  • proof
  • ...and 17 more