Alfred

(Read further only if you are a theoretical computer scientist.) I have implemented model checker Alfred as part of my master's thesis. The model checker decides the validity of formulas of alternation free modal mu-calculus for push down systems, and push down automata. Also available is the source code of the model checker. 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.