MONA
MONA implementation secrets. 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.
Keywords for this software
References in zbMATH (referenced in 99 articles , 2 standard articles )
Showing results 1 to 20 of 99.
Sorted by year (- Unel, Gulay: Incremental reasoning on monadic second-order logics with logic programming (2016)
- Heinen, Jonathan; Jansen, Christina; Katoen, Joost-Pieter; Noll, Thomas: Juggrnaut: using graph grammars for abstracting unbounded heap structures (2015)
- Mesnard, Fred; Payet, Étienne: A second-order formulation of non-termination (2015)
- Veanes, Margus; Bjørner, Nikolaj: Symbolic tree automata (2015)
- Langer, Alexander; Reidl, Felix; Rossmanith, Peter; Sikdar, Somnath: Practical algorithms for MSO model-checking on tree-decomposable graphs (2014)
- Yu, Fang; Alkhalaf, Muath; Bultan, Tevfik; Ibarra, Oscar H.: Automata-based symbolic string analysis for vulnerability detection (2014)
- Zhou, Min; He, Fei; Wang, Bow-Yaw; Gu, Ming; Sun, Jiaguang: Array theory of bounded elements and its applications (2014)
- Bès, Alexis: Expansions of MSO by cardinality relations (2013)
- Bliem, Bernhard; Pichler, Reinhard; Woltran, Stefan: Declarative dynamic programming as an alternative realization of courcelle’s theorem (2013)
- Cau, Antonio; Janicke, Helge; Moszkowski, Ben: Verification and enforcement of access control policies (2013)
- Blume, Christoph; Bruggink, H.J.Sander; Engelke, Dominik; König, Barbara: Efficient symbolic implementation of graph automata with applications to invariant checking (2012)
- Chaturvedi, Namit; Chowdhury, Atish Datta; Meenakshi, B.: A framework for decentralized physical access control using finite state automata (2012)
- Chin, Wei-Ngan; David, Cristina; Nguyen, Huu Hai; Qin, Shengchao: Automated verification of shape, size and bag properties via user-defined predicates in separation logic (2012)
- Courcelle, Bruno; Durand, Irène: Automata for the verification of monadic second-order graph properties (2012)
- Courcelle, Bruno; Engelfriet, Joost: Graph structure and monadic second-order logic. A language-theoretic approach (2012)
- Emoto, Kento; Fischer, Sebastian; Hu, Zhenjiang: Filter-embedding semiring fusion for programming with MapReduce (2012)
- Kupferman, Orna: Recent challenges and ideas in temporal synthesis (2012)
- Lengál, Ondřej; Šimáček, Jiří; Vojnar, Tomáš: VATA: a library for efficient manipulation of non-deterministic tree automata (2012)
- Kneis, Joachim; Langer, Alexander; Rossmanith, Peter: Courcelle’s theorem -- a game-theoretic approach (2011)
- Veanes, Margus; Bjørner, Nikolaj: Foundations of finite symbolic tree transducers (2011)
Further publications can be found at: http://www.brics.dk/mona/publications.html