Abstract
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 consistency 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.
Cite
CITATION STYLE
Pan, G., Sattler, U., & Vardi, M. Y. (2002). BDD-based decision procedures for k. In Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) (Vol. 2392, pp. 16–30). Springer Verlag. https://doi.org/10.1007/3-540-45620-1_2
Register to see more suggestions
Mendeley helps you to discover research relevant for your work.
