| 研究課題/領域番号 |
14540121
|
|---|
| 研究機関 | 愛媛大学 |
|---|
研究代表者 |
大塚 寛 愛媛大学, 理学部, 助教授 (30203839)
|
|---|
| 研究分担者 |
土屋 卓也 愛媛大学, 理学部, 教授 (00163832)
石川 保志 愛媛大学, 理学部, 助教授 (70202976)
|
|---|
| キーワード | 協調型言語 / モデル検査 / 有限オートマトン / 正規表現 / 正規表現関数 / 文字列照合問題 |
|---|
| 研究概要 |
前年度までの研究では、制限された協調型言語で並列プロセスを記述し、タプル空間の状態遷移とプロセスの軌跡によるモデル検査を試みた。この状態遷移は有限状態機械(FSM)でモデル化され、また軌跡とは協調型言語の操作を文字とみなしたときの文字列である。この研究の結果、協調型言語とタプル空間を用いた並列プロセスに対し同時に全てのプロセスを検証の対象とするのではなく、いくつかのプロセスは検証済みとして特定のプロセスとタプル空間との並列動作を対象とすることを想定した。
今年度の研究では、上の想定の下でFSMを有限オートマトン(FA)およびそれと等価な正規表現、プロセスの軌跡を文字列とみなし、モデル検査のうち正規表現による文字列照合問題(RPM)に帰着できる問題を考察した。ただし並列プロセスを考察する場合に生じるFSMの"状態空間爆発問題"を避けるために、従来からあるFAによる文字列の受理問題によってRPMを解くのではなく、正規表現自身を使って解く解法を採用した。更に文字列が正規表現に照合することが確定した後の照合位置の特定、すなわち出現位置とその長さについても考察した。照合位置の特定をFAを用いて解く場合、決定性か非決定性かによって特定が困難であったり容易であったりする事を注意しておく。
具体的には文字列の左商に基づく正規表現関数を用い、RPMをキーワードによる文字列照合問題の一種の拡張とみなし、RPMのKnuth-Morris-Pratt型アルゴリズムによる解法を構築した。更に正規表現関数の性質を調べることで、照合位置の特定が可能であることがわかり、連接の形をした正規表現の場合ではあるが、そのアルゴリズムを構成した。前者のRPMの解法については研究集会「応用数学合同研究集会」で、後者の照合位置の特定については情報処理学会「第67回全国大会」で口頭報告した。
|
