パラメータ化マルチエージェントシステムのSMTベース安全性検証【JST・京大機械翻訳】

Felli Paolo; Gianola Alessandro; Montali Marco

プレプリント

J-GLOBAL ID：202202203225995403 整理番号：22P0180520

パラメータ化マルチエージェントシステムのSMTベース安全性検証【JST・京大機械翻訳】

SMT-based Safety Verification of Parameterised Multi-Agent Systems

出版者サイト {{ this.onShowPLink() }} 複写サービスで全文入手
高度な検索・分析はJDreamⅢで

この文献はプレプリントです。プレプリントについてはこちらをご確認ください。

著者 (3件)： , ,
資料名：
発行年： 2020年08月11日プレプリントサーバーでの情報更新日： 2020年08月14日
JST資料番号： O7000B 資料種別：プレプリント
記事区分：プレプリント発行国：アメリカ合衆国 (USA) 言語：英語 (EN)

本論文では,パラメータ化されたマルチエージェントシステム(MASs)の検証,特に,与えられた状態式として特徴付けられる不必要な状態が与えられたMAS,すなわちMASが不安全であるかどうかを検証するタスクについて,研究した。MASはパラメータ化され,モデルは可能なエージェントテンプレートの有限集合のみを記述し,一方,各テンプレートに対するコンクリートエージェントインスタンスの実際の数は無限であり,予測できない。これは状態空間無限を無限にする。コースの安全は,システムのエージェントインスタンスの数に依存するので,検証結果は,そのような数に関係なく正しくなければならない。アレイベースシステムの理論に依存する,充足可能性モジュロ理論(SMT)に基づく無限状態モデル検査によってこの問題を解決し,著者らは,並列とインタリーブと呼ぶMASのための2つの実行意味論の下で,特定のアレイベースシステムとしてパラメータ化したMASsを提示した。著者らは,これらの仮定の下で,著者らの可解性結果を証明して,SAFEと呼ぶ著者らの実装方式を例示した:第3のパーティーモデルチェッカーMCMTに基づくスウォーム安全検出器を,実験的に評価した。最後に,著者らは,このアプローチが,文献における最先端の解決策を超えて,より豊富なパラメータ化およびデータ意識MAS設定に,どのように,将来の研究として残されているかについて議論する。【JST・京大機械翻訳】

, , , , , , , , , , , ,
, , 【Automatic Indexing@JST】

計算機システム開発 , 人工知能

, , , ,

前のページに戻る