Detail of a work
T. Nagaoka, K. Okano, and S. Kusumoto, "An Abstraction Refinement Technique for Timed Automata Based on Counterexample-Guided Abstraction Refinement Loop," Techinical Report of Software Design Lab in Osaka Univ. SDL-Sep-3-2008, 2008.
ID 35
分類 Technical Report
タグ abstraction refinement technique timed automata counterexample-guided abstraction refinement loop
表題 (title) An Abstraction Refinement Technique for Timed Automata Based on Counterexample-Guided Abstraction Refinement Loop
表題 (英文)
著者名 (author) Takeshi Nagaoka,Kozo Okano,Shinji Kusumoto
英文著者名 (author) Takeshi Nagaoka,Kozo Okano,Shinji Kusumoto
キー (key) Takeshi Nagaoka,Kozo Okano,Shinji Kusumoto
号数 (number)
技術報告書の種別 (type)
発行元組織 (organization) Techinical Report of Software Design Lab in Osaka Univ. SDL-Sep-3-2008
出版社住所 (address)
刊行月 (month) 0
出版年 (year) 2008
URL
付加情報 (note)
注釈 (annote) Submitted to IEICE Transactions on Information and SyStems
内容梗概 (abstract) Model checking techniques are useful for design of high-reliable information systems. Well-known 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. The proposed technique is based on CEGAR, in which we use a counter example as a guide to refine the model abstracted excessively. Although, in general, the refinement operation is applied to abstract models, our method modifies the original timed automata, and next generates refined abstract models from the modified automata. This paper describes formal descriptions of the algorithm and the correctness proof of the algorithm.
論文電子ファイル 0 (application/pdf) [一般閲覧可]
BiBTeXエントリ 
@techreport{id35,
         title = {An Abstraction Refinement Technique for Timed Automata Based on Counterexample-Guided Abstraction Refinement Loop},
        author = {Takeshi Nagaoka and Kozo Okano and Shinji Kusumoto},
    institution = {Techinical Report of Software Design Lab in Osaka Univ. SDL-Sep-3-2008},
         month = {0},
          year = {2008},
        annote = {Submitted to IEICE Transactions on Information and SyStems},
}