Abstraction of Timed Automata Based on Counterexample-Guided Abstraction Refinement Loop

摘要

時間オートマトンを対象としたモデル抽象化手法を著者らは提案している．提案手法では，反例を元に抽象モデルを改良し，適切な抽象モデルを自動的に生成する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 automaton. This paper gives formal descriptions of the algorithm and the correctness proof of the algorithm.