効率の良いモデル空間探査のための抽象化

概要

論文の詳細を見る
インターネット上に分散して存在する複数のe-Learning教材から,学習者の現在の状況と最終目標に応じた妥当なコースの選択を行うことは,生涯学習支援システムにおいて重要な役割をもつ。ここで扱う問い合わせ処理は,分散データベースに対する時相論理を用いた検索処理として特徴付けることができる。本研究では,データベースに対する問い合わせ文として時相演算子を持つ論理式を用い,その解を得るための具体的な手続きとしてモデル検査技法を応用する。モデル検査技法は,近年急速に発達している分野であり,ハードウェアやネットワークプロトコルの検証に対して実用化されている。しかし,本研究の目標は通常のモデル検査ではなく,データベース問い合わせであり,応答時間や実行効率において強い制約が課せられる。特に,モデル検査において典型的に生じる状態数爆発を回避しない限り,実用システムの構築は不可能である。本論文では,複合プロセスのモデル空間を,効率良く探査するための抽象化と詳細化について議論する。
2005-09-30