文章基本信息
- 标题：BDDを用いた2方向CTL論理式充足可能性決定手続きの実装
- 本地全文：下载
- 作者：田辺 良則 ; 高橋 孝一 ; 山本 光晴 等
- 期刊名称：コンピュータ ソフトウェア
- 印刷版ISSN：0289-6540
- 出版年度：2005
- 卷号：22
- 期号：3
- 页码：3_154-3_166
- DOI：10.11309/jssst.22.3_154
- 出版社：Japan Society for Software Science and Technology
- 摘要：
充足可能性の判定は，モデル検査等の抽象化手法において，重要な役割を果たしている．著者たちは，セルオートマトンなどの解析に用いられる，2 方向CTL 論理式の充足可能性決定手続きを考案した．本論文ではその正当性の証明を与え，実装を行う．素朴な実装では多量の空間と時間が必要になるが，BDD を用いることによって実用的な性能が得られることを示す．
