---
_id: '10774'
abstract:
- lang: eng
  text: We study the problem of specifying sequential information-flow properties
    of systems. Information-flow properties are hyperproperties, as they compare different
    traces of a system. Sequential information-flow properties can express changes,
    over time, in the information-flow constraints. For example, information-flow
    constraints during an initialization phase of a system may be different from information-flow
    constraints that are required during the operation phase. We formalize several
    variants of interpreting sequential information-flow constraints, which arise
    from different assumptions about what can be observed of the system. For this
    purpose, we introduce a first-order logic, called Hypertrace Logic, with both
    trace and time quantifiers for specifying linear-time hyperproperties. We prove
    that HyperLTL, which corresponds to a fragment of Hypertrace Logic with restricted
    quantifier prefixes, cannot specify the majority of the studied variants of sequential
    information flow, including all variants in which the transition between sequential
    phases (such as initialization and operation) happens asynchronously. Our results
    rely on new equivalences between sets of traces that cannot be distinguished by
    certain classes of formulas from Hypertrace Logic. This presents a new approach
    to proving inexpressiveness results for HyperLTL.
acknowledgement: This work was funded in part by the Wittgenstein Award Z211-N23 of
  the Austrian Science Fund (FWF) and by the FWF project W1255-N23.
alternative_title:
- LNCS
article_processing_charge: No
arxiv: 1
author:
- first_name: Ezio
  full_name: Bartocci, Ezio
  last_name: Bartocci
- first_name: Thomas
  full_name: Ferrere, Thomas
  id: 40960E6E-F248-11E8-B48F-1D18A9856A87
  last_name: Ferrere
  orcid: 0000-0001-5199-3143
- first_name: Thomas A
  full_name: Henzinger, Thomas A
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000-0002-2985-7724
- first_name: Dejan
  full_name: Nickovic, Dejan
  id: 41BCEE5C-F248-11E8-B48F-1D18A9856A87
  last_name: Nickovic
- first_name: Ana Oliveira
  full_name: Da Costa, Ana Oliveira
  last_name: Da Costa
citation:
  ama: 'Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. Flavors of sequential
    information flow. In: <i>Lecture Notes in Computer Science (Including Subseries
    Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)</i>.
    Vol 13182. Springer Nature; 2022:1-19. doi:<a href="https://doi.org/10.1007/978-3-030-94583-1_1">10.1007/978-3-030-94583-1_1</a>'
  apa: 'Bartocci, E., Ferrere, T., Henzinger, T. A., Nickovic, D., &#38; Da Costa,
    A. O. (2022). Flavors of sequential information flow. In <i>Lecture Notes in Computer
    Science (including subseries Lecture Notes in Artificial Intelligence and Lecture
    Notes in Bioinformatics)</i> (Vol. 13182, pp. 1–19). Philadelphia, PA, United
    States: Springer Nature. <a href="https://doi.org/10.1007/978-3-030-94583-1_1">https://doi.org/10.1007/978-3-030-94583-1_1</a>'
  chicago: Bartocci, Ezio, Thomas Ferrere, Thomas A Henzinger, Dejan Nickovic, and
    Ana Oliveira Da Costa. “Flavors of Sequential Information Flow.” In <i>Lecture
    Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence
    and Lecture Notes in Bioinformatics)</i>, 13182:1–19. Springer Nature, 2022. <a
    href="https://doi.org/10.1007/978-3-030-94583-1_1">https://doi.org/10.1007/978-3-030-94583-1_1</a>.
  ieee: E. Bartocci, T. Ferrere, T. A. Henzinger, D. Nickovic, and A. O. Da Costa,
    “Flavors of sequential information flow,” in <i>Lecture Notes in Computer Science
    (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes
    in Bioinformatics)</i>, Philadelphia, PA, United States, 2022, vol. 13182, pp.
    1–19.
  ista: 'Bartocci E, Ferrere T, Henzinger TA, Nickovic D, Da Costa AO. 2022. Flavors
    of sequential information flow. Lecture Notes in Computer Science (including subseries
    Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics).
    VMCAI: Verifcation, Model Checking, and Abstract Interpretation, LNCS, vol. 13182,
    1–19.'
  mla: Bartocci, Ezio, et al. “Flavors of Sequential Information Flow.” <i>Lecture
    Notes in Computer Science (Including Subseries Lecture Notes in Artificial Intelligence
    and Lecture Notes in Bioinformatics)</i>, vol. 13182, Springer Nature, 2022, pp.
    1–19, doi:<a href="https://doi.org/10.1007/978-3-030-94583-1_1">10.1007/978-3-030-94583-1_1</a>.
  short: E. Bartocci, T. Ferrere, T.A. Henzinger, D. Nickovic, A.O. Da Costa, in:,
    Lecture Notes in Computer Science (Including Subseries Lecture Notes in Artificial
    Intelligence and Lecture Notes in Bioinformatics), Springer Nature, 2022, pp.
    1–19.
conference:
  end_date: 2022-01-18
  location: Philadelphia, PA, United States
  name: 'VMCAI: Verifcation, Model Checking, and Abstract Interpretation'
  start_date: 2022-01-16
date_created: 2022-02-20T23:01:34Z
date_published: 2022-01-14T00:00:00Z
date_updated: 2022-08-05T09:02:56Z
day: '14'
department:
- _id: ToHe
doi: 10.1007/978-3-030-94583-1_1
external_id:
  arxiv:
  - '2105.02013'
intvolume: '     13182'
language:
- iso: eng
main_file_link:
- open_access: '1'
  url: ' https://doi.org/10.48550/arXiv.2105.02013'
month: '01'
oa: 1
oa_version: Preprint
page: 1-19
project:
- _id: 25F42A32-B435-11E9-9278-68D0E5697425
  call_identifier: FWF
  grant_number: Z211
  name: The Wittgenstein Prize
publication: Lecture Notes in Computer Science (including subseries Lecture Notes
  in Artificial Intelligence and Lecture Notes in Bioinformatics)
publication_identifier:
  eissn:
  - '16113349'
  isbn:
  - '9783030945824'
  issn:
  - '03029743'
publication_status: published
publisher: Springer Nature
quality_controlled: '1'
scopus_import: '1'
status: public
title: Flavors of sequential information flow
type: conference
user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87
volume: 13182
year: '2022'
...