POMC is an explicit-state model checker for the temporal logic POTL.
Consult the project page for more.