|
MONA Implementation Secrets
Nils Klarlund
December 2000 |
Abstract:
The MONA tool provides an implementation of automaton-based
decision procedures for the logics WS1S and WS2S. It has been used for
numerous applications, and it is remarkably efficient in practice, even
though it faces a theoretically non-elementary worst-case complexity. The
implementation has matured over a period of six years. Compared to the first
naive version, the present tool is faster by several orders of magnitude.
This speedup is obtained from many different contributions working on all
levels of the compilation and execution of formulas. We present an overview
of MONA and a selection of implementation ``secrets'' that have been
discovered and tested over the years, including formula reductions,
DAGification, guided tree automata, three-valued logic, eager minimization,
BDD-based automata representations, and cache-conscious data structures. We
describe these techniques and quantify their respective effects by
experimenting with separate versions of the MONA tool that in turn omit each
of them
Available as PostScript, PDF. |