This is the download page for
MLSolver, a tool for solving the satisfiability and validity problems for modal fixpoint logics.
The underlying technique is based on characterisations of satisfiability through infinite (cyclic) tableaux in
which branches have an inner thread structure mirroring the regeneration of least and greatest fixpoint
constructs in the infinite. Well-foundedness for unfoldings of least fixpoints is checked using deterministic
parity automata. This reduces the satisfiability and validity problems to the problem of solving a parity
game. MLSolver then uses a parity game solver in order to decide satisfiability and derives example
models from the winning strategies in the parity game.
As a parity game solving backend,
MLSolver employs the parity game solver
PGSolver
that can be also obtained
here. Note that
the current version of
PGSolver is already included in the current distribution of
MLSolver,
hence there is no need to download both separately.
MLSolver is being developed and maintained at the
chair
for theoretical computer science of the
University of Munich, Germany.
The latest version is 1, released on January, 21st, 2010. No warranty can be given. Source code
can be downloaded below. It is distributed under the
BSD
license.
The program is written in
OCaml. You
will therefore need an OCaml compiler to produce the executables. We
recommend version ≥ 3.09, but smaller versions may also suffice.
- Version 1, released January, 21st, 2010
- new validity/satisfiability checker: CTL
- new model checker: CTL
- new feature: local solving
- new benchmark: dining philosophers
- Version 0, released September, 1st, 2009
- validity/satisfiability checker: CTL*, PDL, modal mu-calculus, linear-time mu-calculus
- model checker: CTL*, modal mu-calculus
Click on the download button below to obtain a tar.gz archive with
MLSolver's source
code.
If you want to be notified whenever a newer version is available please provide your details.
Otherwise leave the following fields blank.
For installation instructions see the included install.txt.