Name
Abstract | ||
|---|---|---|
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. |
Year | DOI | Venue |
|---|---|---|
2022 | 10.1007/978-3-030-94583-1_1 | VMCAI |
DocType | Citations | PageRank |
Conference | 0 | 0.34 |
References | Authors | |
0 | 5 | |
Name | Order | Citations | PageRank |
|---|---|---|---|
| Ezio Bartocci | 1 | 733 | 57.55 |
| Thomas Ferrère | 2 | 0 | 1.01 |
| Thomas A. Henzinger | 3 | 14827 | 1317.51 |
| Dejan Nickovic | 4 | 17 | 2.62 |
| Ana Oliveira da Costa | 5 | 1 | 1.08 |