概要: 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. タグ: abstraction, refinement, technique, timed, automata, counterexample-guided, abstraction, refinement, loop

@article{TakeshiNagaoka2008b,
  author = {Takeshi Nagaoka and Kozo Okano and Shinji Kusumoto},
  title = {An Abstraction Refinement Technique for Timed Automata Based on Counterexample-Guided Abstraction Refinement Loop},
  journal = {Techinical Report of Software Design Lab in Osaka Univ. SDL-Sep-3-2008},
  year = {2008}
}