時相論理の充足可能性判定器のための論理式生成法(計算モデル,<特集>フォーマルアプローチ論文)

スポンサーリンク

概要

論文の詳細を見る
時相論理などの充足可能性判定器の性能評価のためには,アルゴリズムの計算量的な解析だけでなく,具体的な論理式を用いたベンチマークが不可欠である.しかし,ベンチマークに用いる論理式セットの明確な基準はなく,また,新たな論理体系に対する充足可能性判定器の性能評価のためには,新たに論理式セットを構成しなければならない.本論文では,2方向CTLを例にとり,ベンチマーク用論理式の生成に向けた系統的な論理式の自動生成法を提案する.また,その準備として,論理式セットに求められる条件について検討する.最後に,提案手法に基づいて生成された論理式セットを用いた実験を行い,結果を述べる.
社団法人電子情報通信学会の論文
2006-04-01

著者

関連論文

もっと見る

スポンサーリンク