このアイテムへのリンクには次のURLをご利用ください: https://hdl.handle.net/11094/27427

閲覧可能ファイル 

ファイル	フォーマット	サイズ	閲覧回数	利用開始日	説明
itr109_456_85	pdf	649 KB	30	2014.04.11

論文情報

タイトル	時間抽象を行う洗練手法を用いた確率時間システムの到達可能性解析
	Reachability Analysis for Probabilistic Timed System based on Timed Abstraction Refinement Technique
	ジカン　チュウショウ　ヲ　オコナウ　センレン　シュホウ　ヲ　モチイタ　カクリツ　ジカン　システム　ノ　トウタツ　カノウセイ　カイセキ
著者	著者名 伊藤, 明彦 イトウ, アキヒコ Ito, Akihiko
	著者名 長岡, 武志 ナガオカ, タケシ Nagaoka, Takeshi
	NRID 1000070252632 1000070252632 著者名 岡野, 浩三 オカノ, コウゾウ Okano, Kozo
	NRID 1000030234438 1000030234438 著者名 楠本, 真二 クスモト, シンジ Kusumoto, Shinji
キーワード等	確立時間システム
	モデル検査
	CEGAR
	シミュレーション
	Teimed Probabilistic System
	Model Checking
	CEGAR
	Simulation
抄録	本稿では,確率時間オートマトンのCEGARを用いた到達可能性解析を行う手法を提案する.確率時間システムでは,反例となるパスの組み合わせが各ロケーションにおける時間経過によって変動するため,単純に複数個のパスの探索では正しい反例を提示できない.本稿で提案する手法では,そのパスの組み合わせを決定するために,元モデルの等価変換を行うことで解決している.
	This paper gives a reachability analysis technique for Probabilistic Timed Automaton (PTA), based on CEGAR loop. The proposed method uses a transformation technique in order to avoid influence caused by dynamic change of behaviour with elapsing time.
出版者	電子情報通信学会
	The Institute of Electronics, Information and Communication Engineers
	デンシ　ジョウホウ　ツウシン　ガッカイ
収録物名	電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
巻	109
号	456
開始ページ	85
終了ページ	90
刊行年月	2010-03-01
言語	日本語
ハンドルURL	https://hdl.handle.net/11094/27427
ISSN	09135685
NCID	AN10013287
アクセス権	open access
権利情報	Copyright © 2010 IEICE
	本文データはCiNiiから複製したものである
出版タイプ	Version of Record
カテゴリ	学術雑誌論文 Journal Article

ホームへ戻る