タイトル

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

概要

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

ファイル

home