MONA Version 1.4 -- User Manual

This manual describes all features of MONA Version 1.4 through a number of examples. Both the classical decision procedure for the WS1S logic and the MONA approach is explained. Also the WS2S logic and the MONA concept of tree automata is presented.

Section 1 contains an introductory example and a brief description of MONA applications. In Section 2, the basic features of the MONA tool are described through a number of examples. Section 3 discusses the automaton-logic connection and the MONA compilation semantics. Section 4 describes DAGification, formula reduction, and separate compilation. In Section 5, it is shown how to make MONA produce detailed information about the processing and the resulting automata. Section 6 describes some more advanced constructs, such as, exporting and importing automata, controlling restrictions, and emulating Presburger arithmetic and M2L-Str. In Section 7, the decision procedure for WS2S is presented along with the MONA concept of Guided Tree Automata and an extension with recursive types. Section 8 discusses our plans for future work. In the appendices, the full syntax is defined, the command-line usage of MONA is shown, and the MONA DFA, GTA, and BDD packages are described.

This 80 page manual is a revised edition of the 1.3 manual updating the survey of applications and related work and adding documentation of the newly implemented features, recursive types for the tree-logic part and formula reductions. Furthermore, a large number of minor modifications and improvements have been made

Abstract: