diff --git a/src/formula/AbstractFormula.h b/src/formula/AbstractFormula.h
index c790d8eae..8ab2fd130 100644
--- a/src/formula/AbstractFormula.h
+++ b/src/formula/AbstractFormula.h
@@ -9,6 +9,7 @@
 #define STORM_FORMULA_ABSTRACTFORMULA_H_
 
 #include <string>
+#include <memory>
 
 namespace storm {
 namespace property {
@@ -16,8 +17,6 @@ template <class T> class AbstractFormula;
 } //namespace property
 } //namespace storm
 
-#include "src/formula/AbstractFormulaChecker.h"
-
 namespace storm {
 namespace property {
 
@@ -64,22 +63,6 @@ public:
 	 */
 	virtual std::string toString() const = 0;
 
-	/*!
-	 *	@brief Checks if all subtrees are valid in some logic.
-	 *
-	 *	@note Every subclass must implement this method.
-	 *
-	 *	This method is given a checker object that knows which formula
-	 *	classes are allowed within the logic the checker represents. Every
-	 *	subclass is supposed to call checker.validate() for all child
-	 *	formulas and return true if and only if all those calls returned
-	 *	true.
-	 *
-	 *	@param checker Checker object.
-	 *	@return true iff all subtrees are valid.
-	 */
-	virtual bool validate(AbstractFormulaChecker<T> const & checker) const = 0;
-
 	/*!
 	 * Returns whether the formula is a propositional logic formula.
 	 * That is, this formula and all its subformulas consist only of And, Or, Not and AP.
diff --git a/src/formula/AbstractFormulaChecker.h b/src/formula/AbstractFormulaChecker.h
deleted file mode 100644
index 97c0446ee..000000000
--- a/src/formula/AbstractFormulaChecker.h
+++ /dev/null
@@ -1,74 +0,0 @@
-#ifndef STORM_FORMULA_ABSTRACTFORMULACHECKER_H_
-#define STORM_FORMULA_ABSTRACTFORMULACHECKER_H_
-
-namespace storm {
-namespace property {
-
-template <class T> class AbstractFormulaChecker;
-
-} //namespace property
-} //namespace storm
-
-
-#include "src/formula/AbstractFormula.h"
-#include <memory>
-
-namespace storm {
-namespace property {
-
-/*!
- *	@brief	Base class for all formula checkers.
- *
- *	A formula checker is used to check if a given formula is valid in some
- *	logic. Hence, this pure virtual base class should be subclassed for
- *	every logic we support.
- *
- *	Every subclass must implement validate(). It gets a pointer to an
- *	AbstractFormula object and should return if the subtree represented by
- *	this formula is valid in the logic.
- *
- *	Usually, this will be implemented like this:
- *	@code
- *	if	(
- *			dynamic_cast<const And<T>*>(formula) ||
- *			dynamic_cast<const Not<T>*>(formula) ||
- *			dynamic_cast<const Or<T>*>(formula)
- *		) {
- *		return formula->validate(*this);
- *	} else	return false;
- *	@endcode
- *
- *	Every formula class implements a validate() method itself which calls
- *	validate() on the given checker for every child in the formula tree.
- *
- *	If the formula structure is not an actual tree, but an directed acyclic
- *	graph, the shared subtrees will be checked twice. If we have directed
- *	cycles, we will have infinite recursions.
- */
-template <class T>
-class AbstractFormulaChecker {
-	public:
-		/*!
-		 * Virtual destructor
-		 * To ensure that the right destructor is called
-		 */
-		virtual ~AbstractFormulaChecker() {
-			//intentionally left empty
-		}
-
-		/*!
-		 *	@brief Checks if the given formula is valid in some logic.
-		 *
-		 *	Every subclass must implement this method and check, if the
-		 *	formula object is valid in the logic of the subclass.
-		 *
-		 *	@param formula A pointer to some formula object.
-		 *	@return true iff the formula is valid.
-		 */
-		virtual bool validate(std::shared_ptr<AbstractFormula<T>> const & formula) const = 0;
-};
-
-} // namespace property
-} // namespace storm
-
-#endif
diff --git a/src/formula/PrctlFormulaChecker.h b/src/formula/PrctlFormulaChecker.h
deleted file mode 100644
index 5ed817e09..000000000
--- a/src/formula/PrctlFormulaChecker.h
+++ /dev/null
@@ -1,49 +0,0 @@
-#ifndef STORM_FORMULA_PRCTLFORMULACHECKER_H_
-#define STORM_FORMULA_PRCTLFORMULACHECKER_H_
-
-#include "src/formula/AbstractFormulaChecker.h"
-#include "src/formula/Prctl.h"
-
-#include <iostream>
-#include <memory>
-
-namespace storm {
-namespace property {
-
-/*!
- *	@brief Checks formulas if they are within PRCTL.
- *
- *	This class implements AbstractFormulaChecker to check if a given formula
- *	is part of PRCTL logic.
- */
-template <class T>
-class PrctlFormulaChecker : public AbstractFormulaChecker<T> {
-	public:
-		/*!
-		 *	Implementation of AbstractFormulaChecker::validate() using code
-		 *	looking exactly like the sample code given there.
-		 */
-		virtual bool validate(std::shared_ptr<storm::property::AbstractFormula<T>> const & formula) const {
-			// What to support: Principles of Model Checking Def. 10.76 + syntactic sugar
-			if (
-					dynamic_pointer_cast<storm::property::prctl::And<T>>(formula) ||
-					dynamic_pointer_cast<storm::property::prctl::Ap<T>>(formula) ||
-					dynamic_pointer_cast<storm::property::prctl::BoundedUntil<T>>(formula) ||
-					dynamic_pointer_cast<storm::property::prctl::Eventually<T>>(formula) ||
-					dynamic_pointer_cast<storm::property::prctl::Globally<T>>(formula) ||
-					dynamic_pointer_cast<storm::property::prctl::Next<T>>(formula) ||
-					dynamic_pointer_cast<storm::property::prctl::Not<T>>(formula) ||
-					dynamic_pointer_cast<storm::property::prctl::Or<T>>(formula) ||
-					dynamic_pointer_cast<storm::property::prctl::ProbabilisticBoundOperator<T>>(formula) ||
-					dynamic_pointer_cast<storm::property::prctl::Until<T>>(formula)
-				) {
-				return formula->validate(*this);
-			}
-			return false;
-		}
-};
-
-} // namespace property
-} // namespace storm
-
-#endif
diff --git a/src/formula/csl/AbstractCslFormula.h b/src/formula/csl/AbstractCslFormula.h
index 6631a753f..73d4f3dcd 100644
--- a/src/formula/csl/AbstractCslFormula.h
+++ b/src/formula/csl/AbstractCslFormula.h
@@ -47,19 +47,23 @@ public:
 	 */
 	bool isProbEventuallyAP() const {
 
+		// Test if a probabilistic bound operator is at the root.
 		if(dynamic_cast<storm::property::csl::ProbabilisticBoundOperator<T> const *>(this) == nullptr) {
 			return false;
 		}
 
 		auto probFormula = dynamic_cast<storm::property::csl::ProbabilisticBoundOperator<T> const *>(this);
 
+		// Check if the direct subformula of the probabilistic bound operator is an eventually or until formula.
 		if(std::dynamic_pointer_cast<storm::property::csl::Eventually<T>>(probFormula->getChild()).get() != nullptr) {
 
+			// Get the subformula and check if its subformulas are propositional.
 			auto eventuallyFormula = std::dynamic_pointer_cast<storm::property::csl::Eventually<T>>(probFormula->getChild());
 			return eventuallyFormula->getChild()->isPropositional();
 		}
 		else if(std::dynamic_pointer_cast<storm::property::csl::Until<T>>(probFormula->getChild()).get() != nullptr) {
 
+			// Get the subformula and check if its subformulas are propositional.
 			auto untilFormula = std::dynamic_pointer_cast<storm::property::csl::Until<T>>(probFormula->getChild());
 			return untilFormula->getLeft()->isPropositional() && untilFormula->getRight()->isPropositional();
 		}
diff --git a/src/formula/csl/And.h b/src/formula/csl/And.h
index 0218edecb..afb78ceeb 100644
--- a/src/formula/csl/And.h
+++ b/src/formula/csl/And.h
@@ -9,7 +9,6 @@
 #define STORM_FORMULA_CSL_AND_H_
 
 #include "src/formula/csl/AbstractStateFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelchecker/csl/ForwardDeclarations.h"
 #include <string>
 
@@ -129,16 +128,6 @@ public:
 		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 validate(AbstractFormulaChecker<T> const & checker) const override {
-		return checker.validate(this->left) && checker.validate(this->right);
-	}
-
 	/*! Returns whether the formula is a propositional logic formula.
 	 *  That is, this formula and all its subformulas consist only of And, Or, Not and AP.
 	 *
diff --git a/src/formula/csl/Ap.h b/src/formula/csl/Ap.h
index 284f94eeb..a80f8fdfe 100644
--- a/src/formula/csl/Ap.h
+++ b/src/formula/csl/Ap.h
@@ -9,7 +9,6 @@
 #define STORM_FORMULA_CSL_AP_H_
 
 #include "src/formula/csl/AbstractStateFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelchecker/csl/ForwardDeclarations.h"
 
 namespace storm {
@@ -94,18 +93,6 @@ public:
 		return modelChecker.template as<IApModelChecker>()->checkAp(*this);
 	}
 
-	/*!
-     *  @brief Checks if all subtrees conform to some logic.
-     *
-     *	As atomic propositions have no subformulas, we return true here.
-     *
-     *  @param checker Formula checker object.
-     *  @return true
-     */
-	virtual bool validate(AbstractFormulaChecker<T> const & checker) const override {
-		return true;
-	}
-
 	/*! Returns whether the formula is a propositional logic formula.
 	 *  That is, this formula and all its subformulas consist only of And, Or, Not and AP.
 	 *
diff --git a/src/formula/csl/Eventually.h b/src/formula/csl/Eventually.h
index 8428d5f00..21bdd71b4 100644
--- a/src/formula/csl/Eventually.h
+++ b/src/formula/csl/Eventually.h
@@ -119,16 +119,6 @@ public:
 		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 validate(AbstractFormulaChecker<T> const & checker) const override {
-		return checker.validate(this->child);
-	}
-
 	/*!
 	 * @returns the child node
 	 */
diff --git a/src/formula/csl/Globally.h b/src/formula/csl/Globally.h
index 211532efb..e93baeca5 100644
--- a/src/formula/csl/Globally.h
+++ b/src/formula/csl/Globally.h
@@ -10,7 +10,6 @@
 
 #include "src/formula/csl/AbstractPathFormula.h"
 #include "src/formula/csl/AbstractStateFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelchecker/csl/ForwardDeclarations.h"
 
 namespace storm {
@@ -120,16 +119,6 @@ public:
 		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 validate(AbstractFormulaChecker<T> const & checker) const override {
-		return checker.validate(this->child);
-	}
-
 	/*!
 	 * @returns the child node
 	 */
diff --git a/src/formula/csl/Next.h b/src/formula/csl/Next.h
index 3148377a6..8c86095b8 100644
--- a/src/formula/csl/Next.h
+++ b/src/formula/csl/Next.h
@@ -10,7 +10,6 @@
 
 #include "src/formula/csl/AbstractPathFormula.h"
 #include "src/formula/csl/AbstractStateFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
 namespace property {
@@ -119,16 +118,6 @@ public:
 		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 validate(AbstractFormulaChecker<T> const & checker) const override {
-		return checker.validate(this->child);
-	}
-
 	/*!
 	 * @returns the child node
 	 */
diff --git a/src/formula/csl/Not.h b/src/formula/csl/Not.h
index 698b92b89..9c23323ce 100644
--- a/src/formula/csl/Not.h
+++ b/src/formula/csl/Not.h
@@ -9,7 +9,6 @@
 #define STORM_FORMULA_CSL_NOT_H_
 
 #include "src/formula/csl/AbstractStateFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelchecker/csl/ForwardDeclarations.h"
 
 namespace storm {
@@ -115,16 +114,6 @@ public:
 		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 validate(AbstractFormulaChecker<T> const & checker) const override {
-		return checker.validate(this->child);
-	}
-
 	/*! Returns whether the formula is a propositional logic formula.
 	 *  That is, this formula and all its subformulas consist only of And, Or, Not and AP.
 	 *
diff --git a/src/formula/csl/Or.h b/src/formula/csl/Or.h
index 2ecc7fab9..b6017d4be 100644
--- a/src/formula/csl/Or.h
+++ b/src/formula/csl/Or.h
@@ -9,7 +9,6 @@
 #define STORM_FORMULA_CSL_OR_H_
 
 #include "src/formula/csl/AbstractStateFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
 namespace property {
@@ -127,16 +126,6 @@ public:
 		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 validate(AbstractFormulaChecker<T> const & checker) const override {
-		return checker.validate(this->left) && checker.validate(this->right);
-	}
-
 	/*! Returns whether the formula is a propositional logic formula.
 	 *  That is, this formula and all its subformulas consist only of And, Or, Not and AP.
 	 *
diff --git a/src/formula/csl/ProbabilisticBoundOperator.h b/src/formula/csl/ProbabilisticBoundOperator.h
index 6d0e0d6a3..f0c51af72 100644
--- a/src/formula/csl/ProbabilisticBoundOperator.h
+++ b/src/formula/csl/ProbabilisticBoundOperator.h
@@ -114,16 +114,6 @@ public:
 		return modelChecker.template as<IProbabilisticBoundOperatorModelChecker>()->checkProbabilisticBoundOperator(*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 validate(AbstractFormulaChecker<T> const & checker) const override {
-		return checker.validate(this->child);
-	}
-
 	/*!
 	 * @returns a string representation of the formula
 	 */
diff --git a/src/formula/csl/SteadyStateBoundOperator.h b/src/formula/csl/SteadyStateBoundOperator.h
index c53823639..3c664f05a 100644
--- a/src/formula/csl/SteadyStateBoundOperator.h
+++ b/src/formula/csl/SteadyStateBoundOperator.h
@@ -9,7 +9,6 @@
 #define STORM_FORMULA_CSL_STEADYSTATEOPERATOR_H_
 
 #include "AbstractStateFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
 #include "src/formula/ComparisonType.h"
 
 namespace storm {
@@ -111,16 +110,6 @@ public:
 		return modelChecker.template as<ISteadyStateBoundOperatorModelChecker>()->checkSteadyStateBoundOperator(*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 validate(AbstractFormulaChecker<T> const & checker) const override {
-		return checker.validate(this->stateFormula);
-	}
-
 	/*!
 	 * @returns a string representation of the formula
 	 */
diff --git a/src/formula/csl/TimeBoundedEventually.h b/src/formula/csl/TimeBoundedEventually.h
index 8564a0db3..e4c6aa483 100644
--- a/src/formula/csl/TimeBoundedEventually.h
+++ b/src/formula/csl/TimeBoundedEventually.h
@@ -86,16 +86,6 @@ public:
 		return modelChecker.template as<ITimeBoundedEventuallyModelChecker>()->checkTimeBoundedEventually(*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 validate(AbstractFormulaChecker<T> const & checker) const override {
-		return checker.validate(this->child);
-	}
-
 	/*!
 	 * @returns a string representation of the formula
 	 */
diff --git a/src/formula/csl/TimeBoundedUntil.h b/src/formula/csl/TimeBoundedUntil.h
index 1bdf2f0aa..170ddf54a 100644
--- a/src/formula/csl/TimeBoundedUntil.h
+++ b/src/formula/csl/TimeBoundedUntil.h
@@ -101,16 +101,6 @@ public:
 		return modelChecker.template as<ITimeBoundedUntilModelChecker>()->checkTimeBoundedUntil(*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 validate(AbstractFormulaChecker<T> const & checker) const override {
-		return checker.validate(this->left) && checker.validate(this->right);
-	}
-
 	/*!
 	 * @returns a string representation of the formula
 	 */
diff --git a/src/formula/csl/Until.h b/src/formula/csl/Until.h
index ea0209053..8d2446489 100644
--- a/src/formula/csl/Until.h
+++ b/src/formula/csl/Until.h
@@ -10,7 +10,6 @@
 
 #include "src/formula/csl/AbstractPathFormula.h"
 #include "src/formula/csl/AbstractStateFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
 namespace property {
@@ -124,16 +123,6 @@ public:
 		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 validate(AbstractFormulaChecker<T> const & checker) const override {
-		return checker.validate(this->left) && checker.validate(this->right);
-	}
-
 	/*!
 	 * Sets the left child node.
 	 *
diff --git a/src/formula/ltl/And.h b/src/formula/ltl/And.h
index 48c4350cb..06fc83cae 100644
--- a/src/formula/ltl/And.h
+++ b/src/formula/ltl/And.h
@@ -9,7 +9,6 @@
 #define STORM_FORMULA_LTL_AND_H_
 
 #include "AbstractLtlFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelchecker/ltl/ForwardDeclarations.h"
 #include <string>
 
@@ -128,16 +127,6 @@ public:
 		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 validate(AbstractFormulaChecker<T> const & checker) const override {
-        return checker.validate(this->left) && checker.validate(this->right);
-    }
-
 	/*!
 	 * Returns whether the formula is a propositional logic formula.
 	 * That is, this formula and all its subformulas consist only of And, Or, Not and AP.
diff --git a/src/formula/ltl/Ap.h b/src/formula/ltl/Ap.h
index c7845604f..451dadb99 100644
--- a/src/formula/ltl/Ap.h
+++ b/src/formula/ltl/Ap.h
@@ -106,18 +106,6 @@ public:
 		return getAp();
 	}
 
-	/*!
-	 *  @brief Checks if all subtrees conform to some logic.
-	 *
-	 *	As atomic propositions have no subformulas, we return true here.
-	 *
-	 *  @param checker Formula checker object.
-	 *  @return true
-	 */
-	virtual bool validate(AbstractFormulaChecker<T> const & checker) const override {
-		return true;
-	}
-
 	/*!
 	 * Returns whether the formula is a propositional logic formula.
 	 * That is, this formula and all its subformulas consist only of And, Or, Not and AP.
diff --git a/src/formula/ltl/BoundedEventually.h b/src/formula/ltl/BoundedEventually.h
index 40cdb4038..630e0bbae 100644
--- a/src/formula/ltl/BoundedEventually.h
+++ b/src/formula/ltl/BoundedEventually.h
@@ -9,7 +9,6 @@
 #define STORM_FORMULA_LTL_BOUNDEDEVENTUALLY_H_
 
 #include "AbstractLtlFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
 #include <cstdint>
 #include <string>
 #include "src/modelchecker/ltl/ForwardDeclarations.h"
@@ -126,16 +125,6 @@ public:
 		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 validate(AbstractFormulaChecker<T> const & checker) const override {
-		return checker.validate(this->child);
-	}
-
 	/*!
 	 * @returns the child node
 	 */
diff --git a/src/formula/ltl/BoundedUntil.h b/src/formula/ltl/BoundedUntil.h
index b17b901f4..87e0a7a2d 100644
--- a/src/formula/ltl/BoundedUntil.h
+++ b/src/formula/ltl/BoundedUntil.h
@@ -135,16 +135,6 @@ public:
 		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 validate(AbstractFormulaChecker<T> const & checker) const override {
-		return checker.validate(this->left) && checker.validate(this->right);
-	}
-
 	/*!
 	 * Sets the left child node.
 	 *
diff --git a/src/formula/ltl/Eventually.h b/src/formula/ltl/Eventually.h
index b8662cd69..328fd993b 100644
--- a/src/formula/ltl/Eventually.h
+++ b/src/formula/ltl/Eventually.h
@@ -117,16 +117,6 @@ public:
 		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 validate(AbstractFormulaChecker<T> const & checker) const override {
-		return checker.validate(this->child);
-	}
-
 	/*!
 	 * @returns the child node
 	 */
diff --git a/src/formula/ltl/Globally.h b/src/formula/ltl/Globally.h
index 50d977ee8..060b5bba2 100644
--- a/src/formula/ltl/Globally.h
+++ b/src/formula/ltl/Globally.h
@@ -9,7 +9,6 @@
 #define STORM_FORMULA_LTL_GLOBALLY_H_
 
 #include "AbstractLtlFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelchecker/ltl/ForwardDeclarations.h"
 
 namespace storm {
@@ -118,16 +117,6 @@ public:
 		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 validate(AbstractFormulaChecker<T> const & checker) const override {
-		return checker.validate(this->child);
-	}
-
 	/*!
 	 * @returns the child node
 	 */
diff --git a/src/formula/ltl/Next.h b/src/formula/ltl/Next.h
index 0fd069135..a038252c2 100644
--- a/src/formula/ltl/Next.h
+++ b/src/formula/ltl/Next.h
@@ -9,7 +9,6 @@
 #define STORM_FORMULA_LTL_NEXT_H_
 
 #include "AbstractLtlFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
 namespace property {
@@ -117,16 +116,6 @@ public:
 		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 validate(AbstractFormulaChecker<T> const & checker) const override {
-		return checker.validate(this->child);
-	}
-
 	/*!
 	 * @returns the child node
 	 */
diff --git a/src/formula/ltl/Not.h b/src/formula/ltl/Not.h
index 99a90736c..2538298a4 100644
--- a/src/formula/ltl/Not.h
+++ b/src/formula/ltl/Not.h
@@ -9,7 +9,6 @@
 #define STORM_FORMULA_LTL_NOT_H_
 
 #include "AbstractLtlFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
 namespace property {
@@ -113,16 +112,6 @@ public:
 		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 validate(AbstractFormulaChecker<T> const & checker) const override {
-		return checker.validate(this->child);
-	}
-
 	/*!
 	 * Returns whether the formula is a propositional logic formula.
 	 * That is, this formula and all its subformulas consist only of And, Or, Not and AP.
diff --git a/src/formula/ltl/Or.h b/src/formula/ltl/Or.h
index 336da397b..42296766f 100644
--- a/src/formula/ltl/Or.h
+++ b/src/formula/ltl/Or.h
@@ -125,16 +125,6 @@ public:
 		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 validate(AbstractFormulaChecker<T> const & checker) const override {
-		return checker.validate(this->left) && checker.validate(this->right);
-	}
-
 	/*!
 	 * Returns whether the formula is a propositional logic formula.
 	 * That is, this formula and all its subformulas consist only of And, Or, Not and AP.
diff --git a/src/formula/ltl/Until.h b/src/formula/ltl/Until.h
index 95c999e39..92a6e4ed1 100644
--- a/src/formula/ltl/Until.h
+++ b/src/formula/ltl/Until.h
@@ -9,7 +9,6 @@
 #define STORM_FORMULA_LTL_UNTIL_H_
 
 #include "AbstractLtlFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
 namespace property {
@@ -146,16 +145,6 @@ public:
 		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 validate(AbstractFormulaChecker<T> const & checker) const override {
-        return checker.validate(this->left) && checker.validate(this->right);
-	}
-
 	/*!
 	 * Sets the left child node.
 	 *
diff --git a/src/formula/prctl/AbstractPrctlFormula.h b/src/formula/prctl/AbstractPrctlFormula.h
index 044996b9c..f728110fe 100644
--- a/src/formula/prctl/AbstractPrctlFormula.h
+++ b/src/formula/prctl/AbstractPrctlFormula.h
@@ -46,19 +46,23 @@ public:
 	 */
 	bool isProbEventuallyAP() const {
 
+		// Test if a probabilistic bound operator is at the root.
 		if(dynamic_cast<storm::property::prctl::ProbabilisticBoundOperator<T> const *>(this) == nullptr) {
 			return false;
 		}
 
 		auto probFormula = dynamic_cast<storm::property::prctl::ProbabilisticBoundOperator<T> const *>(this);
 
+		// Check if the direct subformula of the probabilistic bound operator is an eventually or until formula.
 		if(std::dynamic_pointer_cast<storm::property::prctl::Eventually<T>>(probFormula->getChild()).get() != nullptr) {
 
+			// Get the subformula and check if its subformulas are propositional.
 			auto eventuallyFormula = std::dynamic_pointer_cast<storm::property::prctl::Eventually<T>>(probFormula->getChild());
 			return eventuallyFormula->getChild()->isPropositional();
 		}
 		else if(std::dynamic_pointer_cast<storm::property::prctl::Until<T>>(probFormula->getChild()).get() != nullptr) {
 
+			// Get the subformula and check if its subformulas are propositional.
 			auto untilFormula = std::dynamic_pointer_cast<storm::property::prctl::Until<T>>(probFormula->getChild());
 			return untilFormula->getLeft()->isPropositional() && untilFormula->getRight()->isPropositional();
 		}
diff --git a/src/formula/prctl/And.h b/src/formula/prctl/And.h
index 80a9cffd3..81b33ad28 100644
--- a/src/formula/prctl/And.h
+++ b/src/formula/prctl/And.h
@@ -9,7 +9,6 @@
 #define STORM_FORMULA_PRCTL_AND_H_
 
 #include "src/formula/prctl/AbstractStateFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelchecker/prctl/ForwardDeclarations.h"
 #include <string>
 
@@ -129,16 +128,6 @@ public:
 		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 validate(const AbstractFormulaChecker<T>& checker) const override {
-		return checker.validate(this->left) && checker.validate(this->right);
-	}
-
 	/*!
 	 * Returns whether the formula is a propositional logic formula.
 	 * That is, this formula and all its subformulas consist only of And, Or, Not and AP.
diff --git a/src/formula/prctl/Ap.h b/src/formula/prctl/Ap.h
index ef6d77b12..7df3cabd8 100644
--- a/src/formula/prctl/Ap.h
+++ b/src/formula/prctl/Ap.h
@@ -9,7 +9,6 @@
 #define STORM_FORMULA_PRCTL_AP_H_
 
 #include "src/formula/prctl/AbstractStateFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelchecker/prctl/ForwardDeclarations.h"
 
 namespace storm {
@@ -94,18 +93,6 @@ public:
 		return modelChecker.template as<IApModelChecker>()->checkAp(*this);
 	}
 
-	/*!
-     *  @brief Checks if all subtrees conform to some logic.
-     *
-     *	As atomic propositions have no subformulas, we return true here.
-     *
-     *  @param checker Formula checker object.
-     *  @return true
-     */
-	virtual bool validate(const AbstractFormulaChecker<T>& checker) const override {
-		return true;
-	}
-
 	/*!
 	 * Returns whether the formula is a propositional logic formula.
 	 * That is, this formula and all its subformulas consist only of And, Or, Not and AP.
diff --git a/src/formula/prctl/BoundedEventually.h b/src/formula/prctl/BoundedEventually.h
index 70e10020d..16b7df1d8 100644
--- a/src/formula/prctl/BoundedEventually.h
+++ b/src/formula/prctl/BoundedEventually.h
@@ -10,7 +10,6 @@
 
 #include "src/formula/prctl/AbstractPathFormula.h"
 #include "src/formula/prctl/AbstractStateFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
 #include <cstdint>
 #include <string>
 #include "src/modelchecker/prctl/ForwardDeclarations.h"
@@ -126,16 +125,6 @@ public:
 		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 validate(const AbstractFormulaChecker<T>& checker) const override {
-		return checker.validate(this->child);
-	}
-
 	/*!
 	 * @returns the child node
 	 */
diff --git a/src/formula/prctl/BoundedNaryUntil.h b/src/formula/prctl/BoundedNaryUntil.h
index 0cf02d4f4..1c9863ac7 100644
--- a/src/formula/prctl/BoundedNaryUntil.h
+++ b/src/formula/prctl/BoundedNaryUntil.h
@@ -142,20 +142,6 @@ public:
 		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 validate(const AbstractFormulaChecker<T>& checker) const override {
-		bool res = checker.validate(left);
-		for (auto it = right->begin(); it != right->end(); ++it) {
-			res &= checker.validate(std::get<0>(*it));
-		}
-		return res;
-	}
-
 	/*!
 	 * Sets the left child node.
 	 *
diff --git a/src/formula/prctl/BoundedUntil.h b/src/formula/prctl/BoundedUntil.h
index d018567eb..92d119583 100644
--- a/src/formula/prctl/BoundedUntil.h
+++ b/src/formula/prctl/BoundedUntil.h
@@ -130,16 +130,6 @@ public:
 		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 validate(const AbstractFormulaChecker<T>& checker) const override {
-		return checker.validate(this->left) && checker.validate(this->right);
-	}
-
 	/*!
 	 * Sets the left child node.
 	 *
diff --git a/src/formula/prctl/CumulativeReward.h b/src/formula/prctl/CumulativeReward.h
index 84861ed91..4a94c021b 100644
--- a/src/formula/prctl/CumulativeReward.h
+++ b/src/formula/prctl/CumulativeReward.h
@@ -9,7 +9,6 @@
 #define STORM_FORMULA_PRCTL_CUMULATIVEREWARD_H_
 
 #include "AbstractRewardPathFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
 #include <string>
 
 namespace storm {
@@ -108,18 +107,6 @@ public:
 		return result;
 	}
 
-	/*!
-	 *  @brief Checks if all subtrees conform to some logic.
-	 *
-	 *  As CumulativeReward objects have no subformulas, we return true here.
-	 *
-	 *  @param checker Formula checker object.
-	 *  @return true
-	 */
-	virtual bool validate(AbstractFormulaChecker<T> const & checker) const override {
-		return true;
-	}
-
 	/*!
 	 * @returns the time instance for the instantaneous reward operator
 	 */
diff --git a/src/formula/prctl/Eventually.h b/src/formula/prctl/Eventually.h
index 321ac872f..77dcb3c73 100644
--- a/src/formula/prctl/Eventually.h
+++ b/src/formula/prctl/Eventually.h
@@ -118,16 +118,6 @@ public:
 		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 validate(AbstractFormulaChecker<T> const & checker) const override {
-		return checker.validate(child);
-	}
-
 	/*!
 	 * @returns the child node
 	 */
diff --git a/src/formula/prctl/Globally.h b/src/formula/prctl/Globally.h
index 7296a9534..8f0b9c910 100644
--- a/src/formula/prctl/Globally.h
+++ b/src/formula/prctl/Globally.h
@@ -10,7 +10,6 @@
 
 #include "src/formula/prctl/AbstractPathFormula.h"
 #include "src/formula/prctl/AbstractStateFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelchecker/prctl/ForwardDeclarations.h"
 
 namespace storm {
@@ -119,16 +118,6 @@ public:
 		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 validate(AbstractFormulaChecker<T> const & checker) const override {
-		return checker.validate(child);
-	}
-
 	/*!
 	 * @returns the child node
 	 */
diff --git a/src/formula/prctl/InstantaneousReward.h b/src/formula/prctl/InstantaneousReward.h
index 3a65583a6..18cf7eeae 100644
--- a/src/formula/prctl/InstantaneousReward.h
+++ b/src/formula/prctl/InstantaneousReward.h
@@ -9,7 +9,6 @@
 #define STORM_FORMULA_PRCTL_INSTANTANEOUSREWARD_H_
 
 #include "AbstractRewardPathFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
 #include <cstdint>
 #include <string>
 
@@ -110,18 +109,6 @@ public:
 		return result;
 	}
 
-	/*!
-	 *  @brief Checks if all subtrees conform to some logic.
-	 *
-	 *  As InstantaneousReward formulas have no subformulas, we return true here.
-	 *
-	 *  @param checker Formula checker object.
-	 *  @return true
-	 */
-	virtual bool validate(AbstractFormulaChecker<T> const & checker) const override {
-		return true;
-	}
-
 	/*!
 	 * @returns the time instance for the instantaneous reward operator
 	 */
diff --git a/src/formula/prctl/Next.h b/src/formula/prctl/Next.h
index 49b66c062..052adf9ca 100644
--- a/src/formula/prctl/Next.h
+++ b/src/formula/prctl/Next.h
@@ -10,7 +10,6 @@
 
 #include "src/formula/prctl/AbstractPathFormula.h"
 #include "src/formula/prctl/AbstractStateFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
 namespace property {
@@ -118,16 +117,6 @@ public:
 		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 validate(AbstractFormulaChecker<T> const & checker) const override {
-		return checker.validate(this->child);
-	}
-
 	/*!
 	 * @returns the child node
 	 */
diff --git a/src/formula/prctl/Not.h b/src/formula/prctl/Not.h
index 7531989f6..a58c5d3f4 100644
--- a/src/formula/prctl/Not.h
+++ b/src/formula/prctl/Not.h
@@ -9,7 +9,6 @@
 #define STORM_FORMULA_PRCTL_NOT_H_
 
 #include "AbstractStateFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelchecker/prctl/ForwardDeclarations.h"
 
 namespace storm {
@@ -114,17 +113,6 @@ public:
 		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 validate(AbstractFormulaChecker<T> const & checker) const override {
-		return checker.validate(this->child);
-	}
-
-
 	/*!
 	 * Returns whether the formula is a propositional logic formula.
 	 * That is, this formula and all its subformulas consist only of And, Or, Not and AP.
diff --git a/src/formula/prctl/Or.h b/src/formula/prctl/Or.h
index 7bbc0e045..646b5735c 100644
--- a/src/formula/prctl/Or.h
+++ b/src/formula/prctl/Or.h
@@ -9,7 +9,6 @@
 #define STORM_FORMULA_PRCTL_OR_H_
 
 #include "src/formula/prctl/AbstractStateFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
 namespace property {
@@ -126,16 +125,6 @@ public:
 		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 validate(AbstractFormulaChecker<T> const & checker) const override {
-        return checker.validate(this->left) && checker.validate(this->right);
-    }
-
 	/*!
 	 * Returns whether the formula is a propositional logic formula.
 	 * That is, this formula and all its subformulas consist only of And, Or, Not and AP.
diff --git a/src/formula/prctl/ProbabilisticBoundOperator.h b/src/formula/prctl/ProbabilisticBoundOperator.h
index e1557ce04..6905d9069 100644
--- a/src/formula/prctl/ProbabilisticBoundOperator.h
+++ b/src/formula/prctl/ProbabilisticBoundOperator.h
@@ -113,16 +113,6 @@ public:
 		return modelChecker.template as<IProbabilisticBoundOperatorModelChecker>()->checkProbabilisticBoundOperator(*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 validate(AbstractFormulaChecker<T> const & checker) const override {
-		return checker.validate(child);
-	}
-
 	/*!
 	 * @returns a string representation of the formula
 	 */
diff --git a/src/formula/prctl/ReachabilityReward.h b/src/formula/prctl/ReachabilityReward.h
index eacc49e3e..0fe5f5792 100644
--- a/src/formula/prctl/ReachabilityReward.h
+++ b/src/formula/prctl/ReachabilityReward.h
@@ -10,7 +10,6 @@
 
 #include "AbstractRewardPathFormula.h"
 #include "AbstractStateFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
 namespace property {
@@ -114,16 +113,6 @@ public:
 		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 validate(AbstractFormulaChecker<T> const & checker) const override {
-		return checker.validate(this->child);
-	}
-
 	/*!
 	 * @returns the child node
 	 */
diff --git a/src/formula/prctl/RewardBoundOperator.h b/src/formula/prctl/RewardBoundOperator.h
index cfebea0d6..12900c58c 100644
--- a/src/formula/prctl/RewardBoundOperator.h
+++ b/src/formula/prctl/RewardBoundOperator.h
@@ -111,16 +111,6 @@ public:
 		return modelChecker.template as<IRewardBoundOperatorModelChecker>()->checkRewardBoundOperator(*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 validate(AbstractFormulaChecker<T> const & checker) const override {
-		return checker.validate(this->child);
-	}
-
 	/*!
 	 * @returns a string representation of the formula
 	 */
diff --git a/src/formula/prctl/SteadyStateReward.h b/src/formula/prctl/SteadyStateReward.h
index d7dfc5416..84774998f 100644
--- a/src/formula/prctl/SteadyStateReward.h
+++ b/src/formula/prctl/SteadyStateReward.h
@@ -9,7 +9,6 @@
 #define STORM_FORMULA_PRCTL_STEADYSTATEREWARD_H_
 
 #include "AbstractRewardPathFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
 #include <string>
 
 namespace storm {
@@ -88,18 +87,6 @@ public:
 	virtual std::string toString() const override {
 		return "S";
 	}
-
-	/*!
-     *  @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 validate(AbstractFormulaChecker<T> const & checker) const override {
-		return true;
-	}
 };
 
 } //namespace prctl
diff --git a/src/formula/prctl/Until.h b/src/formula/prctl/Until.h
index 3d8a5f4e2..eb939b54f 100644
--- a/src/formula/prctl/Until.h
+++ b/src/formula/prctl/Until.h
@@ -10,7 +10,6 @@
 
 #include "AbstractPathFormula.h"
 #include "AbstractStateFormula.h"
-#include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
 namespace property {
@@ -124,16 +123,6 @@ public:
 		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 validate(AbstractFormulaChecker<T> const & checker) const override {
-		return checker.validate(left) && checker.validate(right);
-	}
-
 	/*!
 	 * Sets the left child node.
 	 *