| 研究課題/領域番号 |
23300008
|
|---|
| 研究機関 | 名古屋大学 |
|---|
研究代表者 |
関 浩之 名古屋大学, 情報科学研究科, 教授 (80196948)
|
|---|
| 研究分担者 |
小川 瑞史 北陸先端科学技術大学院大学, 情報科学研究科, 教授 (40362024)
楫 勇一 奈良先端科学技術大学院大学, 情報科学研究科, 准教授 (70263431)
橋本 健二 名古屋大学, 情報科学研究科, 助教 (90548447)
|
|---|
| 研究期間 (年度) |
2011-04-01 – 2016-03-31
|
| キーワード | ソフトウェア検証 / 形式言語理論 / モデル検査 / XML / 情報保存性 / 木オートマトン / 木変換器 / 圧縮 |
|---|
| 研究実績の概要 |
(1)T1とT2を木変換器とする。ある部分関数fがあって、T2=f(T1)が成り立つとき、T1はT2を決定するという。また、T1がT2を保存しfがT2と同じ変換器のクラスに属するとき、T1はT2を包摂するという。本研究では、T1が単値線形拡張ボトムアップ木変換器、T2が単値ボトムアップ木変換器で与えられるとき、保存性、包摂性の双方がcoNEXPTIMEで決定可能であることを示した。
(2)拡張線形ボトムアップ木変換器の関数性判定が多項式時間判定可能であることを示した。
(3)関係データベースにおいてアクセス制御を前提とするセキュリティ尺度として、（問合せに基づく）l（エル）-多様性という概念を導入した。データベースインスタンスDがl-多様性を満たすとは、アクセス権限のある問合せとその結果に基づいてどのように推論を行っても、Dに含まれるセンシティブな情報（アクセス権限のない情報）の候補をl個未満に絞れないことをいう。l-多様性の判定法として、SQLを用いて定義に基づいて判定する手法と、Dを命題論理式に変換してモデル計数ソルバーを用いて判定する方法とを実装し、実データに基づいて比較を行った。
|
| 現在までの達成度 (段落) |
27年度が最終年度であるため、記入しない。
|
| 今後の研究の推進方策 |
27年度が最終年度であるため、記入しない。
|
