論文の概要: SMT-based Safety Verification of Parameterised Multi-Agent Systems

• arxiv url: http://arxiv.org/abs/2008.04774v2
• Date: Fri, 14 Aug 2020 17:06:25 GMT
• ステータス: 処理完了
• システム内更新日: 2022-10-31 12:02:24.687462
• Title: SMT-based Safety Verification of Parameterised Multi-Agent Systems
• Title（参考訳）: パラメータ化マルチエージェントシステムのSMTによる安全性検証
• Authors: Paolo Felli and Alessandro Gianola and Marco Montali
• Abstract要約: パラメータ化マルチエージェントシステム(MAS)の検証について検討する。 特に、与えられた状態公式として特徴づけられる不要な状態が、所定のMASで到達可能かどうかについて検討する。
• 参考スコア（独自算出の注目度）: 78.04236259129524
• License: http://arxiv.org/licenses/nonexclusive-distrib/1.0/
• Abstract: In this paper we study the verification of parameterised multi-agent systems (MASs), and in particular the task of verifying whether unwanted states, characterised as a given state formula, are reachable in a given MAS, i.e., whether the MAS is unsafe. The MAS is parameterised and the model only describes the finite set of possible agent templates, while the actual number of concrete agent instances for each template is unbounded and cannot be foreseen. This makes the state-space infinite. As safety may of course depend on the number of agent instances in the system, the verification result must be correct irrespective of such number. We solve this problem via infinite-state model checking based on satisfiability modulo theories (SMT), relying on the theory of array-based systems: we present parameterised MASs as particular array-based systems, under two execution semantics for the MAS, which we call concurrent and interleaved. We prove our decidability results under these assumptions and illustrate our implementation approach, called SAFE: the Swarm Safety Detector, based on the third-party model checker MCMT, which we evaluate experimentally. Finally, we discuss how this approach lends itself to richer parameterised and data-aware MAS settings beyond the state-of-the-art solutions in the literature, which we leave as future work.
• Abstract（参考訳）: 本稿では,パラメータ化マルチエージェントシステム(MAS)の検証について検討し,特に,与えられた状態式として特徴付けられた不必要な状態が,所定のMAS,すなわち,MASが安全でないか否かの検証を行う。 MASはパラメータ化され、モデルは可能なエージェントテンプレートの有限セットのみを記述する。 これにより状態空間は無限になる。 安全性は当然、システム内のエージェントインスタンス数に依存するため、検証結果はそのような数に関係なく正しくなければならない。 我々は、配列ベースシステムの理論に依拠して、無限状態モデルチェック(smt)によってこの問題を解決する:我々は、並列およびインターリーブと呼ばれるmasの実行セマンティクスの下で、特定の配列ベースのシステムとしてパラメータ化された質量を示す。 我々は,これらの仮定に基づいて決定可能性の証明を行い,実験により評価した第三者モデルチェッカーMCMTに基づくSAFE: the Swarm Safety Detectorと呼ばれる実装手法について述べる。 最後に、本手法が文献における最先端のソリューションを超えて、よりリッチなパラメータ化とデータ対応のMAS設定にどのように貢献するかについて議論する。

関連論文リスト

• Data-Driven Distributionally Robust Safety Verification Using Barrier Certificates and Conditional Mean Embeddings [0.24578723416255752]
  問題を非現実的な仮定にシフトすることなく,スケーラブルな形式検証アルゴリズムを開発する。 問題を非現実的な仮定にシフトさせることなく,スケーラブルな形式検証アルゴリズムを開発するためには,バリア証明書の概念を用いる。 本稿では,2乗法最適化とガウス過程エンベロープを用いて効率よくプログラムを解く方法を示す。
  論文  参考訳（メタデータ） (2024-03-15T17:32:02Z)
• Scope Compliance Uncertainty Estimate [0.4262974002462632]
  SafeMLはそのような監視を行うためのモデルに依存しないアプローチである。 この研究は、二項決定を連続計量に変換することによってこれらの制限に対処する。
  論文  参考訳（メタデータ） (2023-12-17T19:44:20Z)
• 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)
• Probabilities Are Not Enough: Formal Controller Synthesis for Stochastic Dynamical Models with Epistemic Uncertainty [68.00748155945047]
  複雑な力学系のモデルにおける不確実性を捉えることは、安全なコントローラの設計に不可欠である。 いくつかのアプローチでは、安全と到達可能性に関する時間的仕様を満たすポリシーを形式的な抽象化を用いて合成する。 我々の貢献は、ノイズ、不確実なパラメータ、外乱を含む連続状態モデルに対する新しい抽象的制御法である。
  論文  参考訳（メタデータ） (2022-10-12T07:57:03Z)
• Relational Action Bases: Formalization, Effective Safety Verification, and Invariants (Extended Version) [67.99023219822564]
  我々はリレーショナルアクションベース(RAB)の一般的な枠組みを紹介する。 RABは両方の制限を解除することで既存のモデルを一般化する。 データ対応ビジネスプロセスのベンチマークにおいて、このアプローチの有効性を実証する。
  論文  参考訳（メタデータ） (2022-08-12T17:03:50Z)
• Adversarial Robustness Verification and Attack Synthesis in Stochastic Systems [8.833548357664606]
  我々は、離散時間マルコフ連鎖(DTMC)として定義されるシステムにおける対向的堅牢性のための公式な枠組みを開発する。 我々は、元の遷移確率の周囲に$varepsilon$ボールで制約された、敵がシステム遷移を摂動できる脅威モデルのクラスを概説する。
  論文  参考訳（メタデータ） (2021-10-05T15:52:47Z)
• SMT-Based Safety Verification of Data-Aware Processes under Ontologies (Extended Version) [71.12474112166767]
  我々は、このスペクトルで最も調査されたモデルの1つ、すなわち単純なアーティファクトシステム(SAS)の変種を紹介する。 このDLは適切なモデル理論特性を享受し、後方到達性を適用可能なSASを定義することができ、対応する安全問題のPSPACEにおける決定可能性をもたらす。
  論文  参考訳（メタデータ） (2021-08-27T15:04:11Z)

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

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