Open AccessMONA: Monadic Second-Order Logic in Practice
Author(s) -
Jesper G. Henriksen,
Ole J.L. Jensen,
Michael E. Jørgensen,
Nils Klarlund,
Robert Paige,
Theis Rauhe,
Anders B. Sandholm
Publication year - 1995
Publication title -
brics report series
Language(s) - English
Resource type - Journals
eISSN - 1601-5355
pISSN - 0909-0878
DOI - 10.7146/brics.v2i21.19923
Subject(s) - binary decision diagram , parameterized complexity , computer science , monadic predicate calculus , automaton , boolean function , theoretical computer science , finite state machine , formalism (music) , boolean circuit , algorithm , discrete mathematics , mathematics , higher order logic , description logic , art , musical , visual arts
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 a new bottom-up algorithm to reduce BDDs in linear time without hashing. 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.