Alfred - Model Checker

(Read further only if you are a theoretical computer scientist.) I have implemented model checker Alfred as part of my master thesis. The model checker decides the validity of formulas of alternation free modal mu-calculus for push down systems, and push down automata. The model checker implements the algorithm described in article Reachability Analysis of Pushdown Automata: Application to Model-Checking. Modal Mu-calculus is a temporal logic with fixed point operators, of branching time, as opposed to a linear-time logic like LTL.

For a pdf file with the text of the master thesis and for the source code of the model checker, see http://sites.google.com/site/danpolansky/alfred. See also Model checking at Wikipedia.