An Abstraction Refinement Technique for Timed Automata Based on Counterexample-Guided Abstraction Refinement Loop
-
- NAGAOKA Takeshi
- Graduate School of Information Science and Technology, Osaka University
-
- OKANO Kozo
- Graduate School of Information Science and Technology, Osaka University
-
- KUSUMOTO Shinji
- Graduate School of Information Science and Technology, Osaka University
この論文をさがす
抄録
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.
収録刊行物
-
- IEICE Transactions on Information and Systems
-
IEICE Transactions on Information and Systems E93-D (5), 994-1005, 2010
一般社団法人 電子情報通信学会
- Tweet
詳細情報 詳細情報について
-
- CRID
- 1390001204379849344
-
- NII論文ID
- 10026815323
-
- NII書誌ID
- AA10826272
-
- ISSN
- 17451361
- 09168532
-
- HANDLE
- 11094/27452
-
- 本文言語コード
- en
-
- データソース種別
-
- JaLC
- IRDB
- Crossref
- CiNii Articles
- KAKEN
-
- 抄録ライセンスフラグ
- 使用不可