diff --git a/src/formula/abstract/AbstractFormula.h b/src/formula/abstract/AbstractFormula.h
index b7f453fcb..0d41d4450 100644
--- a/src/formula/abstract/AbstractFormula.h
+++ b/src/formula/abstract/AbstractFormula.h
@@ -32,7 +32,7 @@ namespace abstract {
  *	@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
- * 	   AbstractPathFormula and AbstractStateFormula offer the method clone().
+ * 	   AbstractFormula and AbstractFormula offer the method clone().
  *
  *	This is the base class for every formula class in every logic.
  */
diff --git a/src/formula/abstract/And.h b/src/formula/abstract/And.h
index 1bdbca9ed..e1b3a07c4 100644
--- a/src/formula/abstract/And.h
+++ b/src/formula/abstract/And.h
@@ -15,26 +15,7 @@
 
 namespace storm {
 namespace formula {
-
-template <class T> class And;
-
-/*!
- *	@brief Interface class for model checkers that support And.
- *
- *	All model checkers that support the formula class And must inherit
- *	this pure virtual class.
- */
-template <class T>
-class IAndModelChecker {
-	public:
-		/*!
-		 *	@brief Evaluates And formula within a model checker.
-		 *
-		 *	@param obj Formula object with subformulas.
-		 *	@return Result of the formula for every node.
-		 */
-		virtual storm::storage::BitVector* checkAnd(const And<T>& obj) const = 0;
-};
+namespace abstract {
 
 /*!
  * @brief
@@ -48,7 +29,7 @@ class IAndModelChecker {
  * 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 AbstractStateFormula
+ * @see AbstractFormula
  * @see AbstractFormula
  */
 template <class T>
@@ -91,12 +72,35 @@ public:
 		}
 	}
 
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const {
+		std::string result = "(";
+		result += left->toString();
+		result += " & ";
+		result += right->toString();
+		result += ")";
+		return result;
+	}
+
+	/*!
+	 *	@brief Checks if all subtrees conform to some logic.
+	 *
+	 *	@param checker Formula checker object.
+	 *	@return true iff all subtrees conform to some logic.
+	 */
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+        return checker.conforms(this->left) && checker.conforms(this->right);
+    }
+
+protected:
 	/*!
 	 * Sets the left child node.
 	 *
 	 * @param newLeft the new left child.
 	 */
-	void setLeft(AbstractStateFormula<T>* newLeft) {
+	void setLeft(AbstractFormula<T>* newLeft) {
 		left = newLeft;
 	}
 
@@ -105,82 +109,31 @@ public:
 	 *
 	 * @param newRight the new right child.
 	 */
-	void setRight(AbstractStateFormula<T>* newRight) {
+	void setRight(AbstractFormula<T>* newRight) {
 		right = newRight;
 	}
 
 	/*!
 	 * @returns a pointer to the left child node
 	 */
-	const AbstractStateFormula<T>& getLeft() const {
+	const AbstractFormula<T>& getLeft() const {
 		return *left;
 	}
 
 	/*!
 	 * @returns a pointer to the right child node
 	 */
-	const AbstractStateFormula<T>& getRight() const {
+	const AbstractFormula<T>& getRight() const {
 		return *right;
 	}
 
-	/*!
-	 * @returns a string representation of the formula
-	 */
-	virtual std::string toString() const {
-		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 AbstractStateFormula<T>* clone() const {
-		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 storm::storage::BitVector* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
-		return modelChecker.template as<IAndModelChecker>()->checkAnd(*this);
-	}
-	
-	/*!
-	 *	@brief Checks if all subtrees conform to some logic.
-	 *
-	 *	@param checker Formula checker object.
-	 *	@return true iff all subtrees conform to some logic.
-	 */
-	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
-        return checker.conforms(this->left) && checker.conforms(this->right);
-    }
-
 private:
 	AbstractFormula<T>* left;
 	AbstractFormula<T>* right;
 };
 
+} //namespace abstract
+
 } //namespace formula
 
 } //namespace storm
diff --git a/src/formula/abstract/Ap.h b/src/formula/abstract/Ap.h
index 0cb0d2480..6378719c4 100644
--- a/src/formula/abstract/Ap.h
+++ b/src/formula/abstract/Ap.h
@@ -5,35 +5,16 @@
  *      Author: Thomas Heinemann
  */
 
-#ifndef STORM_FORMULA_AP_H_
-#define STORM_FORMULA_AP_H_
+#ifndef STORM_FORMULA_ABSTRACT_AP_H_
+#define STORM_FORMULA_ABSTRACT_AP_H_
 
-#include "src/formula/AbstractStateFormula.h"
+#include "src/formula/abstract/AbstractFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelchecker/ForwardDeclarations.h"
 
 namespace storm {
 namespace formula {
-
-template <class T> class Ap;
-
-/*!
- *  @brief Interface class for model checkers that support Ap.
- *
- *  All model checkers that support the formula class Ap must inherit
- *  this pure virtual class.
- */
-template <class T>
-class IApModelChecker {
-    public:
-		/*!
-         *  @brief Evaluates Ap formula within a model checker.
-         *
-         *  @param obj Formula object with subformulas.
-         *  @return Result of the formula for every node.
-         */
-        virtual storm::storage::BitVector* checkAp(const Ap<T>& obj) const = 0;
-};
+namespace abstract {
 
 /*!
  * @brief
@@ -41,11 +22,11 @@ class IApModelChecker {
  *
  * This class represents the leaves in the formula tree.
  *
- * @see AbstractStateFormula
+ * @see AbstractFormula
  * @see AbstractFormula
  */
 template <class T>
-class Ap : public AbstractStateFormula<T> {
+class Ap : public AbstractFormula<T> {
 
 public:
 	/*!
@@ -79,28 +60,6 @@ public:
 	virtual std::string toString() const {
 		return getAp();
 	}
-
-	/*!
-	 * Clones the called object.
-	 *
-	 * @returns a new Ap-object that is identical the called object.
-	 */
-	virtual AbstractStateFormula<T>* clone() const {
-	  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 storm::storage::BitVector *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
-		return modelChecker.template as<IApModelChecker>()->checkAp(*this);
-	}
 	
 	/*!
      *  @brief Checks if all subtrees conform to some logic.
@@ -118,8 +77,10 @@ private:
 	std::string ap;
 };
 
+} //namespace abstract
+
 } //namespace formula
 
 } //namespace storm
 
-#endif /* STORM_FORMULA_AP_H_ */
+#endif /* STORM_FORMULA_ABSTRACT_ABSTRCT_AP_H_ */
diff --git a/src/formula/abstract/BoundedEventually.h b/src/formula/abstract/BoundedEventually.h
index 33c42f1ba..3753fbab3 100644
--- a/src/formula/abstract/BoundedEventually.h
+++ b/src/formula/abstract/BoundedEventually.h
@@ -5,11 +5,10 @@
  *      Author: Christian Dehnert
  */
 
-#ifndef STORM_FORMULA_BOUNDEDEVENTUALLY_H_
-#define STORM_FORMULA_BOUNDEDEVENTUALLY_H_
+#ifndef STORM_FORMULA_ABSTRACT_BOUNDEDEVENTUALLY_H_
+#define STORM_FORMULA_ABSTRACT_BOUNDEDEVENTUALLY_H_
 
-#include "src/formula/AbstractPathFormula.h"
-#include "src/formula/AbstractStateFormula.h"
+#include "src/formula/abstract/AbstractFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include "boost/integer/integer_mask.hpp"
 #include <string>
@@ -19,25 +18,7 @@ namespace storm {
 
 namespace formula {
 
-template <class T> class BoundedEventually;
-
-/*!
- *  @brief Interface class for model checkers that support BoundedEventually.
- *   
- *  All model checkers that support the formula class BoundedEventually must inherit
- *  this pure virtual class.
- */
-template <class T>
-class IBoundedEventuallyModelChecker {
-    public:
-		/*!
-         *  @brief Evaluates BoundedEventually formula within a model checker.
-         *
-         *  @param obj Formula object with subformulas.
-         *  @return Result of the formula for every node.
-         */
-        virtual std::vector<T>* checkBoundedEventually(const BoundedEventually<T>& obj, bool qualitative) const = 0;
-};
+namespace abstract {
 
 /*!
  * @brief
@@ -51,11 +32,11 @@ class IBoundedEventuallyModelChecker {
  * 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 AbstractPathFormula
+ * @see AbstractFormula
  * @see AbstractFormula
  */
 template <class T>
-class BoundedEventually : public AbstractPathFormula<T> {
+class BoundedEventually : public AbstractFormula<T> {
 
 public:
 	/*!
@@ -72,7 +53,7 @@ public:
 	 * @param child The child formula subtree
 	 * @param bound The maximal number of steps
 	 */
-	BoundedEventually(AbstractStateFormula<T>* child, uint_fast64_t bound) {
+	BoundedEventually(AbstractFormula<T>* child, uint_fast64_t bound) {
 		this->child = child;
 		this->bound = bound;
 	}
@@ -89,21 +70,6 @@ public:
 	  }
 	}
 
-	/*!
-	 * @returns the child node
-	 */
-	const AbstractStateFormula<T>& getChild() const {
-		return *child;
-	}
-
-	/*!
-	 * Sets the subtree
-	 * @param child the new child node
-	 */
-	void setChild(AbstractStateFormula<T>* child) {
-		this->child = child;
-	}
-
 	/*!
 	 * @returns the maximally allowed number of steps for the bounded until operator
 	 */
@@ -130,36 +96,6 @@ public:
 		result += child->toString();
 		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 AbstractPathFormula<T>* clone() const {
-		BoundedEventually<T>* result = new BoundedEventually<T>();
-		result->setBound(bound);
-		if (child != nullptr) {
-			result->setChild(child->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(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
-		return modelChecker.template as<IBoundedEventuallyModelChecker>()->checkBoundedEventually(*this, qualitative);
-	}
 	
 	/*!
      *  @brief Checks if the subtree conforms to some logic.
@@ -171,13 +107,32 @@ public:
 		return checker.conforms(this->child);
 	}
 
+protected:
+	/*!
+	 * @returns the child node
+	 */
+	const AbstractFormula<T>& getChild() const {
+		return *child;
+	}
+
+	/*!
+	 * Sets the subtree
+	 * @param child the new child node
+	 */
+	void setChild(AbstractFormula<T>* child) {
+		this->child = child;
+	}
+
+
 private:
-	AbstractStateFormula<T>* child;
+	AbstractFormula<T>* child;
 	uint_fast64_t bound;
 };
 
+} //namespace abstract
+
 } //namespace formula
 
 } //namespace storm
 
-#endif /* STORM_FORMULA_BOUNDEDUNTIL_H_ */
+#endif /* STORM_FORMULA_ABSTRACT_BOUNDEDEVENTUALLY_H_ */
diff --git a/src/formula/abstract/BoundedNaryUntil.h b/src/formula/abstract/BoundedNaryUntil.h
index 9f83df869..63594ff0e 100644
--- a/src/formula/abstract/BoundedNaryUntil.h
+++ b/src/formula/abstract/BoundedNaryUntil.h
@@ -5,11 +5,10 @@
  *      Author: Thomas Heinemann
  */
 
-#ifndef STORM_FORMULA_BOUNDEDNARYUNTIL_H_
-#define STORM_FORMULA_BOUNDEDNARYUNTIL_H_
+#ifndef STORM_FORMULA_ABSTRACT_BOUNDEDNARYUNTIL_H_
+#define STORM_FORMULA_ABSTRACT_BOUNDEDNARYUNTIL_H_
 
-#include "src/formula/AbstractPathFormula.h"
-#include "src/formula/AbstractStateFormula.h"
+#include "src/formula/abstract/AbstractFormula.h"
 #include "boost/integer/integer_mask.hpp"
 #include <string>
 #include <vector>
@@ -19,26 +18,7 @@
 
 namespace storm {
 namespace formula {
-
-template <class T> class BoundedNaryUntil;
-
-/*!
- *  @brief Interface class for model checkers that support BoundedNaryUntil.
- *   
- *  All model checkers that support the formula class BoundedNaryUntil must inherit
- *  this pure virtual class.
- */
-template <class T>
-class IBoundedNaryUntilModelChecker {
-    public:
-		/*!
-         *  @brief Evaluates BoundedNaryUntil formula within a model checker.
-         *
-         *  @param obj Formula object with subformulas.
-         *  @return Result of the formula for every node.
-         */
-        virtual std::vector<T>* checkBoundedNaryUntil(const BoundedNaryUntil<T>& obj, bool qualitative) const = 0;
-};
+namespace abstract {
 
 /*!
  * @brief
@@ -56,11 +36,11 @@ class IBoundedNaryUntilModelChecker {
  * 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 AbstractPathFormula
+ * @see AbstractFormula
  * @see AbstractFormula
  */
 template <class T>
-class BoundedNaryUntil : public AbstractPathFormula<T> {
+class BoundedNaryUntil : public AbstractFormula<T> {
 
 public:
 	/*!
@@ -68,7 +48,7 @@ public:
 	 */
 	BoundedNaryUntil() {
 		this->left = nullptr;
-		this->right = new std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>();
+		this->right = new std::vector<std::tuple<AbstractFormula<T>*,T,T>>();
 	}
 
 	/*!
@@ -77,7 +57,7 @@ public:
 	 * @param left The left formula subtree
 	 * @param right The left formula subtree
 	 */
-	BoundedNaryUntil(AbstractStateFormula<T>* left, std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>* right) {
+	BoundedNaryUntil(AbstractFormula<T>* left, std::vector<std::tuple<AbstractFormula<T>*,T,T>>* right) {
 		this->left = left;
 		this->right = right;
 	}
@@ -97,16 +77,44 @@ public:
 	  }
 	}
 
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const {
+		std::stringstream result;
+		result << "( " << left->toString();
+		for (auto it = this->right->begin(); it != this->right->end(); ++it) {
+			result << " U[" << std::get<1>(*it) << "," << std::get<2>(*it) << "] " << std::get<0>(*it)->toString();
+		}
+		result << ")";
+		return result.str();
+	}
+
+	/*!
+     *  @brief Checks if all subtrees conform to some logic.
+     *
+     *  @param checker Formula checker object.
+     *  @return true iff all subtrees conform to some logic.
+     */
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+		bool res = checker.conforms(this->left);
+		for (auto it = this->right->begin(); it != this->right->end(); ++it) {
+			res &= checker.conforms(std::get<0>(*it));
+		}
+		return res;
+	}
+
+protected:
 	/*!
 	 * Sets the left child node.
 	 *
 	 * @param newLeft the new left child.
 	 */
-	void setLeft(AbstractStateFormula<T>* newLeft) {
+	void setLeft(AbstractFormula<T>* newLeft) {
 		left = newLeft;
 	}
 
-	void setRight(std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>* newRight) {
+	void setRight(std::vector<std::tuple<AbstractFormula<T>*,T,T>>* newRight) {
 		right = newRight;
 	}
 
@@ -116,93 +124,32 @@ public:
 	 *
 	 * @param newRight the new right child.
 	 */
-	void addRight(AbstractStateFormula<T>* newRight, T upperBound, T lowerBound) {
-		this->right->push_back(std::tuple<AbstractStateFormula<T>*,T,T>(newRight, upperBound, lowerBound));
+	void addRight(AbstractFormula<T>* newRight, T upperBound, T lowerBound) {
+		this->right->push_back(std::tuple<AbstractFormula<T>*,T,T>(newRight, upperBound, lowerBound));
 	}
 
 	/*!
 	 * @returns a pointer to the left child node
 	 */
-	const AbstractStateFormula<T>& getLeft() const {
+	const AbstractFormula<T>& getLeft() const {
 		return *left;
 	}
 
 	/*!
 	 * @returns a pointer to the right child nodes.
 	 */
-	const std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>& getRight() const {
+	const std::vector<std::tuple<AbstractFormula<T>*,T,T>>& getRight() const {
 		return *right;
 	}
 
-	/*!
-	 * @returns a string representation of the formula
-	 */
-	virtual std::string toString() const {
-		std::stringstream result;
-		result << "( " << left->toString();
-		for (auto it = this->right->begin(); it != this->right->end(); ++it) {
-			result << " U[" << std::get<1>(*it) << "," << std::get<2>(*it) << "] " << std::get<0>(*it)->toString();
-		}
-		result << ")";
-		return result.str();
-	}
-
-	/*!
-	 * 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 BoundedNaryUntil-object that is identical the called object.
-	 */
-	virtual AbstractPathFormula<T>* clone() const {
-		BoundedNaryUntil<T>* result = new BoundedNaryUntil<T>();
-		if (left != NULL) {
-			result->setLeft(left->clone());
-		}
-		if (right != NULL) {
-			std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>* newright = new std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>();
-			for (auto it = this->right->begin(); it != this->right->end(); ++it) {
-				newright->push_back(std::tuple<AbstractStateFormula<T>*,T,T>(std::get<0>(*it)->clone(), std::get<1>(*it), std::get<2>(*it)));
-			}
-			result->setRight(newright);
-		}
-		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(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
-		return modelChecker.template as<IBoundedNaryUntilModelChecker>()->checkBoundedNaryUntil(*this, qualitative);
-	}
-	
-	/*!
-     *  @brief Checks if all subtrees conform to some logic.
-     * 
-     *  @param checker Formula checker object.
-     *  @return true iff all subtrees conform to some logic.
-     */
-	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
-		bool res = checker.conforms(this->left);
-		for (auto it = this->right->begin(); it != this->right->end(); ++it) {
-			res &= checker.conforms(std::get<0>(*it));
-		}
-		return res;
-	}
 
 private:
-	AbstractStateFormula<T>* left;
-	std::vector<std::tuple<AbstractStateFormula<T>*,T,T>>* right;
+	AbstractFormula<T>* left;
+	std::vector<std::tuple<AbstractFormula<T>*,T,T>>* right;
 };
 
+} //namespace abstract
 } //namespace formula
 } //namespace storm
 
-#endif /* STORM_FORMULA_BOUNDEDNARYUNTIL_H_ */
+#endif /* STORM_FORMULA_ABSTRACT_BOUNDEDNARYUNTIL_H_ */
diff --git a/src/formula/abstract/BoundedUntil.h b/src/formula/abstract/BoundedUntil.h
index 685b1bfe1..1c57a7271 100644
--- a/src/formula/abstract/BoundedUntil.h
+++ b/src/formula/abstract/BoundedUntil.h
@@ -5,37 +5,17 @@
  *      Author: Thomas Heinemann
  */
 
-#ifndef STORM_FORMULA_BOUNDEDUNTIL_H_
-#define STORM_FORMULA_BOUNDEDUNTIL_H_
+#ifndef STORM_FORMULA_ABSTRACT_BOUNDEDUNTIL_H_
+#define STORM_FORMULA_ABSTRACT_BOUNDEDUNTIL_H_
 
-#include "src/formula/AbstractPathFormula.h"
-#include "src/formula/AbstractStateFormula.h"
+#include "src/formula/abstract/AbstractFormula.h"
 #include "boost/integer/integer_mask.hpp"
 #include <string>
 #include "src/modelchecker/ForwardDeclarations.h"
 
 namespace storm {
 namespace formula {
-
-template <class T> class BoundedUntil;
-
-/*!
- *  @brief Interface class for model checkers that support BoundedUntil.
- *   
- *  All model checkers that support the formula class BoundedUntil must inherit
- *  this pure virtual class.
- */
-template <class T>
-class IBoundedUntilModelChecker {
-    public:
-		/*!
-         *  @brief Evaluates BoundedUntil formula within a model checker.
-         *
-         *  @param obj Formula object with subformulas.
-         *  @return Result of the formula for every node.
-         */
-        virtual std::vector<T>* checkBoundedUntil(const BoundedUntil<T>& obj, bool qualitative) const = 0;
-};
+namespace abstract {
 
 /*!
  * @brief
@@ -50,11 +30,11 @@ class IBoundedUntilModelChecker {
  * 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 AbstractPathFormula
+ * @see AbstractFormula
  * @see AbstractFormula
  */
 template <class T>
-class BoundedUntil : public AbstractPathFormula<T> {
+class BoundedUntil : public AbstractFormula<T> {
 
 public:
 	/*!
@@ -73,7 +53,7 @@ public:
 	 * @param right The left formula subtree
 	 * @param bound The maximal number of steps
 	 */
-	BoundedUntil(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right,
+	BoundedUntil(AbstractFormula<T>* left, AbstractFormula<T>* right,
 					 uint_fast64_t bound) {
 		this->left = left;
 		this->right = right;
@@ -95,38 +75,6 @@ public:
 	  }
 	}
 
-	/*!
-	 * Sets the left child node.
-	 *
-	 * @param newLeft the new left child.
-	 */
-	void setLeft(AbstractStateFormula<T>* newLeft) {
-		left = newLeft;
-	}
-
-	/*!
-	 * Sets the right child node.
-	 *
-	 * @param newRight the new right child.
-	 */
-	void setRight(AbstractStateFormula<T>* newRight) {
-		right = newRight;
-	}
-
-	/*!
-	 * @returns a pointer to the left child node
-	 */
-	const AbstractStateFormula<T>& getLeft() const {
-		return *left;
-	}
-
-	/*!
-	 * @returns a pointer to the right child node
-	 */
-	const AbstractStateFormula<T>& getRight() const {
-		return *right;
-	}
-
 	/*!
 	 * @returns the maximally allowed number of steps for the bounded until operator
 	 */
@@ -154,58 +102,60 @@ public:
 		result += right->toString();
 		return result;
 	}
+	
+	/*!
+     *  @brief Checks if all subtrees conform to some logic.
+     * 
+     *  @param checker Formula checker object.
+     *  @return true iff all subtrees conform to some logic.
+     */
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+		return checker.conforms(this->left) && checker.conforms(this->right);
+	}
 
+protected:
 	/*!
-	 * Clones the called object.
-	 *
-	 * Performs a "deep copy", i.e. the subtrees of the new object are clones of the original ones
+	 * Sets the left child node.
 	 *
-	 * @returns a new BoundedUntil-object that is identical the called object.
+	 * @param newLeft the new left child.
 	 */
-	virtual AbstractPathFormula<T>* clone() const {
-		BoundedUntil<T>* result = new BoundedUntil<T>();
-		result->setBound(bound);
-		if (left != NULL) {
-			result->setLeft(left->clone());
-		}
-		if (right != NULL) {
-			result->setRight(right->clone());
-		}
-		return result;
+	void setLeft(AbstractFormula<T>* newLeft) {
+		left = newLeft;
 	}
 
-
 	/*!
-	 * 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.
+	 * Sets the right child node.
 	 *
-	 * @returns A vector indicating the probability that the formula holds for each state.
+	 * @param newRight the new right child.
 	 */
-	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
-		return modelChecker.template as<IBoundedUntilModelChecker>()->checkBoundedUntil(*this, qualitative);
+	void setRight(AbstractFormula<T>* newRight) {
+		right = newRight;
 	}
-	
+
 	/*!
-     *  @brief Checks if all subtrees conform to some logic.
-     * 
-     *  @param checker Formula checker object.
-     *  @return true iff all subtrees conform to some logic.
-     */
-	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
-		return checker.conforms(this->left) && checker.conforms(this->right);
+	 * @returns a pointer to the left child node
+	 */
+	const AbstractFormula<T>& getLeft() const {
+		return *left;
+	}
+
+	/*!
+	 * @returns a pointer to the right child node
+	 */
+	const AbstractFormula<T>& getRight() const {
+		return *right;
 	}
 
 private:
-	AbstractStateFormula<T>* left;
-	AbstractStateFormula<T>* right;
+	AbstractFormula<T>* left;
+	AbstractFormula<T>* right;
 	uint_fast64_t bound;
 };
 
+} //namespace abstract
+
 } //namespace formula
 
 } //namespace storm
 
-#endif /* STORM_FORMULA_BOUNDEDUNTIL_H_ */
+#endif /* STORM_FORMULA_ABSTRACT_BOUNDEDUNTIL_H_ */
diff --git a/src/formula/abstract/Eventually.h b/src/formula/abstract/Eventually.h
index 8db4f1b01..88be7de95 100644
--- a/src/formula/abstract/Eventually.h
+++ b/src/formula/abstract/Eventually.h
@@ -5,36 +5,17 @@
  *      Author: Christian Dehnert
  */
 
-#ifndef STORM_FORMULA_EVENTUALLY_H_
-#define STORM_FORMULA_EVENTUALLY_H_
+#ifndef STORM_FORMULA_ABSTRACT_EVENTUALLY_H_
+#define STORM_FORMULA_ABSTRACT_EVENTUALLY_H_
 
-#include "src/formula/AbstractPathFormula.h"
-#include "src/formula/AbstractStateFormula.h"
+#include "src/formula/abstract/AbstractFormula.h"
 #include "src/modelchecker/ForwardDeclarations.h"
 
 namespace storm {
 
 namespace formula {
 
-template <class T> class Eventually;
-
-/*!
- *  @brief Interface class for model checkers that support Eventually.
- *
- *  All model checkers that support the formula class Eventually must inherit
- *  this pure virtual class.
- */
-template <class T>
-class IEventuallyModelChecker {
-    public:
-		/*!
-         *  @brief Evaluates Eventually formula within a model checker.
-         *
-         *  @param obj Formula object with subformulas.
-         *  @return Result of the formula for every node.
-         */
-        virtual std::vector<T>* checkEventually(const Eventually<T>& obj, bool qualitative) const = 0;
-};
+namespace abstract {
 
 /*!
  * @brief
@@ -48,11 +29,11 @@ class IEventuallyModelChecker {
  * The subtree is seen as part of the object and deleted with the object
  * (this behavior can be prevented by setting them to nullptr before deletion)
  *
- * @see AbstractPathFormula
+ * @see AbstractFormula
  * @see AbstractFormula
  */
 template <class T>
-class Eventually : public AbstractPathFormula<T> {
+class Eventually : public AbstractFormula<T> {
 
 public:
 	/*!
@@ -67,7 +48,7 @@ public:
 	 *
 	 * @param child The child node
 	 */
-	Eventually(AbstractStateFormula<T>* child) {
+	Eventually(AbstractFormula<T>* child) {
 		this->child = child;
 	}
 
@@ -83,21 +64,6 @@ public:
 	  }
 	}
 
-	/*!
-	 * @returns the child node
-	 */
-	const AbstractStateFormula<T>& getChild() const {
-		return *child;
-	}
-
-	/*!
-	 * Sets the subtree
-	 * @param child the new child node
-	 */
-	void setChild(AbstractStateFormula<T>* child) {
-		this->child = child;
-	}
-
 	/*!
 	 * @returns a string representation of the formula
 	 */
@@ -106,34 +72,6 @@ public:
 		result += child->toString();
 		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 Eventually-object that is identical the called object.
-	 */
-	virtual AbstractPathFormula<T>* clone() const {
-		Eventually<T>* result = new Eventually<T>();
-		if (child != nullptr) {
-			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(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
-		return modelChecker.template as<IEventuallyModelChecker>()->checkEventually(*this, qualitative);
-	}
 	
 	/*!
      *  @brief Checks if the subtree conforms to some logic.
@@ -145,12 +83,30 @@ public:
 		return checker.conforms(this->child);
 	}
 
+protected:
+	/*!
+	 * @returns the child node
+	 */
+	const AbstractFormula<T>& getChild() const {
+		return *child;
+	}
+
+	/*!
+	 * Sets the subtree
+	 * @param child the new child node
+	 */
+	void setChild(AbstractFormula<T>* child) {
+		this->child = child;
+	}
+
 private:
-	AbstractStateFormula<T>* child;
+	AbstractFormula<T>* child;
 };
 
+} //namespace abstract
+
 } //namespace formula
 
 } //namespace storm
 
-#endif /* STORM_FORMULA_EVENTUALLY_H_ */
+#endif /* STORM_FORMULA_ABSTRACT_EVENTUALLY_H_ */
diff --git a/src/formula/abstract/Globally.h b/src/formula/abstract/Globally.h
index 31d06bd05..adaac0d85 100644
--- a/src/formula/abstract/Globally.h
+++ b/src/formula/abstract/Globally.h
@@ -5,11 +5,10 @@
  *      Author: Christian Dehnert
  */
 
-#ifndef STORM_FORMULA_GLOBALLY_H_
-#define STORM_FORMULA_GLOBALLY_H_
+#ifndef STORM_FORMULA_ABSTRACT_GLOBALLY_H_
+#define STORM_FORMULA_ABSTRACT_GLOBALLY_H_
 
-#include "AbstractPathFormula.h"
-#include "AbstractStateFormula.h"
+#include "src/formula/abstract/AbstractFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelchecker/ForwardDeclarations.h"
 
@@ -17,25 +16,7 @@ namespace storm {
 
 namespace formula {
 
-template <class T> class Globally;
-
-/*!
- *  @brief Interface class for model checkers that support Globally.
- *   
- *  All model checkers that support the formula class Globally must inherit
- *  this pure virtual class.
- */
-template <class T>
-class IGloballyModelChecker {
-    public:
-		/*!
-         *  @brief Evaluates Globally formula within a model checker.
-         *
-         *  @param obj Formula object with subformulas.
-         *  @return Result of the formula for every node.
-         */
-        virtual std::vector<T>* checkGlobally(const Globally<T>& obj, bool qualitative) const = 0;
-};
+namespace abstract {
 
 /*!
  * @brief
@@ -49,11 +30,11 @@ class IGloballyModelChecker {
  * The subtree is seen as part of the object and deleted with the object
  * (this behavior can be prevented by setting them to nullptr before deletion)
  *
- * @see AbstractPathFormula
+ * @see AbstractFormula
  * @see AbstractFormula
  */
 template <class T>
-class Globally : public AbstractPathFormula<T> {
+class Globally : public AbstractFormula<T> {
 
 public:
 	/*!
@@ -68,7 +49,7 @@ public:
 	 *
 	 * @param child The child node
 	 */
-	Globally(AbstractStateFormula<T>* child) {
+	Globally(AbstractFormula<T>* child) {
 		this->child = child;
 	}
 
@@ -84,21 +65,6 @@ public:
 	  }
 	}
 
-	/*!
-	 * @returns the child node
-	 */
-	const AbstractStateFormula<T>& getChild() const {
-		return *child;
-	}
-
-	/*!
-	 * Sets the subtree
-	 * @param child the new child node
-	 */
-	void setChild(AbstractStateFormula<T>* child) {
-		this->child = child;
-	}
-
 	/*!
 	 * @returns a string representation of the formula
 	 */
@@ -107,34 +73,6 @@ public:
 		result += child->toString();
 		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 Globally-object that is identical the called object.
-	 */
-	virtual AbstractPathFormula<T>* clone() const {
-		Next<T>* result = new Next<T>();
-		if (child != nullptr) {
-			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(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
-		return modelChecker.template as<IGloballyModelChecker>()->checkGlobally(*this, qualitative);
-	}
 	
 	/*!
      *  @brief Checks if the subtree conforms to some logic.
@@ -146,12 +84,30 @@ public:
 		return checker.conforms(this->child);
 	}
 
+protected:
+	/*!
+	 * @returns the child node
+	 */
+	const AbstractFormula<T>& getChild() const {
+		return *child;
+	}
+
+	/*!
+	 * Sets the subtree
+	 * @param child the new child node
+	 */
+	void setChild(AbstractFormula<T>* child) {
+		this->child = child;
+	}
+
 private:
-	AbstractStateFormula<T>* child;
+	AbstractFormula<T>* child;
 };
 
+} //namespace abstract
+
 } //namespace formula
 
 } //namespace storm
 
-#endif /* STORM_FORMULA_GLOBALLY_H_ */
+#endif /* STORM_FORMULA_ABSTRACT_GLOBALLY_H_ */
diff --git a/src/formula/abstract/Next.h b/src/formula/abstract/Next.h
index 5f36b053e..9f2247f81 100644
--- a/src/formula/abstract/Next.h
+++ b/src/formula/abstract/Next.h
@@ -5,36 +5,17 @@
  *      Author: Thomas Heinemann
  */
 
-#ifndef STORM_FORMULA_NEXT_H_
-#define STORM_FORMULA_NEXT_H_
+#ifndef STORM_FORMULA_ABSTRACT_NEXT_H_
+#define STORM_FORMULA_ABSTRACT_NEXT_H_
 
-#include "AbstractPathFormula.h"
-#include "AbstractStateFormula.h"
+#include "src/formula/abstract/AbstractFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
 
 namespace formula {
 
-template <class T> class Next;
-
-/*!
- *  @brief Interface class for model checkers that support Next.
- *   
- *  All model checkers that support the formula class Next must inherit
- *  this pure virtual class.
- */
-template <class T>
-class INextModelChecker {
-    public:
-		/*!
-         *  @brief Evaluates Next formula within a model checker.
-         *
-         *  @param obj Formula object with subformulas.
-         *  @return Result of the formula for every node.
-         */
-        virtual std::vector<T>* checkNext(const Next<T>& obj, bool qualitative) const = 0;
-};
+namespace abstract {
 
 /*!
  * @brief
@@ -48,11 +29,11 @@ class INextModelChecker {
  * 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 AbstractPathFormula
+ * @see AbstractFormula
  * @see AbstractFormula
  */
 template <class T>
-class Next : public AbstractPathFormula<T> {
+class Next : public AbstractFormula<T> {
 
 public:
 	/*!
@@ -67,7 +48,7 @@ public:
 	 *
 	 * @param child The child node
 	 */
-	Next(AbstractStateFormula<T>* child) {
+	Next(AbstractFormula<T>* child) {
 		this->child = child;
 	}
 
@@ -83,21 +64,6 @@ public:
 	  }
 	}
 
-	/*!
-	 * @returns the child node
-	 */
-	const AbstractStateFormula<T>& getChild() const {
-		return *child;
-	}
-
-	/*!
-	 * Sets the subtree
-	 * @param child the new child node
-	 */
-	void setChild(AbstractStateFormula<T>* child) {
-		this->child = child;
-	}
-
 	/*!
 	 * @returns a string representation of the formula
 	 */
@@ -108,34 +74,6 @@ public:
 		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 AbstractPathFormula<T>* clone() const {
-		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(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
-		return modelChecker.template as<INextModelChecker>()->checkNext(*this, qualitative);
-	}
 	
 	/*!
      *  @brief Checks if the subtree conforms to some logic.
@@ -147,12 +85,30 @@ public:
         return checker.conforms(this->child);
     }
 
+protected:
+	/*!
+	 * @returns the child node
+	 */
+	const AbstractFormula<T>& getChild() const {
+		return *child;
+	}
+
+	/*!
+	 * Sets the subtree
+	 * @param child the new child node
+	 */
+	void setChild(AbstractFormula<T>* child) {
+		this->child = child;
+	}
+
 private:
-	AbstractStateFormula<T>* child;
+	AbstractFormula<T>* child;
 };
 
+} //namespace abstract
+
 } //namespace formula
 
 } //namespace storm
 
-#endif /* STORM_FORMULA_NEXT_H_ */
+#endif /* STORM_FORMULA_ABSTRACT_NEXT_H_ */
diff --git a/src/formula/abstract/Not.h b/src/formula/abstract/Not.h
index dde509ec8..4bbc3be7c 100644
--- a/src/formula/abstract/Not.h
+++ b/src/formula/abstract/Not.h
@@ -5,10 +5,10 @@
  *      Author: Thomas Heinemann
  */
 
-#ifndef STORM_FORMULA_NOT_H_
-#define STORM_FORMULA_NOT_H_
+#ifndef STORM_FORMULA_ABSTRACT_NOT_H_
+#define STORM_FORMULA_ABSTRACT_NOT_H_
 
-#include "AbstractStateFormula.h"
+#include "src/formula/abstract/AbstractFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelchecker/ForwardDeclarations.h"
 
@@ -16,25 +16,7 @@ namespace storm {
 
 namespace formula {
 
-template <class T> class Not;
-
-/*!
- *  @brief Interface class for model checkers that support Not.
- *   
- *  All model checkers that support the formula class Not must inherit
- *  this pure virtual class.
- */
-template <class T>
-class INotModelChecker {
-    public:
-		/*!
-         *  @brief Evaluates Not formula within a model checker.
-         *
-         *  @param obj Formula object with subformulas.
-         *  @return Result of the formula for every node.
-         */
-        virtual storm::storage::BitVector* checkNot(const Not<T>& obj) const = 0;
-};
+namespace abstract {
 
 /*!
  * @brief
@@ -45,11 +27,11 @@ class INotModelChecker {
  * 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 AbstractStateFormula
+ * @see AbstractFormula
  * @see AbstractFormula
  */
 template <class T>
-class Not : public AbstractStateFormula<T> {
+class Not : public AbstractFormula<T> {
 
 public:
 	/*!
@@ -63,7 +45,7 @@ public:
 	 * Constructor
 	 * @param child The child node
 	 */
-	Not(AbstractStateFormula<T>* child) {
+	Not(AbstractFormula<T>* child) {
 		this->child = child;
 	}
 
@@ -79,21 +61,6 @@ public:
 	  }
 	}
 
-	/*!
-	 * @returns The child node
-	 */
-	const AbstractStateFormula<T>& getChild() const {
-		return *child;
-	}
-
-	/*!
-	 * Sets the subtree
-	 * @param child the new child node
-	 */
-	void setChild(AbstractStateFormula<T>* child) {
-		this->child = child;
-	}
-
 	/*!
 	 * @returns a string representation of the formula
 	 */
@@ -102,34 +69,6 @@ public:
 		result += child->toString();
 		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 AbstractStateFormula<T>* clone() const {
-		Not<T>* result = new Not<T>();
-		if (child != NULL) {
-			result->setChild(child->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 storm::storage::BitVector *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
-		return modelChecker.template as<INotModelChecker>()->checkNot(*this);  
-	}
 	
 	/*!
      *  @brief Checks if the subtree conforms to some logic.
@@ -141,12 +80,30 @@ public:
 		return checker.conforms(this->child);
 	}
 
+protected:
+	/*!
+	 * @returns The child node
+	 */
+	const AbstractFormula<T>& getChild() const {
+		return *child;
+	}
+
+	/*!
+	 * Sets the subtree
+	 * @param child the new child node
+	 */
+	void setChild(AbstractFormula<T>* child) {
+		this->child = child;
+	}
+
 private:
-	AbstractStateFormula<T>* child;
+	AbstractFormula<T>* child;
 };
 
+} //namespace abstract
+
 } //namespace formula
 
 } //namespace storm
 
-#endif /* STORM_FORMULA_NOT_H_ */
+#endif /* STORM_FORMULA_ABSTRACT_NOT_H_ */
diff --git a/src/formula/abstract/OptimizingOperator.h b/src/formula/abstract/OptimizingOperator.h
index 030655fce..ed08644a1 100644
--- a/src/formula/abstract/OptimizingOperator.h
+++ b/src/formula/abstract/OptimizingOperator.h
@@ -1,10 +1,12 @@
-#ifndef STORM_FORMULA_OPTIMIZINGOPERATOR_H_
-#define STORM_FORMULA_OPTIMIZINGOPERATOR_H_
+#ifndef STORM_FORMULA_ABSTRACT_OPTIMIZINGOPERATOR_H_
+#define STORM_FORMULA_ABSTRACT_OPTIMIZINGOPERATOR_H_
 
 namespace storm {
 
 namespace formula {
 
+namespace abstract {
+
 class OptimizingOperator {
 public:
 	/*!
@@ -49,8 +51,10 @@ private:
 	bool minimumOperator;
 };
 
-} /* namespace formula */
+} //namespace abstract
+
+} //namespace formula
 
-} /* namespace storm */
+} //namespace storm
 
-#endif /* STORM_FORMULA_OPTIMIZINGOPERATOR_H_ */
+#endif /* STORM_FORMULA_ABSTRACT_OPTIMIZINGOPERATOR_H_ */
diff --git a/src/formula/abstract/Or.h b/src/formula/abstract/Or.h
index bb91bfa59..42e86c198 100644
--- a/src/formula/abstract/Or.h
+++ b/src/formula/abstract/Or.h
@@ -5,34 +5,15 @@
  *      Author: Thomas Heinemann
  */
 
-#ifndef STORM_FORMULA_OR_H_
-#define STORM_FORMULA_OR_H_
+#ifndef STORM_FORMULA_ABSTRACT_OR_H_
+#define STORM_FORMULA_ABSTRACT_OR_H_
 
-#include "src/formula/AbstractStateFormula.h"
+#include "src/formula/abstract/AbstractFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
 namespace formula {
-
-template <class T> class Or;
-
-/*!
- *  @brief Interface class for model checkers that support Or.
- *   
- *  All model checkers that support the formula class Or must inherit
- *  this pure virtual class.
- */
-template <class T>
-class IOrModelChecker {
-	public:
-		/*!
-         *  @brief Evaluates Or formula within a model checker.
-         *
-         *  @param obj Formula object with subformulas.
-         *  @return Result of the formula for every node.
-         */
-		virtual storm::storage::BitVector* checkOr(const Or<T>& obj) const = 0;
-};
+namespace abstract {
 
 /*!
  * @brief
@@ -46,11 +27,11 @@ class IOrModelChecker {
  * 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 AbstractStateFormula
+ * @see AbstractFormula
  * @see AbstractFormula
  */
 template <class T>
-class Or : public AbstractStateFormula<T> {
+class Or : public AbstractFormula<T> {
 
 public:
 	/*!
@@ -69,7 +50,7 @@ public:
 	 * @param left The left sub formula
 	 * @param right The right sub formula
 	 */
-	Or(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right) {
+	Or(AbstractFormula<T>* left, AbstractFormula<T>* right) {
 		this->left = left;
 		this->right = right;
 	}
@@ -89,12 +70,35 @@ public:
 	  }
 	}
 
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const {
+		std::string result = "(";
+		result += left->toString();
+		result += " | ";
+		result += right->toString();
+		result += ")";
+		return result;
+	}
+	
+	/*!
+     *  @brief Checks if all subtrees conform to some logic.
+     *
+     *  @param checker Formula checker object.
+     *  @return true iff all subtrees conform to some logic.
+     */
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+        return checker.conforms(this->left) && checker.conforms(this->right);
+    }
+
+protected:
 	/*!
 	 * Sets the left child node.
 	 *
 	 * @param newLeft the new left child.
 	 */
-	void setLeft(AbstractStateFormula<T>* newLeft) {
+	void setLeft(AbstractFormula<T>* newLeft) {
 		left = newLeft;
 	}
 
@@ -103,84 +107,33 @@ public:
 	 *
 	 * @param newRight the new right child.
 	 */
-	void setRight(AbstractStateFormula<T>* newRight) {
+	void setRight(AbstractFormula<T>* newRight) {
 		right = newRight;
 	}
 
 	/*!
 	 * @returns a pointer to the left child node
 	 */
-	const AbstractStateFormula<T>& getLeft() const {
+	const AbstractFormula<T>& getLeft() const {
 		return *left;
 	}
 
 	/*!
 	 * @returns a pointer to the right child node
 	 */
-	const AbstractStateFormula<T>& getRight() const {
+	const AbstractFormula<T>& getRight() const {
 		return *right;
 	}
 
-	/*!
-	 * @returns a string representation of the formula
-	 */
-	virtual std::string toString() const {
-		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 AbstractStateFormula<T>* clone() const {
-		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 storm::storage::BitVector *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
-		return modelChecker.template as<IOrModelChecker>()->checkOr(*this);
-	}
-	
-	/*!
-     *  @brief Checks if all subtrees conform to some logic.
-     *
-     *  @param checker Formula checker object.
-     *  @return true iff all subtrees conform to some logic.
-     */
-	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
-        return checker.conforms(this->left) && checker.conforms(this->right);
-    }
-
 private:
-	AbstractStateFormula<T>* left;
-	AbstractStateFormula<T>* right;
+	AbstractFormula<T>* left;
+	AbstractFormula<T>* right;
 };
 
+} //namespace abstract
+
 } //namespace formula
 
 } //namespace storm
 
-#endif /* STORM_FORMULA_OR_H_ */
+#endif /* STORM_FORMULA_ABSTRACT_OR_H_ */
diff --git a/src/formula/abstract/PathBoundOperator.h b/src/formula/abstract/PathBoundOperator.h
index 2bece5c61..fa65cbe6d 100644
--- a/src/formula/abstract/PathBoundOperator.h
+++ b/src/formula/abstract/PathBoundOperator.h
@@ -5,14 +5,14 @@
  *      Author: Christian Dehnert
  */
 
-#ifndef STORM_FORMULA_PATHBOUNDOPERATOR_H_
-#define STORM_FORMULA_PATHBOUNDOPERATOR_H_
+#ifndef STORM_FORMULA_ABSTRACT_PATHBOUNDOPERATOR_H_
+#define STORM_FORMULA_ABSTRACT_PATHBOUNDOPERATOR_H_
 
-#include "src/formula/AbstractStateFormula.h"
-#include "src/formula/AbstractPathFormula.h"
+#include "src/formula/abstract/AbstractFormula.h"
+#include "src/formula/abstract/AbstractFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 
-#include "src/formula/OptimizingOperator.h"
+#include "src/formula/abstract/OptimizingOperator.h"
 
 #include "src/modelchecker/ForwardDeclarations.h"
 #include "src/utility/ConstTemplates.h"
@@ -21,6 +21,8 @@ namespace storm {
 
 namespace formula {
 
+namespace abstract {
+
 template <class T> class PathBoundOperator;
 
 /*!
@@ -38,14 +40,14 @@ template <class T> class PathBoundOperator;
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
  *
- * @see AbstractStateFormula
- * @see AbstractPathFormula
+ * @see AbstractFormula
+ * @see AbstractFormula
  * @see ProbabilisticOperator
  * @see ProbabilisticNoBoundsOperator
  * @see AbstractFormula
  */
 template<class T>
-class PathBoundOperator : public AbstractStateFormula<T>, public OptimizingOperator {
+class PathBoundOperator : public AbstractFormula<T>, public OptimizingOperator {
 
 public:
 	enum ComparisonType { LESS, LESS_EQUAL, GREATER, GREATER_EQUAL };
@@ -57,7 +59,7 @@ public:
 	 * @param bound The bound for the probability
 	 * @param pathFormula The child node
 	 */
-	PathBoundOperator(ComparisonType comparisonOperator, T bound, AbstractPathFormula<T>* pathFormula)
+	PathBoundOperator(ComparisonType comparisonOperator, T bound, AbstractFormula<T>* pathFormula)
 		: comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula) {
 		// Intentionally left empty
 	}
@@ -70,7 +72,7 @@ public:
 	 * @param pathFormula The child node
 	 * @param minimumOperator Indicator, if operator should be minimum or maximum operator.
 	 */
-	PathBoundOperator(ComparisonType comparisonOperator, T bound, AbstractPathFormula<T>* pathFormula, bool minimumOperator)
+	PathBoundOperator(ComparisonType comparisonOperator, T bound, AbstractFormula<T>* pathFormula, bool minimumOperator)
 		: comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula), OptimizingOperator(minimumOperator) {
 		// Intentionally left empty
 	}
@@ -87,22 +89,6 @@ public:
 	 }
 	}
 
-	/*!
-	 * @returns the child node (representation of a Abstract path formula)
-	 */
-	const AbstractPathFormula<T>& getPathFormula () const {
-		return *pathFormula;
-	}
-
-	/*!
-	 * Sets the child node
-	 *
-	 * @param pathFormula the path formula that becomes the new child node
-	 */
-	void setPathFormula(AbstractPathFormula<T>* pathFormula) {
-		this->pathFormula = pathFormula;
-	}
-
 	/*!
 	 * @returns the comparison relation
 	 */
@@ -159,15 +145,6 @@ public:
 		}
 	}
 
-	/*!
-	 * 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 AbstractStateFormula<T>* clone() const = 0;
-
 	/*!
      *  @brief Checks if the subtree conforms to some logic.
      * 
@@ -178,14 +155,34 @@ public:
         return checker.conforms(this->pathFormula);
     }
 
+protected:
+	/*!
+	 * @returns the child node (representation of a Abstract path formula)
+	 */
+	const AbstractFormula<T>& getPathFormula () const {
+		return *pathFormula;
+	}
+
+	/*!
+	 * Sets the child node
+	 *
+	 * @param pathFormula the path formula that becomes the new child node
+	 */
+	void setPathFormula(AbstractFormula<T>* pathFormula) {
+		this->pathFormula = pathFormula;
+	}
+
+
 private:
 	ComparisonType comparisonOperator;
 	T bound;
-	AbstractPathFormula<T>* pathFormula;
+	AbstractFormula<T>* pathFormula;
 };
 
+} //namespace abstract
+
 } //namespace formula
 
 } //namespace storm
 
-#endif /* STORM_FORMULA_PATHBOUNDOPERATOR_H_ */
+#endif /* STORM_FORMULA_ABSTRACT_PATHBOUNDOPERATOR_H_ */
diff --git a/src/formula/abstract/PathNoBoundOperator.h b/src/formula/abstract/PathNoBoundOperator.h
index f562ecc91..68da9ba40 100644
--- a/src/formula/abstract/PathNoBoundOperator.h
+++ b/src/formula/abstract/PathNoBoundOperator.h
@@ -5,13 +5,13 @@
  *      Author: Christian Dehnert
  */
 
-#ifndef STORM_FORMULA_NOBOUNDOPERATOR_H_
-#define STORM_FORMULA_NOBOUNDOPERATOR_H_
+#ifndef STORM_FORMULA_ABSTRACT_NOBOUNDOPERATOR_H_
+#define STORM_FORMULA_ABSTRACT_NOBOUNDOPERATOR_H_
 
-#include "src/formula/AbstractFormula.h"
-#include "src/formula/AbstractPathFormula.h"
+#include "src/formula/abstract/AbstractFormula.h"
+#include "src/formula/abstract/AbstractFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
-#include "src/formula/OptimizingOperator.h"
+#include "src/formula/abstract/OptimizingOperator.h"
 
 #include "src/modelchecker/ForwardDeclarations.h"
 
@@ -19,26 +19,7 @@ namespace storm {
 
 namespace formula {
 
-template <class T> class PathNoBoundOperator;
-
-/*!
- *  @brief Interface class for model checkers that support PathNoBoundOperator.
- *   
- *  All model checkers that support the formula class NoBoundOperator must inherit
- *  this pure virtual class.
- */
-template <class T>
-class IPathNoBoundOperatorModelChecker {
-    public:
-		/*!
-         *  @brief Evaluates NoBoundOperator formula within a model checker.
-         *
-         *  @param obj Formula object with subformulas.
-         *  @return Result of the formula for every node.
-         */
-        virtual std::vector<T>* checkPathNoBoundOperator(const PathNoBoundOperator<T>& obj) const = 0;
-};
-
+namespace abstract {
 /*!
  * @brief
  * Class for a Abstract formula tree with a P (probablistic) operator without declaration of probabilities
@@ -63,8 +44,8 @@ class IPathNoBoundOperatorModelChecker {
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
  *
- * @see AbstractStateFormula
- * @see AbstractPathFormula
+ * @see AbstractFormula
+ * @see AbstractFormula
  * @see ProbabilisticOperator
  * @see ProbabilisticIntervalOperator
  * @see AbstractFormula
@@ -84,7 +65,7 @@ public:
 	 *
 	 * @param pathFormula The child node.
 	 */
-	PathNoBoundOperator(AbstractPathFormula<T>* pathFormula) : optimalityOperator(false), minimumOperator(false) {
+	PathNoBoundOperator(AbstractFormula<T>* pathFormula) : optimalityOperator(false), minimumOperator(false) {
 		this->pathFormula = pathFormula;
 	}
 
@@ -95,7 +76,7 @@ public:
 	 * @param minimumOperator A flag indicating whether this operator is a minimizing or a
 	 * maximizing operator.
 	 */
-	PathNoBoundOperator(AbstractPathFormula<T>* pathFormula, bool minimumOperator)
+	PathNoBoundOperator(AbstractFormula<T>* pathFormula, bool minimumOperator)
 		: optimalityOperator(true), minimumOperator(minimumOperator) {
 		this->pathFormula = pathFormula;
 	}
@@ -109,37 +90,6 @@ public:
 		}
 	}
 
-	/*!
-	 * @returns the child node (representation of a Abstract path formula)
-	 */
-	const AbstractPathFormula<T>& getPathFormula () const {
-		return *pathFormula;
-	}
-
-	/*!
-	 * Sets the child node
-	 *
-	 * @param pathFormula the path formula that becomes the new child node
-	 */
-	void setPathFormula(AbstractPathFormula<T>* pathFormula) {
-		this->pathFormula = pathFormula;
-	}
-
-	/*!
-	 * 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 all states that satisfy the formula represented by the called object.
-	 */
-	virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
-		return modelChecker.template as<IPathNoBoundOperatorModelChecker>()->checkPathNoBoundOperator(*this);
-	}
-
 	/*!
 	 * @returns a string representation of the formula
 	 */
@@ -186,8 +136,25 @@ public:
 		return optimalityOperator && minimumOperator;
 	}
 
+protected:
+	/*!
+	 * @returns the child node (representation of a Abstract path formula)
+	 */
+	const AbstractFormula<T>& getPathFormula () const {
+		return *pathFormula;
+	}
+
+	/*!
+	 * Sets the child node
+	 *
+	 * @param pathFormula the path formula that becomes the new child node
+	 */
+	void setPathFormula(AbstractFormula<T>* pathFormula) {
+		this->pathFormula = pathFormula;
+	}
+
 private:
-	AbstractPathFormula<T>* pathFormula;
+	AbstractFormula<T>* pathFormula;
 
 	// A flag that indicates whether this operator is meant as an optimizing (i.e. min/max) operator
 	// over a nondeterministic model.
@@ -198,8 +165,10 @@ private:
 	bool minimumOperator;
 };
 
-} /* namespace formula */
+} //namespace abstract
+
+} //namespace formula
 
-} /* namespace storm */
+} //namespace storm
 
-#endif /* STORM_FORMULA_NOBOUNDOPERATOR_H_ */
+#endif /* STORM_FORMULA_ABSTRACT_NOBOUNDOPERATOR_H_ */
diff --git a/src/formula/abstract/ProbabilisticBoundOperator.h b/src/formula/abstract/ProbabilisticBoundOperator.h
index 8d651ef2c..30f37eeba 100644
--- a/src/formula/abstract/ProbabilisticBoundOperator.h
+++ b/src/formula/abstract/ProbabilisticBoundOperator.h
@@ -5,31 +5,17 @@
  *      Author: Thomas Heinemann
  */
 
-#ifndef STORM_FORMULA_PROBABILISTICBOUNDOPERATOR_H_
-#define STORM_FORMULA_PROBABILISTICBOUNDOPERATOR_H_
+#ifndef STORM_FORMULA_ABSTRACT_PROBABILISTICBOUNDOPERATOR_H_
+#define STORM_FORMULA_ABSTRACT_PROBABILISTICBOUNDOPERATOR_H_
 
-#include "AbstractStateFormula.h"
-#include "AbstractPathFormula.h"
-#include "src/formula/PathBoundOperator.h"
-#include "src/formula/OptimizingOperator.h"
+#include "src/formula/abstract/AbstractFormula.h"
+#include "src/formula/abstract/PathBoundOperator.h"
+#include "src/formula/abstract/OptimizingOperator.h"
 #include "utility/ConstTemplates.h"
 
 namespace storm {
 namespace formula {
-
-template <class T> class ProbabilisticBoundOperator;
-
-/*!
- *  @brief Interface class for model checkers that support ProbabilisticBoundOperator.
- *
- *  All model checkers that support the formula class PathBoundOperator must inherit
- *  this pure virtual class.
- */
-template <class T>
-class IProbabilisticBoundOperatorModelChecker {
-    public:
-        virtual storm::storage::BitVector* checkProbabilisticBoundOperator(const ProbabilisticBoundOperator<T>& obj) const = 0;
-};
+namespace abstract {
 
 /*!
  * @brief
@@ -46,8 +32,8 @@ class IProbabilisticBoundOperatorModelChecker {
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
  *
- * @see AbstractStateFormula
- * @see AbstractPathFormula
+ * @see AbstractFormula
+ * @see AbstractFormula
  * @see ProbabilisticOperator
  * @see ProbabilisticNoBoundsOperator
  * @see AbstractFormula
@@ -73,56 +59,44 @@ public:
 	 * @param pathFormula The child node
 	 */
 	ProbabilisticBoundOperator(
-			typename PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractPathFormula<T>* pathFormula)
+			typename PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractFormula<T>* pathFormula)
 			: PathBoundOperator<T>(comparisonRelation, bound, pathFormula) {
 		// Intentionally left empty
 	}
 
+	/*!
+	 * Constructor
+	 *
+	 * @param comparisonRelation
+	 * @param bound
+	 * @param pathFormula
+	 * @param minimumOperator
+	 */
 	ProbabilisticBoundOperator(
-			typename PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractPathFormula<T>* pathFormula, bool minimumOperator)
+			typename PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractFormula<T>* pathFormula, bool minimumOperator)
 			: PathBoundOperator<T>(comparisonRelation, bound, pathFormula, minimumOperator){
 		// Intentionally left empty
 	}
 
 	/*!
-	 * @returns a string representation of the formula
+	 * Destructor
 	 */
-	virtual std::string toString() const {
-		std::string result = "P ";
-		result += PathBoundOperator<T>::toString();
-		return result;
+	virtual ~ProbabilisticBoundOperator() {
+		// Intentionally left empty
 	}
 
 	/*!
-	 * 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.
+	 * @returns a string representation of the formula
 	 */
-	virtual AbstractStateFormula<T>* clone() const {
-		ProbabilisticBoundOperator<T>* result = new ProbabilisticBoundOperator<T>();
-		result->setComparisonOperator(this->getComparisonOperator());
-		result->setBound(this->getBound());
-		result->setPathFormula(this->getPathFormula().clone());
+	virtual std::string toString() const {
+		std::string result = "P ";
+		result += PathBoundOperator<T>::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 storm::storage::BitVector* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
-		return modelChecker.template as<IProbabilisticBoundOperatorModelChecker>()->checkProbabilisticBoundOperator(*this);
-	}
 };
 
+} //namespace abstract
 } //namespace formula
 } //namespace storm
 
-#endif /* STORM_FORMULA_PROBABILISTICBOUNDOPERATOR_H_ */
+#endif /* STORM_FORMULA_ABSTRACT_PROBABILISTICBOUNDOPERATOR_H_ */
diff --git a/src/formula/abstract/ProbabilisticNoBoundOperator.h b/src/formula/abstract/ProbabilisticNoBoundOperator.h
index 66843d965..68e5e1bcb 100644
--- a/src/formula/abstract/ProbabilisticNoBoundOperator.h
+++ b/src/formula/abstract/ProbabilisticNoBoundOperator.h
@@ -5,15 +5,16 @@
  *      Author: thomas
  */
 
-#ifndef STORM_FORMULA_PROBABILISTICNOBOUNDOPERATOR_H_
-#define STORM_FORMULA_PROBABILISTICNOBOUNDOPERATOR_H_
+#ifndef STORM_FORMULA_ABSTRACT_PROBABILISTICNOBOUNDOPERATOR_H_
+#define STORM_FORMULA_ABSTRACT_PROBABILISTICNOBOUNDOPERATOR_H_
 
 #include "AbstractFormula.h"
-#include "AbstractPathFormula.h"
+#include "src/formula/abstract/AbstractFormula.h"
 #include "PathNoBoundOperator.h"
 
 namespace storm {
 namespace formula {
+namespace abstract {
 
 /*!
  * @brief
@@ -39,8 +40,8 @@ namespace formula {
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
  *
- * @see AbstractStateFormula
- * @see AbstractPathFormula
+ * @see AbstractFormula
+ * @see AbstractFormula
  * @see ProbabilisticOperator
  * @see ProbabilisticIntervalOperator
  * @see AbstractFormula
@@ -60,7 +61,14 @@ public:
 	 *
 	 * @param pathFormula The child node.
 	 */
-	ProbabilisticNoBoundOperator(AbstractPathFormula<T>* pathFormula) : PathNoBoundOperator<T>(pathFormula) {
+	ProbabilisticNoBoundOperator(AbstractFormula<T>* pathFormula) : PathNoBoundOperator<T>(pathFormula) {
+		// Intentionally left empty
+	}
+
+	/*!
+	 * Destructor
+	 */
+	virtual ~ProbabilisticNoBoundOperator() {
 		// Intentionally left empty
 	}
 
@@ -69,7 +77,7 @@ public:
 	 *
 	 * @param pathFormula The child node.
 	 */
-	ProbabilisticNoBoundOperator(AbstractPathFormula<T>* pathFormula, bool minimumOperator) : PathNoBoundOperator<T>(pathFormula, minimumOperator) {
+	ProbabilisticNoBoundOperator(AbstractFormula<T>* pathFormula, bool minimumOperator) : PathNoBoundOperator<T>(pathFormula, minimumOperator) {
 		// Intentionally left empty
 	}
 
@@ -83,7 +91,8 @@ public:
 	}
 };
 
-} /* namespace formula */
-} /* namespace storm */
+} //namespace abstract
+} //namespace formula
+} //namespace storm
 
-#endif /* STORM_FORMULA_PROBABILISTICNOBOUNDOPERATOR_H_ */
+#endif /* STORM_FORMULA_ABSTRACT_PROBABILISTICNOBOUNDOPERATOR_H_ */
diff --git a/src/formula/abstract/StateBoundOperator.h b/src/formula/abstract/StateBoundOperator.h
index 441c91f1d..c1f0f2ce7 100644
--- a/src/formula/abstract/StateBoundOperator.h
+++ b/src/formula/abstract/StateBoundOperator.h
@@ -5,31 +5,18 @@
  *      Author: Christian Dehnert
  */
 
-#ifndef STORM_FORMULA_STATEBOUNDOPERATOR_H_
-#define STORM_FORMULA_STATEBOUNDOPERATOR_H_
+#ifndef STORM_FORMULA_ABSTRACT_STATEBOUNDOPERATOR_H_
+#define STORM_FORMULA_ABSTRACT_STATEBOUNDOPERATOR_H_
 
-#include "src/formula/AbstractStateFormula.h"
-#include "src/formula/AbstractPathFormula.h"
+#include "src/formula/abstract/AbstractFormula.h"
+#include "src/formula/abstract/AbstractFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelchecker/AbstractModelChecker.h"
 #include "src/utility/ConstTemplates.h"
 
 namespace storm {
 namespace formula {
-
-template <class T> class StateBoundOperator;
-
-/*!
- *  @brief Interface class for model checkers that support StateBoundOperator.
- *   
- *  All model checkers that support the formula class StateBoundOperator must inherit
- *  this pure virtual class.
- */
-template <class T>
-class IStateBoundOperatorModelChecker {
-    public:
-        virtual storm::storage::BitVector* checkStateBoundOperator(const StateBoundOperator<T>& obj) const = 0;
-};
+namespace abstract {
 
 /*!
  * @brief
@@ -46,14 +33,14 @@ class IStateBoundOperatorModelChecker {
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
  *
- * @see AbstractStateFormula
- * @see AbstractPathFormula
+ * @see AbstractFormula
+ * @see AbstractFormula
  * @see ProbabilisticOperator
  * @see ProbabilisticNoBoundsOperator
  * @see AbstractFormula
  */
 template<class T>
-class StateBoundOperator : public AbstractStateFormula<T> {
+class StateBoundOperator : public AbstractFormula<T> {
 
 public:
 	enum ComparisonType { LESS, LESS_EQUAL, GREATER, GREATER_EQUAL };
@@ -65,7 +52,7 @@ public:
 	 * @param bound The bound for the probability
 	 * @param stateFormula The child node
 	 */
-	StateBoundOperator(ComparisonType comparisonOperator, T bound, AbstractStateFormula<T>* stateFormula)
+	StateBoundOperator(ComparisonType comparisonOperator, T bound, AbstractFormula<T>* stateFormula)
 		: comparisonOperator(comparisonOperator), bound(bound), stateFormula(stateFormula) {
 		// Intentionally left empty
 	}
@@ -82,22 +69,6 @@ public:
 	 }
 	}
 
-	/*!
-	 * @returns the child node (representation of a Abstract state formula)
-	 */
-	const AbstractStateFormula<T>& getStateFormula () const {
-		return *stateFormula;
-	}
-
-	/*!
-	 * Sets the child node
-	 *
-	 * @param stateFormula the state formula that becomes the new child node
-	 */
-	void setStateFormula(AbstractStateFormula<T>* stateFormula) {
-		this->stateFormula = stateFormula;
-	}
-
 	/*!
 	 * @returns the comparison relation
 	 */
@@ -153,28 +124,6 @@ public:
 		}
 	}
 
-	/*!
-	 * 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 AbstractStateFormula<T>* clone() const = 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.
-	 *
-	 * @returns A bit vector indicating all states that satisfy the formula represented by the called object.
-	 */
-	virtual storm::storage::BitVector *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
-		return modelChecker.template as<IStateBoundOperatorModelChecker>()->checkStateBoundOperator(*this);
-	}
-	
 	/*!
      *  @brief Checks if the subtree conforms to some logic.
      * 
@@ -185,13 +134,31 @@ public:
         return checker.conforms(this->stateFormula);
     }
 
+protected:
+	/*!
+	 * @returns the child node (representation of a Abstract state formula)
+	 */
+	const AbstractFormula<T>& getStateFormula () const {
+		return *stateFormula;
+	}
+
+	/*!
+	 * Sets the child node
+	 *
+	 * @param stateFormula the state formula that becomes the new child node
+	 */
+	void setStateFormula(AbstractFormula<T>* stateFormula) {
+		this->stateFormula = stateFormula;
+	}
+
 private:
 	ComparisonType comparisonOperator;
 	T bound;
-	AbstractStateFormula<T>* stateFormula;
+	AbstractFormula<T>* stateFormula;
 };
 
+} //namespace abstract
 } //namespace formula
 } //namespace storm
 
-#endif /* STORM_FORMULA_STATEBOUNDOPERATOR_H_ */
+#endif /* STORM_FORMULA_ABSTRACT_STATEBOUNDOPERATOR_H_ */
diff --git a/src/formula/abstract/StateNoBoundOperator.h b/src/formula/abstract/StateNoBoundOperator.h
index 23e6b816e..d2a4fe369 100644
--- a/src/formula/abstract/StateNoBoundOperator.h
+++ b/src/formula/abstract/StateNoBoundOperator.h
@@ -5,38 +5,17 @@
  *      Author: Thomas Heinemann
  */
 
-#ifndef STORM_FORMULA_STATENOBOUNDOPERATOR_H_
-#define STORM_FORMULA_STATENOBOUNDOPERATOR_H_
+#ifndef STORM_FORMULA_ABSTRACT_STATENOBOUNDOPERATOR_H_
+#define STORM_FORMULA_ABSTRACT_STATENOBOUNDOPERATOR_H_
 
-#include "src/formula/AbstractFormula.h"
-#include "src/formula/AbstractPathFormula.h"
+#include "src/formula/abstract/AbstractFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 
 #include "src/modelchecker/ForwardDeclarations.h"
 
 namespace storm {
 namespace formula {
-
-template <class T> class StateNoBoundOperator;
-
-/*!
- *  @brief Interface class for model checkers that support PathNoBoundOperator.
- *
- *  All model checkers that support the formula class NoBoundOperator must inherit
- *  this pure virtual class.
- */
-template <class T>
-class IStateNoBoundOperatorModelChecker {
-    public:
-		/*!
-         *  @brief Evaluates NoBoundOperator formula within a model checker.
-         *
-         *  @param obj Formula object with subformulas.
-         *  @return Result of the formula for every node.
-         */
-        virtual std::vector<T>* checkStateNoBoundOperator(const StateNoBoundOperator<T>& obj) const = 0;
-};
-
+namespace abstract {
 
 /*!
  * @brief
@@ -62,8 +41,8 @@ class IStateNoBoundOperatorModelChecker {
  * (this behavior can be prevented by setting them to NULL before deletion)
  *
  *
- * @see AbstractStateFormula
- * @see AbstractPathFormula
+ * @see AbstractFormula
+ * @see AbstractFormula
  * @see SteadyStateNoBoundOperator
  * @see AbstractFormula
  */
@@ -80,7 +59,7 @@ public:
 	/*!
 	 * Constructor
 	 */
-	StateNoBoundOperator(AbstractStateFormula<T>* stateFormula) {
+	StateNoBoundOperator(AbstractFormula<T>* stateFormula) {
 		this->stateFormula = stateFormula;
 	}
 
@@ -95,14 +74,6 @@ public:
 		}
 	}
 
-	const AbstractStateFormula<T>& getStateFormula() const {
-		return *(this->stateFormula);
-	}
-
-	void setStateFormula(AbstractStateFormula<T>* stateFormula) {
-		this->stateFormula = stateFormula;
-	}
-
 	/*!
 	 * Calls the model checker to check this formula.
 	 * Needed to infer the correct type of formula class.
@@ -139,10 +110,20 @@ public:
 		return checker.conforms(this->stateFormula);
 	}
 
+protected:
+	const AbstractFormula<T>& getStateFormula() const {
+		return *(this->stateFormula);
+	}
+
+	void setStateFormula(AbstractFormula<T>* stateFormula) {
+		this->stateFormula = stateFormula;
+	}
+
 private:
-	AbstractStateFormula<T>* stateFormula;
+	AbstractFormula<T>* stateFormula;
 };
 
-} /* namespace formula */
-} /* namespace storm */
-#endif /* STORM_FORMULA_STATENOBOUNDOPERATOR_H_ */
+} //namespace abstract
+} //namespace formula
+} //namespace storm
+#endif /* STORM_FORMULA_ABSTRACT_STATENOBOUNDOPERATOR_H_ */
diff --git a/src/formula/abstract/TimeBoundedOperator.h b/src/formula/abstract/TimeBoundedOperator.h
index f0f443f97..9dea94ef0 100644
--- a/src/formula/abstract/TimeBoundedOperator.h
+++ b/src/formula/abstract/TimeBoundedOperator.h
@@ -5,16 +5,17 @@
  *      Author: thomas
  */
 
-#ifndef TIMEBOUNDEDOPERATOR_H_
-#define TIMEBOUNDEDOPERATOR_H_
+#ifndef STORM_FORMULA_ABSTRACT_TIMEBOUNDEDOPERATOR_H_
+#define STORM_FORMULA_ABSTRACT_TIMEBOUNDEDOPERATOR_H_
 
 #include <limits>
 
-#include "AbstractPathFormula.h"
+#include "src/formula/abstract/AbstractFormula.h"
 #include "exceptions/InvalidArgumentException.h"
 
 namespace storm {
 namespace formula {
+namespace abstract {
 
 /*!
  * @brief
@@ -24,12 +25,12 @@ namespace formula {
  * This class does not provide support for sub formulas; this has to be done in concretizations of this abstract class.
  *
  *
- * @see AbstractStateFormula
- * @see AbstractPathFormula
+ * @see AbstractFormula
+ * @see AbstractFormula
  * @see AbstractFormula
  */
 template<class T>
-class TimeBoundedOperator: public storm::formula::AbstractPathFormula<T> {
+class TimeBoundedOperator: public storm::formula::AbstractFormula<T> {
 public:
 	/**
 	 * Constructor
@@ -104,6 +105,8 @@ private:
 	T lowerBound, upperBound;
 };
 
-} /* namespace formula */
-} /* namespace storm */
-#endif /* TIMEBOUNDEDOPERATOR_H_ */
+} //namespace abstract
+} //namespace formula
+} //namespace storm
+
+#endif /* STORM_FORMULA_ABSTRACT_TIMEBOUNDEDOPERATOR_H_ */
diff --git a/src/formula/abstract/Until.h b/src/formula/abstract/Until.h
index b2efe6f45..03b55c460 100644
--- a/src/formula/abstract/Until.h
+++ b/src/formula/abstract/Until.h
@@ -5,35 +5,16 @@
  *      Author: Thomas Heinemann
  */
 
-#ifndef STORM_FORMULA_UNTIL_H_
-#define STORM_FORMULA_UNTIL_H_
+#ifndef STORM_FORMULA_ABSTRACT_UNTIL_H_
+#define STORM_FORMULA_ABSTRACT_UNTIL_H_
 
-#include "AbstractPathFormula.h"
-#include "AbstractStateFormula.h"
+#include "src/formula/abstract/AbstractFormula.h"
+#include "src/formula/abstract/AbstractFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
 namespace formula {
-
-template <class T> class Until;
-
-/*!
- *  @brief Interface class for model checkers that support Until.
- *
- *  All model checkers that support the formula class Until must inherit
- *  this pure virtual class.
- */
-template <class T>
-class IUntilModelChecker {
-    public:
-		/*!
-         *  @brief Evaluates Until formula within a model checker.
-         *
-         *  @param obj Formula object with subformulas.
-         *  @return Result of the formula for every node.
-         */
-        virtual std::vector<T>* checkUntil(const Until<T>& obj, bool qualitative) const = 0;
-};
+namespace abstract {
 
 /*!
  * @brief
@@ -48,11 +29,11 @@ class IUntilModelChecker {
  * 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 AbstractPathFormula
+ * @see AbstractFormula
  * @see AbstractFormula
  */
 template <class T>
-class Until : public AbstractPathFormula<T> {
+class Until : public AbstractFormula<T> {
 
 public:
 	/*!
@@ -69,7 +50,7 @@ public:
 	 * @param left The left formula subtree
 	 * @param right The left formula subtree
 	 */
-	Until(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right) {
+	Until(AbstractFormula<T>* left, AbstractFormula<T>* right) {
 		this->left = left;
 		this->right = right;
 	}
@@ -89,12 +70,33 @@ public:
 	  }
 	}
 
+	/*!
+	 * @returns a string representation of the formula
+	 */
+	virtual std::string toString() const {
+		std::string result = left->toString();
+		result += " U ";
+		result += right->toString();
+		return result;
+	}
+
+	/*!
+     *  @brief Checks if all subtrees conform to some logic.
+     *
+     *  @param checker Formula checker object.
+     *  @return true iff all subtrees conform to some logic.
+     */
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+        return checker.conforms(this->left) && checker.conforms(this->right);
+    }
+
+protected:
 	/*!
 	 * Sets the left child node.
 	 *
 	 * @param newLeft the new left child.
 	 */
-	void setLeft(AbstractStateFormula<T>* newLeft) {
+	void setLeft(AbstractFormula<T>* newLeft) {
 		left = newLeft;
 	}
 
@@ -103,82 +105,33 @@ public:
 	 *
 	 * @param newRight the new right child.
 	 */
-	void setRight(AbstractStateFormula<T>* newRight) {
+	void setRight(AbstractFormula<T>* newRight) {
 		right = newRight;
 	}
 
 	/*!
 	 * @returns a pointer to the left child node
 	 */
-	const AbstractStateFormula<T>& getLeft() const {
+	const AbstractFormula<T>& getLeft() const {
 		return *left;
 	}
 
 	/*!
 	 * @returns a pointer to the right child node
 	 */
-	const AbstractStateFormula<T>& getRight() const {
+	const AbstractFormula<T>& getRight() const {
 		return *right;
 	}
 
-	/*!
-	 * @returns a string representation of the formula
-	 */
-	virtual std::string toString() const {
-		std::string result = left->toString();
-		result += " U ";
-		result += right->toString();
-		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 AbstractPathFormula<T>* clone() const {
-		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(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
-		return modelChecker.template as<IUntilModelChecker>()->checkUntil(*this, qualitative);
-	}
-	
-	/*!
-     *  @brief Checks if all subtrees conform to some logic.
-     *
-     *  @param checker Formula checker object.
-     *  @return true iff all subtrees conform to some logic.
-     */
-	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
-        return checker.conforms(this->left) && checker.conforms(this->right);
-    }
-
 private:
-	AbstractStateFormula<T>* left;
-	AbstractStateFormula<T>* right;
+	AbstractFormula<T>* left;
+	AbstractFormula<T>* right;
 };
 
+} //namespace abstract
+
 } //namespace formula
 
 } //namespace storm
 
-#endif /* STORM_FORMULA_UNTIL_H_ */
+#endif /* STORM_FORMULA_ABSTRACT_UNTIL_H_ */