diff --git a/src/formula/Prctl/AbstractPathFormula.h b/src/formula/Prctl/AbstractPathFormula.h
index 9127a10c8..4431e56db 100644
--- a/src/formula/Prctl/AbstractPathFormula.h
+++ b/src/formula/Prctl/AbstractPathFormula.h
@@ -5,8 +5,8 @@
  *      Author: Thomas Heinemann
  */
 
-#ifndef STORM_FORMULA_ABSTRACTPATHFORMULA_H_
-#define STORM_FORMULA_ABSTRACTPATHFORMULA_H_
+#ifndef STORM_FORMULA_PRCTL_ABSTRACTPATHFORMULA_H_
+#define STORM_FORMULA_PRCTL_ABSTRACTPATHFORMULA_H_
 
 namespace storm { namespace formula {
 template <class T> class AbstractPathFormula;
@@ -69,4 +69,4 @@ public:
 } //namespace formula
 } //namespace storm
 
-#endif /* STORM_FORMULA_ABSTRACTPATHFORMULA_H_ */
+#endif /* STORM_FORMULA_PRCTL_ABSTRACTPATHFORMULA_H_ */
diff --git a/src/formula/Prctl/AbstractStateFormula.h b/src/formula/Prctl/AbstractStateFormula.h
index 51b59b118..d3a10bad7 100644
--- a/src/formula/Prctl/AbstractStateFormula.h
+++ b/src/formula/Prctl/AbstractStateFormula.h
@@ -5,8 +5,8 @@
  *      Author: Thomas Heinemann
  */
 
-#ifndef STORM_FORMULA_ABSTRACTSTATEFORMULA_H_
-#define STORM_FORMULA_ABSTRACTSTATEFORMULA_H_
+#ifndef STORM_FORMULA_PRCTL_ABSTRACTSTATEFORMULA_H_
+#define STORM_FORMULA_PRCTL_ABSTRACTSTATEFORMULA_H_
 
 namespace storm { namespace formula {
 template <class T> class AbstractStateFormula;
@@ -67,4 +67,4 @@ public:
 } //namespace storm
 
 
-#endif /* STORM_FORMULA_AbstractSTATEFORMULA_H_ */
+#endif /* STORM_FORMULA_PRCTL_AbstractSTATEFORMULA_H_ */
diff --git a/src/formula/Prctl/BoundedEventually.h b/src/formula/Prctl/BoundedEventually.h
index 7f104ecd6..03f31f634 100644
--- a/src/formula/Prctl/BoundedEventually.h
+++ b/src/formula/Prctl/BoundedEventually.h
@@ -5,8 +5,8 @@
  *      Author: Christian Dehnert
  */
 
-#ifndef STORM_FORMULA_BOUNDEDEVENTUALLY_H_
-#define STORM_FORMULA_BOUNDEDEVENTUALLY_H_
+#ifndef STORM_FORMULA_PRCTL_BOUNDEDEVENTUALLY_H_
+#define STORM_FORMULA_PRCTL_BOUNDEDEVENTUALLY_H_
 
 #include "src/formula/abstract/BoundedEventually.h"
 #include "src/formula/Prctl/AbstractPathFormula.h"
@@ -123,4 +123,4 @@ public:
 } //namespace formula
 } //namespace storm
 
-#endif /* STORM_FORMULA_BOUNDEDUNTIL_H_ */
+#endif /* STORM_FORMULA_PRCTL_BOUNDEDUNTIL_H_ */
diff --git a/src/formula/Prctl/BoundedNaryUntil.h b/src/formula/Prctl/BoundedNaryUntil.h
index 64dda0452..4dc17bec1 100644
--- a/src/formula/Prctl/BoundedNaryUntil.h
+++ b/src/formula/Prctl/BoundedNaryUntil.h
@@ -5,8 +5,8 @@
  *      Author: Thomas Heinemann
  */
 
-#ifndef STORM_FORMULA_BOUNDEDNARYUNTIL_H_
-#define STORM_FORMULA_BOUNDEDNARYUNTIL_H_
+#ifndef STORM_FORMULA_PRCTL_BOUNDEDNARYUNTIL_H_
+#define STORM_FORMULA_PRCTL_BOUNDEDNARYUNTIL_H_
 
 #include "src/formula/abstract/BoundedNaryUntil.h"
 #include "src/formula/Prctl/AbstractPathFormula.h"
@@ -138,4 +138,4 @@ public:
 } //namespace formula
 } //namespace storm
 
-#endif /* STORM_FORMULA_BOUNDEDNARYUNTIL_H_ */
+#endif /* STORM_FORMULA_PRCTL_BOUNDEDNARYUNTIL_H_ */
diff --git a/src/formula/Prctl/BoundedUntil.h b/src/formula/Prctl/BoundedUntil.h
index 7ef1349ef..0664f4ce1 100644
--- a/src/formula/Prctl/BoundedUntil.h
+++ b/src/formula/Prctl/BoundedUntil.h
@@ -5,8 +5,8 @@
  *      Author: Thomas Heinemann
  */
 
-#ifndef STORM_FORMULA_BOUNDEDUNTIL_H_
-#define STORM_FORMULA_BOUNDEDUNTIL_H_
+#ifndef STORM_FORMULA_PRCTL_BOUNDEDUNTIL_H_
+#define STORM_FORMULA_PRCTL_BOUNDEDUNTIL_H_
 
 #include "src/formula/abstract/BoundedUntil.h"
 #include "src/formula/Prctl/AbstractPathFormula.h"
@@ -128,4 +128,4 @@ public:
 } //namespace formula
 } //namespace storm
 
-#endif /* STORM_FORMULA_BOUNDEDUNTIL_H_ */
+#endif /* STORM_FORMULA_PRCTL_BOUNDEDUNTIL_H_ */
diff --git a/src/formula/Prctl/CumulativeReward.h b/src/formula/Prctl/CumulativeReward.h
index ddd8242a9..71af1a4fc 100644
--- a/src/formula/Prctl/CumulativeReward.h
+++ b/src/formula/Prctl/CumulativeReward.h
@@ -5,8 +5,8 @@
  *      Author: Christian Dehnert
  */
 
-#ifndef STORM_FORMULA_CUMULATIVEREWARD_H_
-#define STORM_FORMULA_CUMULATIVEREWARD_H_
+#ifndef STORM_FORMULA_PRCTL_CUMULATIVEREWARD_H_
+#define STORM_FORMULA_PRCTL_CUMULATIVEREWARD_H_
 
 #include "AbstractPathFormula.h"
 #include "AbstractStateFormula.h"
@@ -146,4 +146,4 @@ private:
 } //namespace formula
 } //namespace storm
 
-#endif /* STORM_FORMULA_INSTANTANEOUSREWARD_H_ */
+#endif /* STORM_FORMULA_PRCTL_INSTANTANEOUSREWARD_H_ */
diff --git a/src/formula/Prctl/Eventually.h b/src/formula/Prctl/Eventually.h
index 8fd5e7200..75c4df2ac 100644
--- a/src/formula/Prctl/Eventually.h
+++ b/src/formula/Prctl/Eventually.h
@@ -5,8 +5,8 @@
  *      Author: Christian Dehnert
  */
 
-#ifndef STORM_FORMULA_EVENTUALLY_H_
-#define STORM_FORMULA_EVENTUALLY_H_
+#ifndef STORM_FORMULA_PRCTL_EVENTUALLY_H_
+#define STORM_FORMULA_PRCTL_EVENTUALLY_H_
 
 #include "src/formula/abstract/Eventually.h"
 #include "src/formula/Prctl/AbstractPathFormula.h"
@@ -117,4 +117,4 @@ public:
 } //namespace formula
 } //namespace storm
 
-#endif /* STORM_FORMULA_EVENTUALLY_H_ */
+#endif /* STORM_FORMULA_PRCTL_EVENTUALLY_H_ */
diff --git a/src/formula/Prctl/Globally.h b/src/formula/Prctl/Globally.h
index c4b7fb3a4..14cbdec41 100644
--- a/src/formula/Prctl/Globally.h
+++ b/src/formula/Prctl/Globally.h
@@ -5,8 +5,8 @@
  *      Author: Christian Dehnert
  */
 
-#ifndef STORM_FORMULA_GLOBALLY_H_
-#define STORM_FORMULA_GLOBALLY_H_
+#ifndef STORM_FORMULA_PRCTL_GLOBALLY_H_
+#define STORM_FORMULA_PRCTL_GLOBALLY_H_
 
 #include "src/formula/abstract/Globally.h"
 #include "AbstractPathFormula.h"
@@ -129,4 +129,4 @@ public:
 } //namespace formula
 } //namespace storm
 
-#endif /* STORM_FORMULA_GLOBALLY_H_ */
+#endif /* STORM_FORMULA_PRCTL_GLOBALLY_H_ */
diff --git a/src/formula/Prctl/InstantaneousReward.h b/src/formula/Prctl/InstantaneousReward.h
index b182a4201..c88534c10 100644
--- a/src/formula/Prctl/InstantaneousReward.h
+++ b/src/formula/Prctl/InstantaneousReward.h
@@ -5,8 +5,8 @@
  *      Author: Christian Dehnert
  */
 
-#ifndef STORM_FORMULA_INSTANTANEOUSREWARD_H_
-#define STORM_FORMULA_INSTANTANEOUSREWARD_H_
+#ifndef STORM_FORMULA_PRCTL_INSTANTANEOUSREWARD_H_
+#define STORM_FORMULA_PRCTL_INSTANTANEOUSREWARD_H_
 
 #include "AbstractPathFormula.h"
 #include "AbstractStateFormula.h"
@@ -108,4 +108,4 @@ public:
 } //namespace formula
 } //namespace storm
 
-#endif /* STORM_FORMULA_INSTANTANEOUSREWARD_H_ */
+#endif /* STORM_FORMULA_PRCTL_INSTANTANEOUSREWARD_H_ */
diff --git a/src/formula/Prctl/Next.h b/src/formula/Prctl/Next.h
index 0464291be..e81be5887 100644
--- a/src/formula/Prctl/Next.h
+++ b/src/formula/Prctl/Next.h
@@ -5,8 +5,8 @@
  *      Author: Thomas Heinemann
  */
 
-#ifndef STORM_FORMULA_NEXT_H_
-#define STORM_FORMULA_NEXT_H_
+#ifndef STORM_FORMULA_PRCTL_NEXT_H_
+#define STORM_FORMULA_PRCTL_NEXT_H_
 
 #include "AbstractPathFormula.h"
 #include "AbstractStateFormula.h"
@@ -117,4 +117,4 @@ public:
 } //namespace formula
 } //namespace storm
 
-#endif /* STORM_FORMULA_NEXT_H_ */
+#endif /* STORM_FORMULA_PRCTL_NEXT_H_ */
diff --git a/src/formula/Prctl/Not.h b/src/formula/Prctl/Not.h
index b1d67423d..17bc27708 100644
--- a/src/formula/Prctl/Not.h
+++ b/src/formula/Prctl/Not.h
@@ -5,10 +5,11 @@
  *      Author: Thomas Heinemann
  */
 
-#ifndef STORM_FORMULA_NOT_H_
-#define STORM_FORMULA_NOT_H_
+#ifndef STORM_FORMULA_PRCTL_NOT_H_
+#define STORM_FORMULA_PRCTL_NOT_H_
 
 #include "AbstractStateFormula.h"
+#include "src/formula/abstract/Not.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelchecker/ForwardDeclarations.h"
 
@@ -49,22 +50,24 @@ class INotModelChecker {
  * @see AbstractFormula
  */
 template <class T>
-class Not : public AbstractStateFormula<T> {
+class Not : public storm::formula::abstract::Not<T, AbstractStateFormula<T>>,
+			   public AbstractStateFormula<T> {
 
 public:
 	/*!
 	 * Empty constructor
 	 */
 	Not() {
-		this->child = NULL;
+		//intentionally left empty
 	}
 
 	/*!
 	 * Constructor
 	 * @param child The child node
 	 */
-	Not(AbstractStateFormula<T>* child) {
-		this->child = child;
+	Not(AbstractStateFormula<T>* child) :
+		storm::formula::abstract::Not<T, AbstractStateFormula<T>>(child){
+		//intentionally left empty
 	}
 
 	/*!
@@ -74,33 +77,7 @@ public:
 	 * (this behavior can be prevented by setting them to NULL before deletion)
 	 */
 	virtual ~Not() {
-	  if (child != NULL) {
-		  delete child;
-	  }
-	}
-
-	/*!
-	 * @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
-	 */
-	virtual std::string toString() const {
-		std::string result = "!";
-		result += child->toString();
-		return result;
+	  //intentionally left empty
 	}
 
 	/*!
@@ -113,7 +90,7 @@ public:
 	virtual AbstractStateFormula<T>* clone() const {
 		Not<T>* result = new Not<T>();
 		if (child != NULL) {
-			result->setChild(child->clone());
+			result->setChild(getChild().clone());
 		}
 		return result;
 	}
@@ -130,23 +107,10 @@ public:
 	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.
-     * 
-     *  @param checker Formula checker object.
-     *  @return true iff the subtree conforms to some logic.
-     */
-	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
-		return checker.conforms(this->child);
-	}
-
-private:
-	AbstractStateFormula<T>* child;
 };
 
 } //namespace prctl
 } //namespace formula
 } //namespace storm
 
-#endif /* STORM_FORMULA_NOT_H_ */
+#endif /* STORM_FORMULA_PRCTL_NOT_H_ */
diff --git a/src/formula/Prctl/Or.h b/src/formula/Prctl/Or.h
index 484ab8557..ecf1202f9 100644
--- a/src/formula/Prctl/Or.h
+++ b/src/formula/Prctl/Or.h
@@ -5,10 +5,11 @@
  *      Author: Thomas Heinemann
  */
 
-#ifndef STORM_FORMULA_OR_H_
-#define STORM_FORMULA_OR_H_
+#ifndef STORM_FORMULA_PRCTL_OR_H_
+#define STORM_FORMULA_PRCTL_OR_H_
 
-#include "src/formula/AbstractStateFormula.h"
+#include "AbstractStateFormula.h"
+#include "src/formula/abstract/Or.h"
 #include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
@@ -51,28 +52,28 @@ class IOrModelChecker {
  * @see AbstractFormula
  */
 template <class T>
-class Or : public AbstractStateFormula<T> {
+class Or : public storm::formula::abstract::Or<T, AbstractStateFormula<T>>,
+			  public AbstractStateFormula<T> {
 
 public:
 	/*!
 	 * Empty constructor.
-	 * Will create an AND-node without subnotes. Will not represent a complete formula!
+	 * Will create an OR-node without subnotes. The result does not represent a complete formula!
 	 */
 	Or() {
-		left = NULL;
-		right = NULL;
+		//intentionally left empty
 	}
 
 	/*!
 	 * Constructor.
-	 * Creates an AND note with the parameters as subtrees.
+	 * Creates an OR note with the parameters as subtrees.
 	 *
 	 * @param left The left sub formula
 	 * @param right The right sub formula
 	 */
-	Or(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right) {
-		this->left = left;
-		this->right = right;
+	Or(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right) :
+		storm::formula::abstract::Or<T, AbstractStateFormula<T>>(left, right) {
+		//intentionally left empty
 	}
 
 	/*!
@@ -82,56 +83,7 @@ public:
 	 * (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(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 a string representation of the formula
-	 */
-	virtual std::string toString() const {
-		std::string result = "(";
-		result += left->toString();
-		result += " | ";
-		result += right->toString();
-		result += ")";
-		return result;
+	  //intentionally left empty
 	}
 
 	/*!
@@ -144,10 +96,10 @@ public:
 	virtual AbstractStateFormula<T>* clone() const {
 		Or<T>* result = new Or();
 		if (this->left != NULL) {
-		  result->setLeft(left->clone());
+		  result->setLeft(getLeft().clone());
 		}
 		if (this->right != NULL) {
-		  result->setRight(right->clone());
+		  result->setRight(getLeft().clone());
 		}
 		return result;
 	}
@@ -164,24 +116,10 @@ public:
 	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;
 };
 
 } //namespace prctl
 } //namespace formula
 } //namespace storm
 
-#endif /* STORM_FORMULA_OR_H_ */
+#endif /* STORM_FORMULA_PRCTL_OR_H_ */
diff --git a/src/formula/Prctl/ProbabilisticBoundOperator.h b/src/formula/Prctl/ProbabilisticBoundOperator.h
index b0d89e707..70e5c8ad5 100644
--- a/src/formula/Prctl/ProbabilisticBoundOperator.h
+++ b/src/formula/Prctl/ProbabilisticBoundOperator.h
@@ -5,13 +5,12 @@
  *      Author: Thomas Heinemann
  */
 
-#ifndef STORM_FORMULA_PROBABILISTICBOUNDOPERATOR_H_
-#define STORM_FORMULA_PROBABILISTICBOUNDOPERATOR_H_
+#ifndef STORM_FORMULA_PRCTL_PROBABILISTICBOUNDOPERATOR_H_
+#define STORM_FORMULA_PRCTL_PROBABILISTICBOUNDOPERATOR_H_
 
 #include "AbstractStateFormula.h"
 #include "AbstractPathFormula.h"
-#include "src/formula/PathBoundOperator.h"
-#include "src/formula/OptimizingOperator.h"
+#include "src/formula/abstract/ProbabilisticBoundOperator.h"
 #include "utility/ConstTemplates.h"
 
 namespace storm {
@@ -54,7 +53,8 @@ class IProbabilisticBoundOperatorModelChecker {
  * @see AbstractFormula
  */
 template<class T>
-class ProbabilisticBoundOperator : public PathBoundOperator<T> {
+class ProbabilisticBoundOperator : public storm::formula::abstract::ProbabilisticBoundOperator<T, AbstractPathFormula<T>>,
+											  public AbstractStateFormula {
 
 public:
 	/*!
@@ -74,24 +74,29 @@ public:
 	 * @param pathFormula The child node
 	 */
 	ProbabilisticBoundOperator(
-			typename PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractPathFormula<T>* pathFormula)
-			: PathBoundOperator<T>(comparisonRelation, bound, pathFormula) {
+			typename storm::formula::abstract::PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractPathFormula<T>* pathFormula)
+			: storm::formula::abstract::ProbabilisticBoundOperator<T>(comparisonRelation, bound, pathFormula) {
 		// Intentionally left empty
 	}
 
+	/*!
+	 *
+	 * @param comparisonRelation
+	 * @param bound
+	 * @param pathFormula
+	 * @param minimumOperator
+	 */
 	ProbabilisticBoundOperator(
-			typename PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractPathFormula<T>* pathFormula, bool minimumOperator)
-			: PathBoundOperator<T>(comparisonRelation, bound, pathFormula, minimumOperator){
+			typename storm::formula::abstract::PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractPathFormula<T>* pathFormula, bool minimumOperator)
+			: storm::formula::abstract::ProbabilisticBoundOperator<T>(comparisonRelation, bound, pathFormula, minimumOperator){
 		// Intentionally left empty
 	}
 
 	/*!
-	 * @returns a string representation of the formula
+	 *
 	 */
-	virtual std::string toString() const {
-		std::string result = "P ";
-		result += PathBoundOperator<T>::toString();
-		return result;
+	virtual ~ProbabilisticBoundOperator() {
+		// Intentionally left empty
 	}
 
 	/*!
@@ -127,4 +132,4 @@ public:
 } //namespace formula
 } //namespace storm
 
-#endif /* STORM_FORMULA_PROBABILISTICBOUNDOPERATOR_H_ */
+#endif /* STORM_FORMULA_PRCTL_PROBABILISTICBOUNDOPERATOR_H_ */
diff --git a/src/formula/Prctl/ProbabilisticNoBoundOperator.h b/src/formula/Prctl/ProbabilisticNoBoundOperator.h
index af9bc29d0..de444bd3c 100644
--- a/src/formula/Prctl/ProbabilisticNoBoundOperator.h
+++ b/src/formula/Prctl/ProbabilisticNoBoundOperator.h
@@ -5,12 +5,12 @@
  *      Author: thomas
  */
 
-#ifndef STORM_FORMULA_PROBABILISTICNOBOUNDOPERATOR_H_
-#define STORM_FORMULA_PROBABILISTICNOBOUNDOPERATOR_H_
+#ifndef STORM_FORMULA_PRCTL_PROBABILISTICNOBOUNDOPERATOR_H_
+#define STORM_FORMULA_PRCTL_PROBABILISTICNOBOUNDOPERATOR_H_
 
 #include "AbstractFormula.h"
 #include "AbstractPathFormula.h"
-#include "PathNoBoundOperator.h"
+#include "src/formula/abstract/ProbabilisticNoBoundOperator.h"
 
 namespace storm {
 namespace formula {
@@ -47,12 +47,13 @@ namespace prctl {
  * @see AbstractFormula
  */
 template <class T>
-class ProbabilisticNoBoundOperator: public PathNoBoundOperator<T> {
+class ProbabilisticNoBoundOperator: public storm::formula::abstract::ProbabilisticNoBoundOperator<T, AbstractPathFormula<T>>,
+												public AbstractStateFormula<T> {
 public:
 	/*!
 	 * Empty constructor
 	 */
-	ProbabilisticNoBoundOperator() : PathNoBoundOperator<T>(nullptr) {
+	ProbabilisticNoBoundOperator() {
 		// Intentionally left empty
 	}
 
@@ -61,7 +62,8 @@ public:
 	 *
 	 * @param pathFormula The child node.
 	 */
-	ProbabilisticNoBoundOperator(AbstractPathFormula<T>* pathFormula) : PathNoBoundOperator<T>(pathFormula) {
+	ProbabilisticNoBoundOperator(AbstractPathFormula<T>* pathFormula)
+		: storm::formula::abstract::ProbabilisticNoBoundOperator<T, AbstractPathFormula<T>>(pathFormula) {
 		// Intentionally left empty
 	}
 
@@ -70,17 +72,16 @@ public:
 	 *
 	 * @param pathFormula The child node.
 	 */
-	ProbabilisticNoBoundOperator(AbstractPathFormula<T>* pathFormula, bool minimumOperator) : PathNoBoundOperator<T>(pathFormula, minimumOperator) {
+	ProbabilisticNoBoundOperator(AbstractPathFormula<T>* pathFormula, bool minimumOperator)
+		: storm::formula::abstract::ProbabilisticNoBoundOperator<T, AbstractPathFormula<T>>(pathFormula, minimumOperator) {
 		// Intentionally left empty
 	}
 
 	/*!
-	 * @returns a string representation of the formula
+	 * Destructor
 	 */
-	virtual std::string toString() const {
-		std::string result = "P";
-		result += PathNoBoundOperator<T>::toString();
-		return result;
+	virtual ~ProbabilisticNoBoundOperator() {
+		// Intentionally left empty
 	}
 };
 
@@ -88,4 +89,4 @@ public:
 } //namespace formula
 } //namespace storm
 
-#endif /* STORM_FORMULA_PROBABILISTICNOBOUNDOPERATOR_H_ */
+#endif /* STORM_FORMULA_PRCTL_PROBABILISTICNOBOUNDOPERATOR_H_ */
diff --git a/src/formula/Prctl/ReachabilityReward.h b/src/formula/Prctl/ReachabilityReward.h
index 3289f3df9..1e182aabc 100644
--- a/src/formula/Prctl/ReachabilityReward.h
+++ b/src/formula/Prctl/ReachabilityReward.h
@@ -5,11 +5,12 @@
  *      Author: Christian Dehnert
  */
 
-#ifndef STORM_FORMULA_REACHABILITYREWARD_H_
-#define STORM_FORMULA_REACHABILITYREWARD_H_
+#ifndef STORM_FORMULA_PRCTL_REACHABILITYREWARD_H_
+#define STORM_FORMULA_PRCTL_REACHABILITYREWARD_H_
 
-#include "src/formula/AbstractPathFormula.h"
-#include "src/formula/AbstractStateFormula.h"
+#include "AbstractPathFormula.h"
+#include "AbstractStateFormula.h"
+#include "../abstract/Eventually.h"
 #include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
@@ -49,14 +50,15 @@ class IReachabilityRewardModelChecker {
  * @see AbstractFormula
  */
 template <class T>
-class ReachabilityReward : public AbstractPathFormula<T> {
+class ReachabilityReward : public storm::formula::abstract::Eventually<T, AbstractStateFormula<T>>,
+									public AbstractPathFormula<T> {
 
 public:
 	/*!
 	 * Empty constructor
 	 */
 	ReachabilityReward() {
-		this->child = nullptr;
+		// Intentionally left empty
 	}
 
 	/*!
@@ -64,8 +66,9 @@ public:
 	 *
 	 * @param child The child node
 	 */
-	ReachabilityReward(AbstractStateFormula<T>* child) {
-		this->child = child;
+	ReachabilityReward(AbstractStateFormula<T>* child) :
+		storm::formula::abstract::Eventually<T, AbstractStateFormula<T>>(child){
+		// Intentionally left empty
 	}
 
 	/*!
@@ -75,33 +78,7 @@ public:
 	 * (this behaviour can be prevented by setting the subtrees to nullptr before deletion)
 	 */
 	virtual ~ReachabilityReward() {
-	  if (child != nullptr) {
-		  delete child;
-	  }
-	}
-
-	/*!
-	 * @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
-	 */
-	virtual std::string toString() const {
-		std::string result = "F ";
-		result += child->toString();
-		return result;
+		// Intentionally left empty
 	}
 
 	/*!
@@ -113,8 +90,8 @@ public:
 	 */
 	virtual AbstractPathFormula<T>* clone() const {
 		ReachabilityReward<T>* result = new ReachabilityReward<T>();
-		if (child != nullptr) {
-			result->setChild(child);
+		if (getChild() != nullptr) {
+			result->setChild(*getChild());
 		}
 		return result;
 	}
@@ -131,23 +108,10 @@ public:
 	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
 		return modelChecker.template as<IReachabilityRewardModelChecker>()->checkReachabilityReward(*this, qualitative);
 	}
-	
-	/*!
-     *  @brief Checks if the subtree conforms to some logic.
-     * 
-     *  @param checker Formula checker object.
-     *  @return true iff the subtree conforms to some logic.
-     */
-	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
-		return checker.conforms(this->child);
-	}
-
-private:
-	AbstractStateFormula<T>* child;
 };
 
 } //namespace prctl
 } //namespace formula
 } //namespace storm
 
-#endif /* STORM_FORMULA_REACHABILITYREWARD_H_ */
+#endif /* STORM_FORMULA_PRCTL_REACHABILITYREWARD_H_ */
diff --git a/src/formula/Prctl/RewardBoundOperator.h b/src/formula/Prctl/RewardBoundOperator.h
index 452d10685..67389bde4 100644
--- a/src/formula/Prctl/RewardBoundOperator.h
+++ b/src/formula/Prctl/RewardBoundOperator.h
@@ -5,32 +5,18 @@
  *      Author: Thomas Heinemann
  */
 
-#ifndef STORM_FORMULA_REWARDBOUNDOPERATOR_H_
-#define STORM_FORMULA_REWARDBOUNDOPERATOR_H_
+#ifndef STORM_FORMULA_PRCTL_REWARDBOUNDOPERATOR_H_
+#define STORM_FORMULA_PRCTL_REWARDBOUNDOPERATOR_H_
 
-#include "AbstractStateFormula.h"
 #include "AbstractPathFormula.h"
-#include "PathBoundOperator.h"
+#include "AbstractStateFormula.h"
+#include "src/formula/abstract/RewardBoundOperator.h"
 #include "utility/ConstTemplates.h"
 
 namespace storm {
 namespace formula {
 namespace prctl {
 
-template <class T> class RewardBoundOperator;
-
-/*!
- *  @brief Interface class for model checkers that support RewardBoundOperator.
- *
- *  All model checkers that support the formula class PathBoundOperator must inherit
- *  this pure virtual class.
- */
-template <class T>
-class IRewardBoundOperatorModelChecker {
-    public:
-        virtual storm::storage::BitVector* checkRewardBoundOperator(const RewardBoundOperator<T>& obj) const = 0;
-};
-
 /*!
  * @brief
  * Class for a Abstract formula tree with a R (reward) operator node over a reward interval as root.
@@ -52,13 +38,14 @@ class IRewardBoundOperatorModelChecker {
  * @see AbstractFormula
  */
 template<class T>
-class RewardBoundOperator : public PathBoundOperator<T> {
+class RewardBoundOperator : public storm::formula::abstract::RewardBoundOperator<T, AbstractPathFormula<T>>,
+									 public AbstractStateFormula<T> {
 
 public:
 	/*!
 	 * Empty constructor
 	 */
-	RewardBoundOperator() : PathBoundOperator<T>(PathBoundOperator<T>::LESS_EQUAL, storm::utility::constGetZero<T>(), nullptr) {
+	RewardBoundOperator() {
 		// Intentionally left empty
 	}
 
@@ -70,26 +57,25 @@ public:
 	 * @param pathFormula The child node
 	 */
 	RewardBoundOperator(
-			typename PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractPathFormula<T>* pathFormula) :
-				PathBoundOperator<T>(comparisonRelation, bound, pathFormula) {
+			typename storm::formula::abstract::PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractPathFormula<T>* pathFormula) :
+				storm::formula::abstract::RewardBoundOperator<T>(comparisonRelation, bound, pathFormula) {
 		// Intentionally left empty
 	}
 
+	/*!
+	 * Constructor
+	 *
+	 * @param comparisonRelation
+	 * @param bound
+	 * @param pathFormula
+	 * @param minimumOperator
+	 */
 	RewardBoundOperator(
 			typename PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractPathFormula<T>* pathFormula, bool minimumOperator)
 			: PathBoundOperator<T>(comparisonRelation, bound, pathFormula, minimumOperator) {
 		// Intentionally left empty
 	}
 
-	/*!
-	 * @returns a string representation of the formula
-	 */
-	virtual std::string toString() const {
-		std::string result = "R ";
-		result += PathBoundOperator<T>::toString();
-		return result;
-	}
-
 	/*!
 	 * Clones the called object.
 	 *
@@ -123,4 +109,4 @@ public:
 } //namespace formula
 } //namespace storm
 
-#endif /* STORM_FORMULA_REWARDBOUNDOPERATOR_H_ */
+#endif /* STORM_FORMULA_PRCTL_REWARDBOUNDOPERATOR_H_ */
diff --git a/src/formula/Prctl/RewardNoBoundOperator.h b/src/formula/Prctl/RewardNoBoundOperator.h
index ed65a5f3c..76ca979c1 100644
--- a/src/formula/Prctl/RewardNoBoundOperator.h
+++ b/src/formula/Prctl/RewardNoBoundOperator.h
@@ -5,11 +5,10 @@
  *      Author: Christian Dehnert
  */
 
-#ifndef STORM_FORMULA_REWARDNOBOUNDOPERATOR_H_
-#define STORM_FORMULA_REWARDNOBOUNDOPERATOR_H_
+#ifndef STORM_FORMULA_PRCTL_REWARDNOBOUNDOPERATOR_H_
+#define STORM_FORMULA_PRCTL_REWARDNOBOUNDOPERATOR_H_
 
 #include "AbstractFormula.h"
-#include "AbstractPathFormula.h"
 #include "PathNoBoundOperator.h"
 
 namespace storm {
@@ -46,8 +45,8 @@ namespace prctl {
  * @see ProbabilisticIntervalOperator
  * @see AbstractFormula
  */
-template <class T>
-class RewardNoBoundOperator: public PathNoBoundOperator<T> {
+template <class T, class FormulaType>
+class RewardNoBoundOperator: public PathNoBoundOperator<T, FormulaType> {
 public:
 	/*!
 	 * Empty constructor
@@ -61,7 +60,7 @@ public:
 	 *
 	 * @param pathFormula The child node.
 	 */
-	RewardNoBoundOperator(AbstractPathFormula<T>* pathFormula) : PathNoBoundOperator<T>(pathFormula) {
+	RewardNoBoundOperator(FormulaType* pathFormula) : PathNoBoundOperator<T>(pathFormula) {
 		// Intentionally left empty
 	}
 
@@ -70,7 +69,7 @@ public:
 	 *
 	 * @param pathFormula The child node.
 	 */
-	RewardNoBoundOperator(AbstractPathFormula<T>* pathFormula, bool minimumOperator) : PathNoBoundOperator<T>(pathFormula, minimumOperator) {
+	RewardNoBoundOperator(FormulaType* pathFormula, bool minimumOperator) : PathNoBoundOperator<T>(pathFormula, minimumOperator) {
 		// Intentionally left empty
 	}
 
@@ -88,4 +87,4 @@ public:
 } //namespace formula
 } //namespace storm
 
-#endif /* STORM_FORMULA_REWARDNOBOUNDOPERATOR_H_ */
+#endif /* STORM_FORMULA_PRCTL_REWARDNOBOUNDOPERATOR_H_ */
diff --git a/src/formula/Prctl/StateBoundOperator.h b/src/formula/Prctl/StateBoundOperator.h
deleted file mode 100644
index 1b6367cfd..000000000
--- a/src/formula/Prctl/StateBoundOperator.h
+++ /dev/null
@@ -1,199 +0,0 @@
-/*
- * BoundOperator.h
- *
- *  Created on: 27.12.2012
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_FORMULA_STATEBOUNDOPERATOR_H_
-#define STORM_FORMULA_STATEBOUNDOPERATOR_H_
-
-#include "src/formula/AbstractStateFormula.h"
-#include "src/formula/AbstractPathFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
-#include "src/modelchecker/AbstractModelChecker.h"
-#include "src/utility/ConstTemplates.h"
-
-namespace storm {
-namespace formula {
-namespace prctl {
-
-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;
-};
-
-/*!
- * @brief
- * Class for a Abstract formula tree with a P (probablistic) operator node over a probability interval
- * as root.
- *
- * Has one Abstract state formula as sub formula/tree.
- *
- * @par Semantics
- * 	  The formula holds iff the probability that the state 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 AbstractStateFormula
- * @see AbstractPathFormula
- * @see ProbabilisticOperator
- * @see ProbabilisticNoBoundsOperator
- * @see AbstractFormula
- */
-template<class T>
-class StateBoundOperator : public AbstractStateFormula<T> {
-
-public:
-	enum ComparisonType { LESS, LESS_EQUAL, GREATER, GREATER_EQUAL };
-
-	/*!
-	 * Constructor
-	 *
-	 * @param comparisonOperator The relation for the bound.
-	 * @param bound The bound for the probability
-	 * @param stateFormula The child node
-	 */
-	StateBoundOperator(ComparisonType comparisonOperator, T bound, AbstractStateFormula<T>* stateFormula)
-		: comparisonOperator(comparisonOperator), bound(bound), stateFormula(stateFormula) {
-		// Intentionally left empty
-	}
-
-	/*!
-	 * Destructor
-	 *
-	 * The subtree is deleted with the object
-	 * (this behavior can be prevented by setting them to NULL before deletion)
-	 */
-	virtual ~StateBoundOperator() {
-	 if (stateFormula != nullptr) {
-		 delete stateFormula;
-	 }
-	}
-
-	/*!
-	 * @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
-	 */
-	const ComparisonType getComparisonOperator() const {
-		return comparisonOperator;
-	}
-
-	void setComparisonOperator(ComparisonType comparisonOperator) {
-		this->comparisonOperator = comparisonOperator;
-	}
-
-	/*!
-	 * @returns the bound for the measure
-	 */
-	const T& getBound() const {
-		return bound;
-	}
-
-	/*!
-	 * Sets the interval in which the probability that the path formula holds may lie in.
-	 *
-	 * @param bound The bound for the measure
-	 */
-	void setBound(T bound) {
-		this->bound = bound;
-	}
-
-	/*!
-	 * @returns a string representation of the formula
-	 */
-	virtual std::string toString() const {
-		std::string result = " ";
-		switch (comparisonOperator) {
-		case LESS: result += "< "; break;
-		case LESS_EQUAL: result += "<= "; break;
-		case GREATER: result += "> "; break;
-		case GREATER_EQUAL: result += ">= "; break;
-		}
-		result += std::to_string(bound);
-		result += " [";
-		result += stateFormula->toString();
-		result += "]";
-		return result;
-	}
-
-	bool meetsBound(T value) const {
-		switch (comparisonOperator) {
-		case LESS: return value < bound; break;
-		case LESS_EQUAL: return value <= bound; break;
-		case GREATER: return value > bound; break;
-		case GREATER_EQUAL: return value >= bound; break;
-		default: return false;
-		}
-	}
-
-	/*!
-	 * 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.
-     * 
-     *  @param checker Formula checker object.
-     *  @return true iff the subtree conforms to some logic.
-     */
-	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
-        return checker.conforms(this->stateFormula);
-    }
-
-private:
-	ComparisonType comparisonOperator;
-	T bound;
-	AbstractStateFormula<T>* stateFormula;
-};
-
-} //namespace prctl
-} //namespace formula
-} //namespace storm
-
-#endif /* STORM_FORMULA_STATEBOUNDOPERATOR_H_ */
diff --git a/src/formula/Prctl/StateNoBoundOperator.h b/src/formula/Prctl/StateNoBoundOperator.h
deleted file mode 100644
index f18edc23e..000000000
--- a/src/formula/Prctl/StateNoBoundOperator.h
+++ /dev/null
@@ -1,150 +0,0 @@
-/*
- * StateNoBoundOperator.h
- *
- *  Created on: 09.04.2013
- *      Author: Thomas Heinemann
- */
-
-#ifndef STORM_FORMULA_STATENOBOUNDOPERATOR_H_
-#define STORM_FORMULA_STATENOBOUNDOPERATOR_H_
-
-#include "src/formula/AbstractFormula.h"
-#include "src/formula/AbstractPathFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
-
-#include "src/modelchecker/ForwardDeclarations.h"
-
-namespace storm {
-namespace formula {
-namespace prctl {
-
-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;
-};
-
-
-/*!
- * @brief
- * Class for a Abstract formula tree with an operator without declaration of probabilities
- * as root.
- *
- * Checking a formula with this operator as root returns the probabilities that the path formula holds
- * (for each state)
- *
- * Has one Abstract state formula as sub formula/tree.
- *
- * @note
- * 	This class is a hybrid of a state and path formula, and may only appear as the outermost operator.
- * 	Hence, it is seen as neither a state nor a path formula, but is directly derived from AbstractFormula.
- *
- * @note
- * 	This class does not contain a check() method like the other formula classes.
- * 	The check method should only be called by the model checker to infer the correct check function for sub
- * 	formulas. As this operator can only appear at the root, the method is not useful here.
- * 	Use the checkProbabilisticNoBoundOperator method from the DtmcPrctlModelChecker class instead.
- *
- * 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 AbstractStateFormula
- * @see AbstractPathFormula
- * @see SteadyStateNoBoundOperator
- * @see AbstractFormula
- */
-template <class T>
-class StateNoBoundOperator: public storm::formula::AbstractFormula<T> {
-public:
-	/*!
-	 * Empty constructor
-	 */
-	StateNoBoundOperator() {
-		stateFormula = nullptr;
-	}
-
-	/*!
-	 * Constructor
-	 */
-	StateNoBoundOperator(AbstractStateFormula<T>* stateFormula) {
-		this->stateFormula = stateFormula;
-	}
-
-	/*!
-	 * Destructor
-	 *
-	 * Deletes the subtree
-	 */
-	virtual ~StateNoBoundOperator() {
-		if (stateFormula != nullptr) {
-			delete stateFormula;
-		}
-	}
-
-	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.
-	 *
-	 * @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<IStateNoBoundOperatorModelChecker>()->checkStateNoBoundOperator(*this);
-	}
-
-	/*!
-	 * @returns a string representation of the formula
-	 */
-	virtual std::string toString() const {
-		std::string result;
-		result += " = ? [";
-		result += this->getStateFormula().toString();
-		result += "]";
-		return result;
-	}
-
-	/*!
-     *  @brief Checks if the subtree conforms to some logic.
-     *
-     *  @param checker Formula checker object.
-     *  @return true iff the subtree conforms to some logic.
-     */
-	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
-		return checker.conforms(this->stateFormula);
-	}
-
-private:
-	AbstractStateFormula<T>* stateFormula;
-};
-
-} //namespace prctl
-} //namespace formula
-} //namespace storm
-#endif /* STORM_FORMULA_STATENOBOUNDOPERATOR_H_ */
diff --git a/src/formula/Prctl/SteadyStateReward.h b/src/formula/Prctl/SteadyStateReward.h
index 51c895b5c..8dde583e9 100644
--- a/src/formula/Prctl/SteadyStateReward.h
+++ b/src/formula/Prctl/SteadyStateReward.h
@@ -5,11 +5,12 @@
  *      Author: Thomas Heinemann
  */
 
-#ifndef STORM_FORMULA_STEADYSTATEREWARD_H_
-#define STORM_FORMULA_STEADYSTATEREWARD_H_
+#ifndef STORM_FORMULA_PRCTL_STEADYSTATEREWARD_H_
+#define STORM_FORMULA_PRCTL_STEADYSTATEREWARD_H_
 
 #include "AbstractPathFormula.h"
 #include "AbstractStateFormula.h"
+#include "src/formula/abstract/SteadyStateReward.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include <string>
 
@@ -45,7 +46,8 @@ class ISteadyStateRewardModelChecker {
  * @see AbstractFormula
  */
 template <class T>
-class SteadyStateReward: public storm::formula::AbstractPathFormula<T> {
+class SteadyStateReward: public storm::formula::abstract::SteadyStateReward<T>,
+								 public storm::formula::AbstractPathFormula<T> {
 public:
 	/*!
 	 * Empty constructor
@@ -58,13 +60,6 @@ public:
 		// Intentionally left empty
 	}
 
-	/*!
-	 * @returns a string representation of the formula
-	 */
-	virtual std::string toString() const {
-		return "S";
-	}
-
 	/*!
 	 * Clones the called object.
 	 *
@@ -88,21 +83,9 @@ public:
 	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
 		return modelChecker.template as<ISteadyStateRewardModelChecker>()->checkSteadyStateReward(*this, qualitative);
 	}
-
-	/*!
-     *  @brief Checks if all subtrees conform to some logic.
-     *
-     *  As SteadyStateReward objects have no subformulas, we return true here.
-     *
-     *  @param checker Formula checker object.
-     *  @return true
-     */
-	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
-		return true;
-	}
 };
 
 } //namespace prctl
 } //namespace formula
 } //namespace storm
-#endif /* STORM_FORMULA_STEADYSTATEREWARD_H_ */
+#endif /* STORM_FORMULA_PRCTL_STEADYSTATEREWARD_H_ */
diff --git a/src/formula/Prctl/Until.h b/src/formula/Prctl/Until.h
index 5f66e47a6..ddfc2ba66 100644
--- a/src/formula/Prctl/Until.h
+++ b/src/formula/Prctl/Until.h
@@ -5,11 +5,12 @@
  *      Author: Thomas Heinemann
  */
 
-#ifndef STORM_FORMULA_UNTIL_H_
-#define STORM_FORMULA_UNTIL_H_
+#ifndef STORM_FORMULA_PRCTL_UNTIL_H_
+#define STORM_FORMULA_PRCTL_UNTIL_H_
 
 #include "AbstractPathFormula.h"
 #include "AbstractStateFormula.h"
+#include "src/formula/abstract/Until.h"
 #include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
@@ -53,15 +54,15 @@ class IUntilModelChecker {
  * @see AbstractFormula
  */
 template <class T>
-class Until : public AbstractPathFormula<T> {
+class Until : public storm::formula::abstract::Until<T, AbstractStateFormula<T>>,
+				  public AbstractPathFormula<T> {
 
 public:
 	/*!
 	 * Empty constructor
 	 */
 	Until() {
-		this->left = NULL;
-		this->right = NULL;
+		// Intentionally left empty
 	}
 
 	/*!
@@ -70,9 +71,9 @@ public:
 	 * @param left The left formula subtree
 	 * @param right The left formula subtree
 	 */
-	Until(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right) {
-		this->left = left;
-		this->right = right;
+	Until(AbstractStateFormula<T>* left, AbstractStateFormula<T>* right)
+		: storm::formula::abstract::Until<T, AbstractStateFormula<T>>(left, right) {
+		// Intentionally left empty
 	}
 
 	/*!
@@ -82,54 +83,7 @@ public:
 	 * (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(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 a string representation of the formula
-	 */
-	virtual std::string toString() const {
-		std::string result = left->toString();
-		result += " U ";
-		result += right->toString();
-		return result;
+	  // Intentionally left empty
 	}
 
 	/*!
@@ -162,24 +116,10 @@ public:
 	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;
 };
 
 } //namespace prctl
 } //namespace formula
 } //namespace storm
 
-#endif /* STORM_FORMULA_UNTIL_H_ */
+#endif /* STORM_FORMULA_PRCTL_UNTIL_H_ */