文献

J-GLOBAL ID：202002285936711864   整理番号：20A1034625

SMTソルバによるLyapunov関数の自動化と音声合成【JST・京大機械翻訳】

Automated and Sound Synthesis of Lyapunov Functions with SMT Solvers

著者 (4件)： Ahmed Daniele (Department of Computer Science, University of Oxford, Oxford, UK) ,  Ahmed Daniele (Amazon Inc, London, UK) ,  Peruffo Andrea (Department of Computer Science, University of Oxford, Oxford, UK) ,  Abate Alessandro (Department of Computer Science, University of Oxford, Oxford, UK)
資料名： Lecture Notes in Computer Science  (Lecture Notes in Computer Science)
巻： 12078  ページ： 97-114  発行年： 2020年 
JST資料番号： H0078D  ISSN： 0302-9743  資料種別： 会議録 (C)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： 本論文では,与えられた動的モデルの安定性を主張するLyapunov関数を健全に合成するために,SMTソルバーを用いた。Lyapunov関数に対する探索は,二次論理式の充足可能性としてフレーム化され,モデルのすべての可能な初期条件に対して,望ましい仕様(安定性)を満足する関数が存在するかどうかを求めた。線形,非線形(多項式)およびパラメトリックモデルに対するLyapunov関数を合成した。非線形モデルに対して,アルゴリズムはLyapunov関数に対する妥当性の領域を決定する。パラメトリックテンプレートから出発するLyapunov関数を合成するための帰納的枠組みを開発した。帰納的枠組みは2つの要素から成る:学習者はLyapunov関数を提案し,検証者はその妥当性をチェックする。その欠如は,学習者による更なる利用のために,反例(状態空間上の点)を介して表現される。この検証器はSMTソルバZ3を用いるが,この手順の全体的健全性を保証するため,学習者に対する2つの代替案を検討した。最適化ツールGurobiに基づく数値アプローチとZ3に基づく音響アプローチである。全体的な技術を広範囲のベンチマークにわたって評価し,この方法が合理的な計算時間内で10次元モデルにスケールするだけでなく,生成したLyapunov関数とその妥当性の領域に対する新しい健全性証明を提供することを示した。Copyright The Author(s) 2020 Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： アルゴリズム ,  *音声合成 ,  最適化 ,  多項式 ,  *自動化 ,  *Lyapunov関数 ,  音響 ,  ダイナミックモデル ,  線形性 ,  ベンチマーク ,  健全性
準シソーラス用語： 非線形モデル ,  *ソルバ ,  パラメトリックモデル ,  状態空間 , 【Automatic Indexing@JST】

著者キーワード (4件)： Lyapunov関数 ,  自動合成 ,  帰納的合成 ,  反例誘導合成

分類 (2件)： 計算機システム開発  (JD02010R) ,  計算理論  (JB02000A)

タイトルに関連する用語 (5件)： SMT ,  ソルバ ,  Lyapunov関数 ,  自動化 ,  音声合成