diff --git a/src/formula/AbstractFormula.h b/src/formula/AbstractFormula.h
index 186415965..517f4ba62 100644
--- a/src/formula/AbstractFormula.h
+++ b/src/formula/AbstractFormula.h
@@ -14,7 +14,7 @@ namespace storm { namespace formula {
 template <class T> class AbstractFormula;
 }}
 
-#include "src/modelchecker/AbstractModelChecker.h"
+#include "src/modelchecker/ForwardDeclarations.h"
 #include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
diff --git a/src/formula/AbstractPathFormula.h b/src/formula/AbstractPathFormula.h
index eeffcb4c1..5d7d6e281 100644
--- a/src/formula/AbstractPathFormula.h
+++ b/src/formula/AbstractPathFormula.h
@@ -13,7 +13,7 @@ template <class T> class AbstractPathFormula;
 }}
 
 #include "src/formula/AbstractFormula.h"
-#include "src/modelchecker/AbstractModelChecker.h"
+#include "src/modelchecker/ForwardDeclarations.h"
 
 #include <vector>
 #include <iostream>
diff --git a/src/formula/AbstractStateFormula.h b/src/formula/AbstractStateFormula.h
index 9f4750f06..9947c5df6 100644
--- a/src/formula/AbstractStateFormula.h
+++ b/src/formula/AbstractStateFormula.h
@@ -14,7 +14,7 @@ template <class T> class AbstractStateFormula;
 
 #include "src/formula/AbstractFormula.h"
 #include "src/storage/BitVector.h"
-#include "src/modelchecker/AbstractModelChecker.h"
+#include "src/modelchecker/ForwardDeclarations.h"
 
 namespace storm {
 namespace formula {
diff --git a/src/formula/And.h b/src/formula/And.h
index db6eafc51..f5d758c2b 100644
--- a/src/formula/And.h
+++ b/src/formula/And.h
@@ -10,7 +10,7 @@
 
 #include "src/formula/AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
-#include "src/modelchecker/AbstractModelChecker.h"
+#include "src/modelchecker/ForwardDeclarations.h"
 #include <string>
 
 namespace storm {
diff --git a/src/formula/Ap.h b/src/formula/Ap.h
index 80bf54fcb..4950b4b72 100644
--- a/src/formula/Ap.h
+++ b/src/formula/Ap.h
@@ -10,7 +10,7 @@
 
 #include "src/formula/AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
-#include "src/modelchecker/AbstractModelChecker.h"
+#include "src/modelchecker/ForwardDeclarations.h"
 
 namespace storm {
 namespace formula {
diff --git a/src/formula/BoundedEventually.h b/src/formula/BoundedEventually.h
index 3d1f85e0b..3bb72d07e 100644
--- a/src/formula/BoundedEventually.h
+++ b/src/formula/BoundedEventually.h
@@ -13,7 +13,7 @@
 #include "src/formula/AbstractFormulaChecker.h"
 #include "boost/integer/integer_mask.hpp"
 #include <string>
-#include "src/modelchecker/AbstractModelChecker.h"
+#include "src/modelchecker/ForwardDeclarations.h"
 
 namespace storm {
 
diff --git a/src/formula/BoundedNaryUntil.h b/src/formula/BoundedNaryUntil.h
index 849274000..91bd44713 100644
--- a/src/formula/BoundedNaryUntil.h
+++ b/src/formula/BoundedNaryUntil.h
@@ -10,13 +10,12 @@
 
 #include "src/formula/AbstractPathFormula.h"
 #include "src/formula/AbstractStateFormula.h"
-#include "src/modelchecker/AbstractModelChecker.h"
 #include "boost/integer/integer_mask.hpp"
 #include <string>
 #include <vector>
 #include <tuple>
 #include <sstream>
-#include "src/formula/AbstractFormulaChecker.h"
+#include "src/modelchecker/ForwardDeclarations.h"
 
 namespace storm {
 namespace formula {
diff --git a/src/formula/BoundedUntil.h b/src/formula/BoundedUntil.h
index 0c3323b61..7b4a7e07c 100644
--- a/src/formula/BoundedUntil.h
+++ b/src/formula/BoundedUntil.h
@@ -10,10 +10,9 @@
 
 #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"
+#include "src/modelchecker/ForwardDeclarations.h"
 
 namespace storm {
 namespace formula {
diff --git a/src/formula/Eventually.h b/src/formula/Eventually.h
index 91623d353..53b7b0dd1 100644
--- a/src/formula/Eventually.h
+++ b/src/formula/Eventually.h
@@ -10,7 +10,7 @@
 
 #include "src/formula/AbstractPathFormula.h"
 #include "src/formula/AbstractStateFormula.h"
-#include "src/modelchecker/AbstractModelChecker.h"
+#include "src/modelchecker/ForwardDeclarations.h"
 
 namespace storm {
 
diff --git a/src/formula/Formulas.h b/src/formula/Formulas.h
index 980c3ca34..6e03975dd 100644
--- a/src/formula/Formulas.h
+++ b/src/formula/Formulas.h
@@ -10,11 +10,6 @@
 
 #include "modelchecker/ForwardDeclarations.h"
 
-#include "AbstractFormula.h"
-#include "AbstractPathFormula.h"
-#include "AbstractStateFormula.h"
-
-
 #include "And.h"
 #include "Ap.h"
 #include "BoundedUntil.h"
@@ -36,6 +31,10 @@
 #include "RewardNoBoundOperator.h"
 #include "SteadyStateOperator.h"
 
+#include "AbstractFormula.h"
+#include "AbstractPathFormula.h"
+#include "AbstractStateFormula.h"
+
 #include "modelchecker/DtmcPrctlModelChecker.h"
 
 #endif /* STORM_FORMULA_FORMULAS_H_ */
diff --git a/src/formula/Globally.h b/src/formula/Globally.h
index e42837091..05041ee17 100644
--- a/src/formula/Globally.h
+++ b/src/formula/Globally.h
@@ -11,6 +11,7 @@
 #include "AbstractPathFormula.h"
 #include "AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
+#include "src/modelchecker/ForwardDeclarations.h"
 
 namespace storm {
 
diff --git a/src/formula/Not.h b/src/formula/Not.h
index 824e6e03b..463f0ca7a 100644
--- a/src/formula/Not.h
+++ b/src/formula/Not.h
@@ -10,7 +10,7 @@
 
 #include "AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
-#include "src/modelchecker/AbstractModelChecker.h"
+#include "src/modelchecker/ForwardDeclarations.h"
 
 namespace storm {
 
diff --git a/src/formula/PathBoundOperator.h b/src/formula/PathBoundOperator.h
index 72bcc6d56..d0f04975f 100644
--- a/src/formula/PathBoundOperator.h
+++ b/src/formula/PathBoundOperator.h
@@ -11,7 +11,7 @@
 #include "src/formula/AbstractStateFormula.h"
 #include "src/formula/AbstractPathFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
-#include "src/modelchecker/AbstractModelChecker.h"
+#include "src/modelchecker/ForwardDeclarations.h"
 #include "src/utility/ConstTemplates.h"
 
 namespace storm {
diff --git a/src/modelchecker/AbstractModelChecker.h b/src/modelchecker/AbstractModelChecker.h
index 110d355dd..5e0920231 100644
--- a/src/modelchecker/AbstractModelChecker.h
+++ b/src/modelchecker/AbstractModelChecker.h
@@ -12,9 +12,7 @@ namespace storm { namespace modelChecker {
 template <class Type> class AbstractModelChecker;
 }}
 
-//#include "src/formula/Formulas.h"
-#include "src/formula/Or.h"
-#include "src/formula/Ap.h"
+#include "src/formula/Formulas.h"
 #include "src/storage/BitVector.h"
 
 #include <iostream>
@@ -33,8 +31,13 @@ namespace modelChecker {
  */
 template<class Type>
 class AbstractModelChecker :
-	public virtual storm::formula::IOrModelChecker<Type>,
-	public virtual storm::formula::IApModelChecker<Type>
+	public virtual storm::formula::IApModelChecker<Type>,
+	public virtual storm::formula::IAndModelChecker<Type>,
+	public virtual storm::formula::IEventuallyModelChecker<Type>,
+	public virtual storm::formula::IGloballyModelChecker<Type>,
+	public virtual storm::formula::INextModelChecker<Type>,
+	public virtual storm::formula::INotModelChecker<Type>,
+	public virtual storm::formula::IOrModelChecker<Type>
 	{
 	
 public:
diff --git a/src/modelchecker/DtmcPrctlModelChecker.h b/src/modelchecker/DtmcPrctlModelChecker.h
index 17ae608c1..90f1672e0 100644
--- a/src/modelchecker/DtmcPrctlModelChecker.h
+++ b/src/modelchecker/DtmcPrctlModelChecker.h
@@ -41,8 +41,7 @@ template<class Type>
 class DtmcPrctlModelChecker : 
 	public virtual AbstractModelChecker<Type>, 
 	public virtual storm::formula::INoBoundOperatorModelChecker<Type>,
-	public virtual storm::formula::IReachabilityRewardModelChecker<Type>,
-	public virtual storm::formula::IEventuallyModelChecker<Type>
+	public virtual storm::formula::IReachabilityRewardModelChecker<Type>
 	{
 public:
 	/*!
diff --git a/src/modelchecker/ForwardDeclarations.h b/src/modelchecker/ForwardDeclarations.h
index 715f1488c..8239e2023 100644
--- a/src/modelchecker/ForwardDeclarations.h
+++ b/src/modelchecker/ForwardDeclarations.h
@@ -13,6 +13,9 @@ namespace storm {
 
 namespace modelChecker {
 
+template <class Type>
+class AbstractModelChecker;
+
 template <class Type>
 class DtmcPrctlModelChecker;