SPEAKER: Anders Møller, BRICS, Aarhus

DATE: Thursday, 27 May 1999

PLACE and TIME: Room E1-214 at 10:15.

ABSTRACT:

It has been known since 1960 that the class of regular languages is linked to decidability questions in formal logics. In particular, the logics WS1S and WS2S (Weak Second-order Logic of One or Two Successors) are decidable through the automaton-logic connection. Unfortunately, the decision problem has a non-elementary lower bound - a fact which for many years caused the decidability property to be considered intractable for practical use. MONA, which is developed at BRICS, is an implementation of this decision procedure. In spite of the discouraging worst-case complexity, the MONA tool has shown that there is a productive niche for these logics. It has been used in a variety of non-trivial settings, for instance in hardware verification, temporal property verification, assertional reasoning, and even computational linguistics. In this talk we will discuss the WS1S and WS2S logics, the automaton-logic connection, BDD representation of automata, and some recent extensions to MONA involving recursive types and symbolic reductions. During the last year, more than 100 have registered as users of the MONA tool. For more information about the project, visit the MONA Web Page.