| Project: | BDD-based decision procedures |
| Contact: |
Moshe Y. Vardi Ullrike Sattler Guoqiang Pan |
| WWW page: | not available |
| Description: |
We investigate empirically methods of deciding satisfiability of
modal K formulas. These methods are based on deciding the emptyness
of automata, and they all use reduced ordereded binary decision
diagrams (BDDs for short).
The underlying idea is to construct for a formula f an automaton A that accepts exactly the model of f. Deciding the satisfiability of f is then reduced to decide the emptiness of the language accepted by A. A naive realization of this approach should behave badly in practice since its worst-case complexity coincides with its best-case complexity. However we use BDDs to represent the states of A, and the operations involved in testing A's emptiness are translated to operations on BDDs. Since BDDs have proven useful in similar problems, there is hope that the chosen approach behaves well in practice. |