文献

J-GLOBAL ID：202202232202790130   整理番号：22A0894224

Farkas補間体の分解における線形代数の利用【JST・京大機械翻訳】

Using linear algebra in decomposition of Farkas interpolants

著者 (5件)： Blicha Martin (Universita della Svizzera italiana (USI), Lugano, Switzerland) ,  Blicha Martin (Charles University, Faculty of Mathematics and Physics, Prague, Czech Republic) ,  Hyvaerinen Antti E. J. (Universita della Svizzera italiana (USI), Lugano, Switzerland) ,  Kofron Jan (Charles University, Faculty of Mathematics and Physics, Prague, Czech Republic) ,  Sharygina Natasha (Universita della Svizzera italiana (USI), Lugano, Switzerland)
資料名： International Journal on Software Tools for Technology Transfer  (International Journal on Software Tools for Technology Transfer)
巻： 24  号： 1  ページ： 111-125  発行年： 2022年 
JST資料番号： W1267A  ISSN： 1433-2779  資料種別： 逐次刊行物 (A)
記事区分： 原著論文  発行国： ドイツ (DEU)  言語： 英語 (EN)

抄録/ポイント： 実物上の線形不等式の命題論理とシステムの使用は,形式的検証のためのソフトウェアをモデル化するための一般的な方法である。Craig補間は,例えば帰納的ループ不変量の候補として,過剰近似到達可能状態に対して,この設定における中心構成ブロックを構成する。線形システムに対する補間は,Farkasの補助定理を適用することにより,単純X線から効率的に計算できる。しかし,これらの補間者は最悪の場合の検証タスクに必ずしも適合せず,それらは収束から検証アルゴリズムを防ぐことができる。本研究では,線形代数からの方法を用いて,補間構造から独立成分を同定および分離することによって得られるFarkas interpolantの基本的拡張である分解補間者を紹介した。また,分解補間者を計算し,その特性を分析するために,効率的な多項式アルゴリズムを提案した。著者らは,モデル検査における分解補間者の使用が,最先端のアプローチが発散する事例の即時収束をもたらすことを実験的に示した。さらに,効率的なシンプレックス法に基づいているので,この手法は,一般に非常に競争力がある。Copyright The Author(s) 2021 Translated from English into Japanese by JST.【JST・京大機械翻訳】

シソーラス用語： アルゴリズム ,  収束 ,  線形系 ,  不等式 ,  シンプレックス法 ,  *内挿法 ,  ループ ,  近似法 ,  *線形代数 ,  命題論理 ,  ソフトウェア ,  不変量 ,  モデル検査
準シソーラス用語： 形式的検証 ,  補題 , 【Automatic Indexing@JST】

著者キーワード (4件)： モデル検査 ,  充足可能性モジュロ理論 ,  線形実演算 ,  Craig内挿

分類 (2件)： 計算機システム開発  (JD02010R) ,  記号処理  (JE03000Q)

タイトルに関連する用語 (3件)： 補間 ,  分解 ,  線形代数