時間抽象を行う洗練手法を用いた確率時間システムの到達可能性解析

伊藤, 明彦; 長岡, 武志; 岡野, 浩三; 楠本, 真二

このアイテムのアクセス数:60件（2020-09-22 02:00 集計）

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

閲覧可能ファイル

ファイル	フォーマット	サイズ	閲覧回数	説明
itr109_456_85	pdf	649 KB	23

論文情報

タイトル	時間抽象を行う洗練手法を用いた確率時間システムの到達可能性解析
別タイトル	Reachability Analysis for Probabilistic Timed System based on Timed Abstraction Refinement Technique
タイトル (ヨミ)	ジカン　チュウショウ　ヲ　オコナウ　センレン　シュホウ　ヲ　モチイタ　カクリツ　ジカン　システム　ノ　トウタツ　カノウセイ　カイセキ
著者	伊藤, 明彦伊藤, 明彦
	長岡, 武志長岡, 武志
	岡野, 浩三岡野, 浩三
	楠本, 真二楠本, 真二
著者の別表記	Ito, Akihiko
	Nagaoka, Takeshi
	Okano, Kozo
	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
ISSN	09135685
NCID	AN10013287
URL	http://hdl.handle.net/11094/27427
権利情報	Copyright © 2010 IEICE
権利情報	本文データはCiNiiから複製したものである
言語	日本語
カテゴリ	学術雑誌論文 Journal Article

著者版フラグ	publisher
NII資源タイプ	学術雑誌論文
ローカル資源タイプ	学術雑誌論文
dcmi資源タイプ	text
DCTERMS.bibliographicCitation	電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス.109(456) P.85-P.90
DC.title	時間抽象を行う洗練手法を用いた確率時間システムの到達可能性解析
DCTERMS.alternative	Reachability Analysis for Probabilistic Timed System based on Timed Abstraction Refinement Technique
DC.creator	伊藤, 明彦
	長岡, 武志
	岡野, 浩三
	楠本, 真二
DC.creator	Ito, Akihiko
	Nagaoka, Takeshi
	Okano, Kozo
	Kusumoto, Shinji
DC.publisher	電子情報通信学会
DC.language" scheme="DCTERMS.RFC1766	日本語
DCTERMS.issued" scheme="DCTERMS.W3CDTF	2010-03-01
DC.identifier" scheme="DCTERMS.URI	http://hdl.handle.net/11094/27427
DC.subject	確立時間システム
	モデル検査
	CEGAR
	シミュレーション
	Teimed Probabilistic System
	Model Checking
	CEGAR
	Simulation
DCTERMS.abstract	本稿では,確率時間オートマトンのCEGARを用いた到達可能性解析を行う手法を提案する.確率時間システムでは,反例となるパスの組み合わせが各ロケーションにおける時間経過によって変動するため,単純に複数個のパスの探索では正しい反例を提示できない.本稿で提案する手法では,そのパスの組み合わせを決定するために,元モデルの等価変換を行うことで解決している.
DCTERMS.abstract	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.
DC.rights	Copyright © 2010 IEICE
DC.rights	本文データはCiNiiから複製したものである
citation_title	時間抽象を行う洗練手法を用いた確率時間システムの到達可能性解析
citation_author	伊藤, 明彦
	長岡, 武志
	岡野, 浩三
	楠本, 真二
citation_publisher	電子情報通信学会
citation_language	日本語
citation_date	2010-03-01
citation_journal_title	電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
citation_volume	109
citation_issue	456
citation_firstpage	85
citation_lastpage	90
citation_issn	09135685
citation_public_url	http://hdl.handle.net/11094/27427
citation_keywords	確立時間システム
	モデル検査
	CEGAR
	シミュレーション
	Teimed Probabilistic System
	Model Checking
	CEGAR
	Simulation

閲覧可能ファイル

論文情報

論文詳細を表示