MONA Implementation Secrets

Nils Klarlund; Anders Møller; Michael Ignatieff Schwartzbach

doi:10.1007/3-540-44674-5_4

MONA Implementation Secrets

Nils Klarlund, Anders Møller, Michael Ignatieff Schwartzbach

Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

22 Citations (Scopus)

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.

Original language	English
Title of host publication	Implementation and Application of Automata : 5th International Conference, CIAA 2000 London, Ontario, Canada, July 24-25, 2000 Revised Papers
Editors	Sheng Yu, Andrei Paun
Number of pages	13
Publisher	Springer
Publication date	2001
Pages	182-194
ISBN (Print)	3-540-42491-1
DOIs	https://doi.org/10.1007/3-540-44674-5_4
Publication status	Published - 2001
Event	International Conference on Implementation and Application of Automata. CIAA '00 - London, ON, Canada Duration: 24 Jul 2000 → 26 Jul 2000 Conference number: 5

Conference

Conference	International Conference on Implementation and Application of Automata. CIAA '00
Number	5
Country/Territory	Canada
City	London, ON
Period	24/07/2000 → 26/07/2000

Series	Lecture Notes in Computer Science
Volume	2088
ISSN	0302-9743

Access to Document

10.1007/3-540-44674-5_4

Cite this

@inproceedings{e40e8330c1fb11dbbee902004c4f4f50,

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.",

author = "Nils Klarlund and Anders M{\o}ller and Schwartzbach, {Michael Ignatieff}",

year = "2001",

doi = "10.1007/3-540-44674-5_4",

language = "English",

isbn = "3-540-42491-1",

series = "Lecture Notes in Computer Science",

publisher = "Springer",

pages = "182--194",

editor = "Sheng Yu and Andrei Paun",

booktitle = "Implementation and Application of Automata",

address = "Netherlands",

note = "International Conference on Implementation and Application of Automata. CIAA '00 ; Conference date: 24-07-2000 Through 26-07-2000",

}

Klarlund, N, Møller, A & Schwartzbach, MI 2001, MONA Implementation Secrets. in S Yu & A Paun (eds), Implementation and Application of Automata: 5th International Conference, CIAA 2000 London, Ontario, Canada, July 24-25, 2000 Revised Papers. Springer, Lecture Notes in Computer Science, vol. 2088, pp. 182-194, International Conference on Implementation and Application of Automata. CIAA '00, London, ON, Canada, 24/07/2000. https://doi.org/10.1007/3-540-44674-5_4

MONA Implementation Secrets. / Klarlund, Nils; Møller, Anders; Schwartzbach, Michael Ignatieff.
Implementation and Application of Automata: 5th International Conference, CIAA 2000 London, Ontario, Canada, July 24-25, 2000 Revised Papers. ed. / Sheng Yu; Andrei Paun. Springer, 2001. p. 182-194 (Lecture Notes in Computer Science, Vol. 2088).

Research output: Contribution to book/anthology/report/proceeding › Article in proceedings › Research › peer-review

TY - GEN

T1 - MONA Implementation Secrets

AU - Klarlund, Nils

AU - Møller, Anders

AU - Schwartzbach, Michael Ignatieff

N1 - Conference code: 5

PY - 2001

Y1 - 2001

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.

U2 - 10.1007/3-540-44674-5_4

DO - 10.1007/3-540-44674-5_4

M3 - Article in proceedings

SN - 3-540-42491-1

T3 - Lecture Notes in Computer Science

SP - 182

EP - 194

BT - Implementation and Application of Automata

A2 - Yu, Sheng

A2 - Paun, Andrei

PB - Springer

T2 - International Conference on Implementation and Application of Automata. CIAA '00

Y2 - 24 July 2000 through 26 July 2000

ER -

MONA Implementation Secrets

Abstract

Conference

Access to Document

Fingerprint

Cite this