论文标题
K-Safety Hyperproperties的规范表示
Canonical Representations of k-Safety Hyperproperties
论文作者
论文摘要
HyperProperties将痕量属性的传统视图提升到痕迹集的痕迹集，并为表达信息流策略提供形式主义。对于痕量属性，用于验证，监视和合成的算法通常基于对欧米茄 - Automata属性的表示。对于超专制，到目前为止，类似的典型自动机理论表示。这是开发算法的严重障碍，因为无法应用基本结构（例如学习算法）。 在本文中，我们为广泛使用的常规K安全性超腐烂类别提供了一个规范表示，其中包括重要的策略，例如非干预。我们表明，常规的k安全性超植物可以由有限的自动机表示，在该自动机中，自动机接受的每个单词代表违反S。表示代表提供了一种自动机理论的方法来定期K-Savety Hyperproperties，并允许我们比较常规的K-Safety Hyperproperties，并简化它们，并了解它们，并学习此类超级专制。我们研究了通常的k-safety Hyperproperties和HyperLTL公式的自动机的问题，并为不同的翻译提供复杂性界限。我们还提出了一种基于确定性有限自动机的L*学习算法的常规K-Safety Hyproperties的学习算法。
Hyperproperties elevate the traditional view of trace properties form sets of traces to sets of sets of traces and provide a formalism for expressing information-flow policies. For trace properties, algorithms for verification, monitoring, and synthesis are typically based on a representation of the properties as omega-automata. For hyperproperties, a similar, canonical automata-theoretic representation is, so far, missing. This is a serious obstacle for the development of algorithms, because basic constructions, such as learning algorithms, cannot be applied. In this paper, we present a canonical representation for the widely used class of regular k-safety hyperproperties, which includes important polices such as noninterference. We show that a regular k-safety hyperproperty S can be represented by a finite automaton, where each word accepted by the automaton represents a violation of S. The representation provides an automata-theoretic approach to regular k-safety hyperproperties and allows us to compare regular k-safety hyperproperties, simplify them, and learn such hyperproperties. We investigate the problem of constructing automata for regular k-safety hyperproperties in general and from formulas in HyperLTL, and provide complexity bounds for the different translations. We also present a learning algorithm for regular k-safety hyperproperties based on the L* learning algorithm for deterministic finite automata.
