時相論理の充足可能性判定器のための論理式生成法

関澤 俊弦  高井 利憲  田辺 良則  高橋 孝一  

誌名
電子情報通信学会論文誌 D   Vol.J89-D   No.4   pp.642-650
発行日: 2006/04/01
Online ISSN: 1881-0225
Print ISSN: 1880-4535
論文種別: 特集論文 (フォーマルアプローチ論文特集)
専門分野: 計算モデル
キーワード: 
時相論理,  2方向CTL,  充足可能性判定,  論理式生成,  自動生成,  

本文: PDF(242.5KB)
>>論文を購入


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