Mona: Monadic second-order logic in practice

  • Jesper G. Henriksen
  • Jakob Jensen
  • Michael Jørgensen
  • Nils KlarlundEmail author
  • Robert Paige
  • Theis Rauhe
  • Anders Sandholm
Conference paper
Part of the Lecture Notes in Computer Science book series (LNCS, volume 1019)


The purpose of this article is to introduce Monadic Second-order Logic as a practical means of specifying regularity. The logic is a highly succinct alternative to the use of regular expressions. We have built a tool MONA, which acts as a decision procedure and as a translator to finite-state automata. The tool is based on new algorithms for minimizing finite-state automata that use binary decision diagrams (BDDs) to represent transition functions in compressed form. A byproduct of this work is an algorithm that matches the time but improves the space of Sieling and Wegener's algorithm to reduce OBDDs in linear time.

The potential applications are numerous. We discuss text processing, Boolean circuits, and distributed systems. Our main example is an automatic proof of properties for the “Dining Philosophers with Encyclopedia” example by Kurshan and MacMillan. We establish these properties for the parameterized case without the use of induction.

Our results show that, contrary to common beliefs, high computational complexity may be a desired feature of a specification formalism.


Boolean Function Regular Expression Transition Relation Regular Language Decision Node 
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.


  1. [AHU74]
    A. Aho, J. Hopcroft, and J. Ullman. Design and Analysis of Computer Algorithms. Addison-Wesley, 1974.Google Scholar
  2. [BK95]
    D. Basin and N. Klarlund. Hardware verification using monadic second-order logic. Technical Report RS-96-7, BRICS, 1995. To appear in CAV '95 Proceedings.Google Scholar
  3. [Bry86]
    R.E. Bryant. Graph-based algorithms for boolean function manipulation. IEEE Transactions on Computers, C-35(8):677–691, Aug 1986.Google Scholar
  4. [Bry92]
    R. E. Bryant. Symbolic Boolean manipulation with ordered binary-decision diagrams. ACM Computing surveys, 24(3):293–318, September 1992.Google Scholar
  5. [BSV93]
    F. Balarin and A.L. Sangiovanni-Vincentelli. An iterative approach to language containment. In Computer Aided Verification, CAV '93, LNCS 697, pages 29–40, 1993.Google Scholar
  6. [CP94]
    J. Cai and R. Paige. Using multiset discrimination to solve language processing problems without hashing. to appear Theoretical Computer Science, 1994. also, U. of Copenhagen Tech. Report, DIKU-TR Num. D-209, 94/16, URL Scholar
  7. [CR94]
    M-M Corsini and A. Rauzy. Symbolic model checking and constraint logic programming: a cross-fertilisation. In 5th. Europ. Symp. on Programming, LNCS 788, pages 180–194, 1994.Google Scholar
  8. [GF93]
    A. Gupta and A.L. Fisher. Parametric circuit representation using inductive boolean functions. In Computer Aided Verification, CAV '93, LNCS 697, pages 15–28, 1993.Google Scholar
  9. [Hop71]
    J. Hopcroft. An n log n algorithm for minimizing states in a finite automaton. In Z. Kohavi and Paz A., editors, Theory of machines and computations, pages 189–196. Academic Press, 1971.Google Scholar
  10. [JJK94]
    J. Jensen, M. Jørgensen, and N. Klarlund. Monadic second-order logic for parameterized verification. Technical report, BRICS Report Series RS-94-10, Department of Computer Science, University of Aarhus, 1994.Google Scholar
  11. [KM89]
    B. Kurshan and K. McMillan. A structural induction theorem for processes. In Proc. Eigth Symp. Princ. of Distributed Computing, pages 239–247, 1989.Google Scholar
  12. [PT87]
    R. Paige and R. Tarjan. Three efficient algorithms based on partition refinement. SIAM Journal of Computing, 16(6), 1987.Google Scholar
  13. [Rev92]
    D. Revuz. Minimisation of acyclic deterministic automata in linear time. Theoretical Computer Science, 92(1):181–189, 1992.Google Scholar
  14. [RS93]
    J-K. Rho and F. Somenzi. Automatic generation of network invariants for the verification of iterative sequential systems. In Computer Aided Verification, CAV '93, LNCS 697, pages 123–137, 1993.Google Scholar
  15. [Ste93]
    M. Steinmann. Übersetzung von logischen Ausdrücken in Baumautomaten: Entwicklung eines Verfahrens und seine Implementierung. Unpublished, 1993.Google Scholar
  16. [SW93]
    D. Sieling and I. Wegener. Reduction of OBDDs in linear time. IPL, 48:139–144, 1993.Google Scholar
  17. [Tho90]
    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

Copyright information

© Springer-Verlag Berlin Heidelberg 1995

Authors and Affiliations

  • Jesper G. Henriksen
    • 1
  • Jakob Jensen
    • 1
  • Michael Jørgensen
    • 1
  • Nils Klarlund
    • 2
    Email author
  • Robert Paige
    • 2
  • Theis Rauhe
    • 1
  • Anders Sandholm
    • 1
  1. 1.BRICS, Centre of the Danish National Research Foundation for Basic Research in Computer Science, Department of Computer ScienceUniversity of AarhusGermany
  2. 2.BRICS, Department of Computer ScienceUniversity of AarhusAarhus

Personalised recommendations