文献

J-GLOBAL ID：201702243641165911   整理番号：17A1546229

反例誘導抽象化精密化を用いた大規模離散状態空間を持つ線形ハイブリッド系の検証【Powered by NICT】

Verification of linear hybrid systems with large discrete state spaces using counterexample-guided abstraction refinement

著者 (12件)： Althaus Ernst (Johannes Gutenberg-Universitaet Mainz, Staudinger Weg 9, 55128 Mainz, Germany) ,  Althaus Ernst (Max-Planck-Institut fuer Informatik, Campus E1.4, 66123 Saarbruecken, Germany) ,  Beber Bjorn (Johannes Gutenberg-Universitaet Mainz, Staudinger Weg 9, 55128 Mainz, Germany) ,  Beber Bjorn (Max-Planck-Institut fuer Informatik, Campus E1.4, 66123 Saarbruecken, Germany) ,  Damm Werner (Carl von Ossietzky Universitaet Oldenburg, Ammerlaender Heerstr. 114-118, 26111 Oldenburg, Germany) ,  Damm Werner (OFFIS e.V., Escherweg 2, 26121 Oldenburg, Germany) ,  Disch Stefan (Albert-Ludwigs-Universitaet Freiburg, Georges-Kohler-Allee 51, 79110 Freiburg, Germany) ,  Hagemann Willem (Carl von Ossietzky Universitaet Oldenburg, Ammerlaender Heerstr. 114-118, 26111 Oldenburg, Germany) ,  Rakow Astrid (Carl von Ossietzky Universitaet Oldenburg, Ammerlaender Heerstr. 114-118, 26111 Oldenburg, Germany) ,  Scholl Christoph (Albert-Ludwigs-Universitaet Freiburg, Georges-Kohler-Allee 51, 79110 Freiburg, Germany) ,  Waldmann Uwe (Max-Planck-Institut fuer Informatik, Campus E1.4, 66123 Saarbruecken, Germany) ,  Wirtz Boris (Carl von Ossietzky Universitaet Oldenburg, Ammerlaender Heerstr. 114-118, 26111 Oldenburg, Germany)
資料名： Science of Computer Programming  (Science of Computer Programming)
巻： 148  ページ： 123-160  発行年： 2017年 
JST資料番号： H0806A  ISSN： 0167-6423  CODEN： SCPGD4  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： オランダ (NLD)  言語： 英語 (EN)

抄録/ポイント： 大規模離散状態空間を持つ線形ハイブリッドオートマトンの安全特性の検証のための反例誘導抽象洗練(CEGAR)アプローチを提示し,コントローラ設計に健康状態モニタリングと分解レベルを取込んだ場合自然発生である。そのようなモデルは,純粋な機能コントローラモデルと対照的に,モードの明示的表現に依存するハイブリッド検証エンジンで分析できないが,状態空間の連続および離散部分の両方のための完全記号表現を必要とする。提示した引抜法は線形制約の任意の非凸組合せとLinAIGsを用いたブール変数の記号表現にした。いくつかの補間法は,より少ない線形制約の抽象化を計算することを可能にし,従って可到達状態集合計算の複雑さを減少させる。抽象化の正確さを保証する方法と組み合わせて,これは厳密な検証と比較検証プロセスの実行時間が大幅に削減される。Copyright 2017 Elsevier B.V., Amsterdam. All rights reserved. Translated from English into Japanese by JST.【Powered by NICT】

シソーラス用語： 計算量 ,  安全性 ,  *線形性 ,  *精密化 ,  凸形 ,  *ハイブリッド系 ,  モデリング ,  内挿法 ,  自然発生
準シソーラス用語： 実行時間 ,  健康状態 ,  制御設計 ,  ハイブリッドオートマトン ,  *状態空間 ,  *反例 , 【Automatic Indexing@JST】

著者キーワード (5件)： 検証 ,  線形ハイブリッドオートマトン ,  記号表現 ,  CEGAR ,  補間

分類 (3件)： オートマトン理論  (JB04000O) ,  システム設計・解析  (IA02030D) ,  計算理論  (JB02000A)

タイトルに関連する用語 (9件)： 反例 ,  誘導 ,  抽象化 ,  精密化 ,  大規模 ,  状態空間 ,  線形 ,  ハイブリッド系 ,  検証