diff --git a/src/formula/AbstractFormula.h b/src/formula/AbstractFormula.h
index ee99f88f2..b7d51e70b 100644
--- a/src/formula/AbstractFormula.h
+++ b/src/formula/AbstractFormula.h
@@ -15,6 +15,7 @@ template <class T> class AbstractFormula;
 }}
 
 #include "src/modelChecker/AbstractModelChecker.h"
+#include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
 namespace formula {
@@ -44,6 +45,8 @@ public:
 	 * @returns a string representation of the formula
 	 */
 	virtual std::string toString() const = 0;
+	
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const = 0;
 };
 
 } //namespace formula
diff --git a/src/formula/AbstractFormulaChecker.h b/src/formula/AbstractFormulaChecker.h
new file mode 100644
index 000000000..9a80b3051
--- /dev/null
+++ b/src/formula/AbstractFormulaChecker.h
@@ -0,0 +1,18 @@
+#ifndef STORM_FORMULA_ABSTRACTFORMULACHECKER_H_
+#define STORM_FORMULA_ABSTRACTFORMULACHECKER_H_
+
+#include "src/formula/AbstractFormula.h"
+
+namespace storm {
+namespace formula {
+
+template <class T>
+class AbstractFormulaChecker {
+	public:
+		virtual bool conforms(const AbstractFormula<T>* formula) const = 0;
+};
+
+}
+}
+
+#endif
\ No newline at end of file
diff --git a/src/formula/Ap.h b/src/formula/Ap.h
index ceca11193..32e6c962e 100644
--- a/src/formula/Ap.h
+++ b/src/formula/Ap.h
@@ -8,7 +8,8 @@
 #ifndef STORM_FORMULA_AP_H_
 #define STORM_FORMULA_AP_H_
 
-#include "AbstractStateFormula.h"
+#include "src/formula/AbstractStateFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelChecker/AbstractModelChecker.h"
 
 namespace storm {
@@ -89,6 +90,10 @@ public:
 	virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<IApModelChecker>()->checkAp(*this);
 	}
+	
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+		return true;
+	}
 
 private:
 	std::string ap;
diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h
index 89ae6e35d..3110ce8be 100644
--- a/src/formula/BoundedUntil.h
+++ b/src/formula/BoundedUntil.h
@@ -8,11 +8,12 @@
 #ifndef STORM_FORMULA_BOUNDEDUNTIL_H_
 #define STORM_FORMULA_BOUNDEDUNTIL_H_
 
-#include "AbstractPathFormula.h"
-#include "AbstractStateFormula.h"
+#include "src/formula/AbstractPathFormula.h"
+#include "src/formula/AbstractStateFormula.h"
 #include "src/modelChecker/AbstractModelChecker.h"
 #include "boost/integer/integer_mask.hpp"
 #include <string>
+#include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
 
@@ -178,6 +179,10 @@ public:
 	virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<IBoundedUntilModelChecker>()->checkBoundedUntil(*this);
 	}
+	
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+		return checker.conforms(this->left) && checker.conforms(this->right);
+	}
 
 private:
 	AbstractStateFormula<T>* left;
diff --git a/src/formula/Eventually.h b/src/formula/Eventually.h
index ac9d38981..8978510ea 100644
--- a/src/formula/Eventually.h
+++ b/src/formula/Eventually.h
@@ -122,6 +122,10 @@ public:
 	virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<IEventuallyModelChecker>()->checkEventually(*this);
 	}
+	
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+		return checker.conforms(this->child);
+	}
 
 private:
 	AbstractStateFormula<T>* child;
diff --git a/src/formula/NoBoundOperator.h b/src/formula/NoBoundOperator.h
index c2cab764d..c7a14d155 100644
--- a/src/formula/NoBoundOperator.h
+++ b/src/formula/NoBoundOperator.h
@@ -10,6 +10,7 @@
 
 #include "AbstractFormula.h"
 #include "AbstractPathFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
 
@@ -116,6 +117,10 @@ public:
 	 * @returns a string representation of the formula
 	 */
 	virtual std::string toString() const = 0;
+	
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+		return checker.conforms(this->pathFormula);
+	}
 
 private:
 	AbstractPathFormula<T>* pathFormula;
diff --git a/src/formula/Not.h b/src/formula/Not.h
index f3f5186ec..56eaf6c6a 100644
--- a/src/formula/Not.h
+++ b/src/formula/Not.h
@@ -9,6 +9,7 @@
 #define STORM_FORMULA_NOT_H_
 
 #include "AbstractStateFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelChecker/AbstractModelChecker.h"
 
 namespace storm {
@@ -117,6 +118,10 @@ public:
 	virtual storm::storage::BitVector *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<INotModelChecker>()->checkNot(*this);  
 	}
+	
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+		return checker.conforms(this->child);
+	}
 
 private:
 	AbstractStateFormula<T>* child;
diff --git a/src/formula/PrctlFormulaChecker.h b/src/formula/PrctlFormulaChecker.h
new file mode 100644
index 000000000..2a8d882e7
--- /dev/null
+++ b/src/formula/PrctlFormulaChecker.h
@@ -0,0 +1,35 @@
+#ifndef STORM_FORMULA_PRCTLFORMULACHECKER_H_
+#define STORM_FORMULA_PRCTLFORMULACHECKER_H_
+
+#include "src/formula/AbstractFormulaChecker.h"
+#include "src/formula/Formulas.h"
+
+#include <iostream>
+
+namespace storm {
+namespace formula {
+
+template <class T>
+class PrctlFormulaChecker : public AbstractFormulaChecker<T> {
+	public:
+		virtual bool conforms(const AbstractFormula<T>* formula) const {
+			if (
+					dynamic_cast<const And<T>*>(formula) ||
+					dynamic_cast<const Ap<T>*>(formula) ||
+					dynamic_cast<const Eventually<T>*>(formula) ||
+					dynamic_cast<const Not<T>*>(formula) ||
+					dynamic_cast<const Or<T>*>(formula) ||
+					dynamic_cast<const ProbabilisticNoBoundOperator<T>*>(formula)
+				) {
+				return formula->conforms(*this);
+			}
+			return false;
+		}
+	
+	private:
+};
+
+}
+}
+
+#endif
\ No newline at end of file
diff --git a/src/formula/ReachabilityReward.h b/src/formula/ReachabilityReward.h
index 4c214ae12..cef56ab6d 100644
--- a/src/formula/ReachabilityReward.h
+++ b/src/formula/ReachabilityReward.h
@@ -10,6 +10,7 @@
 
 #include "src/formula/AbstractPathFormula.h"
 #include "src/formula/AbstractStateFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
 #include "src/modelChecker/AbstractModelChecker.h"
 
 namespace storm {
@@ -119,6 +120,10 @@ public:
 	virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<IReachabilityRewardModelChecker>()->checkReachabilityReward(*this);
 	}
+	
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+		return checker.conforms(this->child);
+	}
 
 private:
 	AbstractStateFormula<T>* child;
diff --git a/src/formula/Until.h b/src/formula/Until.h
index 764175f1c..cfc186f56 100644
--- a/src/formula/Until.h
+++ b/src/formula/Until.h
@@ -10,6 +10,7 @@
 
 #include "AbstractPathFormula.h"
 #include "AbstractStateFormula.h"
+#include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
 
@@ -151,6 +152,10 @@ public:
 	virtual std::vector<T> *check(const storm::modelChecker::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<IUntilModelChecker>()->checkUntil(*this);
 	}
+	
+	virtual bool conforms(const AbstractFormulaChecker<T>& checker) const {
+        return checker.conforms(this->left) && checker.conforms(this->right);
+    }
 
 private:
 	AbstractStateFormula<T>* left;