文献

J-GLOBAL ID：202202281774959039   整理番号：22A0980282

ハイブリッド状態空間表現に関するハイブリッドLTLのハイブリッド並列モデル検査【JST・京大機械翻訳】

Hybrid Parallel Model Checking of Hybrid LTL on Hybrid State Space Representation

著者 (5件)： Klai Kais (University of Sorbonne Paris Nord, LIPN, Villetaneuse, France) ,  Abid Chiheb Ameur (Faculty of Sciences of Tunis, University of Tunis El Manar, Tunis, Tunisia) ,  Abid Chiheb Ameur (Mediatron Lab, SupCom, University of Carthage, Tunis, Tunisia) ,  Arias Jaime (University of Sorbonne Paris Nord, LIPN, Villetaneuse, France) ,  Evangelista Sami (University of Sorbonne Paris Nord, LIPN, Villetaneuse, France)
資料名： Lecture Notes in Computer Science  (Lecture Notes in Computer Science)
巻： 13187  ページ： 27-42  発行年： 2022年 
JST資料番号： H0078D  ISSN： 0302-9743  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： 本論文では,共有および分散メモリアーキテクチャの両方に対するハイブリッド並列モデル検査アルゴリズムを提案した。モデル検査を,分散マルチコアマシンによるシステム状態空間の並列構築と同時に実行した。システムの状態空間の表現は,記号的観測グラフ(SOG)と呼ばれるハイブリッドグラフであり,そのノードの記号表現(単一状態のセット)とそのアークの明示的表現を結合した。SOGは,状態および事象ベースのLTL式(ハイブリッドLTL)の両方の保存を可能にするために適応され,すなわち,チェックすべき式に含まれる原子命題は,状態または事象ベースの命題である。C++プロトタイプ内の提案モデルチェッカーを実装し,予備結果をLTSminモデルチェッカーと比較した。Copyright Springer Nature Switzerland AG 2022 Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： アルゴリズム ,  システム ,  記憶構造 ,  命題 ,  C++言語 ,  *モデル検査 ,  プロトタイプ
準シソーラス用語： 状態空間 ,  線形時間論理 ,  記号表現 , 【Automatic Indexing@JST】

著者キーワード (4件)： 決定図 ,  線形時間論理 ,  モデル検査 ,  並列検証

分類 (2件)： システム・制御理論一般  (IA02010H) ,  人工知能  (JE08000Z)

タイトルに関連する用語 (3件)： 状態空間 ,  表現 ,  モデル検査