Monitoring Second-Order Hyperproperties

要約

ハイパープロパティは、システムの複数の実行間の関係を表します。
これは、知識、情報フロー、プライバシーに関連するシステム プロパティを取得するために、知識の表現や計画などの AI 関連の多くの分野で必要となります。
この論文では、実行時の複雑なハイパープロパティのモニタリングについて研究します。
この分野におけるこれまでの研究は、トレース プロパティ (トレースのセットであるのに対し、ハイパープロパティはトレースのセットのセットである) を監視するというより単純な問題、または 1 次の時相論理で表現可能な 1 次のハイパープロパティを監視することに焦点を当てていました。
HyperLTL などのトレース上の定量化。
我々は、二次ハイパープロパティのより表現力豊かなクラスに対する最初の監視アルゴリズムを提示します。
2 次ハイパープロパティには、HyperLTL のような 1 次ロジックでは表現できない、一般知識などのシステム プロパティが含まれます。
Hyper$^2$LTL$_f$ を導入します。これは、トレースのセットに対する 2 次定量化を可能にする、有限トレースに対する時相論理です。
私たちは 2 つの基本的な実行モデルでモニタリングの問題を研究します。(1) 固定数のトレースが並行して監視される並列モデル、および (2) 1 つのトレースの後に無制限の数のトレースが連続的に観察されるシーケンシャル モデル。
もう一方。
並列モデルの場合、Hyper$^2$LTL$_f$ の 2 次超特性の監視を 1 次超特性の監視に縮小できることを示します。
逐次モデルについては、部分式の単調性に基づく最適化、実行のグラフベースの保存、および固定点ハッシュを利用して、二次定量化を効率的に処理する監視アルゴリズムを提示します。
一般的な知識や計画からの例を含む、さまざまなベンチマークからの実験結果を示します。

要約(オリジナル)

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.

arxiv情報

提供元, 利用サービス

arxiv.jp, Google