(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.
SelectionFile type iconFile nameDescriptionSizeRevisionTimeUser

Source code of Alfred model checker  697k v. 1 Apr 27, 2011, 4:59 AM Daniel Polansky
View Download
The text of the master's thesis.  299k v. 1 Apr 27, 2011, 5:15 AM Daniel Polansky