論文の概要: Deductive Controller Synthesis for Probabilistic Hyperproperties

• arxiv url: http://arxiv.org/abs/2307.04503v1
• Date: Mon, 10 Jul 2023 11:55:44 GMT
• ステータス: 処理完了
• システム内更新日: 2023-07-11 13:23:38.283590
• Title: Deductive Controller Synthesis for Probabilistic Hyperproperties
• Title（参考訳）: 確率的ハイパープロパタイトのための導出制御器合成
• Authors: Roman Andriushchenko, Ezio Bartocci, Milan Ceska, Francesco Pontiggia, and Sarah Sallinger
• Abstract要約: 本稿では,マルコフ決定過程(MDP)と確率的超越性(probabilistic hyperproperties)に対する制御器合成問題の解法を提案する。 我々のアプローチは、確率的超正則と追加の制御子内制約を効果的に組み合わせることのできる最初の手法である。
• 参考スコア（独自算出の注目度）: 0.31317409221921133
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: 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).
• Abstract（参考訳）: 確率的超越性は、異なる初期状態集合から異なる目標状態集合に到達する確率の間の定量的な関係を規定する。 このタイプの行動特性は、重要なセキュリティ、プライバシ、システムレベルの要求を捉えるのに適している。 本稿では,マルコフ決定過程(MDP)と確率的超越性に対する制御器合成問題の解法を提案する。 我々の仕様言語はHyperPCTLの論理の上に構築され、合成されたコントローラに対する構造的制約で拡張される。 私たちのアプローチは、MDPと同じコピー上でシンボル的に表現され定義されたコントローラのファミリーから始まります。 次に,複数の計算木を関連付ける抽象的洗練戦略を導入し,探索空間を推論的にpruneする手法を提案する。 実験評価の結果,提案手法がhyperpctlの最先端smtベースモデルチェックツールであるhyperprobをかなり上回っていることが示された。 さらに,確率的ハイパープロペラティと追加のコントローラ内制約(部分的可観測性など),コントローラ間制約(共通動作上の合意など)を効果的に組み合わせることができる最初のアプローチである。

関連論文リスト

• Provable Guarantees for Generative Behavior Cloning: Bridging Low-Level Stability and High-Level Behavior [51.60683890503293]
  生成モデルを用いた複雑な専門家による実演の行動クローニングに関する理論的枠組みを提案する。 任意の専門的軌跡の時間ごとのステップ分布に一致するトラジェクトリを生成することができることを示す。
  論文  参考訳（メタデータ） (2023-07-27T04:27:26Z)
• Optimal State Manipulation for a Two-Qubit System Driven by Coherent and Incoherent Controls [77.34726150561087]
  2量子ビット量子系の最適制御には状態準備が重要である。 物理的に異なる2つのコヒーレント制御を利用し、ヒルベルト・シュミット目標密度行列を最適化する。
  論文  参考訳（メタデータ） (2023-04-03T10:22:35Z)
• Robust Control for Dynamical Systems With Non-Gaussian Noise via Formal Abstractions [59.605246463200736]
  雑音分布の明示的な表現に依存しない新しい制御器合成法を提案する。 まず、連続制御系を有限状態モデルに抽象化し、離散状態間の確率的遷移によってノイズを捕捉する。 我々は最先端の検証技術を用いてマルコフ決定プロセスの間隔を保証し、これらの保証が元の制御システムに受け継がれるコントローラを演算する。
  論文  参考訳（メタデータ） (2023-01-04T10:40:30Z)
• Formal Controller Synthesis for Markov Jump Linear Systems with Uncertain Dynamics [64.72260320446158]
  マルコフジャンプ線形系に対する制御器の合成法を提案する。 本手法は,MJLSの離散(モードジャンピング)と連続(確率線形)の両方の挙動を捉える有限状態抽象化に基づいている。 本手法を複数の現実的なベンチマーク問題,特に温度制御と航空機の配送問題に適用する。
  論文  参考訳（メタデータ） (2022-12-01T17:36:30Z)
• Efficiently Controlling Multiple Risks with Pareto Testing [34.83506056862348]
  本稿では,多目的最適化と複数仮説テストを組み合わせた2段階プロセスを提案する。 自然言語処理(NLP)アプリケーションにおいて,大規模トランスフォーマーモデルの実行を確実に高速化する手法の有効性を実証する。
  論文  参考訳（メタデータ） (2022-10-14T15:54:39Z)
• Model predictive control for robust quantum state preparation [4.069849286089743]
  量子制御のためのモデル予測制御(MPC)を導入する。 MPCは、測定フィードバックを取り入れることで、自然の障害拒絶の程度を継承する。 実用的な最適化制御シーケンスを生成するために, MPC をどのように利用できるかを示す。
  論文  参考訳（メタデータ） (2022-01-14T00:55:41Z)
• Improving Hyperparameter Optimization by Planning Ahead [3.8673630752805432]
  本稿では,モデルに基づく強化学習の文脈内で定義された新しい伝達学習手法を提案する。 本稿では,シンプルなルックアヘッド戦略をポリシーとして用いたモデル予測制御法を提案する。 最新のHPOアルゴリズムと比較した3つのメタデータセット実験により,提案手法が全ベースラインを上回り得ることを示す。
  論文  参考訳（メタデータ） (2021-10-15T11:46:14Z)
• Sparsity in Partially Controllable Linear Systems [56.142264865866636]
  本研究では, 部分制御可能な線形力学系について, 基礎となる空間パターンを用いて検討する。 最適制御には無関係な状態変数を特徴付ける。
  論文  参考訳（メタデータ） (2021-10-12T16:41:47Z)
• Gaussian Process-based Min-norm Stabilizing Controller for Control-Affine Systems with Uncertain Input Effects and Dynamics [90.81186513537777]
  本稿では,この問題の制御・アフィン特性を捉えた新しい化合物カーネルを提案する。 この結果の最適化問題は凸であることを示し、ガウス過程に基づく制御リャプノフ関数第二次コーンプログラム(GP-CLF-SOCP)と呼ぶ。
  論文  参考訳（メタデータ） (2020-11-14T01:27:32Z)
• Heteroscedastic Bayesian Optimisation for Stochastic Model Predictive Control [23.180330602334223]
  モデル予測制御(MPC)は、複雑な物理システムの制御を含むアプリケーションで成功している。 制御器の動作のランダム性に起因した余分な課題を提示する,MPC のコンテキストにおける微調整 MPC 手法について検討する。
  論文  参考訳（メタデータ） (2020-10-01T05:31:41Z)
• Stochastic Finite State Control of POMDPs with LTL Specifications [14.163899014007647]
  部分的に観測可能なマルコフ決定プロセス(POMDP)は、不確実性の下での自律的な意思決定のためのモデリングフレームワークを提供する。 本稿では,POMDPに対する準最適有限状態制御器(sFSC)の合成に関する定量的問題について考察する。 本稿では,sFSC サイズが制御される有界ポリシアルゴリズムと,連続的な繰り返しにより制御器の性能が向上する任意の時間アルゴリズムを提案する。
  論文  参考訳（メタデータ） (2020-01-21T18:10:47Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。