MONA Implementation Secrets

Research output: Contribution to book/anthology/report/proceedingArticle in proceedingsResearchpeer-review

  • Nils Klarlund, AT&T Labs - Research, United States
  • Anders Møller
  • Michael Ignatieff Schwartzbach, Denmark
  • Department of Computer Science
The Mona tool provides an implementation of the 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 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.
Original languageEnglish
Title of host publicationImplementation and Application of Automata : 5th International Conference, CIAA 2000 London, Ontario, Canada, July 24-25, 2000 Revised Papers
EditorsSheng Yu, Andrei Paun
Number of pages13
Publication year2001
ISBN (print)3-540-42491-1
Publication statusPublished - 2001
EventInternational Conference on Implementation and Application of Automata. CIAA '00 - London, ON, Canada
Duration: 24 Jul 200026 Jul 2000
Conference number: 5


ConferenceInternational Conference on Implementation and Application of Automata. CIAA '00
ByLondon, ON
SeriesLecture Notes in Computer Science

See relations at Aarhus University Citationformats

ID: 3742764