文献

J-GLOBAL ID：201202200923948402   整理番号：12A0799067

確率時間CEGARの開発とその実証実験

Development and Experiments of Probabilistic Timed CEGAR

著者 (3件)： 清水隆也 (金沢大 大学院自然科学研究科) ,  森下篤 (金沢大 大学院自然科学研究科) ,  山根智 (金沢大 大学院自然科学研究科)
資料名： 情報処理学会論文誌トランザクション(CD-ROM)  (情報処理学会論文誌 Computer Vision and Applications(CD-ROM))
巻： 2011  号： 2  ページ： ROMBUNNO.PUROGURAMINGU,VOL.5,NO.2,43-66  発行年： 2012年04月15日 
JST資料番号： L7379A  ISSN： 1882-7772  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： 日本 (JPN)  言語： 日本語 (JA)

抄録/ポイント： 本論文では,確率時間オートマトンの到達可能性解析に述語抽象化と反例を用いた精錬の枠組み(CEGAR)を適用する手法を提案する。CEGARを用いることにより,組込システムのようなリアルタイム動作,確率動作を持つシステムに対する,効率的な自動検証が可能となる。(著者抄録)

シソーラス用語： 確率モデル ,  可到達性 ,  フレームワーク【ソフトウェア開発】 ,  システム ,  実時間処理 ,  *プログラム検証 ,  *確率オートマトン ,  実証実験 ,  組込みシステム
準シソーラス用語： *確率時間オートマトン ,  時間付きオートマトン

分類 (2件)： オートマトン理論  (JB04000O) ,  計算機システム開発  (JD02010R)

引用文献 (17件)：

• [1] Alur, R., Dang, T. and Ivancic, F.: Predicate abstrac-tion for reachability analysis of hybrid systems, TECS, Vol.5, No.1, pp.152-199 (2006).
• [2] Bengtsson, J. and Yi, W.: Timed Automata: Seman-tics, Algorithms and Tools, LNCS, Vol.3098, pp.87-124 (2004).
• [3] Bianco, A. and de Alfaro, L.: Model checking of proba-bilistic and nondeterministic systems, LNCS, Vol.1026, pp.499-513 (1995).
• [4] Bouyer, P.: Untameable Timed Automata!, LNCS, Vol.2607, pp.620-631 (2003).
• [5] Clarke, E.M., Grumberg,0. and Peled, D.: Model I Checking, MIT (2000).

タイトルに関連する用語 (3件)： 確率 ,  開発 ,  実証実験