有限オートマトン学習による時間オートマトンの検証と合成

要旨 我々は、時間オートマトンのモデルチェックおよびコントローラ合成のためのアルゴリズムを提示します。時間オートマトンモデルを、大規模な有限状態機械と比較的小さな時間オートマトンの並列合成と見なし、この合成に対して構成的推論を使用します。我々は、自動機学習アルゴリズムを用いて、時間オートマトンコンポーネントの有限オートマトン近似を学習し、直面している問題を有限状態のモデルチェックまたは有限状態のコントローラ合成に還元します。我々のアプローチに関する実験評価も提示します。