License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2021.24
URN: urn:nbn:de:0030-drops-144019
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2021/14401/
Beutner, Raven ;
Finkbeiner, Bernd
A Temporal Logic for Strategic Hyperproperties
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.
BibTeX - Entry
@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/opus/volltexte/2021/14401},
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}
}
|
Keywords: |
|
hyperproperties, temporal logic, alternating-time temporal logic, model checking, multi-agent systems, information flow, asynchronous hyperproperties |
|
Collection: |
|
32nd International Conference on Concurrency Theory (CONCUR 2021) |
|
Issue Date: |
|
2021 |
|
Date of publication: |
|
13.08.2021 |
