反例に基づく抽象化改良ループによる時間オートマトンの抽象化手法

長岡, 武志; 岡野, 浩三; 楠本, 真二

電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス, 2008, 107(505), 103-108

Number of Access:461（2025-09-01 10:11 Counts）

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

Link to primary information 

File Format Terms of use Size Views Date.Available Description information
itr107_505_103 pdf None 723 KB 85 2014.04.11  

Item Information

Output File Export EndNote Basic Export Mendeley

Title
反例に基づく抽象化改良ループによる時間オートマトンの抽象化手法
Abstraction of Timed Automata Based on Counterexample-Guided Abstraction Refinement Loop
ハンレイ　ニ　モトヅク　チュウショウカ　カイリョウ　ループ　ニ　ヨル　ジカン　オートマトン　ノ　チュウショウカ　シュホウ
Creator
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
Model Checking
Timed Automaton
Model Abstraction
Abstract
時間オートマトンを対象としたモデル抽象化手法を著者らは提案している.提案手法では,反例を元に抽象モデルを改良し,適切な抽象モデルを自動的に生成するCEGAR(CounterExample-Guided Abstraction Refinement)ループに基づく.抽象モデルの改良の際,元になる時間オートマトンの変形で行うなどの特徴を持つ.本稿では,提案手法の具体的なアルゴリズムを形式的に記述し,アルゴリズムの正当性の証明を与える.
We have proposed a method of model abstraction for timed automata. The proposed method is based on CEGAR (CounterExample-Guided Abstraction Refinement) loop which automatically refines an abstract model using counter examples. Our algorithm has some features such as refinements are performed indirectly through transformation of the original timed automation. This paper gives formal descriptions of the algorithm and the correctness proof of the algorithm.
Publisher
電子情報通信学会
The Institute of Electronics, Information and Communication Engineers
デンシ　ジョウホウ　ツウシン　ガッカイ
Source Title
電子情報通信学会技術研究報告. SS, ソフトウェアサイエンス
Volume (Issue)
107(505)
Page
103-108
Date of Issued
2008-02-25
Language
Japanese
Handle URL
https://hdl.handle.net/11094/27453
PISSN
09135685
NCID
AN10013287
Access Rights
open access
CopyRight
Copyright © 2008 IEICE
本文データはCiNiiから複製したものである
oaire:version
Version of Record
Category
学術雑誌論文 Journal Article