文献

J-GLOBAL ID：201702288370649267   整理番号：17A1774645

合理的探索による検査正確な定量的確率モデル【Powered by NICT】

Exact quantitative probabilistic model checking through rational search

著者 (5件)： Bauer Matthew S. (University of Illinois at Urbana-Champaign) ,  Mathur Umang (University of Illinois at Urbana-Champaign) ,  Chadha Rohit (University of Missouri) ,  Sistla A. Prasad (University of Illinois at Chicago) ,  Viswanathan Mahesh (University of Illinois at Urbana-Champaign)
資料名： IEEE Conference Proceedings  (IEEE Conference Proceedings)
巻： 2017  号： FMCAD  ページ： 92-99  発行年： 2017年 
JST資料番号： W2441A  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： アメリカ合衆国 (USA)  言語： 英語 (EN)

抄録/ポイント： 離散時間Markov連鎖(DTMCs)とMarkov決定過程(MDP)のような確率モデルを用いた形式化システムのモデルチェッキングは,制約された計算到達可能性特性に減らすことができた。DTMCsとMDP(Markov決定過程)のための可到達性確率を計算するための線形計画法は,大規模モデルに対するスケーラビリティを持たない。,モデル検査ツールはしばしば近似可到達性確率への反復法を採用した。これらの近似は実際の確率から遠く離れた,不正確なモデル検査結果に導くことができる。本論文では,新しいアルゴリズムと厳密な可到達性確率を計算するための値反復のようなスケーラブル技術により得られた近似結果を改善することをその実装を提示した。Copyright 2017 The Institute of Electrical and Electronics Engineers, Inc. All Rights reserved. Translated from English into Japanese by JST【Powered by NICT】

シソーラス用語： 逐次近似 ,  線形計画法 ,  Markov連鎖 ,  *モデル ,  アルゴリズム ,  モデル検査 ,  *確率モデル ,  近似法
準シソーラス用語： Markov決定過程 , 【Automatic Indexing@JST】

分類 (2件)： 人工知能  (JE08000Z) ,  数理計画法  (KA03030M)

タイトルに関連する用語 (4件)： 探索 ,  検査 ,  定量 ,  確率モデル