论文标题
超句的层次结构
The Hierarchy of Hyperlogics
论文作者
论文摘要
通过与多个轨迹相关的超构物，在信息流安全性中广泛研究了跟踪属性。最近，已经提出了许多用于超专业的逻辑，并且有必要了解它们的可决定性和相对表现力。新逻辑是从具有两个主要扩展的标准逻辑中获得的：通过添加迹线或路径的变量，已将时间逻辑（如LTL和CTL $^*$）概括为超副词。一阶和二阶逻辑（如订单和MSO的Monadic一阶逻辑）已通过等级谓词扩展。我们研究了两种扩展在线性时间和分支时间逻辑范围内的影响，尤其是对术语进行量化的逻辑。超期的产生层次结构与经典的层次结构有显着不同，这表明相等级别的谓词比痕量和路径变量增加了表现力。在超时学的层次结构中，我们确定了有关可满足性问题的可决定性的新界限。具体而言，我们表明，尽管HyperQptl和HyperCtl $^*$一般都不确定，但其$ \ forall^*$ fragments的$ \ forall^*$ fragments中的公式是可决定的。
Hyperproperties, which generalize trace properties by relating multiple traces, are widely studied in information-flow security. Recently, a number of logics for hyperproperties have been proposed, and there is a need to understand their decidability and relative expressiveness. The new logics have been obtained from standard logics with two principal extensions: temporal logics, like LTL and CTL$^*$, have been generalized to hyperproperties by adding variables for traces or paths. First-order and second-order logics, like monadic first-order logic of order and MSO, have been extended with the equal-level predicate. We study the impact of the two extensions across the spectrum of linear-time and branching-time logics, in particular for logics with quantification over propositions. The resulting hierarchy of hyperlogics differs significantly from the classical hierarchy, suggesting that the equal-level predicate adds more expressiveness than trace and path variables. Within the hierarchy of hyperlogics, we identify new boundaries on the decidability of the satisfiability problem. Specifically, we show that while HyperQPTL and HyperCTL$^*$ are both undecidable in general, formulas within their $\exists^*\forall^*$ fragments are decidable.
