1. Damien Pous
  2. monaco


MonaCo: Symbolic Coalgebraic Algorithms for
  Weak Monadic Second-Order Logic of One Successor (WS1S)

        Damien Pous
    CNRS - LIP, ENS Lyon (UMR 5668), France
        Dmitriy Traytel
    Department of Computer Science, ETH Zurich, Switzerland

This library is distributed under the terms of the GNU Lesser General
Public License version 3. See files LICENSE and COPYING.

Webpage of the project: http://perso.ens-lyon.fr/damien.pous/monaco

This OCaml library contains constructions for M2L/WS1S formulas, that
produce symbolic automata out of formulas, which can then be
checked for equivalence using the symbolic algorithms provided in the
SAFA library.

The automata construction uses a variant of Brzozowski derivatives
which is due to Dmitriy Traytel. These derivatives are computed
symbolically using BDDs, so that one can use the algorithms recently
proposed by Damien Pous.

 ocamlfind, safa (all available through opam)

You can compile a standalone program by typing [make].
Run [./monaco.native -help] to get a list of options and the syntax for
Typically [./monaco.native '\A x, \E Y, x\in Y' 'T'] will check whether
the two given expressions are equivalent.

Alternatively, you can build an OCaml library by typing [make lib], or
look at the makefile for other targets.

Here is a succinct description of each module:

ast		   : simple datatype for M2L/WS1S formulas
formula		   : normalised M2L/WS1S formulas,
                     symbolic Brzozowski derivatives

parse		   : parser for formulas

m2l		   : M2L automaton
ws1s		   : WS1S automaton

monaco		   : high-level interface of the library,
		     main entry point for standalone program

tests		   : a few sanity tests (not so much for now)
bench		   : a few benchmarks