MonaCo: Symbolic Coalgebraic Algorithms for
Weak Monadic Second-Order Logic of One Successor (WS1S)
CNRS - LIP, ENS Lyon (UMR 5668), France
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
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