1 0 0 0 OA 高階モデル検査の深化と発展
本課題では、高階モデル検査の(1)理論的基盤の強化とそれに基づく高階モデル検査アルゴリズムの改良、(2)プログラム検証への応用、(3)高階モデル検査の拡張とそのプログラム検証への応用、(4)データ圧縮への応用、の4つを柱に研究を進めている。以下、それぞれの項目について、平成28年度(およびその繰越として遂行した平成29年度の一部の結果)について述べる。(1)理論的基盤の強化:HORSモデル検査とHFLモデル検査という2種類の高階モデル検査の間に相互変換が存在することを示すとともに、HFLモデル検査問題を型推論問題に帰着できることを示した。後者の結果に基づき、HFLモデル検査器のプロトタイプを作成した。また、高階文法の性質について調べ、語を生成するオーダーnの文法と木文法を生成するオーダーn-1の文法と間の対応関係を示した。さらに、高階モデル検査アルゴリズムの改良を行い、値呼びプログラムに対して直接的に高階モデル検査を適用する手法を考案、実装した。(2)プログラム検証への応用:プログラム検証で扱える対象プログラムや性質の拡充を行い、関数型プログラムの公平非停止性の検証、コード生成プログラムの検証、動的なスレッド生成を伴う高階並列プログラムの検証、などを可能にした。(3)拡張高階モデル検査:HORSに再帰型を加えて拡張したμHORSに対するモデル検査アルゴリズムの改良を行い、その有効性をJavaプログラムの検証を通して示した。(4)データ圧縮への応用:データをそれを生成する関数型プログラムの形に圧縮する方式(高階圧縮)について、圧縮後のプログラムをビット列に変換する部分の改良を行った。また、高階圧縮のための様々な要素技術について研究を進めた。
1 0 0 0 一般化三並べの変種:負け型のペアは勝てるのか?
- 著者
- 八鍬 友貴 本田 耕一 篠原 歩
- 雑誌
- ゲームプログラミングワークショップ2009論文集
- 巻号頁・発行日
- vol.2009, no.12, pp.35-42, 2009-11-06
1 0 0 0 移調を許した圧縮文字列照合アルゴリズム
- 著者
- 松原 渉 篠原 歩
- 出版者
- 一般社団法人電子情報通信学会
- 雑誌
- 電子情報通信学会技術研究報告. COMP, コンピュテーション (ISSN:09135685)
- 巻号頁・発行日
- vol.110, no.12, pp.39-45, 2010-04-15
移調を許したマッチングとは,与えられたテキストとパタンに対して,任意のオフセットを許した移調パタンの出現を発見する問題であり,例として音楽検索が挙げられる.本研究では,移調を一般に文字の置き換え関数としてとらえ,任意の置換が与えられたとき,すべてのパタンを検出する問題について取り組む.入力のテキストとパタンは,文法圧縮の一種である直線的プログラム(SLP)で与えられるものとし,文字列を陽に展開することなく処理を完了する効率の良いアルゴリズムを与える.
1 0 0 0 平衡直線的プログラムで圧縮された文字列の非反復性検証アルゴリズム
- 著者
- 松原 渉 稲永 俊介 篠原 歩
- 出版者
- 一般社団法人電子情報通信学会
- 雑誌
- 電子情報通信学会技術研究報告. COMP, コンピュテーション (ISSN:09135685)
- 巻号頁・発行日
- vol.108, no.443, pp.9-16, 2009-02-23
平衡直線的プログラム(Balanced Straight line program,BSLP)は単元集合を生成する文脈自由文法とみなすことができ,そこで生成される文字列の長さNは,変数の個数nに対して指数的に長くなりうる.そのため,BSLPによって圧縮表現された文字列に対してnの多項式時間で効率よく処理を行うには,陽に展開することなく処理を行うことが必要不可欠となる.本研究では,BSLPとして表現された文字列の非反復性判定をO(max(n^2,nlog^2N))時間,O(n^2)領域で解くアルゴリズムを示す.
1 0 0 0 半導体歩留り解析へのデータマイニング適用手法の提案
- 著者
- 津田 英隆 白井 英大 寺邊 正大 橋本 和夫 篠原 歩
- 出版者
- 一般社団法人 電気学会
- 雑誌
- 電気学会論文誌D(産業応用部門誌) (ISSN:09136339)
- 巻号頁・発行日
- vol.129, no.12, pp.1201-1211, 2009-12-01 (Released:2009-12-01)
- 参考文献数
- 11
- 被引用文献数
- 4 5
The conventional semiconductor yield analysis is a hypothesis verification process, which heavily depends on engineers' knowledge. Data mining methodology, on the other hand, is a hypothesis discovery process that is free from this constraint. This paper proposes a data mining method for semiconductor yield analysis, which consists of the following two phases: discovering hypothetical failure causes by regression tree analysis and verifying the hypotheses by visualizing the measured data based on engineers' knowledge. It is shown, through experiment under the real environment, that the proposed method detects hypothetical failure causes, which were considered practically impossible to detect, and that yield improvement is achieved by taking preventive actions based on the detected failure causes.
1 0 0 0 OA 超高速圧縮データストリーム処理に基づく軽量XMLデータベース管理システム基盤技術
本研究では,圧縮データ処理に基づいて軽量XMLデータベース管理システム(DBMS)のための基盤技術を確立することを目標とし,主として以下の成果を得た.(1) 高速で軽量なオンライン文法圧縮アルゴリズムの開発. (2) 圧縮データ上で動作するq-グラム頻度計算アルゴリズムの開発. (3) 高速XMLデータストリームフィルタリング技術の開発. この他,DBMSの備えるべき知的データ処理機能として,パターンの効率的な枚挙,分類,オンライン予測等に関する研究を行い,多くの成果を得ている.
- 著者
- 稲永 俊介 船本 崇 竹田 正幸 篠原 歩
- 出版者
- 一般社団法人電子情報通信学会
- 雑誌
- 電子情報通信学会技術研究報告. COMP, コンピュテーション (ISSN:09135685)
- 巻号頁・発行日
- vol.103, no.622, pp.29-36, 2004-01-22
文字列の文法に基づく圧縮とは,与えられたテキストを生成する文法を構築することによってデータのサイズを縮小する圧縮法である.この中で長さ優先置換法とは,テキスト中の部分文字列のうち,重複なく複数回現れている最長のものを生成規則として別の一文字に置換していくものである.本論文では,文字列に対する索引構造の一つである接尾辞木に対して極めて技巧的な構造の更新を行うことにより,この長さ優先置換を線形時間で行うアルゴリズムを提案する.