MC3 — Modal Mu Calculus Model Checking Using Myopic Constraints

This is mc3 v0.1.0, a prototype implementation of a satisfiability-based modal mu calculus (MMC) model checking algorithm.

Organization

Directory	Contents
src	the prototype solver, written in Racket
examples	example problems
benchmarks	benchmark problems

Usage

Print some info about mc3’s command-line interface:

racket src/mc3.rkt --help

Run mc3 on one of the examples:

racket src/mc3.rkt examples/mmc-1.rkt

Compile the Racket code and run all the examples:

make all

Dependencies

N.B.: This project is developed on Linux, so these instructions may need to be adapted to other platforms.

Racket

The prototype solver is written in Racket; on Debian-like Linux distributions, run the following command:

apt install racket

Current development of mc3 uses Racket v8.0.

Racket Packages

Rosette

Rosette is used for its interface to SAT/SMT solvers. Current development of mc3 uses Rosette 4.0, installed from source.

git clone https://github.com/emina/rosette.git --branch 4.0
raco pkg install ./rosette

It includes a copy of the SMT solver Z3, which is what mc3 uses.

brag: a better Racket AST generator

brag is used to parse NuSMV models and Büchi automata encoded in the LBTT format.

raco pkg install brag

Racket Generic Graph Library

The graph library is used to analyze the structure of MMC formulas.

raco pkg install graph

The associated visualizations depend on Graphviz.

apt install graphviz

Optional

Spot: a platform for LTL and ω-automata manipulation

Spot’s ltl2tgba command-line tool is used to convert an LTL formula (or, more generally, a “path subformula” that appears in a CTL* formula) to a Büchi automaton as part of the translation from CTL* to MMC.

NuSMV

NuSMV is a reimplementation and extension of SMV, the first model checker based on BDDs. NuSMV has been designed to be an open architecture for model checking, which can be reliably used for the verification of industrial designs, as a core for custom verification tools, as a testbed for formal verification techniques, and applied to other research areas.

mc3 can parse and analyze a subset of NuSMV models (refer to src/parser/grammar/nusmv.rkt and src/parser/nusmv.rkt). Follow the links on NuSMV’s website to download a copy.

AIGER

AIGER is a format, library and set of utilities for And-Inverter Graphs (AIGs).

The AIGER tools can be downloaded from http://fmv.jku.at/aiger/aiger-1.9.9.tar.gz. Two of them in particular — aigtoaig and aigtosmv — are used for processing benchmark problems that are defined in the AIGER format (refer to src/parser/aiger.rkt and benchmarks/Makefile).