diff --git a/src/formula/AP.h b/src/formula/AP.h
index 9113c5bbd..00a3e8734 100644
--- a/src/formula/AP.h
+++ b/src/formula/AP.h
@@ -15,7 +15,9 @@ namespace mrmc {
 namespace formula {
 
 /*!
+ * @brief
  * Class for a PCTL formula tree with atomic proposition as root.
+ *
  * This class represents the leaves in the formula tree.
  *
  * @see PCTLStateFormula
diff --git a/src/formula/And.h b/src/formula/And.h
index 025ac2f6e..8a1cd9696 100644
--- a/src/formula/And.h
+++ b/src/formula/And.h
@@ -16,7 +16,9 @@ namespace mrmc {
 namespace formula {
 
 /*!
+ * @brief
  * Class for a PCTL formula tree with AND node as root.
+ *
  * Has two PCTL state formulas as sub formulas/trees.
  *
  * As AND is commutative, the order is \e theoretically not important, but will influence the order in which
diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h
index dc7640e95..3e48dc132 100644
--- a/src/formula/BoundedUntil.h
+++ b/src/formula/BoundedUntil.h
@@ -19,10 +19,12 @@ namespace mrmc {
 namespace formula {
 
 /*!
+ * @brief
  * Class for a PCTL (path) formula tree with a BoundedUntil node as root.
+ *
  * Has two PCTL state formulas as sub formulas/trees.
  *
- * \par Semantics
+ * @par Semantics
  * The formula holds iff in at most \e bound steps, formula \e right (the right subtree) holds, and before,
  * \e left holds.
  *
diff --git a/src/formula/Next.h b/src/formula/Next.h
index 5a243b5f1..6000366ff 100644
--- a/src/formula/Next.h
+++ b/src/formula/Next.h
@@ -16,10 +16,12 @@ namespace mrmc {
 namespace formula {
 
 /*!
+ * @brief
  * Class for a PCTL (path) formula tree with a Next node as root.
+ *
  * Has two PCTL state formulas as sub formulas/trees.
  *
- * \par Semantics
+ * @par Semantics
  * The formula holds iff in the next step, \e child holds
  *
  * The subtree is seen as part of the object and deleted with the object
diff --git a/src/formula/Not.h b/src/formula/Not.h
index 52a9311aa..59f100f70 100644
--- a/src/formula/Not.h
+++ b/src/formula/Not.h
@@ -15,7 +15,9 @@ namespace mrmc {
 namespace formula {
 
 /*!
+ * @brief
  * Class for a PCTL formula tree with NOT node as root.
+ *
  * Has one PCTL state formula as sub formula/tree.
  *
  * The subtree is seen as part of the object and deleted with the object
diff --git a/src/formula/Or.h b/src/formula/Or.h
index 94c01ba29..a5cdbc659 100644
--- a/src/formula/Or.h
+++ b/src/formula/Or.h
@@ -15,7 +15,9 @@ namespace mrmc {
 namespace formula {
 
 /*!
+ * @brief
  * Class for a PCTL formula tree with OR node as root.
+ *
  * Has two PCTL state formulas as sub formulas/trees.
  *
  * As OR is commutative, the order is \e theoretically not important, but will influence the order in which
diff --git a/src/formula/PCTLPathFormula.h b/src/formula/PCTLPathFormula.h
index cebc3d15f..70255f8b3 100644
--- a/src/formula/PCTLPathFormula.h
+++ b/src/formula/PCTLPathFormula.h
@@ -17,9 +17,11 @@ namespace mrmc {
 namespace formula {
 
 /*!
+ * @brief
  * Abstract base class for PCTL path formulas.
+ *
  * @attention This class is abstract.
-  * @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so
+ * @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so
  * 	   the syntax conflicts with copy constructors for unary operators. To produce an identical object, use the method
  * 	   clone().
  */
diff --git a/src/formula/PCTLStateFormula.h b/src/formula/PCTLStateFormula.h
index 67ed9a899..de8d0e117 100644
--- a/src/formula/PCTLStateFormula.h
+++ b/src/formula/PCTLStateFormula.h
@@ -17,7 +17,9 @@ namespace mrmc {
 namespace formula {
 
 /*!
+ * @brief
  * Abstract base class for PCTL state formulas.
+ *
  * @attention This class is abstract.
  * @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so
  * 	   the syntax conflicts with copy constructors for unary operators. To produce an identical object, use the method
diff --git a/src/formula/PCTLformula.h b/src/formula/PCTLformula.h
index 60f361f25..12f51a4ce 100644
--- a/src/formula/PCTLformula.h
+++ b/src/formula/PCTLformula.h
@@ -17,7 +17,9 @@ namespace formula {
 
 //abstract
 /*!
+ * @brief
  * Abstract base class for PCTL formulas in general.
+ *
  * @attention This class is abstract.
  * @note Formula classes do not have copy constructors. The parameters of the constructors are usually the subtrees, so
  * 	   the syntax conflicts with copy constructors for unary operators. To produce an identical object, the classes
diff --git a/src/formula/ProbabilisticOperator.h b/src/formula/ProbabilisticOperator.h
index 4d71e0be6..89978f30f 100644
--- a/src/formula/ProbabilisticOperator.h
+++ b/src/formula/ProbabilisticOperator.h
@@ -17,10 +17,12 @@ namespace mrmc {
 namespace formula {
 
 /*!
+ * @brief
  * Class for a PCTL formula tree with a P (probablistic) operator node as root.
+ *
  * Has one PCTL path formula as sub formula/tree.
  *
- * \par Semantics
+ * @par Semantics
  * 	  The formula holds iff the probability that the path formula holds is inside the bounds specified in this operator
  *
  * The subtree is seen as part of the object and deleted with it
diff --git a/src/formula/Until.h b/src/formula/Until.h
index 8da6d0928..39f361e11 100644
--- a/src/formula/Until.h
+++ b/src/formula/Until.h
@@ -16,10 +16,12 @@ namespace mrmc {
 namespace formula {
 
 /*!
- * Class for a PCTL (path) formula tree with a BoundedUntil node as root.
+ * @brief
+ * Class for a PCTL (path) formula tree with an Until node as root.
+ *
  * Has two PCTL state formulas as sub formulas/trees.
  *
- * \par Semantics
+ * @par Semantics
  * The formula holds iff eventually, formula \e right (the right subtree) holds, and before,
  * \e left holds always.
  *
diff --git a/src/modelChecker/DtmcPrctlModelChecker.h b/src/modelChecker/DtmcPrctlModelChecker.h
index ddb4b1f9b..7c6932ccb 100644
--- a/src/modelChecker/DtmcPrctlModelChecker.h
+++ b/src/modelChecker/DtmcPrctlModelChecker.h
@@ -43,41 +43,147 @@ namespace mrmc {
 
 namespace modelChecker {
 
+/*!
+ * @brief
+ * Interface for model checker classes.
+ *
+ * This class provides basic functions that are the same for all subclasses, but mainly only declares
+ * abstract methods that are to be implemented in concrete instances.
+ *
+ * @attention This class is abstract.
+ */
 template<class T>
 class DtmcPrctlModelChecker {
    private:
       mrmc::models::Dtmc<T>* dtmc;
 
    protected:
+      /*!
+       * @returns A reference to the dtmc of the model checker.
+       */
       mrmc::models::Dtmc<T>* getDtmc() const {
          return this->dtmc;
       }
 
    public:
+      /*!
+       * Constructor
+       */
       explicit DtmcPrctlModelChecker(mrmc::models::Dtmc<T>* DTMC);
-      virtual ~DtmcPrctlModelChecker();
 
-      virtual void makeAbsorbing(mrmc::storage::BitVector*) = 0;
-      virtual mrmc::storage::BitVector& getStatesSatisying(std::string) = 0;
-      virtual std::vector<T> multiplyMatrixVector(std::vector<T>*) = 0;
+      /*!
+       * Destructor
+       */
+      virtual ~DtmcPrctlModelChecker();
 
+      /*!
+       * Makes all states in a given set absorbing (i.e. adds self loops with probability 1 and removes all
+       * other edges from these states)
+       *
+       * @param states A bit vector representing a set of states that should become absorbing.
+       */
+      virtual void makeAbsorbing(mrmc::storage::BitVector* states) = 0;
+
+      /*!
+       * Returns all states that are labeled with a given atomic proposition.
+       *
+       * @param ap A string representing an atomic proposition.
+       * @returns The set of states labeled with the atomic proposition ap.
+       */
+      virtual mrmc::storage::BitVector& getStatesLabeledWith(std::string ap) = 0;
+
+      /*!
+       * Multiplies the matrix with a given vector; the result again is a vector.
+       *
+       * @param vector The vector to multiply the matrix with.
+       * @returns The result of multiplying the transition probability matrix with vector.
+       */
+      virtual std::vector<T> multiplyMatrixVector(std::vector<T>* vector) = 0;
+
+      /*!
+       * The check method for a state formula; Will infer the actual type of formula and delegate it
+       * to the specialized method
+       *
+       * @param formula The state formula to check
+       * @returns The set of states satisfying the formula, represented by a bit vector
+       */
       virtual mrmc::storage::BitVector checkStateFormula(mrmc::formula::PCTLStateFormula<T>* formula) {
          return formula->check(this);
       }
 
-
-      virtual mrmc::storage::BitVector checkAnd(mrmc::formula::And<T>*) = 0;
+      /*!
+       * The check method for a state formula with an And node as root in its formula tree
+       *
+       * @param formula The And formula to check
+       * @returns The set of states satisfying the formula, represented by a bit vector
+       */
+      virtual mrmc::storage::BitVector checkAnd(mrmc::formula::And<T>* formula) = 0;
+
+      /*!
+       * The check method for a formula with an AP node as root in its formula tree
+       *
+       * @param formula The AP state formula to check
+       * @returns The set of states satisfying the formula, represented by a bit vector
+       */
       virtual mrmc::storage::BitVector checkAP(mrmc::formula::AP<T>*) = 0;
+
+      /*!
+       * The check method for a formula with a Not node as root in its formula tree
+       *
+       * @param formula The Not state formula to check
+       * @returns The set of states satisfying the formula, represented by a bit vector
+       */
       virtual mrmc::storage::BitVector checkNot(mrmc::formula::Not<T>*) = 0;
+
+      /*!
+       * The check method for a state formula with an Or node as root in its formula tree
+       *
+       * @param formula The Or state formula to check
+       * @returns The set of states satisfying the formula, represented by a bit vector
+       */
       virtual mrmc::storage::BitVector checkOr(mrmc::formula::Or<T>*) = 0;
+
+      /*!
+       * The check method for a state formula with a probabilistic operator node as root in its formula tree
+       *
+       * @param formula The state formula to check
+       * @returns The set of states satisfying the formula, represented by a bit vector
+       */
       virtual mrmc::storage::BitVector checkProbabilisticOperator(mrmc::formula::ProbabilisticOperator<T>*) = 0;
 
+      /*!
+       * The check method for a path formula; Will infer the actual type of formula and delegate it
+       * to the specialized method
+       *
+       * @param formula The path formula to check
+       * @returns for each state the probability that the path formula holds.
+       */
       virtual std::vector<T> checkPathFormula(mrmc::formula::PCTLPathFormula<T>* formula) {
          return formula->check(this);
       }
 
+      /*!
+       * The check method for a path formula with a Bounded Until operator node as root in its formula tree
+       *
+       * @param formula The Bounded Until path formula to check
+       * @returns for each state the probability that the path formula holds.
+       */
       virtual std::vector<T> checkBoundedUntil(mrmc::formula::BoundedUntil<T>*) = 0;
+
+      /*!
+       * The check method for a path formula with a Next operator node as root in its formula tree
+       *
+       * @param formula The Next path formula to check
+       * @returns for each state the probability that the path formula holds.
+       */
       virtual std::vector<T> checkNext(mrmc::formula::Next<T>*) = 0;
+
+      /*!
+       * The check method for a path formula with an Until operator node as root in its formula tree
+       *
+       * @param formula The Until path formula to check
+       * @returns for each state the probability that the path formula holds.
+       */
       virtual std::vector<T> checkUntil(mrmc::formula::Until<T>*) = 0;
 };