2021/05/05 by Ezio Bartocci, Bartocci, Ezio, Thomas Ferrère +7
Computer Science · #Distributed systems and fault tolerance #F.4.1 #FOS: Computer and information sciences #Formal Methods in Verification #Logic in Computer Science (cs.LO) #Security and Verification in Computing
paper · pdf · doi:10.48550/arxiv.2105.02013
openalex publication_date 2021/05/05 · openalex created_date 2025/10/10 · openalex updated_date 2026/07/28
Information-flow policies prescribe which information is available to a given user or subsystem. We study the problem of specifying such properties in reactive systems, which may require dynamic changes in information-flow restrictions between their states. We formalize several flavours of sequential information-flow, which cover different assumptions about the semantic relation between multiple observations of a system. Information-flow specification falls into the category of hyperproperties. We define different variants of sequential information-flow specification using a first-order logic with both trace quantifiers and temporal quantifiers called Hypertrace Logic. We prove that HyperLTL, equivalent to a subset of Hypertrace Logic with restricted quantifier prefixes, cannot specify the majority of the studied two-state independence variants. For our results, we introduce a notion of equivalence between sets of traces that cannot be distinguished by certain classes of formulas in Hypertrace Logic. This presents a new approach to proving inexpressiveness results for logics such as HyperLTL.