diff --git a/src/formula/abstract/And.h b/src/formula/abstract/And.h
index e1b3a07c4..74e6c2e24 100644
--- a/src/formula/abstract/And.h
+++ b/src/formula/abstract/And.h
@@ -32,7 +32,7 @@ namespace abstract {
  * @see AbstractFormula
  * @see AbstractFormula
  */
-template <class T>
+template <class T, class FormulaType>
 class And : public AbstractFormula<T> {
 
 public:
@@ -52,7 +52,7 @@ public:
 	 * @param left The left sub formula
 	 * @param right The right sub formula
 	 */
-	And(AbstractFormula<T>* left, AbstractFormula<T>* right) {
+	And(FormulaType* left, FormulaType* right) {
 		this->left = left;
 		this->right = right;
 	}
@@ -72,35 +72,12 @@ 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(AbstractFormula<T>* newLeft) {
+	void setLeft(FormulaType* newLeft) {
 		left = newLeft;
 	}
 
@@ -109,27 +86,50 @@ protected:
 	 *
 	 * @param newRight the new right child.
 	 */
-	void setRight(AbstractFormula<T>* newRight) {
+	void setRight(FormulaType* newRight) {
 		right = newRight;
 	}
 
 	/*!
 	 * @returns a pointer to the left child node
 	 */
-	const AbstractFormula<T>& getLeft() const {
+	const FormulaType& getLeft() const {
 		return *left;
 	}
 
 	/*!
 	 * @returns a pointer to the right child node
 	 */
-	const AbstractFormula<T>& getRight() const {
+	const FormulaType& 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;
+	}
+
+	/*!
+	 *	@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;
+	FormulaType* left;
+	FormulaType* right;
 };
 
 } //namespace abstract
diff --git a/src/formula/abstract/BoundedEventually.h b/src/formula/abstract/BoundedEventually.h
index 3753fbab3..250804b8a 100644
--- a/src/formula/abstract/BoundedEventually.h
+++ b/src/formula/abstract/BoundedEventually.h
@@ -35,7 +35,7 @@ namespace abstract {
  * @see AbstractFormula
  * @see AbstractFormula
  */
-template <class T>
+template <class T, class FormulaType>
 class BoundedEventually : public AbstractFormula<T> {
 
 public:
@@ -53,7 +53,7 @@ public:
 	 * @param child The child formula subtree
 	 * @param bound The maximal number of steps
 	 */
-	BoundedEventually(AbstractFormula<T>* child, uint_fast64_t bound) {
+	BoundedEventually(FormulaType* child, uint_fast64_t bound) {
 		this->child = child;
 		this->bound = bound;
 	}
@@ -70,6 +70,21 @@ public:
 	  }
 	}
 
+	/*!
+	 * @returns the child node
+	 */
+	const FormulaType& getChild() const {
+		return *child;
+	}
+
+	/*!
+	 * Sets the subtree
+	 * @param child the new child node
+	 */
+	void setChild(FormulaType* child) {
+		this->child = child;
+	}
+
 	/*!
 	 * @returns the maximally allowed number of steps for the bounded until operator
 	 */
@@ -107,25 +122,9 @@ 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:
-	AbstractFormula<T>* child;
+	FormulaType* child;
 	uint_fast64_t bound;
 };
 
diff --git a/src/formula/abstract/BoundedNaryUntil.h b/src/formula/abstract/BoundedNaryUntil.h
index 63594ff0e..e8a65cb9a 100644
--- a/src/formula/abstract/BoundedNaryUntil.h
+++ b/src/formula/abstract/BoundedNaryUntil.h
@@ -39,7 +39,7 @@ namespace abstract {
  * @see AbstractFormula
  * @see AbstractFormula
  */
-template <class T>
+template <class T, class FormulaType>
 class BoundedNaryUntil : public AbstractFormula<T> {
 
 public:
@@ -48,7 +48,7 @@ public:
 	 */
 	BoundedNaryUntil() {
 		this->left = nullptr;
-		this->right = new std::vector<std::tuple<AbstractFormula<T>*,T,T>>();
+		this->right = new std::vector<std::tuple<FormulaType*,T,T>>();
 	}
 
 	/*!
@@ -57,7 +57,7 @@ public:
 	 * @param left The left formula subtree
 	 * @param right The left formula subtree
 	 */
-	BoundedNaryUntil(AbstractFormula<T>* left, std::vector<std::tuple<AbstractFormula<T>*,T,T>>* right) {
+	BoundedNaryUntil(FormulaType* left, std::vector<std::tuple<FormulaType*,T,T>>* right) {
 		this->left = left;
 		this->right = right;
 	}
@@ -77,44 +77,16 @@ 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(AbstractFormula<T>* newLeft) {
+	void setLeft(FormulaType* newLeft) {
 		left = newLeft;
 	}
 
-	void setRight(std::vector<std::tuple<AbstractFormula<T>*,T,T>>* newRight) {
+	void setRight(std::vector<std::tuple<FormulaType*,T,T>>* newRight) {
 		right = newRight;
 	}
 
@@ -124,28 +96,55 @@ protected:
 	 *
 	 * @param newRight the new right child.
 	 */
-	void addRight(AbstractFormula<T>* newRight, T upperBound, T lowerBound) {
-		this->right->push_back(std::tuple<AbstractFormula<T>*,T,T>(newRight, upperBound, lowerBound));
+	void addRight(FormulaType* newRight, T upperBound, T lowerBound) {
+		this->right->push_back(std::tuple<FormulaType*,T,T>(newRight, upperBound, lowerBound));
 	}
 
 	/*!
 	 * @returns a pointer to the left child node
 	 */
-	const AbstractFormula<T>& getLeft() const {
+	const FormulaType& getLeft() const {
 		return *left;
 	}
 
 	/*!
 	 * @returns a pointer to the right child nodes.
 	 */
-	const std::vector<std::tuple<AbstractFormula<T>*,T,T>>& getRight() const {
+	const std::vector<std::tuple<FormulaType*,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();
+	}
+
+	/*!
+     *  @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:
-	AbstractFormula<T>* left;
-	std::vector<std::tuple<AbstractFormula<T>*,T,T>>* right;
+	FormulaType* left;
+	std::vector<std::tuple<FormulaType*,T,T>>* right;
 };
 
 } //namespace abstract
diff --git a/src/formula/abstract/BoundedUntil.h b/src/formula/abstract/BoundedUntil.h
index 1c57a7271..83838b0da 100644
--- a/src/formula/abstract/BoundedUntil.h
+++ b/src/formula/abstract/BoundedUntil.h
@@ -33,7 +33,7 @@ namespace abstract {
  * @see AbstractFormula
  * @see AbstractFormula
  */
-template <class T>
+template <class T, class FormulaType>
 class BoundedUntil : public AbstractFormula<T> {
 
 public:
@@ -53,7 +53,7 @@ public:
 	 * @param right The left formula subtree
 	 * @param bound The maximal number of steps
 	 */
-	BoundedUntil(AbstractFormula<T>* left, AbstractFormula<T>* right,
+	BoundedUntil(FormulaType* left, FormulaType* right,
 					 uint_fast64_t bound) {
 		this->left = left;
 		this->right = right;
@@ -75,6 +75,38 @@ public:
 	  }
 	}
 
+	/*!
+	 * Sets the left child node.
+	 *
+	 * @param newLeft the new left child.
+	 */
+	void setLeft(FormulaType* newLeft) {
+		left = newLeft;
+	}
+
+	/*!
+	 * Sets the right child node.
+	 *
+	 * @param newRight the new right child.
+	 */
+	void setRight(FormulaType* newRight) {
+		right = newRight;
+	}
+
+	/*!
+	 * @returns a pointer to the left child node
+	 */
+	const FormulaType& getLeft() const {
+		return *left;
+	}
+
+	/*!
+	 * @returns a pointer to the right child node
+	 */
+	const FormulaType& getRight() const {
+		return *right;
+	}
+
 	/*!
 	 * @returns the maximally allowed number of steps for the bounded until operator
 	 */
@@ -113,42 +145,9 @@ public:
 		return checker.conforms(this->left) && checker.conforms(this->right);
 	}
 
-protected:
-	/*!
-	 * Sets the left child node.
-	 *
-	 * @param newLeft the new left child.
-	 */
-	void setLeft(AbstractFormula<T>* newLeft) {
-		left = newLeft;
-	}
-
-	/*!
-	 * Sets the right child node.
-	 *
-	 * @param newRight the new right child.
-	 */
-	void setRight(AbstractFormula<T>* newRight) {
-		right = newRight;
-	}
-
-	/*!
-	 * @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:
-	AbstractFormula<T>* left;
-	AbstractFormula<T>* right;
+	FormulaType* left;
+	FormulaType* right;
 	uint_fast64_t bound;
 };
 
diff --git a/src/formula/abstract/Eventually.h b/src/formula/abstract/Eventually.h
index 88be7de95..508401390 100644
--- a/src/formula/abstract/Eventually.h
+++ b/src/formula/abstract/Eventually.h
@@ -32,7 +32,7 @@ namespace abstract {
  * @see AbstractFormula
  * @see AbstractFormula
  */
-template <class T>
+template <class T, class FormulaType>
 class Eventually : public AbstractFormula<T> {
 
 public:
@@ -48,7 +48,7 @@ public:
 	 *
 	 * @param child The child node
 	 */
-	Eventually(AbstractFormula<T>* child) {
+	Eventually(FormulaType* child) {
 		this->child = child;
 	}
 
@@ -64,6 +64,21 @@ public:
 	  }
 	}
 
+	/*!
+	 * @returns the child node
+	 */
+	const FormulaType& getChild() const {
+		return *child;
+	}
+
+	/*!
+	 * Sets the subtree
+	 * @param child the new child node
+	 */
+	void setChild(FormulaType* child) {
+		this->child = child;
+	}
+
 	/*!
 	 * @returns a string representation of the formula
 	 */
@@ -83,24 +98,8 @@ 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:
-	AbstractFormula<T>* child;
+	FormulaType* child;
 };
 
 } //namespace abstract
diff --git a/src/formula/abstract/Globally.h b/src/formula/abstract/Globally.h
index adaac0d85..1e46ab2b3 100644
--- a/src/formula/abstract/Globally.h
+++ b/src/formula/abstract/Globally.h
@@ -33,7 +33,7 @@ namespace abstract {
  * @see AbstractFormula
  * @see AbstractFormula
  */
-template <class T>
+template <class T, class FormulaType>
 class Globally : public AbstractFormula<T> {
 
 public:
@@ -49,7 +49,7 @@ public:
 	 *
 	 * @param child The child node
 	 */
-	Globally(AbstractFormula<T>* child) {
+	Globally(FormulaType* child) {
 		this->child = child;
 	}
 
@@ -65,6 +65,21 @@ public:
 	  }
 	}
 
+	/*!
+	 * @returns the child node
+	 */
+	const FormulaType& getChild() const {
+		return *child;
+	}
+
+	/*!
+	 * Sets the subtree
+	 * @param child the new child node
+	 */
+	void setChild(FormulaType* child) {
+		this->child = child;
+	}
+
 	/*!
 	 * @returns a string representation of the formula
 	 */
@@ -84,24 +99,8 @@ 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:
-	AbstractFormula<T>* child;
+	FormulaType* child;
 };
 
 } //namespace abstract
diff --git a/src/formula/abstract/Next.h b/src/formula/abstract/Next.h
index 9f2247f81..1f94afd4d 100644
--- a/src/formula/abstract/Next.h
+++ b/src/formula/abstract/Next.h
@@ -32,7 +32,7 @@ namespace abstract {
  * @see AbstractFormula
  * @see AbstractFormula
  */
-template <class T>
+template <class T, class FormulaType>
 class Next : public AbstractFormula<T> {
 
 public:
@@ -48,7 +48,7 @@ public:
 	 *
 	 * @param child The child node
 	 */
-	Next(AbstractFormula<T>* child) {
+	Next(FormulaType* child) {
 		this->child = child;
 	}
 
@@ -64,6 +64,21 @@ public:
 	  }
 	}
 
+	/*!
+	 * @returns the child node
+	 */
+	const FormulaType& getChild() const {
+		return *child;
+	}
+
+	/*!
+	 * Sets the subtree
+	 * @param child the new child node
+	 */
+	void setChild(FormulaType* child) {
+		this->child = child;
+	}
+
 	/*!
 	 * @returns a string representation of the formula
 	 */
@@ -85,24 +100,8 @@ 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:
-	AbstractFormula<T>* child;
+	FormulaType* child;
 };
 
 } //namespace abstract
diff --git a/src/formula/abstract/Not.h b/src/formula/abstract/Not.h
index 4bbc3be7c..3d4ca6216 100644
--- a/src/formula/abstract/Not.h
+++ b/src/formula/abstract/Not.h
@@ -30,7 +30,7 @@ namespace abstract {
  * @see AbstractFormula
  * @see AbstractFormula
  */
-template <class T>
+template <class T, class FormulaType>
 class Not : public AbstractFormula<T> {
 
 public:
@@ -45,7 +45,7 @@ public:
 	 * Constructor
 	 * @param child The child node
 	 */
-	Not(AbstractFormula<T>* child) {
+	Not(FormulaType* child) {
 		this->child = child;
 	}
 
@@ -61,6 +61,21 @@ public:
 	  }
 	}
 
+	/*!
+	 * @returns The child node
+	 */
+	const FormulaType& getChild() const {
+		return *child;
+	}
+
+	/*!
+	 * Sets the subtree
+	 * @param child the new child node
+	 */
+	void setChild(FormulaType* child) {
+		this->child = child;
+	}
+
 	/*!
 	 * @returns a string representation of the formula
 	 */
@@ -80,24 +95,8 @@ 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:
-	AbstractFormula<T>* child;
+	FormulaType* child;
 };
 
 } //namespace abstract
diff --git a/src/formula/abstract/Or.h b/src/formula/abstract/Or.h
index 42e86c198..689fa4d7a 100644
--- a/src/formula/abstract/Or.h
+++ b/src/formula/abstract/Or.h
@@ -30,7 +30,7 @@ namespace abstract {
  * @see AbstractFormula
  * @see AbstractFormula
  */
-template <class T>
+template <class T, class FormulaType>
 class Or : public AbstractFormula<T> {
 
 public:
@@ -50,7 +50,7 @@ public:
 	 * @param left The left sub formula
 	 * @param right The right sub formula
 	 */
-	Or(AbstractFormula<T>* left, AbstractFormula<T>* right) {
+	Or(FormulaType* left, FormulaType* right) {
 		this->left = left;
 		this->right = right;
 	}
@@ -69,36 +69,13 @@ public:
 		  delete 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;
-	}
 	
 	/*!
-     *  @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(AbstractFormula<T>* newLeft) {
+	void setLeft(FormulaType* newLeft) {
 		left = newLeft;
 	}
 
@@ -107,27 +84,49 @@ protected:
 	 *
 	 * @param newRight the new right child.
 	 */
-	void setRight(AbstractFormula<T>* newRight) {
+	void setRight(FormulaType* newRight) {
 		right = newRight;
 	}
 
 	/*!
 	 * @returns a pointer to the left child node
 	 */
-	const AbstractFormula<T>& getLeft() const {
+	const FormulaType& getLeft() const {
 		return *left;
 	}
 
 	/*!
 	 * @returns a pointer to the right child node
 	 */
-	const AbstractFormula<T>& getRight() const {
+	const FormulaType& 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;
+	}
+
+	/*!
+     *  @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;
+	FormulaType* left;
+	FormulaType* right;
 };
 
 } //namespace abstract
diff --git a/src/formula/abstract/PathBoundOperator.h b/src/formula/abstract/PathBoundOperator.h
index fa65cbe6d..f1a2c196b 100644
--- a/src/formula/abstract/PathBoundOperator.h
+++ b/src/formula/abstract/PathBoundOperator.h
@@ -23,8 +23,6 @@ namespace formula {
 
 namespace abstract {
 
-template <class T> class PathBoundOperator;
-
 /*!
  * @brief
  * Class for a Abstract formula tree with a P (probablistic) operator node over a probability interval
@@ -46,7 +44,7 @@ template <class T> class PathBoundOperator;
  * @see ProbabilisticNoBoundsOperator
  * @see AbstractFormula
  */
-template<class T>
+template<class T, class FormulaType>
 class PathBoundOperator : public AbstractFormula<T>, public OptimizingOperator {
 
 public:
@@ -59,7 +57,7 @@ public:
 	 * @param bound The bound for the probability
 	 * @param pathFormula The child node
 	 */
-	PathBoundOperator(ComparisonType comparisonOperator, T bound, AbstractFormula<T>* pathFormula)
+	PathBoundOperator(ComparisonType comparisonOperator, T bound, FormulaType* pathFormula)
 		: comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula) {
 		// Intentionally left empty
 	}
@@ -72,7 +70,7 @@ public:
 	 * @param pathFormula The child node
 	 * @param minimumOperator Indicator, if operator should be minimum or maximum operator.
 	 */
-	PathBoundOperator(ComparisonType comparisonOperator, T bound, AbstractFormula<T>* pathFormula, bool minimumOperator)
+	PathBoundOperator(ComparisonType comparisonOperator, T bound, FormulaType* pathFormula, bool minimumOperator)
 		: comparisonOperator(comparisonOperator), bound(bound), pathFormula(pathFormula), OptimizingOperator(minimumOperator) {
 		// Intentionally left empty
 	}
@@ -89,6 +87,22 @@ public:
 	 }
 	}
 
+	/*!
+	 * @returns the child node (representation of a Abstract path formula)
+	 */
+	const FormulaType& getPathFormula () const {
+		return *pathFormula;
+	}
+
+	/*!
+	 * Sets the child node
+	 *
+	 * @param pathFormula the path formula that becomes the new child node
+	 */
+	void setPathFormula(FormulaType* pathFormula) {
+		this->pathFormula = pathFormula;
+	}
+
 	/*!
 	 * @returns the comparison relation
 	 */
@@ -155,28 +169,10 @@ 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;
-	AbstractFormula<T>* pathFormula;
+	FormulaType* pathFormula;
 };
 
 } //namespace abstract
diff --git a/src/formula/abstract/PathNoBoundOperator.h b/src/formula/abstract/PathNoBoundOperator.h
index 68da9ba40..428ba99ca 100644
--- a/src/formula/abstract/PathNoBoundOperator.h
+++ b/src/formula/abstract/PathNoBoundOperator.h
@@ -50,7 +50,7 @@ namespace abstract {
  * @see ProbabilisticIntervalOperator
  * @see AbstractFormula
  */
-template <class T>
+template <class T, class FormulaType>
 class PathNoBoundOperator: public storm::formula::AbstractFormula<T>, public OptimizingOperator {
 public:
 	/*!
@@ -65,7 +65,7 @@ public:
 	 *
 	 * @param pathFormula The child node.
 	 */
-	PathNoBoundOperator(AbstractFormula<T>* pathFormula) : optimalityOperator(false), minimumOperator(false) {
+	PathNoBoundOperator(FormulaType* pathFormula) : optimalityOperator(false), minimumOperator(false) {
 		this->pathFormula = pathFormula;
 	}
 
@@ -76,7 +76,7 @@ public:
 	 * @param minimumOperator A flag indicating whether this operator is a minimizing or a
 	 * maximizing operator.
 	 */
-	PathNoBoundOperator(AbstractFormula<T>* pathFormula, bool minimumOperator)
+	PathNoBoundOperator(FormulaType* pathFormula, bool minimumOperator)
 		: optimalityOperator(true), minimumOperator(minimumOperator) {
 		this->pathFormula = pathFormula;
 	}
@@ -90,6 +90,22 @@ public:
 		}
 	}
 
+	/*!
+	 * @returns the child node (representation of a Abstract path formula)
+	 */
+	const FormulaType& getPathFormula () const {
+		return *pathFormula;
+	}
+
+	/*!
+	 * Sets the child node
+	 *
+	 * @param pathFormula the path formula that becomes the new child node
+	 */
+	void setPathFormula(FormulaType* pathFormula) {
+		this->pathFormula = pathFormula;
+	}
+
 	/*!
 	 * @returns a string representation of the formula
 	 */
@@ -136,25 +152,8 @@ 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:
-	AbstractFormula<T>* pathFormula;
+	FormulaType* pathFormula;
 
 	// A flag that indicates whether this operator is meant as an optimizing (i.e. min/max) operator
 	// over a nondeterministic model.
diff --git a/src/formula/abstract/ProbabilisticBoundOperator.h b/src/formula/abstract/ProbabilisticBoundOperator.h
index 30f37eeba..18be5a834 100644
--- a/src/formula/abstract/ProbabilisticBoundOperator.h
+++ b/src/formula/abstract/ProbabilisticBoundOperator.h
@@ -38,7 +38,7 @@ namespace abstract {
  * @see ProbabilisticNoBoundsOperator
  * @see AbstractFormula
  */
-template<class T>
+template<class T, class FormulaType>
 class ProbabilisticBoundOperator : public PathBoundOperator<T> {
 
 public:
@@ -59,7 +59,7 @@ public:
 	 * @param pathFormula The child node
 	 */
 	ProbabilisticBoundOperator(
-			typename PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractFormula<T>* pathFormula)
+			typename PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, FormulaType* pathFormula)
 			: PathBoundOperator<T>(comparisonRelation, bound, pathFormula) {
 		// Intentionally left empty
 	}
@@ -73,7 +73,7 @@ public:
 	 * @param minimumOperator
 	 */
 	ProbabilisticBoundOperator(
-			typename PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, AbstractFormula<T>* pathFormula, bool minimumOperator)
+			typename PathBoundOperator<T>::ComparisonType comparisonRelation, T bound, FormulaType* pathFormula, bool minimumOperator)
 			: PathBoundOperator<T>(comparisonRelation, bound, pathFormula, minimumOperator){
 		// Intentionally left empty
 	}
diff --git a/src/formula/abstract/ProbabilisticNoBoundOperator.h b/src/formula/abstract/ProbabilisticNoBoundOperator.h
index 68e5e1bcb..7f565e1b7 100644
--- a/src/formula/abstract/ProbabilisticNoBoundOperator.h
+++ b/src/formula/abstract/ProbabilisticNoBoundOperator.h
@@ -46,7 +46,7 @@ namespace abstract {
  * @see ProbabilisticIntervalOperator
  * @see AbstractFormula
  */
-template <class T>
+template <class T, class FormulaType>
 class ProbabilisticNoBoundOperator: public PathNoBoundOperator<T> {
 public:
 	/*!
@@ -61,7 +61,7 @@ public:
 	 *
 	 * @param pathFormula The child node.
 	 */
-	ProbabilisticNoBoundOperator(AbstractFormula<T>* pathFormula) : PathNoBoundOperator<T>(pathFormula) {
+	ProbabilisticNoBoundOperator(FormulaType* pathFormula) : PathNoBoundOperator<T>(pathFormula) {
 		// Intentionally left empty
 	}
 
@@ -77,7 +77,7 @@ public:
 	 *
 	 * @param pathFormula The child node.
 	 */
-	ProbabilisticNoBoundOperator(AbstractFormula<T>* pathFormula, bool minimumOperator) : PathNoBoundOperator<T>(pathFormula, minimumOperator) {
+	ProbabilisticNoBoundOperator(FormulaType* pathFormula, bool minimumOperator) : PathNoBoundOperator<T>(pathFormula, minimumOperator) {
 		// Intentionally left empty
 	}
 
diff --git a/src/formula/abstract/StateBoundOperator.h b/src/formula/abstract/StateBoundOperator.h
index c1f0f2ce7..117ab3c8f 100644
--- a/src/formula/abstract/StateBoundOperator.h
+++ b/src/formula/abstract/StateBoundOperator.h
@@ -52,7 +52,7 @@ public:
 	 * @param bound The bound for the probability
 	 * @param stateFormula The child node
 	 */
-	StateBoundOperator(ComparisonType comparisonOperator, T bound, AbstractFormula<T>* stateFormula)
+	StateBoundOperator(ComparisonType comparisonOperator, T bound, FormulaType* stateFormula)
 		: comparisonOperator(comparisonOperator), bound(bound), stateFormula(stateFormula) {
 		// Intentionally left empty
 	}
@@ -69,6 +69,22 @@ public:
 	 }
 	}
 
+	/*!
+	 * @returns the child node (representation of a Abstract state formula)
+	 */
+	const FormulaType& getStateFormula () const {
+		return *stateFormula;
+	}
+
+	/*!
+	 * Sets the child node
+	 *
+	 * @param stateFormula the state formula that becomes the new child node
+	 */
+	void setStateFormula(FormulaType* stateFormula) {
+		this->stateFormula = stateFormula;
+	}
+
 	/*!
 	 * @returns the comparison relation
 	 */
@@ -134,27 +150,10 @@ 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;
-	AbstractFormula<T>* stateFormula;
+	FormulaType* stateFormula;
 };
 
 } //namespace abstract
diff --git a/src/formula/abstract/StateNoBoundOperator.h b/src/formula/abstract/StateNoBoundOperator.h
index d2a4fe369..58f2343d4 100644
--- a/src/formula/abstract/StateNoBoundOperator.h
+++ b/src/formula/abstract/StateNoBoundOperator.h
@@ -46,7 +46,7 @@ namespace abstract {
  * @see SteadyStateNoBoundOperator
  * @see AbstractFormula
  */
-template <class T>
+template <class T, class FormulaType>
 class StateNoBoundOperator: public storm::formula::AbstractFormula<T> {
 public:
 	/*!
@@ -59,7 +59,7 @@ public:
 	/*!
 	 * Constructor
 	 */
-	StateNoBoundOperator(AbstractFormula<T>* stateFormula) {
+	StateNoBoundOperator(FormulaType* stateFormula) {
 		this->stateFormula = stateFormula;
 	}
 
@@ -74,6 +74,14 @@ public:
 		}
 	}
 
+	const FormulaType& getStateFormula() const {
+		return *(this->stateFormula);
+	}
+
+	void setStateFormula(FormulaType* stateFormula) {
+		this->stateFormula = stateFormula;
+	}
+
 	/*!
 	 * Calls the model checker to check this formula.
 	 * Needed to infer the correct type of formula class.
@@ -110,17 +118,8 @@ public:
 		return checker.conforms(this->stateFormula);
 	}
 
-protected:
-	const AbstractFormula<T>& getStateFormula() const {
-		return *(this->stateFormula);
-	}
-
-	void setStateFormula(AbstractFormula<T>* stateFormula) {
-		this->stateFormula = stateFormula;
-	}
-
 private:
-	AbstractFormula<T>* stateFormula;
+	FormulaType* stateFormula;
 };
 
 } //namespace abstract
diff --git a/src/formula/abstract/Until.h b/src/formula/abstract/Until.h
index 03b55c460..a172c64ee 100644
--- a/src/formula/abstract/Until.h
+++ b/src/formula/abstract/Until.h
@@ -32,7 +32,7 @@ namespace abstract {
  * @see AbstractFormula
  * @see AbstractFormula
  */
-template <class T>
+template <class T, class FormulaType>
 class Until : public AbstractFormula<T> {
 
 public:
@@ -50,7 +50,7 @@ public:
 	 * @param left The left formula subtree
 	 * @param right The left formula subtree
 	 */
-	Until(AbstractFormula<T>* left, AbstractFormula<T>* right) {
+	Until(FormulaType* left, FormulaType* right) {
 		this->left = left;
 		this->right = right;
 	}
@@ -70,33 +70,12 @@ 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(AbstractFormula<T>* newLeft) {
+	void setLeft(FormulaType* newLeft) {
 		left = newLeft;
 	}
 
@@ -105,27 +84,47 @@ protected:
 	 *
 	 * @param newRight the new right child.
 	 */
-	void setRight(AbstractFormula<T>* newRight) {
+	void setRight(FormulaType* newRight) {
 		right = newRight;
 	}
 
 	/*!
 	 * @returns a pointer to the left child node
 	 */
-	const AbstractFormula<T>& getLeft() const {
+	const FormulaType& getLeft() const {
 		return *left;
 	}
 
 	/*!
 	 * @returns a pointer to the right child node
 	 */
-	const AbstractFormula<T>& getRight() const {
+	const FormulaType& 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;
+	}
+
+	/*!
+     *  @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;
+	FormulaType* left;
+	FormulaType* right;
 };
 
 } //namespace abstract