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

伊藤, 明彦; 長岡, 武志; 岡野, 浩三 他

電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス, 2010, 109(456), 85-90

アクセス数:497件（2025-07-11 11:30 集計）

固定URL: https://hdl.handle.net/11094/27427

閲覧可能ファイル 

ファイル フォーマット 利用条件 サイズ 閲覧回数 利用開始日 説明 information
itr109_456_85 pdf なし 649 KB 70 2014.04.11  

論文情報

ファイル出力 EndNote Basic出力 Mendeley出力

タイトル
時間抽象を行う洗練手法を用いた確率時間システムの到達可能性解析
Reachability Analysis for Probabilistic Timed System based on Timed Abstraction Refinement Technique
ジカン　チュウショウ　ヲ　オコナウ　センレン　シュホウ　ヲ　モチイタ　カクリツ　ジカン　システム　ノ　トウタツ　カノウセイ　カイセキ
著者
著者名
伊藤, 明彦 ; イトウ, アキヒコ ; Ito, Akihiko
著者名
長岡, 武志 ; ナガオカ, タケシ ; Nagaoka, Takeshi
NRID
1000070252632 1000070252632
著者名
岡野, 浩三 ; オカノ, コウゾウ ; Okano, Kozo
NRID
1000030234438 1000030234438
researchmap permalink
read0013799 read0013799
Scopus Author ID
7102741360 7102741360
著者名
楠本, 真二 ; クスモト, シンジ ; 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
PISSN
09135685
NCID
AN10013287
アクセス権
open access
権利情報
Copyright © 2010 IEICE
本文データはCiNiiから複製したものである
出版タイプ
Version of Record
カテゴリ
学術雑誌論文 Journal Article