en | de

Model Checking

master program

VO2  SS 2008  703521

Tools

Implementation of the on-the-fly non-emptyness check for NBAs

Daniel Strigl has implemented the algorithm of Yannakakis & al. to check whether L(A) = ∅ for a given NBA A. It is implemented in C++ and produces nice LaTeX documents which illustrate the execution of the algorithm.

The tool is available under the Boost Software License which is also available from www.boost.org.

To input NBAs one has to encode the NBA directly into the source-file mcotf.cpp (examples are provided), then compile the program via make and run it. So, the overall procedure is as follows.