Hyperproperties express the relationship between multiple executions of a system. This is needed in many AI-related fields, such as knowledge representation and planning, to capture system properties related to knowledge, information flow, and privacy. In this paper, we study the monitoring of complex hyperproperties at runtime. Previous work in this area has either focused on the simpler problem of monitoring trace properties (which are sets of traces, while hyperproperties are sets of sets of traces) or on monitoring first-order hyperproperties, which are expressible in temporal logics with first-order quantification over traces, such as HyperLTL. We present the first monitoring algorithm for the much more expressive class of second-order hyperproperties. Second-order hyperproperties include system properties like common knowledge, which cannot be expressed in first-order logics like HyperLTL. We introduce Hyper$^2$LTL$_f$, a temporal logic over finite traces that allows for second-order quantification over sets of traces. We study the monitoring problem in two fundamental execution models: (1) the parallel model, where a fixed number of traces is monitored in parallel, and (2) the sequential model, where an unbounded number of traces is observed sequentially, one trace after the other. For the parallel model, we show that the monitoring of the second-order hyperproperties of Hyper$^2$LTL$_f$ can be reduced to monitoring first-order hyperproperties. For the sequential model, we present a monitoring algorithm that handles second-order quantification efficiently, exploiting optimizations based on the monotonicity of subformulas, graph-based storing of executions, and fixpoint hashing. We present experimental results from a range of benchmarks, including examples from common knowledge and planning.

翻译：超性质表达了系统多个执行轨迹之间的关系。这在许多与人工智能相关的领域（如知识表示与规划）中不可或缺，用于捕获与知识、信息流及隐私相关的系统性质。本文研究了运行时复杂超性质的监控问题。此前该领域的研究要么聚焦于更简单的轨迹性质监控问题（轨迹性质是轨迹的集合，而超性质是轨迹集合的集合），要么聚焦于一阶超性质的监控（一阶超性质可用包含一阶轨迹量化的时序逻辑如HyperLTL表达）。我们首次提出了针对表达能力更强的二阶超性质类的监控算法。二阶超性质包括诸如共同知识（common knowledge）等无法用HyperLTL等一阶逻辑表达的系统性质。我们引入Hyper$^2$LTL$_f$——一种基于有限轨迹且允许对轨迹集合进行二阶量化的时序逻辑。我们在两种基本执行模型中研究了监控问题：(1)并行模型——固定数量的轨迹被并行监控；(2)序列模型——无数量上限的轨迹被顺序观察（一条接一条）。对于并行模型，我们证明Hyper$^2$LTL$_f$的二阶超性质监控可归约为对一阶超性质的监控。对于序列模型，我们提出了一种能高效处理二阶量化的监控算法，利用子公式单调性优化、基于图的执行存储以及不动点哈希技术。我们给出了涵盖共同知识与规划实例等一系列基准测试的实验结果。