BRICS Notes Series, Abstracts, 2001

July 8, 2003

This document is also available as PostScript and DVI.

References

[NS-01-8] PostScript, PDF.

Anders Mller and Michael I. Schwartzbach. The XML Revolution (Revised). December 2001. 186 pp. This revised and extended report superseeds the earlier

BRICS Report NS-00-8. Abstract: This slide collection provides an overview of XML and

the essential related technologies: Namespaces, XInclude, XML Base, XLink, XPointer, XPath, DTD, XML Schema, DSD, XSLT, XQuery, DOM, SAX, and JDOM.

[NS-01-7] PDF.

Patrick Cousot, Lisbeth Fajstrup, Eric Goubault, Jeremy Gunawardena, Maurice Herlihy, Martin Rauen, and Vladimiro Sassone, editors.

Preliminary Proceedings of the Workshop on Geometry and Topology in Concurrency Theory, GETCO ’01, (Aalborg, Denmark, August 25, 2001), August 2001.

vi+97 pp. Abstract: This volume contains the preliminary proceedings of

GETCO ’01 held at the University of Aalborg on August 25, 2001, as a satellite workshop of CONCUR ’01.

[NS-01-6] PDF.

Luca Aceto and Prakash Panangaden, editors. Preliminary Proceedings of the 8th International Workshop on Ex-

pressiveness in Concurrency, EXPRESS ’01, (Aalborg, Denmark, August 20, 2001), August 2001.

vi+139 pp. Abstract: This volume contains the preliminary proceedings of EX-

PRESS ’01 held at the University of Aalborg on August 20, 2001, as a satellite workshop of CONCUR ’01. The final proceedings will appear as volume 52 number 1 in the ENTCS series, which can be accessed at www.elsevier.nl/locate/entcs/volume52.html.

[NS-01-5] PDF.

Flavio Corradini and Walter Vogler, editors.

Preliminary Proceedings of the 2nd International Workshop on Models for Time-Critical Systems, MTCS ’01, (Aalborg, Denmark, August 25, 2001), August 2001.

vi+ 127pp. Abstract: This volume contains the preliminary proceedings of

MTCS ’01 held at the University of Aalborg on August 25, 2001, as a satellite workshop of CONCUR ’01.

[NS-01-4] PDF.

Ed Brinksma and Jan Tretmans, editors. Proceedings of the Workshop on Formal Approaches to Testing of

Software, FATES ’01, (Aalborg, Denmark, August 25, 2001), August 2001.

viii+156 pp. Abstract: This volume contains the proceedings of FATES ’01 held

at the University of Aalborg on August 25, 2001, as a satellite workshop of CONCUR ’01.

[NS-01-3] Martin Hofmann, editor.

Proceedings of the 3rd International Workshop on Implicit Computational Complexity, ICC ’01, (Aarhus, Denmark, May 20–21, 2001), May 2001.

vi+144 pp. Abstract: This volume contains the proceedings of ICC’01, which

was held at the University of Aarhus on 20–21 May 2001.

[NS-01-2] PostScript, PDF.

Stephen Brookes and Michael Mislove, editors. Preliminary Proceedings of the 17th Annual Conference on Mathemat-

ical Foundations of Programming Semantics, MFPS ’01, (Aarhus, Denmark, May 24–27, 2001), May 2001.

viii+279 pp. Abstract: This volume contains the preliminary proceedings

of MFPS’01, which was held at the University of Aarhus on 24–27 May 2001. The final proceedings will appear as volume 45 in the ENTCS series, which can be found at www.elsevier.nl/locate/entcs/volume45.html.

[NS-01-1] PostScript, PDF.

Nils Klarlund and Anders Mller. MONA Version 1.4 — User Manual. January 2001. 83 pp. Abstract: 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.