--- res: bibo_abstract: - 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.@eng bibo_authorlist: - foaf_Person: foaf_givenName: Ezio foaf_name: Bartocci, Ezio foaf_surname: Bartocci - foaf_Person: foaf_givenName: Thomas foaf_name: Ferrere, Thomas foaf_surname: Ferrere foaf_workInfoHomepage: http://www.librecat.org/personId=40960E6E-F248-11E8-B48F-1D18A9856A87 orcid: 0000-0001-5199-3143 - foaf_Person: foaf_givenName: Thomas A foaf_name: Henzinger, Thomas A foaf_surname: Henzinger foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87 orcid: 0000-0002-2985-7724 - foaf_Person: foaf_givenName: Dejan foaf_name: Nickovic, Dejan foaf_surname: Nickovic foaf_workInfoHomepage: http://www.librecat.org/personId=41BCEE5C-F248-11E8-B48F-1D18A9856A87 - foaf_Person: foaf_givenName: Ana Oliveira foaf_name: Da Costa, Ana Oliveira foaf_surname: Da Costa bibo_doi: 10.1007/978-3-030-94583-1_1 bibo_volume: 13182 dct_date: 2022^xs_gYear dct_isPartOf: - http://id.crossref.org/issn/03029743 - http://id.crossref.org/issn/16113349 - http://id.crossref.org/issn/9783030945824 dct_language: eng dct_publisher: Springer Nature@ dct_title: Flavors of sequential information flow@ ...