| 研究課題/領域番号 |
23300005
|
|---|
| 研究機関 | 北陸先端科学技術大学院大学 |
|---|
研究代表者 |
小川 瑞史 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (40362024)
|
|---|
| 研究分担者 |
廣川 直 北陸先端科学技術大学院大学, 情報科学研究科, 准教授 (50467122)
関 浩之 奈良先端科学技術大学院大学, 情報科学研究科, 教授 (80196948)
|
|---|
| 研究期間 (年度) |
2011-04-01 – 2015-03-31
|
| キーワード | ソフトウェア / 仕様記述 / 仕様検証 / 制約解消 / 数式処理 |
|---|
| 研究概要 |
1.実数多項式不等式の制約を解くSMTの設計・実装（北陸先端大・小川）、2.実数多項式制約の厳密解を与えるQE-CADアルゴリズムの持ち上げ段階への書換え手法の応用の検討（北陸先端大・廣川）、3.量的情報流解析への応用の検討（奈良先端大・関）を進めた。
1.は多項式制約を不等式に制限することで問題の大幅な簡単化となることを示し、raSATとして実装を行った。構成的数学の知見から不等式は決定可能だが、実数上の等式は決定不能であり、代数的数上でも高度な代数的計算が必要となる。また実数計算を有理数計算に還元でき、ツール実装上、深刻な問題となる浮動小数点演算の丸め誤差の影響を正確な有理数計算(Ocamlのnumライブラリ等)により排除できる。新たな区間演算法や戦略の導入により、raSAT の初期実装は SMT-LIBベンチマーク群の不等式問題で最新の SMT Z3 4.3 (Microsoft reseach)にせまる性能を示している。（国際ワークショップ TAPAS2012発表）現在、代数的手法以外の単純な手法の範囲でどこまで等式問題へ拡張可能か検討を進めている。
2.は、項書換え系の完備化手法のGroebner基底の計算への応用を検討したが、効率化のポイントが項書換え系とGroebner基底で異なることが判明し、再検討を進めている。今後、H25年度新規入学の修士課程学生（研究員雇用）による実装・実験を進める。
3.は、連続値となる量的情報流の前段階として、離散値の場合のXMLデータベースの質問処理における確定依存性の決定可能性について研究を進めた。木変換器T1,T2で表されるXML質問処理において T2がT1に確定依存とは、部分関数f が存在して、f・T1 = T2 となることをいう。線形上昇型木変換器では確定依存性が決定可能であることを示した。（国際会議 LATA2013発表）
|
| 現在までの達成度 (区分) |
現在までの達成度 (区分)
2: おおむね順調に進展している
理由
当初は、区間演算を用いる近似手法と数式処理QE-CADアルゴリズムとの融合を図る計画であったが、現在、近似的手法による多項式不等式処理、代数的手法（Groebner基底など）による多項式等式処理を組み合わせた、QE-CADアルゴリズムとは異なるアプローチによる実用的効率化の可能性が見えており、当初計画以上のインパクトの可能性を示している。
|
| 今後の研究の推進方策 |
当面は、（オーヴァー）近似区間演算を用いたSMTに（アンダー）近似としてのテスト手法を組合せ、相互に詳細化して、精度を得るアプローチを設計・実装を進め、さらに2013年のSMT competitionへの参加を目標とする。さらにツール自体の健全性を保証するために精度保証付数値計算の利用を検討する。
また量的情報流解析については、（連続値）情報流解析の実数多項式制約による定式化、さらに暗号アルゴリズムのサイドチャネル攻撃に対する耐性評価の応用の検討を進める。QE-CADアルゴリズムの効率化については、原点に戻り、anti-chain の手法の適用可能性を検討する。
|
