タイトル
田辺良則，高橋孝一，山本光晴，佐藤貴洋，萩谷昌己:
BDDを用いた2方向CTL論理式充足可能性決定手続きの実装．
概要
充足可能性の判定は，モデル検査等の抽象化手法において，
重要な役割を果たしている．
著者たちは，セルオートマトンなどの解析に用いられる，
2方向CTL論理式の充足可能性決定手続きを考案した．
本論文ではその正当性の証明を与え，実装を行う．
素朴な実装では多量の空間と時間が必要になるが，
BDDを用いることによって実用的な性能が得られることを示す．
バージョン
ここは
産業技術総合研究所 (AIST)
のwebページの一部です。
このページの内容に関する電子メールでの連絡先: tanabe.yoshinoriアットマークaist.go.jp
田辺のページトップ