Skip to main content
SpringerLink
Log in

MONA Implementation Secrets

  • Conference paper
  • First Online:
Book cover Implementation and Application of Automata (CIAA 2000)

Part of the book series: Lecture Notes in Computer Science ((LNCS,volume 2088))

Included in the following conference series:

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.

This is a preview of subscription content, log in via an institution to check access.

Access this chapter

Log in via an institution
Chapter
USD 29.95
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
eBook
USD 39.99
Price excludes VAT (USA)
  • Available as PDF
  • Read on any device
  • Instant download
  • Own it forever
Softcover Book
USD 54.99
Price excludes VAT (USA)
  • Compact, lightweight edition
  • Dispatched in 3 to 5 business days
  • Free shipping worldwide - see info

Tax calculation will be finalised at checkout

Purchases are for personal use only

Institutional subscriptions

Preview

Unable to display preview. Download preview PDF.

Unable to display preview. Download preview PDF.

References

  1. Parosh Aziz Abdulla, Ahmed Bouajjani, Bengt Jonsson, and Marcus Nilsson. Handling global conditions in parameterized system verification. In Computer Aided Verification, CAV’ 99, volume 1633 of LNCS, 1999.

    Google Scholar 

  2. David Basin and Nils Klarlund. Hardware verification using monadic second-order logic. In Computer Aided Verification, CAV’ 95, volume 939 of LNCS, 1995.

    Google Scholar 

  3. David Basin and Nils Klarlund. Automata based symbolic reasoning in hardware verification. Formal Methods in Systems Design, 13(3):255–288, 1998.

    Article  Google Scholar 

  4. Morten Biehl, Nils Klarlund, and Theis Rauhe. Algorithms for guided tree automata. In WIA’ 96, volume 1260 of LNCS, 1996.

    Google Scholar 

  5. Jean-Paul Bodeveix and Mamoun Filali. FMona: a tool for expressing validation techniques over infinite state systems. In Tools and Algorithms for the Construction and Analysis of Systems, TACAS 2000, volume 1785 of LNCS, 2000.

    Chapter  Google Scholar 

  6. R.E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, Aug 1986.

    Article  Google Scholar 

  7. J.R. Büchi. Weak second-order arithmetic and finite automata. Z. Math. Logik Grundl. Math., 6:66–92, 1960.

    Article  MATH  Google Scholar 

  8. J.R. Büchi. On a decision method in restricted second-order arithmetic. In Proc. Internat. Cong. on Logic, Methodol., and Philos. of Sci. Stanford University Press, 1962.

    Google Scholar 

  9. K.M. Butler, D.E. Ross, R. Kapur, and M.R. Mercer. Heuristics to compute variable orderings for efficient manipulation of ordered binary decision diagrams. In Proc. ACM/IEEE Design Automation Conference (DAC), pages 417–420, 1991.

    Google Scholar 

  10. Niels Damgaard, Nils Klarlund, and Michael I. Schwartzbach. YakYak: Parsing with logical side constraints. In Proceedings of DLT’99, 1999.

    Google Scholar 

  11. Jacob Elgaard, Nils Klarlund, and Anders Møller. Mona 1.x: New techniques for WS1S and WS2S. In Computer Aided Verification, CAV’ 98, volume 1427 of LNCS, 1998.

    Chapter  Google Scholar 

  12. Jacob Elgaard, Anders Møller, and Michael I. Schwartzbach. Compile-time debugging of C programs working on trees. In Proceedings of European Symposium on Programming Languages and Systems, volume 1782 of LNCS, 2000.

    Google Scholar 

  13. C.C. Elgot. Decision problems of finite automata design and related arithmetics. Trans. Amer. Math. Soc., 98:21–52, 1961.

    Article  MathSciNet  Google Scholar 

  14. J.G. Henriksen, J. Jensen, M. Jørgensen, N. Klarlund, B. Paige, T. Rauhe, and A. Sandholm. Mona: Monadic second-order logic in practice. In Tools and Algorithms for the Construction and Analysis of Systems, First International Workshop, TACAS’ 95, volume 1019 of LNCS, 1996.

    Google Scholar 

  15. Thomas Hune and Anders Sandholm. A case study on using automata in control synthesis. In Proceedings of FASE’00, 2000.

    Google Scholar 

  16. J.L. Jensen, M.E. Jørgensen, N. Klarlund, and M.I. Schwartzbach. Automatic verification of pointer programs using monadic second-order logic. In SIGPLAN’ 97 Conference on Programming Language Design and Implementation,, pages 226–234, 1997.

    Google Scholar 

  17. N. Klarlund, M. Nielsen, and K. Sunesen. A case study in automated verification based on trace abstractions. In M. Broy, S. Merz, and K. Spies, editors, Formal System Specification, The RPC-Memory Specification Case Study, volume 1169 of LNCS, pages 341–374. Springer Verlag, 1996.

    Google Scholar 

  18. N. Klarlund and T. Rauhe. BDD algorithms and cache misses. Technical report, BRICS Report Series RS-96-5, Department of Computer Science, University of Aarhus, 1996.

    Google Scholar 

  19. Nils Klarlund. A theory of restrictions for logics and automata. In Computer Aided Verification, CAV’ 99, volume 1633 of LNCS, 1999.

    Chapter  Google Scholar 

  20. Nils Klarlund and Anders Møller. MONA Version 1.3 User Manual. BRICS Notes Series NS-98-3 (2.revision), Department of Computer Science, University of Aarhus, October 1998. URL: http://www.brics.dk/mona/manual.html.

  21. A.R. Meyer. Weak monadic second-order theory of successor is not elementary recursive. In R. Parikh, editor, Logic Colloquium, (Proc. Symposium on Logic, Boston, 1972), volume 453 of LNCS, pages 132–154, 1975.

    Google Scholar 

  22. Anders Møller. MONA homepage. URL: http://www.brics.dk/mona/.

  23. Frank Morawietz and Tom Cornell. The logic-automaton connection in linguistics. In Proceedings of LACL 1997, volume 1582 of LNAI, 1997.

    Google Scholar 

  24. Paritosh K. Pandya. DCVALID 1.2. Technical report, Theoretical Computer Science Group, Tata Institute of Fundamental Research, 1997.

    Google Scholar 

  25. Anders Sandholm and Michael I. Schwartzbach. Distributed safety controllers for web services. In FASE, volume 1382 of LNCS, 1998.

    Google Scholar 

  26. Thomas R. Shiple, James H. Kukula, and Rajeev K. Ranjan. A comparison of Presburger engines for EFSM reachability. In CAV, volume 1427 of LNCS, 1998.

    Google Scholar 

  27. Mark A. Smith and Nils Klarlund. Verification of a sliding window protocol using IOA and Mona, 1999. Submitted for publication.

    Google Scholar 

  28. W. Thomas. Automata on infinite objects. In J. van Leeuwen, editor, Handbook of Theoretical Computer Science, volume B, pages 133–191. MIT Press/Elsevier, 1990.

    Google Scholar 

  29. S. Yang. Logic synthesis and optimization benchmarks user guide version 3.0. In Tech. Rep. MCNC, 1991.

    Google Scholar 

Download references

Author information

Authors and Affiliations

  1. AT&T Labs-Research, USA

    Nils Klarlund

  2. BRICS, University of Aarhus, Aarhus

    Anders Møller & Michael I. Schwartzbach

Authors
  1. Nils Klarlund
    View author publications

    You can also search for this author in PubMed Google Scholar

  2. Anders Møller
    View author publications

    You can also search for this author in PubMed Google Scholar

  3. Michael I. Schwartzbach
    View author publications

    You can also search for this author in PubMed Google Scholar

Editor information

Editors and Affiliations

  1. Department of Computer Science, Middlesex College, The University of Western Ontario, London, ON, Canada, N6A 5B7

    Shen Yu  & Andrei Păun  & 

Rights and permissions

Reprints and permissions

Copyright information

© 2001 Springer-Verlag Berlin Heidelberg

About this paper

Cite this paper

Klarlund, N., Møller, A., Schwartzbach, M.I. (2001). MONA Implementation Secrets. In: Yu, S., Păun, A. (eds) Implementation and Application of Automata. CIAA 2000. Lecture Notes in Computer Science, vol 2088. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44674-5_15

Download citation

  • DOI: https://doi.org/10.1007/3-540-44674-5_15

  • Published:

  • Publisher Name: Springer, Berlin, Heidelberg

  • Print ISBN: 978-3-540-42491-8

  • Online ISBN: 978-3-540-44674-3

  • eBook Packages: Springer Book Archive

Publish with us

Policies and ethics

Search

Navigation