MONA Implementation Secrets

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

Standard

MONA Implementation Secrets. / Klarlund, Nils; Møller, Anders; Schwartzbach, Michael Ignatieff.

In: International Journal of Foundations of Computer Science, Vol. 13, No. 4, 2002, p. 571-586.

Research output: Contribution to journal/Conference contribution in journal/Contribution to newspaperJournal articleResearchpeer-review

Harvard

Klarlund, N, Møller, A & Schwartzbach, MI 2002, 'MONA Implementation Secrets', International Journal of Foundations of Computer Science, vol. 13, no. 4, pp. 571-586. https://doi.org/10.1142/S012905410200128X

APA

Klarlund, N., Møller, A., & Schwartzbach, M. I. (2002). MONA Implementation Secrets. International Journal of Foundations of Computer Science, 13(4), 571-586. https://doi.org/10.1142/S012905410200128X

CBE

Klarlund N, Møller A, Schwartzbach MI. 2002. MONA Implementation Secrets. International Journal of Foundations of Computer Science. 13(4):571-586. https://doi.org/10.1142/S012905410200128X

MLA

Klarlund, Nils, Anders Møller and Michael Ignatieff Schwartzbach. "MONA Implementation Secrets". International Journal of Foundations of Computer Science. 2002, 13(4). 571-586. https://doi.org/10.1142/S012905410200128X

Vancouver

Klarlund N, Møller A, Schwartzbach MI. MONA Implementation Secrets. International Journal of Foundations of Computer Science. 2002;13(4):571-586. https://doi.org/10.1142/S012905410200128X

Author

Klarlund, Nils ; Møller, Anders ; Schwartzbach, Michael Ignatieff. / MONA Implementation Secrets. In: International Journal of Foundations of Computer Science. 2002 ; Vol. 13, No. 4. pp. 571-586.

Bibtex

@article{29ef4e70c1fc11dbbee902004c4f4f50,
title = "MONA Implementation Secrets",
abstract = "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.",
keywords = "Monadic second-order logic, finite-state automata, the MONA tool",
author = "Nils Klarlund and Anders M{\o}ller and Schwartzbach, {Michael Ignatieff}",
year = "2002",
doi = "10.1142/S012905410200128X",
language = "English",
volume = "13",
pages = "571--586",
journal = "International Journal of Foundations of Computer Science",
issn = "0129-0541",
publisher = "World Scientific Publishing Co. Pte. Ltd.",
number = "4",

}

RIS

TY - JOUR

T1 - MONA Implementation Secrets

AU - Klarlund, Nils

AU - Møller, Anders

AU - Schwartzbach, Michael Ignatieff

PY - 2002

Y1 - 2002

N2 - 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.

AB - 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.

KW - Monadic second-order logic

KW - finite-state automata

KW - the MONA tool

U2 - 10.1142/S012905410200128X

DO - 10.1142/S012905410200128X

M3 - Journal article

VL - 13

SP - 571

EP - 586

JO - International Journal of Foundations of Computer Science

JF - International Journal of Foundations of Computer Science

SN - 0129-0541

IS - 4

ER -