タイトル

田辺良則,高橋孝一,山本光晴,佐藤貴洋,戸沢晶彦,萩谷昌己: BDDによる実装が可能な様相論理の充足可能性判定手続き

概要

様相μ計算に代表される各種様相論理の充足可能性判定問題は, 決定可能であることが知られていても, 効率的な実装は得られていないものが多い. 本研究では, 無交代様相μ計算や μLGF のフラグメントなど, いくつかの論理体系について, タブロー法を用いた判定が可能であることを示す. これらの体系が「交代性を有しない」ことが, タブロー法が適用できる本質的な条件である. また,タブロー法で扱うことになる膨大な論理式の集合を,BDDを用 いて表現する方法を提案する.これらによって,小さい時間・空間計算量によ る充足可能判定手続きの実装が可能となる.

ファイル

home