Monitoring Second-Order Hyperproperties（二阶超性质监控）
Monitoring Second-Order Hyperproperties
AI总结：
本文针对现有超性质监控无法处理二阶性质的局限，提出支持二阶轨迹集合量化的Hyper$^2$LTL$_f$逻辑，分别给出并行模型下的规约方法和串行模型下的高效监控算法，并通过多基准实验验证有效性。
摘要：
超性质表达系统多个执行轨迹之间的关系，在知识表示、规划等众多AI相关领域中，是刻画与知识、信息流和隐私相关的系统性质所必需的。本文研究复杂超性质的运行时监控问题。该领域此前的研究要么聚焦于更简单的轨迹性质监控（轨迹性质是轨迹的集合，而超性质是轨迹集合的集合），要么聚焦于一阶超性质监控——这类性质可在支持轨迹一阶量化的时序逻辑（如HyperLTL）中表达。本文提出了首个针对表达能力强得多的二阶超性质类别的监控算法，二阶超性质包含公共知识等无法用HyperLTL等一阶逻辑表达的系统性质。\n本文引入了Hyper$^2$LTL$_f$，这是一种定义在有限轨迹上的时序逻辑，支持对轨迹集合进行二阶量化。研究在两种基础执行模型下展开监控问题：（1）并行模型，即固定数量的轨迹被并行监控；（2）串行模型，即无界数量的轨迹被一条接一条地串行观测。针对并行模型，本文证明Hyper$^2$LTL$_f$的二阶超性质监控可规约为一阶超性质监控。针对串行模型，本文提出了一种能高效处理二阶量化的监控算法，该算法利用了子公式单调性优化、基于图的执行存储以及不动点哈希技术。本文还展示了在多个基准测试上的实验结果，涵盖公共知识和规划领域的相关示例。
英文摘要：
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.
机构、总结、中文摘要均由AI分析而来，可能存在错误，请以论文正文为准。
