MONA swMATH ID: 6170 Software Authors: Klarlund, Nils; Møller, Anders; Schwartzbach, Michael I.; Elgaard, J. Description: 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. Homepage: http://www.brics.dk/mona/ Keywords: monadic second-order logic; finite-state automata; MONA tool Related Software: DCVALID; z3; Isabelle/HOL; NuSMV; Uppaal; Rex; SIMPLIFY; SPIN; Isabelle; HyTech; LASH; FAST; Slide; PVS; Mosel; HIP; CESAR; Archive Formal Proofs; ESC/Java; Java-MOP Cited in: 139 Documents Further Publications: http://www.brics.dk/mona/publications.html Standard Articles 2 Publications describing the Software, including 2 Publications in zbMATH Year MONA implementation secrets. Zbl 1066.68079Klarlund, Nils; Møller, Anders; Schwartzbach, Michael I. 2002 MONA implementation secrets. Zbl 0989.03500Klarlund, Nils; Møller, Anders; Schwartzbach, Michael I. 2001 all top 5 Cited by 236 Authors 9 Vojnar, Tomáš 6 Klarlund, Nils 6 Kuncak, Viktor 5 Klaedtke, Felix 5 Lengál, Ondřej 5 Pandya, Paritosh K. 4 Basin, David A. 4 Bouajjani, Ahmed 4 Bultan, Tevfik 4 Esparza, Javier 4 Holík, Lukáš 4 Langer, Alexander 4 Rinard, Martin C. 4 Rossmanith, Peter 4 Sagiv, Mooly 4 Schwartzbach, Michael I. 4 Vardi, Moshe Ya’akov 3 Ayari, Abdelwaheb 3 Courcelle, Bruno 3 Møller, Anders Pape 3 Nguyen, Huu Hai 3 Veanes, Margus 3 Welzel, Christoph 2 Bartzis, Constantinos 2 Baukus, Kai 2 Bjørner, Nikolaj S. 2 Bollig, Benedikt 2 Bozga, Marius 2 Eisinger, Jochen 2 Feldman, Yotam M. Y. 2 Fiedor, Tomáš 2 Fioravanti, Fabio 2 Gottlob, Georg 2 Habermehl, Peter 2 Havelund, Klaus 2 Havlena, Vojtěch 2 Iosif, Radu 2 Kneis, Joachim 2 Lakhnech, Yassine 2 Löding, Christof 2 Meyer, Antoine 2 Padon, Oded 2 Peled, Doron A. 2 Pettorossi, Alberto 2 Pichler, Reinhard 2 Pnueli, Amir 2 Proietti, Maurizio 2 Raskin, Mikhail 2 Reidl, Felix 2 Shoham, Sharon 2 Sifakis, Joseph 2 Sikdar, Somnath 2 Stahl, Karsten 2 Tabajara, Lucas M. 2 Traytel, Dmitry 2 Unel, Gulay 2 Wakankar, Amol 2 Wies, Thomas 2 Yorsh, Greta 1 Abdulla, Parosh Aziz 1 Aiswarya, Cyriac 1 Alkhalaf, Muath 1 Arnborg, Stefan 1 Avni, Guy 1 Barrett, Clark W. 1 Barth, Stephan 1 Beldiceanu, Nicolas 1 Bensalem, Saddek 1 Berezin, Sergey 1 Berghammer, Rudolf 1 Berghofer, Stefan 1 Bès, Alexis 1 Biere, Armin 1 Bingham, Jesse D. 1 Bird, Steven 1 Bliem, Bernhard 1 Blume, Christoph 1 Bodeveix, Jean-Paul 1 Boigelot, Bernard 1 Bolander, Thomas 1 Bruggink, H. J. Sander 1 Carlsson, Mats 1 Cau, Antonio 1 Češka, Milan 1 Chakraborty, Supratik 1 Charlton, Nathaniel 1 Chatterjee, Siddhartha 1 Chaturvedi, Namit 1 Chin, Wei-Ngan 1 Chowdhury, Atish Datta 1 Cimatti, Alessandro 1 Cornell, Tom 1 Couvreur, Jean-Michel 1 Dahlberg, Axel 1 Damgaard, Niels 1 D’Antoni, Loris 1 David, Cristina 1 Dax, Christian 1 de Rijke, Maarten 1 Demassey, Sophie ...and 136 more Authors all top 5 Cited in 34 Serials 7 Theoretical Computer Science 6 Formal Methods in System Design 4 Information and Computation 4 Journal of Automated Reasoning 3 Formal Aspects of Computing 3 International Journal of Foundations of Computer Science 2 Information Processing Letters 2 Computer Science Review 2 Journal of Logical and Algebraic Methods in Programming 1 Acta Informatica 1 Artificial Intelligence 1 Discrete Applied Mathematics 1 International Journal of General Systems 1 Science of Computer Programming 1 Journal of Logic, Language and Information 1 Journal of Applied Non-Classical Logics 1 Mathematical Logic Quarterly (MLQ) 1 Journal of Functional Programming 1 Constraints 1 Theory of Computing Systems 1 Journal of the ACM 1 Bulletin of the European Association for Theoretical Computer Science EATCS 1 Higher-Order and Symbolic Computation 1 Fundamenta Informaticae 1 1 The Journal of Logic and Algebraic Programming 1 Computer Languages, Systems & Structures 1 Journal of Applied Logic 1 Discrete Optimization 1 Encyclopedia of Mathematics and Its Applications 1 Pure and Applied Mathematics (Amsterdam) 1 Logical Methods in Computer Science 1 ACM Transactions on Computation Theory 1 Philosophical Transactions of the Royal Society of London. A. Mathematical, Physical and Engineering Sciences all top 5 Cited in 10 Fields 133 Computer science (68-XX) 55 Mathematical logic and foundations (03-XX) 5 Game theory, economics, finance, and other social and behavioral sciences (91-XX) 4 Combinatorics (05-XX) 1 Order, lattices, ordered algebraic structures (06-XX) 1 Group theory and generalizations (20-XX) 1 Quantum theory (81-XX) 1 Operations research, mathematical programming (90-XX) 1 Systems theory; control (93-XX) 1 Information and communication theory, circuits (94-XX) Citations by Year