diff --git a/src/formula/AP.h b/src/formula/AP.h
index 6305dfebf..8bda0df06 100644
--- a/src/formula/AP.h
+++ b/src/formula/AP.h
@@ -14,29 +14,87 @@ namespace mrmc {
 
 namespace formula {
 
-class AP : public PCTLStateFormula {
-   private:
-   std::string ap;
-   public:
-      AP(std::string ap) {
-         this->ap = ap;
-      }
-
-      AP(char* ap) {
-         this->ap = ap;
-      }
-
-      std::string getAP() {
-         return ap;
-      }
-
-      std::string toString() {
-         return getAP();
-      }
-
-      virtual enum stateFormulaTypes type() {
-            return stateFormulaTypes::AP;
-      }
+/*!
+ * @brief
+ * Class for a PCTL formula tree with atomic proposition as root.
+ *
+ * This class represents the leaves in the formula tree.
+ *
+ * @see PCTLStateFormula
+ * @see PCTLFormula
+ */
+template <class T>
+class AP : public PCTLStateFormula<T> {
+
+public:
+	/*!
+	 * Constructor
+	 *
+	 * Creates a new atomic proposition leaf, with the label AP
+	 *
+	 * @param ap The string representing the atomic proposition
+	 */
+	AP(std::string ap) {
+		this->ap = ap;
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * Creates a new atomic proposition leaf, with the label AP
+	 *
+	 * @param ap The string representing the atomic proposition
+	 */
+	AP(char* ap) {
+	 //TODO: Does that really work?
+		this->ap = ap;
+	}
+
+	/*!
+	 * Destructor.
+	 * At this time, empty...
+	 */
+	virtual ~AP() { }
+
+	/*!
+	 * @returns the name of the atomic proposition
+	 */
+	std::string getAP() {
+		return ap;
+	}
+
+	/*!
+	 * @returns a string representation of the leaf.
+	 *
+	 */
+	virtual std::string toString() {
+		return getAP();
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * @returns a new AP-object that is identical the called object.
+	 */
+	virtual PCTLStateFormula<T>* clone() {
+	  return new AP(ap);
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
+	 */
+	virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
+	  return modelChecker->checkAP(this);
+	}
+
+private:
+	std::string ap;
 };
 
 } //namespace formula
diff --git a/src/formula/And.h b/src/formula/And.h
index 9d09c526e..16f0b6d8e 100644
--- a/src/formula/And.h
+++ b/src/formula/And.h
@@ -15,48 +15,139 @@ namespace mrmc {
 
 namespace formula {
 
-class And : public PCTLStateFormula {
-   private:
-      PCTLStateFormula* left;
-      PCTLStateFormula* right;
-   public:
-      And() {
-         left = NULL;
-         right = NULL;
-      }
-      And(PCTLStateFormula* left, PCTLStateFormula* right) {
-         this->left = left;
-         this->right = right;
-      }
-
-      void setLeft(PCTLStateFormula* newLeft) {
-         left = newLeft;
-      }
-
-      void setRight(PCTLStateFormula* newRight) {
-         right = newRight;
-      }
-
-      PCTLStateFormula* getLeft() {
-         return left;
-      }
-
-      PCTLStateFormula* getRight() {
-         return right;
-      }
-
-      std::string toString() {
-         std::string result = "(";
-         result += left->toString();
-         result += " && ";
-         result += right->toString();
-         result += ")";
-         return result;
-      }
-
-      virtual enum stateFormulaTypes type() {
-            return AND;
-      }
+/*!
+ * @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
+ * the model checker works.
+ *
+ * The subtrees are seen as part of the object and deleted with the object
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ *
+ * @see PCTLStateFormula
+ * @see PCTLFormula
+ */
+template <class T>
+class And : public PCTLStateFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor.
+	 * Will create an AND-node without subnotes. Will not represent a complete formula!
+	 */
+	And() {
+		left = NULL;
+		right = NULL;
+	}
+
+	/*!
+	 * Constructor.
+	 * Creates an AND note with the parameters as subtrees.
+	 *
+	 * @param left The left sub formula
+	 * @param right The right sub formula
+	 */
+	And(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right) {
+		this->left = left;
+		this->right = right;
+	}
+
+	/*!
+	 * Destructor.
+	 *
+	 * The subtrees are deleted with the object
+	 * (this behavior can be prevented by setting them to NULL before deletion)
+	 */
+	virtual ~And() {
+		if (left != NULL) {
+			delete left;
+		}
+		if (right != NULL) {
+			delete right;
+		}
+	}
+
+	/*!
+	 * Sets the left child node.
+	 *
+	 * @param newLeft the new left child.
+	 */
+	void setLeft(PCTLStateFormula<T>* newLeft) {
+		left = newLeft;
+	}
+
+	/*!
+	 * Sets the right child node.
+	 *
+	 * @param newRight the new right child.
+	 */
+	void setRight(PCTLStateFormula<T>* newRight) {
+		right = newRight;
+	}
+
+	/*!
+	 * @returns a pointer to the left child node
+	 */
+	PCTLStateFormula<T>* getLeft() {
+		return left;
+	}
+
+	/*!
+	 * @returns a pointer to the right child node
+	 */
+	PCTLStateFormula<T>* getRight() {
+		return right;
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() {
+		std::string result = "(";
+		result += left->toString();
+		result += " && ";
+		result += right->toString();
+		result += ")";
+		return result;
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new AND-object that is identical the called object.
+	 */
+	virtual PCTLStateFormula<T>* clone() {
+		And<T>* result = new And();
+		if (this->left != NULL) {
+		  result->setLeft(left->clone());
+		}
+		if (this->right != NULL) {
+		  result->setRight(right->clone());
+		}
+		return result;
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
+	 */
+	virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
+		return modelChecker->checkAnd(this);
+	}
+
+private:
+	PCTLStateFormula<T>* left;
+	PCTLStateFormula<T>* right;
 };
 
 } //namespace formula
diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h
index 425e5afaf..c0061691c 100644
--- a/src/formula/BoundedUntil.h
+++ b/src/formula/BoundedUntil.h
@@ -11,69 +11,170 @@
 #include "PCTLPathFormula.h"
 #include "PCTLStateFormula.h"
 #include "boost/integer/integer_mask.hpp"
+#include "boost/lexical_cast.hpp"
+#include <string>
 
 namespace mrmc {
 
 namespace formula {
 
-class BoundedUntil : public PCTLPathFormula {
-      PCTLStateFormula* left;
-      PCTLStateFormula* right;
-      uint_fast64_t bound;
-   public:
-      BoundedUntil() {
-         this->left = NULL;
-         this->right = NULL;
-         bound = 0;
-      }
-
-      BoundedUntil(PCTLStateFormula* left, PCTLStateFormula* right,
-                   uint_fast64_t bound) {
-         this->left = left;
-         this->right = right;
-         this->bound = bound;
-      }
-
-      virtual ~BoundedUntil();
-
-      void setLeft(PCTLStateFormula* newLeft) {
-         left = newLeft;
-      }
-
-      void setRight(PCTLStateFormula* newRight) {
-         right = newRight;
-      }
-
-      PCTLStateFormula* getLeft() {
-         return left;
-      }
-
-      PCTLStateFormula* getRight() {
-         return right;
-      }
-
-      uint_fast64_t getBound() {
-         return bound;
-      }
-
-      void setBound(uint_fast64_t bound) {
-         this->bound = bound;
-      }
-
-      std::string toString() {
-         std::string result = "(";
-         result += left->toString();
-         result += " U<=";
-         result +=  std::to_string(bound);
-         result += " ";
-         result += right->toString();
-         result += ")";
-         return result;
-      }
-
-      virtual enum pathFormulaTypes type() {
-            return BOUNDED_UNTIL;
-      }
+/*!
+ * @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
+ * The formula holds iff in at most \e bound steps, formula \e right (the right subtree) holds, and before,
+ * \e left holds.
+ *
+ * The subtrees are seen as part of the object and deleted with the object
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ *
+ * @see PCTLPathFormula
+ * @see PCTLFormula
+ */
+template <class T>
+class BoundedUntil : public PCTLPathFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	BoundedUntil() {
+		this->left = NULL;
+		this->right = NULL;
+		bound = 0;
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param left The left formula subtree
+	 * @param right The left formula subtree
+	 * @param bound The maximal number of steps
+	 */
+	BoundedUntil(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right,
+					 uint_fast64_t bound) {
+		this->left = left;
+		this->right = right;;
+		this->bound = bound;
+	}
+
+	/*!
+	 * Destructor.
+	 *
+	 * Also deletes the subtrees.
+	 * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
+	 */
+	virtual ~BoundedUntil() {
+	  if (left != NULL) {
+		  delete left;
+	  }
+	  if (right != NULL) {
+		  delete right;
+	  }
+	}
+
+	/*!
+	 * Sets the left child node.
+	 *
+	 * @param newLeft the new left child.
+	 */
+	void setLeft(PCTLStateFormula<T>* newLeft) {
+		left = newLeft;
+	}
+
+	/*!
+	 * Sets the right child node.
+	 *
+	 * @param newRight the new right child.
+	 */
+	void setRight(PCTLStateFormula<T>* newRight) {
+		right = newRight;
+	}
+
+	/*!
+	 * @returns a pointer to the left child node
+	 */
+	PCTLStateFormula<T>* getLeft() {
+		return left;
+	}
+
+	/*!
+	 * @returns a pointer to the right child node
+	 */
+	PCTLStateFormula<T>* getRight() {
+		return right;
+	}
+
+	/*!
+	 * @returns the maximally allowed number of steps for the bounded until operator
+	 */
+	uint_fast64_t getBound() {
+		return bound;
+	}
+
+	/*!
+	 * Sets the maximally allowed number of steps for the bounded until operator
+	 *
+	 * @param bound the new bound.
+	 */
+	void setBound(uint_fast64_t bound) {
+		this->bound = bound;
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() {
+		std::string result = "(";
+		result += left->toString();
+		result += " U<=";
+		result +=  boost::lexical_cast<std::string>(bound);
+		result += " ";
+		result += right->toString();
+		result += ")";
+		return result;
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new BoundedUntil-object that is identical the called object.
+	 */
+	virtual PCTLPathFormula<T>* clone() {
+		BoundedUntil<T>* result = new BoundedUntil();
+		result->setBound(bound);
+		if (left != NULL) {
+			result->setLeft(left->clone());
+		}
+		if (right != NULL) {
+			result->setRight(right->clone());
+		}
+		return result;
+	}
+
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A vector indicating the probability that the formula holds for each state.
+	 */
+	virtual std::vector<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
+	  return modelChecker->checkBoundedUntil(this);
+	}
+
+private:
+	PCTLStateFormula<T>* left;
+	PCTLStateFormula<T>* right;
+	uint_fast64_t bound;
 };
 
 } //namespace formula
diff --git a/src/formula/Next.h b/src/formula/Next.h
index 2fa5e1d02..4ec120b80 100644
--- a/src/formula/Next.h
+++ b/src/formula/Next.h
@@ -15,38 +15,109 @@ 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
+ * 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
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ *
+ * @see PCTLPathFormula
+ * @see PCTLFormula
+ */
+template <class T>
+class Next : public PCTLPathFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	Next() {
+		this->child = NULL;
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param child The child node
+	 */
+	Next(PCTLStateFormula<T>* child) {
+		this->child = child;
+	}
+
+	/*!
+	 * Constructor.
+	 *
+	 * Also deletes the subtree.
+	 * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
+	 */
+	virtual ~Next() {
+	  if (child != NULL) {
+		  delete child;
+	  }
+	}
+
+	/*!
+	 * @returns the child node
+	 */
+	PCTLStateFormula<T>* getChild() {
+		return child;
+	}
+
+	/*!
+	 * Sets the subtree
+	 * @param child the new child node
+	 */
+	void setChild(PCTLStateFormula<T>* child) {
+		this->child = child;
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() {
+		std::string result = "(";
+		result += " X ";
+		result += child->toString();
+		result += ")";
+		return result;
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new BoundedUntil-object that is identical the called object.
+	 */
+	virtual PCTLPathFormula<T>* clone() {
+		Next<T>* result = new Next<T>();
+		if (child != NULL) {
+			result->setChild(child);
+		}
+		return result;
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A vector indicating the probability that the formula holds for each state.
+	 */
+	virtual std::vector<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
+	  return modelChecker->checkNext(this);
+	}
 
-class Next : public PCTLPathFormula {
-   private:
-      PCTLStateFormula* child;
-   public:
-      Next() {
-         this->child = NULL;
-      }
-
-      Next(PCTLStateFormula* child) {
-         this->child = child;
-      }
-
-      PCTLStateFormula* getChild() {
-         return child;
-      }
-
-      void setChild(PCTLStateFormula* child) {
-         this->child = child;
-      }
-
-      std::string toString() {
-         std::string result = "(";
-         result += " X ";
-         result += child->toString();
-         result += ")";
-         return result;
-      }
-
-      virtual enum pathFormulaTypes type() {
-            return NEXT;
-      }
+private:
+	PCTLStateFormula<T>* child;
 };
 
 } //namespace formula
diff --git a/src/formula/Not.h b/src/formula/Not.h
index 36993c18a..dfcb7c100 100644
--- a/src/formula/Not.h
+++ b/src/formula/Not.h
@@ -8,45 +8,109 @@
 #ifndef NOT_H_
 #define NOT_H_
 
+#include "PCTLStateFormula.h"
+
 namespace mrmc {
 
 namespace formula {
 
-#include "PCTLStateFormula.h"
+/*!
+ * @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
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ *
+ * @see PCTLStateFormula
+ * @see PCTLFormula
+ */
+template <class T>
+class Not : public PCTLStateFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	Not() {
+		this->child = NULL;
+	}
 
-class Not : public PCTLStateFormula {
-   private:
-      PCTLStateFormula* child;
-   public:
-      Not() {
-         this->child = NULL;
-      }
+	/*!
+	 * Constructor
+	 * @param child The child node
+	 */
+	Not(PCTLStateFormula<T>* child) {
+		this->child = child;
+	}
 
-      Not(PCTLStateFormula* child) {
-         this->child = child;
-      }
+	/*!
+	 * Destructor
+	 *
+	 * Also deletes the subtree
+	 * (this behavior can be prevented by setting them to NULL before deletion)
+	 */
+	virtual ~Not() {
+	  if (child != NULL) {
+		  delete child;
+	  }
+	}
 
-      virtual ~Not() {
+	/*!
+	 * @returns The child node
+	 */
+	PCTLStateFormula<T>* getChild() {
+		return child;
+	}
 
-      }
+	/*!
+	 * Sets the subtree
+	 * @param child the new child node
+	 */
+	void setChild(PCTLStateFormula<T>* child) {
+		this->child = child;
+	}
 
-      PCTLStateFormula* getChild() {
-         return child;
-      }
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() {
+		std::string result = "!";
+		result += child->toString();
+		return result;
+	}
 
-      void setChild(PCTLStateFormula* child) {
-         this->child = child;
-      }
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new AND-object that is identical the called object.
+	 */
+	virtual PCTLStateFormula<T>* clone() {
+		Not<T>* result = new Not<T>();
+		if (child != NULL) {
+			result->setChild(child);
+		}
+		return result;
+	}
 
-      std::string toString() {
-         std::string result = "!";
-         result += child->toString();
-         return result;
-      }
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
+	 */
+	virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
+	  return modelChecker->checkNot(this);
+	}
 
-      virtual enum stateFormulaTypes type() {
-            return NOT;
-      }
+private:
+	PCTLStateFormula<T>* child;
 };
 
 } //namespace formula
diff --git a/src/formula/Or.h b/src/formula/Or.h
index 6559d36aa..51a2f88fd 100644
--- a/src/formula/Or.h
+++ b/src/formula/Or.h
@@ -14,48 +14,139 @@ namespace mrmc {
 
 namespace formula {
 
-class Or : public PCTLStateFormula {
-   private:
-      PCTLStateFormula* left;
-      PCTLStateFormula* right;
-   public:
-      Or() {
-         left = NULL;
-         right = NULL;
-      }
-      Or(PCTLStateFormula* left, PCTLStateFormula* right) {
-         this->left = left;
-         this->right = right;
-      }
-
-      void setLeft(PCTLStateFormula* newLeft) {
-         left = newLeft;
-      }
-
-      void setRight(PCTLStateFormula* newRight) {
-         right = newRight;
-      }
-
-      PCTLStateFormula* getLeft() {
-         return left;
-      }
-
-      PCTLStateFormula* getRight() {
-         return right;
-      }
-
-      std::string toString() {
-         std::string result = "(";
-         result += left->toString();
-         result += " || ";
-         result += right->toString();
-         result += ")";
-         return result;
-      }
-
-      virtual enum stateFormulaTypes type() {
-            return OR;
-      }
+/*!
+ * @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
+ * the model checker works.
+ *
+ * The subtrees are seen as part of the object and deleted with the object
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ *
+ * @see PCTLStateFormula
+ * @see PCTLFormula
+ */
+template <class T>
+class Or : public PCTLStateFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor.
+	 * Will create an AND-node without subnotes. Will not represent a complete formula!
+	 */
+	Or() {
+		left = NULL;
+		right = NULL;
+	}
+
+	/*!
+	 * Constructor.
+	 * Creates an AND note with the parameters as subtrees.
+	 *
+	 * @param left The left sub formula
+	 * @param right The right sub formula
+	 */
+	Or(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right) {
+		this->left = left;
+		this->right = right;
+	}
+
+	/*!
+	 * Destructor.
+	 *
+	 * The subtrees are deleted with the object
+	 * (this behavior can be prevented by setting them to NULL before deletion)
+	 */
+	virtual ~Or() {
+	  if (left != NULL) {
+		  delete left;
+	  }
+	  if (right != NULL) {
+		  delete right;
+	  }
+	}
+
+	/*!
+	 * Sets the left child node.
+	 *
+	 * @param newLeft the new left child.
+	 */
+	void setLeft(PCTLStateFormula<T>* newLeft) {
+		left = newLeft;
+	}
+
+	/*!
+	 * Sets the right child node.
+	 *
+	 * @param newRight the new right child.
+	 */
+	void setRight(PCTLStateFormula<T>* newRight) {
+		right = newRight;
+	}
+
+	/*!
+	 * @returns a pointer to the left child node
+	 */
+	PCTLStateFormula<T>* getLeft() {
+		return left;
+	}
+
+	/*!
+	 * @returns a pointer to the right child node
+	 */
+	PCTLStateFormula<T>* getRight() {
+		return right;
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() {
+		std::string result = "(";
+		result += left->toString();
+		result += " || ";
+		result += right->toString();
+		result += ")";
+		return result;
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new AND-object that is identical the called object.
+	 */
+	virtual PCTLStateFormula<T>* clone() {
+		Or<T>* result = new Or();
+		if (this->left != NULL) {
+		  result->setLeft(left->clone());
+		}
+		if (this->right != NULL) {
+		  result->setRight(right->clone());
+		}
+		return result;
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
+	 */
+	virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
+	  return modelChecker->checkOr(this);
+	}
+
+private:
+	PCTLStateFormula<T>* left;
+	PCTLStateFormula<T>* right;
 };
 
 } //namespace formula
diff --git a/src/formula/PCTLPathFormula.h b/src/formula/PCTLPathFormula.h
index 7114caca9..b795244e3 100644
--- a/src/formula/PCTLPathFormula.h
+++ b/src/formula/PCTLPathFormula.h
@@ -9,16 +9,53 @@
 #define PCTLPATHFORMULA_H_
 
 #include "PCTLformula.h"
-#include "formulaTypes.h"
+#include "modelChecker/DtmcPrctlModelChecker.h"
+#include <vector>
 
 namespace mrmc {
 
 namespace formula {
 
-//abstract
-class PCTLPathFormula : public PCTLFormula {
-   public:
-      virtual enum pathFormulaTypes type() = 0;
+/*!
+ * @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
+ * 	   the syntax conflicts with copy constructors for unary operators. To produce an identical object, use the method
+ * 	   clone().
+ */
+template <class T>
+class PCTLPathFormula : public PCTLFormula<T> {
+
+public:
+	/*!
+	 * empty destructor
+	 */
+	virtual ~PCTLPathFormula() { }
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @note This function is not implemented in this class.
+	 * @returns a new AND-object that is identical the called object.
+	 */
+	virtual PCTLPathFormula<T>* clone() = 0;
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @note This function is not implemented in this class.
+	 *
+	 * @returns A vector indicating the probability that the formula holds for each state.
+	 */
+	virtual std::vector<T>* check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) = 0;
 };
 
 } //namespace formula
diff --git a/src/formula/PCTLStateFormula.h b/src/formula/PCTLStateFormula.h
index 3361a11a4..daf369510 100644
--- a/src/formula/PCTLStateFormula.h
+++ b/src/formula/PCTLStateFormula.h
@@ -9,17 +9,53 @@
 #define PCTLSTATEFORMULA_H_
 
 #include "PCTLformula.h"
-#include "formulaTypes.h"
+#include "storage/BitVector.h"
+#include "modelChecker/DtmcPrctlModelChecker.h"
 
 namespace mrmc {
 
 namespace formula {
 
-//abstract
-class PCTLStateFormula : public PCTLFormula {
-   public:
-      virtual enum stateFormulaTypes type() = 0;
+/*!
+ * @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
+ * 	   clone().
+ */
+template <class T>
+class PCTLStateFormula : public PCTLFormula<T> {
+
+public:
+	/*!
+	 * empty destructor
+	 */
+	virtual ~PCTLStateFormula() { }
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @note This function is not implemented in this class.
+	 * @returns a new AND-object that is identical the called object.
+	 */
+	virtual PCTLStateFormula<T>* clone() = 0;
 
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @note This function is not implemented in this class.
+	 *
+	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
+	 */
+	virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) = 0;
 };
 
 } //namespace formula
diff --git a/src/formula/PCTLformula.h b/src/formula/PCTLformula.h
index 996416a2c..b1e7bf0b9 100644
--- a/src/formula/PCTLformula.h
+++ b/src/formula/PCTLformula.h
@@ -16,9 +16,29 @@ 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
+ * 	   PCTLPathFormula and PCTLStateFormula offer the method clone().
+ */
+template <class T>
 class PCTLFormula {
-   public:
-      virtual std::string toString() = 0;
+
+public:
+	/*!
+	 * virtual destructor
+	 */
+	virtual ~PCTLFormula() { }
+
+	/*!
+	 * @note This function is not implemented in this class.
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() = 0;
 };
 
 } //namespace formula
diff --git a/src/formula/ProbabilisticOperator.h b/src/formula/ProbabilisticOperator.h
index bd83a1431..b0585fd58 100644
--- a/src/formula/ProbabilisticOperator.h
+++ b/src/formula/ProbabilisticOperator.h
@@ -9,63 +9,156 @@
 #define PROBABILISTICOPERATOR_H_
 
 #include "PCTLStateFormula.h"
+#include "PCTLPathFormula.h"
+#include "misc/const_templates.h"
 
 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
+ * 	  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
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ *
+ * @see PCTLStateFormula
+ * @see PCTLPathFormula
+ * @see PCTLFormula
+ */
 template<class T>
-class ProbabilisticOperator : public PCTLStateFormula {
-      T lower;
-      T upper;
-      PCTLPathFormula* pathFormula;
-   public:
-      ProbabilisticOperator(T lowerBound, T upperBound, PCTLPathFormula* pathFormula=NULL) {
-         this->lower = lowerBound;
-         this->upper = upperBound;
-         this->pathFormula = pathFormula;
-      }
-
-      virtual ~ProbabilisticOperator() {
-         delete pathFormula;
-      }
-
-      PCTLPathFormula* getPathFormula () {
-         return pathFormula;
-      }
-
-      T getLowerBound() {
-         return lower;
-      }
-
-      T getUpperBound() {
-         return upper;
-      }
-
-      void setPathFormula(PCTLPathFormula* pathFormula) {
-         this->pathFormula = pathFormula;
-      }
-
-      void setInterval(T lowerBound, T upperBound) {
-         this->lower = lowerBound;
-         this->upper = upperBound;
-      }
-
-      std::string toString() {
-         std::string result = "(";
-         result += " P[";
-         result += lower;
-         result += ";";
-         result += upper;
-         result += "] ";
-         result += pathFormula->toString();
-         result += ")";
-         return result;
-      }
-
-      virtual enum stateFormulaTypes type() {
-            return PROBABILISTIC;
-      }
+class ProbabilisticOperator : public PCTLStateFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	ProbabilisticOperator() {
+		upper = mrmc::misc::constGetZero(&upper);
+		lower = mrmc::misc::constGetZero(&lower);
+		pathFormula = NULL;
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param lowerBound The lower bound for the probability
+	 * @param upperBound The upper bound for the probability
+	 * @param pathFormula The child node (can be omitted, is then set to NULL)
+	 */
+	ProbabilisticOperator(T lowerBound, T upperBound, PCTLPathFormula<T>* pathFormula=NULL) {
+		this->lower = lowerBound;
+		this->upper = upperBound;
+		this->pathFormula = pathFormula;
+	}
+
+	/*!
+	 * Destructor
+	 *
+	 * The subtree is deleted with the object
+	 * (this behavior can be prevented by setting them to NULL before deletion)
+	 */
+	virtual ~ProbabilisticOperator() {
+	 if (pathFormula != NULL) {
+		 delete pathFormula;
+	 }
+	}
+
+	/*!
+	 * @returns the child node (representation of a PCTL path formula)
+	 */
+	PCTLPathFormula<T>* getPathFormula () {
+		return pathFormula;
+	}
+
+	/*!
+	 * @returns the lower bound for the probability
+	 */
+	T getLowerBound() {
+		return lower;
+	}
+
+	/*!
+	 * @returns the upper bound for the probability
+	 */
+	T getUpperBound() {
+		return upper;
+	}
+
+	/*!
+	 * Sets the child node
+	 *
+	 * @param pathFormula the path formula that becomes the new child node
+	 */
+	void setPathFormula(PCTLPathFormula<T>* pathFormula) {
+		this->pathFormula = pathFormula;
+	}
+
+	/*!
+	 * Sets the interval in which the probability that the path formula holds may lie.
+	 *
+	 * @param lowerBound The lower bound for the probability
+	 * @param upperBound The upper bound for the probability
+	 */
+	void setInterval(T lowerBound, T upperBound) {
+		this->lower = lowerBound;
+		this->upper = upperBound;
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() {
+		std::string result = "(";
+		result += " P[";
+		result += lower;
+		result += ";";
+		result += upper;
+		result += "] ";
+		result += pathFormula->toString();
+		result += ")";
+		return result;
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new AND-object that is identical the called object.
+	 */
+	virtual PCTLStateFormula<T>* clone() {
+		ProbabilisticOperator<T>* result = new ProbabilisticOperator<T>();
+		result->setInterval(lower, upper);
+		if (pathFormula != NULL) {
+			result->setPathFormula(pathFormula->clone());
+		}
+		return result;
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
+	 */
+	virtual mrmc::storage::BitVector *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
+	  return modelChecker->checkProbabilisticOperator(this);
+	}
+
+private:
+	T lower;
+	T upper;
+	PCTLPathFormula<T>* pathFormula;
 };
 
 } //namespace formula
diff --git a/src/formula/Until.h b/src/formula/Until.h
index d12f6ed78..df80ee0e0 100644
--- a/src/formula/Until.h
+++ b/src/formula/Until.h
@@ -15,49 +15,138 @@ namespace mrmc {
 
 namespace formula {
 
-class Until : public PCTLPathFormula {
-      PCTLStateFormula* left;
-      PCTLStateFormula* right;
-   public:
-      Until() {
-         this->left = NULL;
-         this->right = NULL;
-      }
-
-      Until(PCTLStateFormula* left, PCTLStateFormula* right) {
-         this->left = left;
-         this->right = right;
-      }
-      virtual ~Until();
-
-      void setLeft(PCTLStateFormula* newLeft) {
-         left = newLeft;
-      }
-
-      void setRight(PCTLStateFormula* newRight) {
-         right = newRight;
-      }
-
-      PCTLStateFormula* getLeft() {
-         return left;
-      }
-
-      PCTLStateFormula* getRight() {
-         return right;
-      }
-
-      std::string toString() {
-         std::string result = "(";
-         result += left->toString();
-         result += " U ";
-         result += right->toString();
-         result += ")";
-         return result;
-      }
-
-      virtual enum pathFormulaTypes type() {
-            return UNTIL;
-      }
+/*!
+ * @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
+ * The formula holds iff eventually, formula \e right (the right subtree) holds, and before,
+ * \e left holds always.
+ *
+ * The subtrees are seen as part of the object and deleted with the object
+ * (this behavior can be prevented by setting them to NULL before deletion)
+ *
+ * @see PCTLPathFormula
+ * @see PCTLFormula
+ */
+template <class T>
+class Until : public PCTLPathFormula<T> {
+
+public:
+	/*!
+	 * Empty constructor
+	 */
+	Until() {
+		this->left = NULL;
+		this->right = NULL;
+	}
+
+	/*!
+	 * Constructor
+	 *
+	 * @param left The left formula subtree
+	 * @param right The left formula subtree
+	 */
+	Until(PCTLStateFormula<T>* left, PCTLStateFormula<T>* right) {
+		this->left = left;
+		this->right = right;
+	}
+
+	/*!
+	 * Destructor.
+	 *
+	 * Also deletes the subtrees.
+	 * (this behaviour can be prevented by setting the subtrees to NULL before deletion)
+	 */
+	virtual ~Until() {
+	  if (left != NULL) {
+		  delete left;
+	  }
+	  if (right != NULL) {
+		  delete right;
+	  }
+	}
+
+	/*!
+	 * Sets the left child node.
+	 *
+	 * @param newLeft the new left child.
+	 */
+	void setLeft(PCTLStateFormula<T>* newLeft) {
+		left = newLeft;
+	}
+
+	/*!
+	 * Sets the right child node.
+	 *
+	 * @param newRight the new right child.
+	 */
+	void setRight(PCTLStateFormula<T>* newRight) {
+		right = newRight;
+	}
+
+	/*!
+	 * @returns a pointer to the left child node
+	 */
+	PCTLStateFormula<T>* getLeft() {
+		return left;
+	}
+
+	/*!
+	 * @returns a pointer to the right child node
+	 */
+	PCTLStateFormula<T>* getRight() {
+		return right;
+	}
+
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() {
+		std::string result = "(";
+		result += left->toString();
+		result += " U ";
+		result += right->toString();
+		result += ")";
+		return result;
+	}
+
+	/*!
+	 * Clones the called object.
+	 *
+	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 *
+	 * @returns a new BoundedUntil-object that is identical the called object.
+	 */
+	virtual PCTLPathFormula<T>* clone() {
+		Until<T>* result = new Until();
+		if (left != NULL) {
+			result->setLeft(left->clone());
+		}
+		if (right != NULL) {
+			result->setRight(right->clone());
+		}
+		return result;
+	}
+
+	/*!
+	 * Calls the model checker to check this formula.
+	 * Needed to infer the correct type of formula class.
+	 *
+	 * @note This function should only be called in a generic check function of a model checker class. For other uses,
+	 *       the methods of the model checker should be used.
+	 *
+	 * @returns A vector indicating the probability that the formula holds for each state.
+	 */
+	virtual std::vector<T> *check(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
+	  return modelChecker->checkUntil(this);
+	}
+
+private:
+	PCTLStateFormula<T>* left;
+	PCTLStateFormula<T>* right;
 };
 
 } //namespace formula
diff --git a/src/formula/formulaTypes.h b/src/formula/formulaTypes.h
deleted file mode 100644
index 41f245fa3..000000000
--- a/src/formula/formulaTypes.h
+++ /dev/null
@@ -1,27 +0,0 @@
-/*
- * formulaTypes.h
- *
- *  Created on: 21.10.2012
- *      Author: Thomas Heinemann
- */
-
-#ifndef FORMULATYPES_H_
-#define FORMULATYPES_H_
-
-enum stateFormulaTypes {
-      AND,
-      AP,
-      NOT,
-      OR,
-      PROBABILISTIC
-};
-
-enum pathFormulaTypes {
-      NEXT,
-      UNTIL,
-      BOUNDED_UNTIL,
-      EVENTUALLY,
-      ALWAYS
-};
-
-#endif /* FORMULATYPES_H_ */
diff --git a/src/modelChecker/DtmcPrctlModelChecker.cpp b/src/modelChecker/DtmcPrctlModelChecker.cpp
index d308005cf..f5a884921 100644
--- a/src/modelChecker/DtmcPrctlModelChecker.cpp
+++ b/src/modelChecker/DtmcPrctlModelChecker.cpp
@@ -12,8 +12,8 @@ namespace mrmc {
 namespace modelChecker {
 
 template<class T>
-DtmcPrctlModelChecker<T>::DtmcPrctlModelChecker(mrmc::models::Dtmc<T>* DTMC) {
-   this->DTMC = DTMC;
+DtmcPrctlModelChecker<T>::DtmcPrctlModelChecker(mrmc::models::Dtmc<T>* dtmc) {
+   this->dtmc = dtmc;
 }
 
 template<class T>
@@ -21,6 +21,11 @@ DtmcPrctlModelChecker<T>::~DtmcPrctlModelChecker() {
    delete this->dtmc;
 }
 
+template<class T>
+DtmcPrctlModelChecker<T>::DtmcPrctlModelChecker(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker) {
+	this->dtmc = new mrmc::models::Dtmc<T>(modelChecker->getDtmc());
+}
+
 
 } //namespace modelChecker
 
diff --git a/src/modelChecker/DtmcPrctlModelChecker.h b/src/modelChecker/DtmcPrctlModelChecker.h
index 9a7a7be01..3061dc75b 100644
--- a/src/modelChecker/DtmcPrctlModelChecker.h
+++ b/src/modelChecker/DtmcPrctlModelChecker.h
@@ -8,6 +8,24 @@
 #ifndef DTMCPRCTLMODELCHECKER_H_
 #define DTMCPRCTLMODELCHECKER_H_
 
+namespace mrmc {
+
+namespace modelChecker {
+
+/* The formula classes need to reference a model checker for the check function,
+ * which is used to infer the correct type of formula,
+ * so the model checker class is declared here already.
+ *
+ */
+template <class T>
+class DtmcPrctlModelChecker;
+}
+
+}
+
+#include "src/formula/PCTLPathFormula.h"
+#include "src/formula/PCTLStateFormula.h"
+
 #include "src/formula/And.h"
 #include "src/formula/AP.h"
 #include "src/formula/BoundedUntil.h"
@@ -25,65 +43,156 @@ 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:
-      mrmc::models::Dtmc<T>* getDtmc() const {
-         return this->dtmc;
-      }
-
-   public:
-      explicit DtmcPrctlModelChecker(mrmc::models::Dtmc<T>* DTMC);
-      ~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;
-
-      virtual mrmc::storage::BitVector checkStateFormula(mrmc::formula::PCTLStateFormula* formula) {
-         if (formula->type() == AND) {
-            return checkAnd(static_cast<mrmc::formula::And*>(formula));
-         }
-         if (formula->type() == stateFormulaTypes::AP) {
-            return checkAP(static_cast<mrmc::formula::AP*>(formula));
-         }
-         if (formula->type() == NOT) {
-            return checkNot(static_cast<mrmc::formula::Not*>(formula));
-         }
-         if (formula->type() == OR) {
-            return checkOr(static_cast<mrmc::formula::Or*>(formula));
-         }
-         if (formula->type() == PROBABILISTIC) {
-            return checkProbabilisticOperator(
-                  static_cast<mrmc::formula::ProbabilisticOperator<T>*>(formula));
-         }
-      }
-
-
-      virtual mrmc::storage::BitVector checkAnd(mrmc::formula::And*) = 0;
-      virtual mrmc::storage::BitVector checkAP(mrmc::formula::AP*) = 0;
-      virtual mrmc::storage::BitVector checkNot(mrmc::formula::Not*) = 0;
-      virtual mrmc::storage::BitVector checkOr(mrmc::formula::Or*) = 0;
-      virtual mrmc::storage::BitVector checkProbabilisticOperator(mrmc::formula::ProbabilisticOperator<T>*) = 0;
-
-      virtual std::vector<T> checkPathFormula(mrmc::formula::PCTLPathFormula* formula) {
-         if (formula->type() == NEXT) {
-            return checkNext(static_cast<mrmc::formula::Next*>(formula));
-         }
-         if (formula->type() == UNTIL) {
-            return checkUntil(static_cast<mrmc::formula::Until*>(formula));
-         }
-         if (formula->type() == BOUNDED_UNTIL) {
-            return checkBoundedUntil(static_cast<mrmc::formula::BoundedUntil*>(formula));
-         }
-      }
-
-      virtual std::vector<T> checkBoundedUntil(mrmc::formula::BoundedUntil*) = 0;
-      virtual std::vector<T> checkNext(mrmc::formula::Next*) = 0;
-      virtual std::vector<T> checkUntil(mrmc::formula::Until*) = 0;
+public:
+	/*!
+	 * Constructor
+	 *
+	 * @param Dtmc The dtmc model which is checked.
+	 */
+	explicit DtmcPrctlModelChecker(mrmc::models::Dtmc<T>* Dtmc);
+
+	/*!
+	 * Copy constructor
+	 *
+	 * @param modelChecker The model checker that is copied.
+	 */
+	explicit DtmcPrctlModelChecker(mrmc::modelChecker::DtmcPrctlModelChecker<T>* modelChecker);
+
+	/*!
+	 * Destructor
+	 */
+	virtual ~DtmcPrctlModelChecker();
+
+	/*!
+	 * @returns A reference to the dtmc of the model checker.
+	 */
+	mrmc::models::Dtmc<T>* getDtmc() const {
+		return this->dtmc;
+	}
+
+	/*!
+	 * 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);
+	}
+
+	/*!
+	 * 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>* formula) = 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>* formula) = 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>* formula) = 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>* formula) = 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>* formula) = 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>* formula) = 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>* formula) = 0;
+
+private:
+	mrmc::models::Dtmc<T>* dtmc;
 };
 
 } //namespace modelChecker
diff --git a/src/models/AtomicPropositionsLabeling.h b/src/models/AtomicPropositionsLabeling.h
index 2f051cf9b..0ed215a86 100644
--- a/src/models/AtomicPropositionsLabeling.h
+++ b/src/models/AtomicPropositionsLabeling.h
@@ -133,6 +133,26 @@ public:
 		this->singleLabelings[nameToLabelingMap[ap]]->set(state, true);
 	}
 
+	/*!
+	 * Creates a list of atomic propositions for a given state
+	 * @param state The index of a state
+	 * @returns The list of propositions for the given state
+	 */
+	std::set<std::string> getPropositionsForState(uint_fast32_t state) {
+		if (state >= stateCount) {
+			throw std::out_of_range("State index out of range.");
+		}
+		std::set<std::string> result;
+		for (auto it = nameToLabelingMap.begin();
+					 it != nameToLabelingMap.end();
+					 it++) {
+			if (stateHasAtomicProposition(it->first, state)) {
+				result.insert(it->first);
+			}
+		}
+		return result;
+	}
+
 	/*!
 	 * Checks whether a given state is labeled with the given atomic proposition.
 	 * @param ap The name of the atomic proposition.
diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h
index 6edd0272e..8ac46ffee 100644
--- a/src/models/Dtmc.h
+++ b/src/models/Dtmc.h
@@ -106,6 +106,13 @@ public:
 		return this->probabilityMatrix;
 	}
 
+	/*!
+	 *
+	 */
+	std::set<std::string> getPropositionsForState(uint_fast32_t state) {
+		return stateLabeling->getPropositionsForState(state);
+	}
+
 	/*!
 	 * Retrieves a reference to the backwards transition relation.
 	 * @return A reference to the backwards transition relation.
diff --git a/src/parser/parser.cpp b/src/parser/parser.cpp
index 5c776a316..403ff6fd9 100644
--- a/src/parser/parser.cpp
+++ b/src/parser/parser.cpp
@@ -7,9 +7,9 @@
 
 #include <sys/stat.h>
 #include <fcntl.h>
-#if defined MACOSX
+//#if defined MACOSX
 	#include <unistd.h>
-#endif
+//#endif
 #include <errno.h>
 #include <iostream>
 #include <cstring>
diff --git a/src/parser/readPrctlFile.cpp b/src/parser/readPrctlFile.cpp
index 40aa6deb4..8e7d216b9 100644
--- a/src/parser/readPrctlFile.cpp
+++ b/src/parser/readPrctlFile.cpp
@@ -61,7 +61,7 @@ namespace
 		/*!
 		 *	@brief Resulting formula.
 		 */
-		mrmc::formula::PCTLFormula* result;
+		mrmc::formula::PCTLFormula<double>* result;
 		
 		struct dump
 		{
@@ -106,7 +106,7 @@ namespace
 	};
 }
 
-mrmc::formula::PCTLFormula* mrmc::parser::readPrctlFile(const char* filename)
+mrmc::formula::PCTLFormula<double>* mrmc::parser::readPrctlFile(const char* filename)
 {
 	PRCTLParser p;
 	mrmc::parser::MappedFile file(filename);
diff --git a/src/parser/readPrctlFile.h b/src/parser/readPrctlFile.h
index 80393482d..7a4bc1a5b 100644
--- a/src/parser/readPrctlFile.h
+++ b/src/parser/readPrctlFile.h
@@ -9,7 +9,7 @@ namespace parser {
 /*!
  *	@brief Load PRCTL file
  */
-mrmc::formula::PCTLFormula* readPrctlFile(const char * filename);
+mrmc::formula::PCTLFormula<double>* readPrctlFile(const char * filename);
 
 } // namespace parser
 } // namespace mrmc
diff --git a/src/utility/utility.cpp b/src/utility/utility.cpp
index 783ee9120..e2ef43833 100644
--- a/src/utility/utility.cpp
+++ b/src/utility/utility.cpp
@@ -9,70 +9,57 @@
 #include "src/parser/readTraFile.h"
 #include "src/parser/readLabFile.h"
 
+#include <fstream>
+
 namespace mrmc {
 
 namespace utility {
 
-void dtmcToDot(mrmc::models::Dtmc<double>* dtmc, const char* filename) {
-	//FIXME: adapt this to the refactored names
-	//FIXME: use C++-style for file output here, as performance is not critical here
-/*   FILE *P;
-   mrmc::sparse::StaticSparseMatrix<double>* matrix = dtmc->getTransitions();
-   mrmc::dtmc::Labeling* labels = dtmc->getLabels();
-
-   uint_fast64_t* row_indications = matrix->getRowIndications();
-   uint_fast64_t* column_indications = matrix->getColumnIndications();
-   double* value_storage = matrix->getStoragePointer();
-   double* diagonal_storage = matrix->getDiagonalStorage();
+void dtmcToDot(mrmc::models::Dtmc<double>* dtmc, std::string filename) {
+   mrmc::storage::SquareSparseMatrix<double>* matrix = dtmc->getTransitionProbabilityMatrix();
+   double* diagonal_storage = matrix->getDiagonalStoragePointer();
 
-   P = fopen(filename, "w");
+   std::ofstream file;
+   file.open(filename);
 
-   if (P == NULL) {
-      pantheios::log_ERROR("File could not be opened.");
-      throw mrmc::exceptions::file_IO_exception();
-   }
-
-   fprintf(P, "digraph dtmc {\n");
+   file << "digraph dtmc {\n";
 
    //Specify the nodes and their labels
-   for (uint_fast64_t i = 1; i <= dtmc->getNodeCount(); i++) {
-      fprintf(P, "\t%Lu[label=\"%Lu\\n{", i, i);
+   for (uint_fast64_t i = 1; i < dtmc->getNumberOfStates(); i++) {
+      file << "\t" << i << "[label=\"" << i << "\\n{";
       char komma=' ';
-      for(auto it = labels->getPropositionMap()->begin();
-               it != labels->getPropositionMap()->end();
+      std::set<std::string> propositions = dtmc->getPropositionsForState(i);
+      for(auto it = propositions.begin();
+               it != propositions.end();
                it++) {
-         if(labels->nodeHasProposition(it->first, i)) {
-            fprintf(P, "%c%s", komma, (it->first).c_str());
-         }
-         char komma=',';
+      	file << komma << *it;
+         komma=',';
       }
 
-      fprintf(P, " }\"];\n");
-   }
+      file << " }\"];\n";
 
-   uint_fast64_t row = 0;
-
-   for (uint_fast64_t i = 0; i < matrix->getNonZeroEntryCount(); i++ ) {
-      //Check whether we have to switch to the new row
-      while (row_indications[row] <= i) {
-         ++row;
-         //write diagonal entry/self loop first
-         if (diagonal_storage[row] != 0) {
-            fprintf(P, "\t%Lu -> %Lu [label=%f]\n",
-                  row, row, diagonal_storage[row]);
-         }
-      }
-      fprintf(P, "\t%Lu -> %Lu [label=%f]\n",
-            row, column_indications[i], value_storage[i]);
    }
 
+   for (uint_fast64_t row = 0; row < dtmc->getNumberOfStates(); row++ ) {
+   	//write diagonal entry/self loop first
+   	if (diagonal_storage[row] != 0) {
+   	            file << "\t" << row << " -> " << row << " [label=" << diagonal_storage[row] <<"]\n";
+   	         }
+   	//Then, iterate through the row and write each non-diagonal value into the file
+   	for (	auto it = matrix->beginConstColumnNoDiagIterator(row);
+   			it !=  matrix->endConstColumnNoDiagIterator(row);
+   			it++) {
+   		double value = 0;
+   		matrix->getValue(row,*it,&value);
+   		file << "\t" << row << " -> " << *it << " [label=" << value << "]\n";
+   	}
+   }
 
-
-   fprintf(P, "}\n");
-
-   fclose(P); */
+   file << "}\n";
+   file.close();
 }
 
+//TODO: Should this stay here or be integrated in the new parser structure?
 mrmc::models::Dtmc<double>* parseDTMC(const char* tra_file, const char* lab_file) {
 	mrmc::parser::TraParser tp(tra_file);
 	uint_fast64_t node_count = tp.getMatrix()->getRowCount();
diff --git a/src/utility/utility.h b/src/utility/utility.h
index 65eb9113f..ebfa964b7 100644
--- a/src/utility/utility.h
+++ b/src/utility/utility.h
@@ -25,7 +25,7 @@ namespace utility {
                      it will be overwritten.
 
  */
-void dtmcToDot(mrmc::models::Dtmc<double>* dtmc, const char* filename);
+void dtmcToDot(mrmc::models::Dtmc<double>* dtmc, std::string filename);
 
 /*!
     Parses a transition file and a labeling file and produces a DTMC out of them.
diff --git a/test/parser/parse_dtmc_test.cpp b/test/parser/parse_dtmc_test.cpp
new file mode 100644
index 000000000..e89ec331e
--- /dev/null
+++ b/test/parser/parse_dtmc_test.cpp
@@ -0,0 +1,24 @@
+/*
+ * parse_dtmc_test.cpp
+ *
+ *  Created on: 03.12.2012
+ *      Author: Thomas Heinemann
+ */
+
+
+#include "gtest/gtest.h"
+#include "mrmc-config.h"
+#include "src/utility/utility.h"
+
+TEST(ParseDtmcTest, parseAndOutput) {
+	mrmc::models::Dtmc<double>* myDtmc;
+	ASSERT_NO_THROW(myDtmc = mrmc::utility::parseDTMC(
+			MRMC_CPP_TESTS_BASE_PATH "/parser/tra_files/pctl_general_input_01.tra",
+			MRMC_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab"));
+
+	ASSERT_NO_THROW(mrmc::utility::dtmcToDot(myDtmc, MRMC_CPP_TESTS_BASE_PATH "/parser/output.dot"));
+
+	delete myDtmc;
+}
+
+
diff --git a/test/parser/read_tra_file_test.cpp b/test/parser/read_tra_file_test.cpp
index 9aad2b927..d8cf64c8e 100644
--- a/test/parser/read_tra_file_test.cpp
+++ b/test/parser/read_tra_file_test.cpp
@@ -12,6 +12,8 @@
 #include "src/exceptions/file_IO_exception.h"
 #include "src/exceptions/wrong_file_format.h"
 
+#include "src/utility/utility.h"
+
 TEST(ReadTraFileTest, NonExistingFileTest) {
    //No matter what happens, please don't create a file with the name "nonExistingFile.not"! :-)
    ASSERT_THROW(mrmc::parser::TraParser(MRMC_CPP_TESTS_BASE_PATH "/nonExistingFile.not"), mrmc::exceptions::file_IO_exception);
@@ -61,8 +63,6 @@ TEST(ReadTraFileTest, ParseFileTest1) {
 		ASSERT_TRUE(result->getValue(4,4,&val));
 		ASSERT_EQ(val,0);
 
-		// FIXME: adapt this test case to the new dot-output routines
-		/* result->toDOTFile("output.dot"); */
 		delete result;
 		delete parser;
 	} else {