DROPS

Document

DOI: 10.4230/LIPIcs.CONCUR.2021.24

A Temporal Logic for Strategic Hyperproperties

Authors: Raven Beutner and Bernd Finkbeiner

Published in: LIPIcs, Volume 203, 32nd International Conference on Concurrency Theory (CONCUR 2021)

Abstract

Hyperproperties are commonly used in computer security to define information-flow policies and other requirements that reason about the relationship between multiple computations. In this paper, we study a novel class of hyperproperties where the individual computation paths are chosen by the strategic choices of a coalition of agents in a multi-agent system. We introduce HyperATL^*, an extension of computation tree logic with path variables and strategy quantifiers. HyperATL^* can express strategic hyperproperties, such as that the scheduler in a concurrent system has a strategy to avoid information leakage. HyperATL^* is particularly useful to specify asynchronous hyperproperties, i.e., hyperproperties where the speed of the execution on the different computation paths depends on the choices of the scheduler. Unlike other recent logics for the specification of asynchronous hyperproperties, our logic is the first to admit decidable model checking for the full logic. We present a model checking algorithm for HyperATL^* based on alternating word automata, and show that our algorithm is asymptotically optimal by providing a matching lower bound. We have implemented a prototype model checker for a fragment of HyperATL^*, able to check various security properties on small programs.

Cite as

Raven Beutner and Bernd Finkbeiner. A Temporal Logic for Strategic Hyperproperties. In 32nd International Conference on Concurrency Theory (CONCUR 2021). Leibniz International Proceedings in Informatics (LIPIcs), Volume 203, pp. 24:1-24:19, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2021)

Copy BibTex To Clipboard

@InProceedings{beutner_et_al:LIPIcs.CONCUR.2021.24,
  author =	{Beutner, Raven and Finkbeiner, Bernd},
  title =	{{A Temporal Logic for Strategic Hyperproperties}},
  booktitle =	{32nd International Conference on Concurrency Theory (CONCUR 2021)},
  pages =	{24:1--24:19},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-203-7},
  ISSN =	{1868-8969},
  year =	{2021},
  volume =	{203},
  editor =	{Haddad, Serge and Varacca, Daniele},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2021.24},
  URN =		{urn:nbn:de:0030-drops-144019},
  doi =		{10.4230/LIPIcs.CONCUR.2021.24},
  annote =	{Keywords: hyperproperties, temporal logic, alternating-time temporal logic, model checking, multi-agent systems, information flow, asynchronous hyperproperties}
}

Document

DOI: 10.4230/LIPIcs.CONCUR.2019.26

Translating Asynchronous Games for Distributed Synthesis

Authors: Raven Beutner, Bernd Finkbeiner, and Jesko Hecking-Harbusch

Published in: LIPIcs, Volume 140, 30th International Conference on Concurrency Theory (CONCUR 2019)

Abstract

In distributed synthesis, a set of process implementations is generated, which together, accomplish an objective against all possible behaviors of the environment. A lot of recent work has focussed on systems with causal memory, i.e., sets of asynchronous processes that exchange their causal histories upon synchronization. Decidability results for this problem have been stated either in terms of control games, which extend Zielonka’s asynchronous automata by partitioning the actions into controllable and uncontrollable, or in terms of Petri games, which extend Petri nets by partitioning the tokens into system and environment players. The precise connection between these two models was so far, however, an open question. In this paper, we provide the first formal connection between control games and Petri games. We establish the equivalence of the two game types based on weak bisimulations between their strategies. For both directions, we show that a game of one type can be translated into an equivalent game of the other type. We provide exponential upper and lower bounds for the translations. Our translations allow to transfer and combine decidability results between the two types of games. Exemplarily, we translate decidability in acyclic communication architectures, originally obtained for control games, to Petri games, and decidability in single-process systems, originally obtained for Petri games, to control games.

Cite as

Raven Beutner, Bernd Finkbeiner, and Jesko Hecking-Harbusch. Translating Asynchronous Games for Distributed Synthesis. In 30th International Conference on Concurrency Theory (CONCUR 2019). Leibniz International Proceedings in Informatics (LIPIcs), Volume 140, pp. 26:1-26:16, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2019)

Copy BibTex To Clipboard

@InProceedings{beutner_et_al:LIPIcs.CONCUR.2019.26,
  author =	{Beutner, Raven and Finkbeiner, Bernd and Hecking-Harbusch, Jesko},
  title =	{{Translating Asynchronous Games for Distributed Synthesis}},
  booktitle =	{30th International Conference on Concurrency Theory (CONCUR 2019)},
  pages =	{26:1--26:16},
  series =	{Leibniz International Proceedings in Informatics (LIPIcs)},
  ISBN =	{978-3-95977-121-4},
  ISSN =	{1868-8969},
  year =	{2019},
  volume =	{140},
  editor =	{Fokkink, Wan and van Glabbeek, Rob},
  publisher =	{Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
  address =	{Dagstuhl, Germany},
  URL =		{https://drops.dagstuhl.de/entities/document/10.4230/LIPIcs.CONCUR.2019.26},
  URN =		{urn:nbn:de:0030-drops-109289},
  doi =		{10.4230/LIPIcs.CONCUR.2019.26},
  annote =	{Keywords: synthesis, distributed systems, causal memory, Petri games, control games}
}

Search Results

Documents authored by Beutner, Raven

A Temporal Logic for Strategic Hyperproperties

Abstract

Cite as

Translating Asynchronous Games for Distributed Synthesis

Abstract

Cite as

Thanks for your feedback!

Could not send message