Plugins in ePMC

In the following, we introduce the plugins in the tool.

1. Algorithm group

   • algorithm. This plugin provides classical algorithms which are often used in model checking procedures. The algorithms currently provided are:
     • FoxGlynn which computes Poisson probabilities for CTMCs. The implementation follows the paper^url by David N. Jansen.
     • Tarjan which is a well-known SCC decomposition algorithm by Robert Tarjan^url. It can only be used for explicit data structure.
     • Bloem and Chatterjee algorithms compute the SCCs using BDDs. They were proposed by Roderick Bloem et al. and Krishnendu Chatterjee et al., respectively.

2. Automata group

   • automata. This plugin provides an uniform interface for automata such as Büchi and Rabin automata.
   • automata-determinisation. This plugin provides the algorithms proposed by Sven Schewe to determinize nondeterministic Büchi automata to deterministic Rabin automata and deterministic Parity automata.

3. Command group

   • command-check. This plugin calls the model checker to do the model checking task.
   • command-help. This plugin prints out the usage messages.
   • command-lump. This plugin takes as input a probabilistic model and outputs a new model which is bisimilar to the original model.
   • command-server. This plugin serves as a server to handle the model checking request.

4. BDD group

   • dd. This plugin provides an uniform interface to use a Binary Decision Diagrams (BDDs) library.
   • dd-buddy. This plugin implements the dd interface by using the C library BuDDy^url, which is a small and an efficient BDD library.
   • dd-cacdd. This plugin implements the dd interface by using the C++ library CacBDD^url, which implements a dynamic cache management algorithm.
   • dd-cudd. This plugin implements the dd interface by using the C library CUDD^url. CUDD is the most well-known BDD library, which is the default BDD library in PRISM model checker.
   • dd-cudd-mtbdd. This plugin implements the dd interface by using the multi-terminal binary decision diagrams (MTBDDs) in CUDD.
   • dd-jdd. This plugin implements the dd interface by using the library JDD^url, which is a Java implementation of binary decision diagrams inspired by BuDDy.
   • dd-sylvan. This plugin implements the dd interface by using the library Sylvan^url, which is a parallel (multi-core) BDD library written in C.

   Note that, if dd is used, then at least one of the concrete implementations has to be included as well.

5. Expression group

   • expression-basic (used to be expression-standard). This plugin is designed to provide an uniform interface as well as the corresponding data structures to handle formulas such as PCTL and PLTL.

6. Graph group

   • graph. This plugin provides an uniform interface as well as the data structures to store various models as a graph. The model can be a Markov chain, a Markov decision process, an automaton and any models which could be interpreted as a labeled graph. It also provides the interfaces to access the properties in the nodes or the properties on the edges. For instance, you can collect all atomic propositions which hold in a state via evaluating the properties of that state node.

7. Graph solver group

   • graphsolver. This plugin provides an uniform interface to solve linear programming problems on a graph.
   • graphsolver-iterative. This plugin implements the graphsolver interface to solve the given linear programming problem by value iteration. It provides Jacobi method and Gauss-Seidel method to do the iteration. Note that, if graphsolver is used, then at least one of the concrete implementations has to be included as well.

8. Jani format group

   • jani-exporter. This plugin allows you to export the models and properties in JANI format.
   • jani-interaction. This plugin implements the communication architecture between the client and the server using JANI format.
   • jani-model. This plugin provides a parser to transform an input JANI model to a graph or an MTBDD. It is also able to parse the input JANI formula.

9. Lumping algorithms

   • lumper-explicit-signature. This plugin implements a signature based lumping algorithm for probabilistic systems.
   • lumper-dd (used to be lumping-dd). This plugin implements a lumping algorithm for probabilistic systems by using MTBDDs.

10. Prism format group

    • prism-format (used to be prism). This plugin provides a parser to transform a given PRISM model description to an explicit graph or an MTBDD. It also provides a parser for the input formula.

11. Property solvers group In order to build a model checker, one has to implement the interface propertysolver. The property solvers contained in ePMC are listed as follows.

    • propertysolver-coalition. This plugin provides a solution to solve a probabilistic Parity game against linear temporal properties.
    • propertysolver-filter. This plugin provides a way to handle the filter operation in the given PRISM formula.
    • propertysolver-ltl-lazy. This plugin implements an efficient method to model check the LTL over the probabilistic systems which is published at CONCUR 2015^url.
    • propertysolver-operator. This plugin provides a way to handle all operators occurred in the given formula.
    • propertysolver-pctl. This plugin implements the PCTL model checking algorithm over probabilistic systems.
    • propertysolver-propositional. This plugin provides a way to identify all states which satisfy the given propositional formula.
    • propertysolver-reachability. This plugin implements an example model checking algorithm to handle the reachability formula P=? [F a] over Markov chains. One will have a rough idea to implement new model checking algorithms from this example.
    • propertysolver-reward. This plugin implements a model checking algorithm to handle the probabilistic systems with rewards.

12. Value group

    • value-basic (used to be value-standard). This plugin contains an unifom interface to use all kinds of variables occurred in ePMC.