• ePMC: the successor of IscasMC, from which it keeps all features about Linear Time Logic probabilistic model checking. ePMC is highly modular, which allows everyone to extend and improve the functionalities of the model checker.
  • ROLL: a library of learning algorithms for ω-regular languages.  It consists of some learning algorithms for FDFAs and for Büchi automata.
  • IscasMCIscasMC is a model checker for probabilistic models. It supports Markov chains and Markov decision Processes (MDP), and properties specified in PCTLPLTL and their combination PCTL*. It implements the efficient algorithm in particularly tuned to handle linear time properties.