2013 Fiscal Year Annual Research Report
形式言語理論に基づく静的解析法とその安全性検査への応用
| Project/Area Number |
23300008
|
|---|
| Research Institution | Nagoya University |
|---|
Principal Investigator |
関 浩之 名古屋大学, 情報科学研究科, 教授 (80196948)
|
|---|
| Co-Investigator(Kenkyū-buntansha) |
小川 瑞史 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (40362024)
楫 勇一 奈良先端科学技術大学院大学, 情報科学研究科, 准教授 (70263431)
橋本 健二 名古屋大学, 情報科学研究科, 助教 (90548447)
|
|---|
| Project Period (FY) |
2011-04-01 – 2015-03-31
|
| Keywords | XML / 情報保存性 / 木変換器 / 頂点問合せ / 圧縮 / 木文法 / 木オートマトン |
|---|
| Outline of Annual Research Achievements |
木言語理論に基づく静的解析法に関する研究として以下の２つのテーマに取り組んだ．
一つ目のテーマとして，XMLデータベースにおける問合せ保存性に関する研究を行った．長期運用されるデータベースにおいては，その内容や構造が更新されても，更新前に取り出せた情報を更新後も取り出せる必要がある．変換Trが問合せQを保存するとは，ある問合せQ’ が存在して，任意のデータベースtに対して，Tr(t)に対するQ’の解集合がtに対するQの解集合と一致することをいう．XMLデータベースは階層構造をもち，木によって自然に表現できる．従来研究では，変換と問合せの双方が木変換器で与えられたときの問合せ保存性を議論しているが，ここでは，変換が木変換器，問合せが木オートマトンに基づく頂点問合せで与えられるときの問合せ保存性の判定可能性を考察した．
二つ目のテーマとして，木文法によって圧縮されたXML文書に対して，圧縮した状態で問合せや更新を行う手法を提案した．問合せは木オートマトンで与え，更新操作は置換，挿入，削除のいずれかとする．木文法による圧縮では，もとのXML文書に頻繁に現れる部分構造を一つにまとめるため，その部分構造を右辺とする生成規則を構成する．そこで本提案手法では，もとのXML文書に対して問合せを実行するのではなく，生成規則右辺に対して問合せを実行する．また，問合せ実行で得られた更新位置等の情報を保持し，文書内の同一部分構造に対する探索の重複を回避する．提案手法に基づいて問合せや更新を行うツールを試作した．DBLPやTreeBank（自然言語処理研究用コーパス）等の実用規模のXML文書をベンチマークとして実験を行った．その結果，本提案手法は，解凍・問合せ／更新・再圧縮という通常手法と比較して，実行時間，使用メモリ量とも，大幅に効率化できることが分かった．
|
| Current Status of Research Progress |
Current Status of Research Progress
2: Research has progressed on the whole more than it was originally planned.
Reason
一つ目のテーマについては，問合せがn-引数頂点問合せ，変換が値つき決定性線形トップダウン木変換器で与えられるとき，問合せ保存性の判定問題は，２重指数時間で解け，指数時間困難であること，もしnが定数のときは，指数時間完全であることを示した．また，関連して弱問合せ保存性という性質を定義し，それを判定する問題がcoNP完全であることを示した．
二つ目のテーマについては，Sebastianらが提案し実装しているTreeRepairと呼ばれる圧縮法を前提としている．TreeRepairではStraight Line Context-Free Tree Grammarと呼ばれる木文法を用いて，XML文書を圧縮する．本研究では，ボトムアップ木オートマトン(DBTA)に基づく頂点問合せ，または，トップダウン選択木オートマトン(DSTA)に基づく頂点問合せによって頂点位置を指定し，更新の場合は指定位置に対して置換，挿入，削除のいずれかを行う操作を前提とした．DBTA, DSTAのいずれにおいても，提案手法では，いったん解凍し問合せ・更新処理後，再圧縮を行う場合と比較して，約15％～0.1％の実行時間，約30%～0.1％のメモリ使用量で問合せ・更新を実行できることが分かった．
|
| Strategy for Future Research Activity |
問合せ保存性については，問合せクラスおよび変換のクラスを拡張した場合の，問合せ保存性の判定可能性について引き続き考察する．特に，重み付き木変換器で問合せを与える場合は，理論的な新規性の他に，機械翻訳等の応用も考えられる．
XML文書圧縮については，次のような展開を考えている．問合せとして前提としているDBTA, DSTAのいずれにおいても，一方向の木の走査しか行えない．そこで，その両方を組み合わせた問合せのクラス，例えば，DSTAで根頂点から下降して位置を決め，そこからDBTAを用いて子孫に関するパターンを照合する機能をもつクラスを設定し，そのようなクラスに対して今年度までの手法を拡張することを検討する．
|
Research Products
(3 results)
