Deductive Controller Synthesis for Probabilistic Hyperproperties

要約

確率的超特性は、異なる初期状態セットから異なるターゲット状態セットに到達する確率間の定量的関係を指定します。
このクラスの動作プロパティは、重要なセキュリティ、プライバシー、およびシステム レベルの要件を把握するのに適しています。
マルコフ決定プロセス (MDP) と確率的超特性のコントローラー合成問題を解決するための新しいアプローチを提案します。
私たちの仕様言語は、ロジック HyperPCTL の上に構築されており、合成されたコントローラーに対する構造上の制約によって強化されています。
私たちのアプローチは、シンボリックに表現され、MDP の同じコピー上で定義されたコントローラー ファミリから始まります。
次に、複数の計算ツリーを関連付けることができ、演繹的に検索空間を枝刈りするために採用する抽象化洗練戦略を導入します。
実験による評価は、提案されたアプローチが、HyperPCTL 用の最先端の SMT ベースのモデル チェック ツールである HyperProb よりも大幅に優れていることを示しています。
さらに、私たちのアプローチは、確率的ハイパープロパティを追加のコントローラー内制約 (部分可観測性など) およびコントローラー間の制約 (共通アクションに関する合意など) と効果的に組み合わせることができる最初のアプローチです。

要約(オリジナル)

Probabilistic hyperproperties specify quantitative relations between the probabilities of reaching different target sets of states from different initial sets of states. This class of behavioral properties is suitable for capturing important security, privacy, and system-level requirements. We propose a new approach to solve the controller synthesis problem for Markov decision processes (MDPs) and probabilistic hyperproperties. Our specification language builds on top of the logic HyperPCTL and enhances it with structural constraints over the synthesized controllers. Our approach starts from a family of controllers represented symbolically and defined over the same copy of an MDP. We then introduce an abstraction refinement strategy that can relate multiple computation trees and that we employ to prune the search space deductively. The experimental evaluation demonstrates that the proposed approach considerably outperforms HyperProb, a state-of-the-art SMT-based model checking tool for HyperPCTL. Moreover, our approach is the first one that is able to effectively combine probabilistic hyperproperties with additional intra-controller constraints (e.g. partial observability) as well as inter-controller constraints (e.g. agreements on a common action).

arxiv情報

提供元, 利用サービス

arxiv.jp, Google