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 …