論文の概要: Synthesis of Safety Specifications for Probabilistic Systems

• arxiv url: http://arxiv.org/abs/2511.16579v1
• Date: Thu, 20 Nov 2025 17:34:56 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-11-21 17:08:52.763015
• Title: Synthesis of Safety Specifications for Probabilistic Systems
• Title（参考訳）: 確率システムの安全仕様の合成
• Authors: Gaspard Ohlmann, Edwin Hamel-De le Court, Francesco Belardinelli,
• Abstract要約: 我々は,安全PCTL仕様作成のための理論的枠組みを開発する。 グローバルな仕様満足度を局所的な制約に減らし、安全なPCTLの断片であるCPCTLを定義する方法について述べる。 より一般的な時間特性の合成問題を解くために,新しい値イテレーションに基づくアルゴリズムを提案する。
• 参考スコア（独自算出の注目度）: 11.125968799758434
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Ensuring that agents satisfy safety specifications can be crucial in safety-critical environments. While methods exist for controller synthesis with safe temporal specifications, most existing methods restrict safe temporal specifications to probabilistic-avoidance constraints. Formal methods typically offer more expressive ways to express safety in probabilistic systems, such as Probabilistic Computation Tree Logic (PCTL) formulas. Thus, in this paper, we develop a new approach that supports more general temporal properties expressed in PCTL. Our contribution is twofold. First, we develop a theoretical framework for the Synthesis of safe-PCTL specifications. We show how the reducing global specification satisfaction to local constraints, and define CPCTL, a fragment of safe-PCTL. We demonstrate how the expressiveness of CPCTL makes it a relevant fragment for the Synthesis Problem. Second, we leverage these results and propose a new Value Iteration-based algorithm to solve the synthesis problem for these more general temporal properties, and we prove the soundness and completeness of our method.
• Abstract（参考訳）: エージェントが安全仕様を満たすことを保証することは、安全クリティカルな環境において不可欠である。 制御系を安全な時間的仕様で合成する手法は存在するが、既存の手法のほとんどは、確率論的回避制約に安全な時間的仕様を制限している。 形式的手法は一般に確率的計算木論理(PCTL)のような確率的システムの安全性を表現するためのより表現力のある方法を提供する。 そこで本稿では,PCTLで表現されるより一般的な時間特性をサポートする新しい手法を提案する。 私たちの貢献は2倍です。 まず,安全なPCTL仕様作成のための理論的枠組みを開発する。 グローバルな仕様満足度を局所的な制約に減らし、安全なPCTLの断片であるCPCTLを定義する方法について述べる。 本稿では,CPCTLの表現性が合成問題にどのように関係するかを示す。 第二に、これらの結果を活用し、より一般的な時間的特性の合成問題を解くために、新しい値反復に基づくアルゴリズムを提案し、提案手法の健全性と完全性を証明する。

関連論文リスト

• Constrained and Robust Policy Synthesis with Satisfiability-Modulo-Probabilistic-Model-Checking [4.064849471241967]
  本稿では,任意の構造制約を受けるロバストポリシを効果的に計算するための最初のアプローチを提案する。 数百のベンチマークの実験は、制約付きかつ堅牢なポリシー合成の実現可能性を示している。
  論文  参考訳（メタデータ） (2025-11-11T10:28:42Z)
• Unlocking Symbol-Level Precoding Efficiency Through Tensor Equivariant Neural Network [84.22115118596741]
  シンボルレベルのプリコーディングにおいて,推論の複雑さの低いエンドツーエンドディープラーニング(DL)フレームワークを提案する。 提案手法は,従来の手法よりも約80倍の高速化を実現しつつ,SLPの大幅な性能向上を達成できることを示す。
  論文  参考訳（メタデータ） (2025-10-02T15:15:50Z)
• Advancing Neural Network Verification through Hierarchical Safety Abstract Interpretation [52.626086874715284]
  我々は、安全でない出力の階層構造を検証する抽象的DNN検証と呼ばれる新しい問題定式化を導入する。 出力到達可能な集合に関する抽象的解釈と推論を活用することにより,形式的検証プロセスにおいて,複数の安全性レベルを評価することができる。 我々の貢献には、新しい抽象的安全性の定式化と既存のアプローチとの関係を理論的に探求することが含まれる。
  論文  参考訳（メタデータ） (2025-05-08T13:29:46Z)
• Efficient Reactive Synthesis Using Mode Decomposition [0.0]
  そこで本研究では,モードに基づく新しい分解アルゴリズムを提案する。 我々のアルゴリズムへの入力は、元の仕様とモードの記述である。 サブ仕様の自動生成方法を示し、全てのサブプロブレムが実現可能であれば、完全な仕様が実現可能であることを示す。
  論文  参考訳（メタデータ） (2023-12-14T08:01:35Z)
• SCPO: Safe Reinforcement Learning with Safety Critic Policy Optimization [1.3597551064547502]
  本研究では,新しい安全強化学習アルゴリズム,セーフティ・クリティカル・ポリシー・オプティマイゼーションを導入する。 本研究では,安全制約に違反して得られる報酬を無効化する機構である安全評論家を定義した。 理論的解析により,提案アルゴリズムは安全制約への付着と報酬の最大化との間のトレードオフを自動的にバランスできることが示された。
  論文  参考訳（メタデータ） (2023-11-01T22:12:50Z)
• Probabilistic Constraint for Safety-Critical Reinforcement Learning [13.502008069967552]
  確率的制約付き強化学習(RL)における安全な政策学習の課題について考察する。 SPG-Actor-Critic は SPG-REINFORCE よりも低い分散をもたらす。 両SPGを利用して安全なポリシを学習できるSafe Primal-Dualアルゴリズムを提案する。
  論文  参考訳（メタデータ） (2023-06-29T19:41:56Z)
• Log Barriers for Safe Black-box Optimization with Application to Safe Reinforcement Learning [72.97229770329214]
  本稿では,学習時の安全性維持が不可欠である高次元非線形最適化問題に対する一般的なアプローチを提案する。 LBSGDと呼ばれるアプローチは、慎重に選択されたステップサイズで対数障壁近似を適用することに基づいている。 安全強化学習における政策課題の違反を最小限に抑えるためのアプローチの有効性を実証する。
  論文  参考訳（メタデータ） (2022-07-21T11:14:47Z)
• Pointwise Feasibility of Gaussian Process-based Safety-Critical Control under Model Uncertainty [77.18483084440182]
  制御バリア関数(CBF)と制御リアプノフ関数(CLF)は、制御システムの安全性と安定性をそれぞれ強化するための一般的なツールである。 本稿では, CBF と CLF を用いた安全クリティカルコントローラにおいて, モデル不確実性に対処するためのガウスプロセス(GP)に基づくアプローチを提案する。
  論文  参考訳（メタデータ） (2021-06-13T23:08:49Z)
• Cautious Reinforcement Learning with Logical Constraints [78.96597639789279]
  適応型安全なパッドディングは、学習プロセス中の安全性を確保しつつ、RL(Reinforcement Learning)に最適な制御ポリシーの合成を強制する。 理論的な保証は、合成されたポリシーの最適性と学習アルゴリズムの収束について利用できる。
  論文  参考訳（メタデータ） (2020-02-26T00:01:08Z)

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

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