論文の概要: Probabilistic Bisimulation for Parameterized Anonymity and Uniformity Verification
- arxiv url: http://arxiv.org/abs/2505.09963v1
- Date: Thu, 15 May 2025 04:56:53 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-05-16 22:29:06.185869
- Title: Probabilistic Bisimulation for Parameterized Anonymity and Uniformity Verification
- Title（参考訳）: パラメータ化された匿名性と一様性検証のための確率的ビシミュレーション
- Authors: Chih-Duo Hong, Anthony W. Lin, Philipp Rümmer, Rupak Majumdar,
- Abstract要約: ビシミュレーションは確率的システムにおけるプロセス等価性の検証に不可欠である。
本稿では,有限状態確率系の無限族におけるビシミュレーションを解析するための新しい枠組みを提案する。
匿名性や均一性のような本質的な性質は、このフレームワーク内でエンコードされ、検証可能であることを示す。
- 参考スコア（独自算出の注目度）: 5.806034991979994
- License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
- Abstract: Bisimulation is crucial for verifying process equivalence in probabilistic systems. This paper presents a novel logical framework for analyzing bisimulation in probabilistic parameterized systems, namely, infinite families of finite-state probabilistic systems. Our framework is built upon the first-order theory of regular structures, which provides a decidable logic for reasoning about these systems. We show that essential properties like anonymity and uniformity can be encoded and verified within this framework in a manner aligning with the principles of deductive software verification, where systems, properties, and proofs are expressed in a unified decidable logic. By integrating language inference techniques, we achieve full automation in synthesizing candidate bisimulation proofs for anonymity and uniformity. We demonstrate the efficacy of our approach by addressing several challenging examples, including cryptographic protocols and randomized algorithms that were previously beyond the reach of fully automated methods.
- Abstract（参考訳）: ビシミュレーションは確率的システムにおけるプロセス等価性の検証に不可欠である。
本稿では,有限状態確率系の無限族という,確率パラメータ化系におけるビシミュレーションを解析するための新しい論理的枠組みを提案する。
我々のフレームワークは正規構造の一階述語理論に基づいて構築されており、これらのシステムについて推論するための決定可能な論理を提供する。
匿名性や均一性といった本質的な性質は,システム,特性,証明が統一的な決定可能な論理で表現される演目的ソフトウェア検証の原則に則って,この枠組み内でコード化され,検証可能であることを示す。
言語推論技術を統合することにより、匿名性と均一性のための候補バイシミュレート証明を完全自動化する。
我々は,これまで完全に自動化された手法の範囲を超えていた暗号プロトコルやランダム化アルゴリズムなど,いくつかの挑戦的な事例に対処して,このアプローチの有効性を実証する。
関連論文リスト
- Probabilistic Numeric SMC Sampling for Bayesian Nonlinear System Identification in Continuous Time [0.0]
工学において、ノイズによって汚染されたデータから非線形力学系を正確にモデル化することは必須かつ複雑である。
連続時間常微分方程式(ODE)の統合は、理論モデルと離散サンプリングデータとの整合に不可欠である。
本稿では,非線形力学系の結合パラメータ-状態同定におけるODEの確率論的数値解法の適用例を示す。
論文 参考訳（メタデータ） (2024-04-19T14:52:14Z) - Formal Controller Synthesis for Markov Jump Linear Systems with
Uncertain Dynamics [64.72260320446158]
マルコフジャンプ線形系に対する制御器の合成法を提案する。
本手法は,MJLSの離散(モードジャンピング)と連続(確率線形)の両方の挙動を捉える有限状態抽象化に基づいている。
本手法を複数の現実的なベンチマーク問題,特に温度制御と航空機の配送問題に適用する。
論文 参考訳（メタデータ） (2022-12-01T17:36:30Z) - Logical Credal Networks [87.25387518070411]
本稿では,論理と確率を組み合わせた先行モデルの多くを一般化した表現的確率論的論理である論理的クレダルネットワークを紹介する。
本稿では,不確実性のあるマスターミンドゲームを解くこと,クレジットカード詐欺を検出することを含む,最大後部推論タスクの性能について検討する。
論文 参考訳（メタデータ） (2021-09-25T00:00:47Z) - Refining Labelled Systems for Modal and Constructive Logics with
Applications [0.0]
この論文は、モーダル論理や構成論理のセマンティクスを「経済的な」証明システムに変換する手段として機能する。
精製法は、ラベル付きおよびネストされたシーケント計算の2つの証明理論パラダイムを結合する。
導入された洗練されたラベル付き電卓は、デオン性STIT論理に対する最初の証明探索アルゴリズムを提供するために使用される。
論文 参考訳（メタデータ） (2021-07-30T08:27:15Z) - Tractable Inference in Credal Sentential Decision Diagrams [116.6516175350871]
確率感性決定図は、解離ゲートの入力が確率値によってアノテートされる論理回路である。
我々は、局所確率を質量関数のクレーダル集合に置き換えることができる確率の一般化である、クレーダル感性決定図を開発する。
まず,ノイズの多い7セグメント表示画像に基づく簡単なアプリケーションについて検討する。
論文 参考訳（メタデータ） (2020-08-19T16:04:34Z) - Verification of ML Systems via Reparameterization [6.482926592121413]
確率的プログラムを定理証明器で自動的に表現する方法を示す。
また、ベイズ仮説テストで用いられるヌルモデルは、人口統計学的パリティ(英語版)と呼ばれる公平性基準を満たすことを証明した。
論文 参考訳（メタデータ） (2020-07-14T02:19:25Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。