An Abstraction Refinement Technique for Timed Automata Based on Counterexample-Guided Abstraction Refinement Loop

Nagaoka, Takeshi; Okano, Kozo; Kusumoto, Shinji

IEICE TRANSACTIONS on Information and Systems, 2010, E93-D(5), 994-1005

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

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

Link to primary information 

File Format Terms of use Size Views Date.Available Description information
IEICE_E93-D_5_994 pdf None 1.54 MB 288 2014.04.11  

Item Information

Output File Export EndNote Basic Export Mendeley

Title
An Abstraction Refinement Technique for 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
model checking
timed automaton
model abstraction
CEGAR
Abstract
Model checking techniques are useful for design of high-reliable information systems. The well-known problem of state explosion, however, might occur in model checking of large systems. Such explosion severely limits the scalability of model checking. In order to avoid it, several abstraction techniques have been proposed. Some of them are based on CounterExample-Guided Abstraction Refinement (CEGAR) loop technique proposed by E. Clarke et al.. This paper proposes a concrete abstraction technique for timed automata used in model checking of real time systems. Our technique is based on CEGAR, in which we use a counter example as a guide to refine the abstract model. Although, in general, the refinement operation is applied to abstract models, our method modifies the original timed automaton. Next, we generate refined abstract models from the modified automaton. This paper describes formal descriptions of the algorithm and the correctness proof of the algorithm.
Publisher
電子情報通信学会
The Institute of Electronics, Information and Communication Engineers
デンシ　ジョウホウ　ツウシン　ガッカイ
Source Title
IEICE TRANSACTIONS on Information and Systems
Volume (Issue)
E93-D(5)
Page
994-1005
Date of Issued
2010-05-01
Language
English
Handle URL
https://hdl.handle.net/11094/27452
PISSN
09168532
NCID
AA10826272
Relation.references
URI
http://search.ieice.org/
Relation.isIdenticalTo
DOI (Publisher Version)
https://doi.org/10.1587/transinf.E93.D.994
Access Rights
open access
CopyRight
Copyright © 2010 The Institute of Electronics, Information and Communication Engineers
oaire:version
Version of Record
Category
学術雑誌論文 Journal Article