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

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

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

Number of Access:528（2025-09-04 14:41 Counts）

Identifier to cite or link to this item: https://hdl.handle.net/11094/27427

Link to primary information 

File Format Terms of use Size Views Date.Available Description information
itr109_456_85 pdf None 649 KB 72 2014.04.11  

Item Information

Output File Export EndNote Basic Export Mendeley

Title
時間抽象を行う洗練手法を用いた確率時間システムの到達可能性解析
Reachability Analysis for Probabilistic Timed System based on Timed Abstraction Refinement Technique
ジカン　チュウショウ　ヲ　オコナウ　センレン　シュホウ　ヲ　モチイタ　カクリツ　ジカン　システム　ノ　トウタツ　カノウセイ　カイセキ
Creator
CreatorName
伊藤, 明彦 ; イトウ, アキヒコ ; Ito, Akihiko
CreatorName
長岡, 武志 ; ナガオカ, タケシ ; Nagaoka, Takeshi
NRID
1000070252632 1000070252632
CreatorName
岡野, 浩三 ; オカノ, コウゾウ ; Okano, Kozo
NRID
1000030234438 1000030234438
researchmap permalink
read0013799 read0013799
Scopus Author ID
7102741360 7102741360
CreatorName
楠本, 真二 ; クスモト, シンジ ; Kusumoto, Shinji
Subject
確立時間システム
モデル検査
CEGAR
シミュレーション
Teimed Probabilistic System
Model Checking
CEGAR
Simulation
Abstract
本稿では,確率時間オートマトンの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.
Publisher
電子情報通信学会
The Institute of Electronics, Information and Communication Engineers
デンシ　ジョウホウ　ツウシン　ガッカイ
Source Title
電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
Volume (Issue)
109(456)
Page
85-90
Date of Issued
2010-03-01
Language
Japanese
Handle URL
https://hdl.handle.net/11094/27427
PISSN
09135685
NCID
AN10013287
Access Rights
open access
CopyRight
Copyright © 2010 IEICE
本文データはCiNiiから複製したものである
oaire:version
Version of Record
Category
学術雑誌論文 Journal Article