BDD-Based Decision Procedures for K
Guoqiang Pan, Ulrike Sattler, Moshe Y. Vardi · 2002
We describe BDD-based decision procedures for K. Our approach is inspired by the automata-theoretic approach, but we avoid explicit automata construction. Our algorithms compute the fixpoint of a set of types, which are sets of formulas satisfying some conststency conditions. We use BDDs to represent and manipulate such sets. Experimental results show that our algorithms are competitive with contemporary methods using benchmarks from TANCS 98 and TANCS 2000.