研究紹介

【重要】本研究室教授の関は2025年3月に定年退職します．

   学部生の卒業研究，大学院生（博士前期課程，後期課程）はいずれも受け入れていません．

【研究概要】本研究室では、形式言語理論の研究を行っています。その応用として、ソフトウェア自動検証・自動合成技術、構造化データの圧縮技術が挙げられます。

さて、研究では、なぜ問題がうまく解けたのか（もしくは、解けなかったのか）を客観的に理解することも重要です。理論に立脚した研究の面白さは、現実の問題解決で得た知見を基礎理論にフィードバックして、理論自体を発展させられることにあります。

本研究室は直近の課題だけでなく長期的な応用を見据えた研究に積極的に取り組んでゆきます。そのような研究が行えるために大切なことは、物事の見かけにまどわされず、見かけからその本質を抽象化する力だと思います。先入観にとらわれず、自由に考えることも重要です。シンプルで独創的な研究を行い、「あたかも誰かに発見されるのをその形で待っていたかのような」美しく、いろんなことに応用可能な結果を得たいと思っています。

前置きが長くなってしまいました。具体的なテーマを紹介します。

（１） データ値や重みを扱うオートマトンや形式文法

有限オートマトンや文脈自由文法（CFG）は、整数などのデータ値を直接扱えないため、現実のプログラムを直接表現することはできません。しかし、有限オートマトンやCFGにデータ値を扱える能力を加えるとすぐにチューリング機械と能力等価になってしまい、いろいろな処理の自動化が困難になります。

近年、大規模構造化データ処理の基本モデルとして、レジスタオートマトンが再注目されています。レジスタオートマトン（RA）は、有限オートマトンに、データ値を記憶するためのいくつかのレジスタを付加したモデルです。データ値に対しては比較演算のみが許され、そのことで計算能力が大きくなりすぎず、有限オートマトンのよい性質を受け継いでいます。

私達はこのような背景のもと、以下のような研究を行っています。

- RAをさらに抽象化した計算モデルとして、ノミナルオートマトン（NA）が知られています。NAでは、群作用による軌道が有限であるような（無限）集合に基づいて有限オートマトンを一般化することで、高い抽象度で議論を行うことができます。私たちはノミナル木オートマトンを定義して、正則言語の学習アルゴリズムや正則保存性に基づくモデル検査技法の開発を行っています。

- RAをXML文書（(3)でも説明します）問合せに利用しようとすると、いくつかの問題点があります。そこで、文脈自由文法 (CFG) にレジスタを付加したレジスタCFG (RCFG) に着目し、RCFGの諸性質を究明する理論的研究を行っています。現在まで、RCFGの所属問題、空問題はEXPTIME完全であり、ε-規則や単記号規則を禁止すると計算量が下がるなどの興味深い結果を得ています。

- CFGに重みを導入して拡張した計算モデルとして、重み付き文脈自由文法（MCFG）が知られています。重みは、確率、コストなど、計算の進行に付随して発生する定量的尺度を表現する概念であり、一般的には半環上の値として表現されます。通常のオートマトンや文法が言語を表現するのに対して、重み付きモデルは文字列から重みへの関数を定義します。 一方で、オートマトンや文法には曖昧さという概念があります。文字列の曖昧さとは、それを受理（文法の場合は生成）するオートマトンの実行の種類の数（文法の場合は導出木の数）を表します。オートマトンの場合、（重みのない）非決定性オートマトンを決定性オートマトンに等価変換できることはよく知られていますが、重み付きの場合、曖昧さによる関数の階層が存在することが知られています。CFGの場合、重みがなくても曖昧さによる言語階層が存在することが知られていました。本研究室では、WCFGにおいて重みに由来する曖昧さ階層が存在することを証明するなど、WCFGに関する理論的研究を行っています。

- 多重文脈自由文法(MCFG)という文法を提案しその諸性質を解明してきました。MCFGの生成能力は文脈自由文法(CFG) よりも大きく文脈規定文法(CSG) よりも小さいこと、多項式時間構文解析可能性や言語演算に対する閉包性など、CFG のよい性質を受け継いでいることがわかっています。本研究室では、MCFGに重みを導入したWMCFGを定義し、その諸性質を理論的に明らかにするための研究を行っています。これらの成果は理論的に興味深いとともに、(W)MCFGを生物系列解析に応用する際に重要な指針を与えます。

（２）ゲーム構造

ゲーム構造は、応用数学や経済学の分野で研究されてきましたが、近年、ソフトウェア自動合成、特にリアクティブプログラムの自動合成（リアクティブ合成と略す）と関連して、情報学においても盛んに研究がなされています。オートマトンでは状態遷移図を用いてその動作が定義されているのと同様に、ゲーム構造においても状態遷移図（ゲームアリーナと呼ばれる）によってその動作が定義されます。ただし、ゲーム構造では参加者が複数おり、それらが時には協調し時には争いながら動作する点がオートマトンと異なります。例えばリアクティブ合成への応用においては、プレイヤのうちの１人は自動生成しようとするプログラム、他のプレイヤは環境（例えば、他車の動作・温度・速度等のセンシングデータ）に対応します。ゲーム構造では、プレイヤが何人であるか（さらにプレイヤが制御できない自然手番があるか）、プレイヤの目的や効用はどのように定義されるか、最適戦略や均衡はどのように定義されるか、プレイヤの戦略に利用できる記憶は有限か、戦略に確率的動作を許すか等によって多くのバリエーションがあります。本研究室では現在、多プレイヤ・ω-正則目的・確率付き自然手番の存在するゲーム構造において、ナッシュ均衡に基づき、非協調的リアクティブ合成問題の可解性や計算量の解析に取り組んでいます。

（３）木言語理論とXML文書処理・変換への応用

現在、情報システム上のデータ交換には、XML (eXtensible Markup Language) に代表される構造化文書が用いられています。XMLはタグを使ってユーザが自由に文書内に階層構造を定義できる便利なマークアップ言語です。一方で、SQL等の関係データベースに比べて柔軟な構造をもつがゆえに、構造化文書処理には特有の問題があります。これから益々発展するクラウドサービスの効率的で安全な運用のためには、構造化文書に対する効率的な検索・問合せ処理、文書変換、文書圧縮の技術を開発しなければなりません。

　クラウドサービス等の効率的な運用のためには、データ圧縮が欠かせません。どのようなデータも記号列として圧縮できますが、その内容を知りたいときにはいったん解凍し内容を変更した場合は再圧縮しなければなりません。大規模データに対してそのような「迂回」をすることなく、圧縮したままで検索や更新ができれば望ましいと言えます。このような目的から本研究室では、木文法を用いて木構造を圧縮する技術（TreeRePair等）を利用し、XML文書を圧縮し、解凍せずに直接問合せを行う技術を開発してきました。