diff --git a/src/formula/Csl.h b/src/formula/Csl.h
index 9266df327..b9724eab3 100644
--- a/src/formula/Csl.h
+++ b/src/formula/Csl.h
@@ -5,8 +5,10 @@
  *      Author: thomas
  */
 
-#ifndef CSL_H_
-#define CSL_H_
+#ifndef STORM_FORMULA_CSL_H_
+#define STORM_FORMULA_CSL_H_
+
+#include "src/modelchecker/csl/ForwardDeclarations.h"
 
 #include "Csl/And.h"
 #include "Csl/Ap.h"
@@ -24,5 +26,7 @@
 #include "Csl/TimeBoundedEventually.h"
 #include "Csl/TimeBoundedUntil.h"
 
+#include "modelchecker/csl/AbstractModelChecker.h"
+
 
-#endif /* CSL_H_ */
+#endif /* STORM_FORMULA_CSL_H_ */
diff --git a/src/formula/Csl/AbstractNoBoundOperator.h b/src/formula/Csl/AbstractNoBoundOperator.h
index d083a2afa..f2b56711a 100644
--- a/src/formula/Csl/AbstractNoBoundOperator.h
+++ b/src/formula/Csl/AbstractNoBoundOperator.h
@@ -74,7 +74,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const = 0;
+	virtual std::vector<T>* check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const = 0;
 };
 
 } /* namespace csl */
diff --git a/src/formula/Csl/AbstractPathFormula.h b/src/formula/Csl/AbstractPathFormula.h
index e2f63c9ac..63b20feaa 100644
--- a/src/formula/Csl/AbstractPathFormula.h
+++ b/src/formula/Csl/AbstractPathFormula.h
@@ -17,7 +17,7 @@ template<class T> class AbstractPathFormula;
 } //namespace storm
 
 #include "src/formula/abstract/AbstractFormula.h"
-#include "src/modelchecker/ForwardDeclarations.h"
+#include "src/modelchecker/csl/ForwardDeclarations.h"
 
 #include <vector>
 #include <iostream>
@@ -71,7 +71,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const = 0;
+	virtual std::vector<T>* check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const = 0;
 };
 
 } //namespace csl
diff --git a/src/formula/Csl/AbstractStateFormula.h b/src/formula/Csl/AbstractStateFormula.h
index 9578b6b2e..d96f02f5d 100644
--- a/src/formula/Csl/AbstractStateFormula.h
+++ b/src/formula/Csl/AbstractStateFormula.h
@@ -18,7 +18,7 @@ template<class T> class AbstractStateFormula;
 
 #include "AbstractCslFormula.h"
 #include "src/storage/BitVector.h"
-#include "src/modelchecker/ForwardDeclarations.h"
+#include "src/modelchecker/csl/ForwardDeclarations.h"
 
 namespace storm {
 namespace property {
@@ -65,7 +65,7 @@ public:
 	 *
 	 * @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 = 0;
+	virtual storm::storage::BitVector* check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker) const = 0;
 };
 
 } //namespace csl
diff --git a/src/formula/Csl/And.h b/src/formula/Csl/And.h
index acac02281..ebaf0fe9f 100644
--- a/src/formula/Csl/And.h
+++ b/src/formula/Csl/And.h
@@ -11,7 +11,7 @@
 #include "AbstractStateFormula.h"
 #include "src/formula/abstract/And.h"
 #include "src/formula/AbstractFormulaChecker.h"
-#include "src/modelchecker/ForwardDeclarations.h"
+#include "src/modelchecker/csl/ForwardDeclarations.h"
 #include <string>
 
 namespace storm {
@@ -114,7 +114,7 @@ public:
 	 *
 	 * @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 {
+	virtual storm::storage::BitVector* check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<IAndModelChecker>()->checkAnd(*this);
 	}
 
diff --git a/src/formula/Csl/Ap.h b/src/formula/Csl/Ap.h
index a5cdf9373..cc0cad9e3 100644
--- a/src/formula/Csl/Ap.h
+++ b/src/formula/Csl/Ap.h
@@ -11,7 +11,7 @@
 #include "AbstractStateFormula.h"
 #include "src/formula/abstract/Ap.h"
 #include "src/formula/AbstractFormulaChecker.h"
-#include "src/modelchecker/ForwardDeclarations.h"
+#include "src/modelchecker/csl/ForwardDeclarations.h"
 
 namespace storm {
 namespace property {
@@ -91,7 +91,7 @@ public:
 	 *
 	 * @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 {
+	virtual storm::storage::BitVector *check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<IApModelChecker>()->checkAp(*this);
 	}
 
diff --git a/src/formula/Csl/Eventually.h b/src/formula/Csl/Eventually.h
index 7ea81763e..d4dd43030 100644
--- a/src/formula/Csl/Eventually.h
+++ b/src/formula/Csl/Eventually.h
@@ -11,7 +11,7 @@
 #include "src/formula/abstract/Eventually.h"
 #include "src/formula/Csl/AbstractPathFormula.h"
 #include "src/formula/Csl/AbstractStateFormula.h"
-#include "src/modelchecker/ForwardDeclarations.h"
+#include "src/modelchecker/csl/ForwardDeclarations.h"
 
 namespace storm {
 namespace property {
@@ -108,7 +108,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+	virtual std::vector<T> *check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
 		return modelChecker.template as<IEventuallyModelChecker>()->checkEventually(*this, qualitative);
 	}
 };
diff --git a/src/formula/Csl/Globally.h b/src/formula/Csl/Globally.h
index c4b4b1c31..7bc209d25 100644
--- a/src/formula/Csl/Globally.h
+++ b/src/formula/Csl/Globally.h
@@ -12,7 +12,7 @@
 #include "AbstractPathFormula.h"
 #include "AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
-#include "src/modelchecker/ForwardDeclarations.h"
+#include "src/modelchecker/csl/ForwardDeclarations.h"
 
 namespace storm {
 namespace property {
@@ -110,7 +110,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+	virtual std::vector<T> *check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
 		return modelChecker.template as<IGloballyModelChecker>()->checkGlobally(*this, qualitative);
 	}
 };
diff --git a/src/formula/Csl/Next.h b/src/formula/Csl/Next.h
index 226c854b9..c37a8165b 100644
--- a/src/formula/Csl/Next.h
+++ b/src/formula/Csl/Next.h
@@ -108,7 +108,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+	virtual std::vector<T> *check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
 		return modelChecker.template as<INextModelChecker>()->checkNext(*this, qualitative);
 	}
 };
diff --git a/src/formula/Csl/Not.h b/src/formula/Csl/Not.h
index 3cd58d268..0f77142ae 100644
--- a/src/formula/Csl/Not.h
+++ b/src/formula/Csl/Not.h
@@ -11,7 +11,7 @@
 #include "AbstractStateFormula.h"
 #include "src/formula/abstract/Not.h"
 #include "src/formula/AbstractFormulaChecker.h"
-#include "src/modelchecker/ForwardDeclarations.h"
+#include "src/modelchecker/csl/ForwardDeclarations.h"
 
 namespace storm {
 namespace property {
@@ -104,7 +104,7 @@ public:
 	 *
 	 * @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 {
+	virtual storm::storage::BitVector *check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<INotModelChecker>()->checkNot(*this);  
 	}
 };
diff --git a/src/formula/Csl/Or.h b/src/formula/Csl/Or.h
index c4ca658a2..edc1fd697 100644
--- a/src/formula/Csl/Or.h
+++ b/src/formula/Csl/Or.h
@@ -113,7 +113,7 @@ public:
 	 *
 	 * @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 {
+	virtual storm::storage::BitVector *check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<IOrModelChecker>()->checkOr(*this);
 	}
 };
diff --git a/src/formula/Csl/ProbabilisticBoundOperator.h b/src/formula/Csl/ProbabilisticBoundOperator.h
index ba7ba4e7a..48db99b44 100644
--- a/src/formula/Csl/ProbabilisticBoundOperator.h
+++ b/src/formula/Csl/ProbabilisticBoundOperator.h
@@ -109,7 +109,7 @@ public:
 	 *
 	 * @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 {
+	virtual storm::storage::BitVector* check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<IProbabilisticBoundOperatorModelChecker>()->checkProbabilisticBoundOperator(*this);
 	}
 };
diff --git a/src/formula/Csl/ProbabilisticNoBoundOperator.h b/src/formula/Csl/ProbabilisticNoBoundOperator.h
index 582839b8f..4eb1a227e 100644
--- a/src/formula/Csl/ProbabilisticNoBoundOperator.h
+++ b/src/formula/Csl/ProbabilisticNoBoundOperator.h
@@ -34,7 +34,7 @@ namespace csl {
  * 	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.
+ * 	Use the checkProbabilisticNoBoundOperator method from the DtmccslModelChecker 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)
@@ -103,7 +103,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const {
+	virtual std::vector<T>* check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const {
 		return this->getPathFormula().check(modelChecker, qualitative);
 	}
 };
diff --git a/src/formula/Csl/SteadyStateBoundOperator.h b/src/formula/Csl/SteadyStateBoundOperator.h
index 3db48445e..e9ac6a3e5 100644
--- a/src/formula/Csl/SteadyStateBoundOperator.h
+++ b/src/formula/Csl/SteadyStateBoundOperator.h
@@ -105,7 +105,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual storm::storage::BitVector* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
+	virtual storm::storage::BitVector* check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<ISteadyStateBoundOperatorModelChecker>()->checkSteadyStateBoundOperator(*this);
 	}
 	
diff --git a/src/formula/Csl/SteadyStateNoBoundOperator.h b/src/formula/Csl/SteadyStateNoBoundOperator.h
index f49bbce35..51c407d02 100644
--- a/src/formula/Csl/SteadyStateNoBoundOperator.h
+++ b/src/formula/Csl/SteadyStateNoBoundOperator.h
@@ -87,7 +87,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T>*  check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const {
+	virtual std::vector<T>*  check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const {
 		return modelChecker.template as<ISteadyStateNoBoundOperatorModelChecker>()->checkSteadyStateNoBoundOperator(*this);
 	}
 
diff --git a/src/formula/Csl/TimeBoundedEventually.h b/src/formula/Csl/TimeBoundedEventually.h
index 17c046851..06c03b49c 100644
--- a/src/formula/Csl/TimeBoundedEventually.h
+++ b/src/formula/Csl/TimeBoundedEventually.h
@@ -85,7 +85,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+	virtual std::vector<T>* check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
 		return modelChecker.template as<ITimeBoundedEventuallyModelChecker>()->checkTimeBoundedEventually(*this, qualitative);
 	}
 };
diff --git a/src/formula/Csl/TimeBoundedUntil.h b/src/formula/Csl/TimeBoundedUntil.h
index ac16d95a5..4249888f0 100644
--- a/src/formula/Csl/TimeBoundedUntil.h
+++ b/src/formula/Csl/TimeBoundedUntil.h
@@ -99,7 +99,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+	virtual std::vector<T>* check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
 		return modelChecker.template as<ITimeBoundedUntilModelChecker>()->checkTimeBoundedUntil(*this, qualitative);
 	}
 };
diff --git a/src/formula/Csl/Until.h b/src/formula/Csl/Until.h
index 78f924176..defd1e35b 100644
--- a/src/formula/Csl/Until.h
+++ b/src/formula/Csl/Until.h
@@ -113,7 +113,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+	virtual std::vector<T> *check(const storm::modelchecker::csl::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
 		return modelChecker.template as<IUntilModelChecker>()->checkUntil(*this, qualitative);
 	}
 };
diff --git a/src/formula/Ltl.h b/src/formula/Ltl.h
index 17a51d68b..63569ea79 100644
--- a/src/formula/Ltl.h
+++ b/src/formula/Ltl.h
@@ -8,7 +8,7 @@
 #ifndef STORM_FORMULA_LTL_H_
 #define STORM_FORMULA_LTL_H_
 
-#include "src/modelchecker/ForwardDeclarations.h"
+#include "src/modelchecker/ltl/ForwardDeclarations.h"
 
 #include "Ltl/And.h"
 #include "Ltl/Ap.h"
@@ -21,6 +21,6 @@
 #include "Ltl/Or.h"
 #include "Ltl/Until.h"
 
-#include "modelchecker/AbstractModelChecker.h"
+#include "modelchecker/ltl/AbstractModelChecker.h"
 
 #endif /* STORM_FORMULA_LTL_H_ */
diff --git a/src/formula/Ltl/AbstractLtlFormula.h b/src/formula/Ltl/AbstractLtlFormula.h
index a71966df2..e4afe81c8 100644
--- a/src/formula/Ltl/AbstractLtlFormula.h
+++ b/src/formula/Ltl/AbstractLtlFormula.h
@@ -9,7 +9,7 @@
 #define STORM_LTL_ABSTRACTLTLFORMULA_H_
 
 #include <vector>
-#include "src/modelchecker/ForwardDeclarations.h"
+#include "src/modelchecker/ltl/ForwardDeclarations.h"
 #include "src/formula/abstract/AbstractFormula.h"
 
 namespace storm {
@@ -40,7 +40,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const = 0;
+	virtual std::vector<T>* check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const = 0;
 
 	/*!
 	 * Clones the called object.
diff --git a/src/formula/Ltl/And.h b/src/formula/Ltl/And.h
index 3745ed518..b8f5ad320 100644
--- a/src/formula/Ltl/And.h
+++ b/src/formula/Ltl/And.h
@@ -11,7 +11,7 @@
 #include "AbstractLtlFormula.h"
 #include "src/formula/abstract/And.h"
 #include "src/formula/AbstractFormulaChecker.h"
-#include "src/modelchecker/ForwardDeclarations.h"
+#include "src/modelchecker/ltl/ForwardDeclarations.h"
 #include <string>
 
 namespace storm {
@@ -113,7 +113,7 @@ public:
 	 *
 	 * @returns A bit 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 {
+	virtual std::vector<T>* check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<IAndModelChecker>()->checkAnd(*this);
 	}
 
diff --git a/src/formula/Ltl/Ap.h b/src/formula/Ltl/Ap.h
index 23a943610..4669c1131 100644
--- a/src/formula/Ltl/Ap.h
+++ b/src/formula/Ltl/Ap.h
@@ -84,7 +84,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
+	virtual std::vector<T>* check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<IApModelChecker>()->checkAp(*this);
 	}
 
diff --git a/src/formula/Ltl/BoundedEventually.h b/src/formula/Ltl/BoundedEventually.h
index 5cbaad135..79868ef8e 100644
--- a/src/formula/Ltl/BoundedEventually.h
+++ b/src/formula/Ltl/BoundedEventually.h
@@ -13,7 +13,7 @@
 #include "src/formula/AbstractFormulaChecker.h"
 #include "boost/integer/integer_mask.hpp"
 #include <string>
-#include "src/modelchecker/ForwardDeclarations.h"
+#include "src/modelchecker/ltl/ForwardDeclarations.h"
 
 namespace storm {
 namespace property {
@@ -112,7 +112,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
+	virtual std::vector<T>* check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<IBoundedEventuallyModelChecker>()->checkBoundedEventually(*this);
 	}
 };
diff --git a/src/formula/Ltl/BoundedUntil.h b/src/formula/Ltl/BoundedUntil.h
index a50dcfa43..63e6f851f 100644
--- a/src/formula/Ltl/BoundedUntil.h
+++ b/src/formula/Ltl/BoundedUntil.h
@@ -12,7 +12,7 @@
 #include "AbstractLtlFormula.h"
 #include "boost/integer/integer_mask.hpp"
 #include <string>
-#include "src/modelchecker/ForwardDeclarations.h"
+#include "src/modelchecker/ltl/ForwardDeclarations.h"
 
 namespace storm {
 namespace property {
@@ -129,7 +129,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
+	virtual std::vector<T> *check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<IBoundedUntilModelChecker>()->checkBoundedUntil(*this);
 	}
 };
diff --git a/src/formula/Ltl/Eventually.h b/src/formula/Ltl/Eventually.h
index 862271743..6d5c9a99d 100644
--- a/src/formula/Ltl/Eventually.h
+++ b/src/formula/Ltl/Eventually.h
@@ -10,7 +10,7 @@
 
 #include "src/formula/abstract/Eventually.h"
 #include "AbstractLtlFormula.h"
-#include "src/modelchecker/ForwardDeclarations.h"
+#include "src/modelchecker/ltl/ForwardDeclarations.h"
 
 namespace storm {
 namespace property {
@@ -106,7 +106,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
+	virtual std::vector<T> *check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<IEventuallyModelChecker>()->checkEventually(*this);
 	}
 };
diff --git a/src/formula/Ltl/Globally.h b/src/formula/Ltl/Globally.h
index 3863ae853..8ac8c5816 100644
--- a/src/formula/Ltl/Globally.h
+++ b/src/formula/Ltl/Globally.h
@@ -11,7 +11,7 @@
 #include "src/formula/abstract/Globally.h"
 #include "AbstractLtlFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
-#include "src/modelchecker/ForwardDeclarations.h"
+#include "src/modelchecker/ltl/ForwardDeclarations.h"
 
 namespace storm {
 namespace property {
@@ -108,7 +108,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
+	virtual std::vector<T> *check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<IGloballyModelChecker>()->checkGlobally(*this);
 	}
 };
diff --git a/src/formula/Ltl/Next.h b/src/formula/Ltl/Next.h
index 889b09e01..e631755ec 100644
--- a/src/formula/Ltl/Next.h
+++ b/src/formula/Ltl/Next.h
@@ -106,7 +106,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
+	virtual std::vector<T> *check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<INextModelChecker>()->checkNext(*this);
 	}
 };
diff --git a/src/formula/Ltl/Not.h b/src/formula/Ltl/Not.h
index c7709b33c..40772b418 100644
--- a/src/formula/Ltl/Not.h
+++ b/src/formula/Ltl/Not.h
@@ -102,7 +102,7 @@ public:
 	 *
 	 * @returns A bit 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 {
+	virtual std::vector<T>* check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<INotModelChecker>()->checkNot(*this);
 	}
 };
diff --git a/src/formula/Ltl/Or.h b/src/formula/Ltl/Or.h
index bd07c36f9..4c1e5b535 100644
--- a/src/formula/Ltl/Or.h
+++ b/src/formula/Ltl/Or.h
@@ -107,7 +107,7 @@ public:
 	 *
 	 * @returns A bit 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 {
+	virtual std::vector<T>* check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<IOrModelChecker>()->checkOr(*this);
 	}
 
diff --git a/src/formula/Ltl/Until.h b/src/formula/Ltl/Until.h
index 2fd0030f0..9a02e9a05 100644
--- a/src/formula/Ltl/Until.h
+++ b/src/formula/Ltl/Until.h
@@ -123,7 +123,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker) const {
+	virtual std::vector<T> *check(const storm::modelchecker::ltl::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<IUntilModelChecker>()->checkUntil(*this);
 	}
 };
diff --git a/src/formula/Prctl.h b/src/formula/Prctl.h
index f90a488c7..f3d727fc1 100644
--- a/src/formula/Prctl.h
+++ b/src/formula/Prctl.h
@@ -5,10 +5,10 @@
  *      Author: chris
  */
 
-#ifndef STORM_FORMULA_FORMULAS_H_
-#define STORM_FORMULA_FORMULAS_H_
+#ifndef STORM_FORMULA_PRCTL_H_
+#define STORM_FORMULA_PRCTL_H_
 
-#include "modelchecker/ForwardDeclarations.h"
+#include "modelchecker/prctl/ForwardDeclarations.h"
 
 #include "Prctl/And.h"
 #include "Prctl/Ap.h"
@@ -32,18 +32,11 @@
 #include "Prctl/RewardNoBoundOperator.h"
 #include "Prctl/SteadyStateReward.h"
 
-/*
-#include "SteadyStateNoBoundOperator.h"
-#include "SteadyStateBoundOperator.h"
-
-#include "TimeBoundedUntil.h"
-#include "TimeBoundedEventually.h"
-*/
 #include "Prctl/AbstractPrctlFormula.h"
 #include "Prctl/AbstractStateFormula.h"
 #include "Prctl/AbstractNoBoundOperator.h"
 #include "Prctl/AbstractPathFormula.h"
 
-#include "modelchecker/AbstractModelChecker.h"
+#include "modelchecker/prctl/AbstractModelChecker.h"
 
-#endif /* STORM_FORMULA_FORMULAS_H_ */
+#endif /* STORM_FORMULA_PRCTL_H_ */
diff --git a/src/formula/Prctl/AbstractNoBoundOperator.h b/src/formula/Prctl/AbstractNoBoundOperator.h
index 0343c2762..e28c0df34 100644
--- a/src/formula/Prctl/AbstractNoBoundOperator.h
+++ b/src/formula/Prctl/AbstractNoBoundOperator.h
@@ -74,7 +74,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const = 0;
+	virtual std::vector<T>* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const = 0;
 };
 
 } /* namespace prctl */
diff --git a/src/formula/Prctl/AbstractPathFormula.h b/src/formula/Prctl/AbstractPathFormula.h
index fe9797819..62c788452 100644
--- a/src/formula/Prctl/AbstractPathFormula.h
+++ b/src/formula/Prctl/AbstractPathFormula.h
@@ -13,7 +13,7 @@ template <class T> class AbstractPathFormula;
 }}}
 
 #include "src/formula/abstract/AbstractFormula.h"
-#include "src/modelchecker/ForwardDeclarations.h"
+#include "src/modelchecker/prctl/ForwardDeclarations.h"
 
 #include <vector>
 #include <iostream>
@@ -66,7 +66,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const = 0;
+	virtual std::vector<T>* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const = 0;
 };
 
 } //namespace prctl
diff --git a/src/formula/Prctl/AbstractStateFormula.h b/src/formula/Prctl/AbstractStateFormula.h
index da4968e36..d06c48b30 100644
--- a/src/formula/Prctl/AbstractStateFormula.h
+++ b/src/formula/Prctl/AbstractStateFormula.h
@@ -14,7 +14,7 @@ template <class T> class AbstractStateFormula;
 
 #include "AbstractPrctlFormula.h"
 #include "src/storage/BitVector.h"
-#include "src/modelchecker/ForwardDeclarations.h"
+#include "src/modelchecker/prctl/ForwardDeclarations.h"
 
 namespace storm {
 namespace property {
@@ -61,7 +61,7 @@ public:
 	 *
 	 * @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 = 0;
+	virtual storm::storage::BitVector *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker) const = 0;
 };
 
 } //namespace prctl
diff --git a/src/formula/Prctl/And.h b/src/formula/Prctl/And.h
index a05f3db4f..b14606b54 100644
--- a/src/formula/Prctl/And.h
+++ b/src/formula/Prctl/And.h
@@ -11,7 +11,7 @@
 #include "AbstractStateFormula.h"
 #include "src/formula/abstract/And.h"
 #include "src/formula/AbstractFormulaChecker.h"
-#include "src/modelchecker/ForwardDeclarations.h"
+#include "src/modelchecker/prctl/ForwardDeclarations.h"
 #include <string>
 
 namespace storm {
@@ -114,7 +114,7 @@ public:
 	 *
 	 * @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 {
+	virtual storm::storage::BitVector* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<IAndModelChecker>()->checkAnd(*this);
 	}
 
diff --git a/src/formula/Prctl/Ap.h b/src/formula/Prctl/Ap.h
index 5f20174b9..d7d878366 100644
--- a/src/formula/Prctl/Ap.h
+++ b/src/formula/Prctl/Ap.h
@@ -11,7 +11,7 @@
 #include "AbstractStateFormula.h"
 #include "src/formula/abstract/Ap.h"
 #include "src/formula/AbstractFormulaChecker.h"
-#include "src/modelchecker/ForwardDeclarations.h"
+#include "src/modelchecker/prctl/ForwardDeclarations.h"
 
 namespace storm {
 namespace property {
@@ -91,7 +91,7 @@ public:
 	 *
 	 * @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 {
+	virtual storm::storage::BitVector *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<IApModelChecker>()->checkAp(*this);
 	}
 
diff --git a/src/formula/Prctl/BoundedEventually.h b/src/formula/Prctl/BoundedEventually.h
index 45b883160..5f716006d 100644
--- a/src/formula/Prctl/BoundedEventually.h
+++ b/src/formula/Prctl/BoundedEventually.h
@@ -14,7 +14,7 @@
 #include "src/formula/AbstractFormulaChecker.h"
 #include "boost/integer/integer_mask.hpp"
 #include <string>
-#include "src/modelchecker/ForwardDeclarations.h"
+#include "src/modelchecker/prctl/ForwardDeclarations.h"
 
 namespace storm {
 namespace property {
@@ -114,7 +114,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+	virtual std::vector<T>* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
 		return modelChecker.template as<IBoundedEventuallyModelChecker>()->checkBoundedEventually(*this, qualitative);
 	}
 };
diff --git a/src/formula/Prctl/BoundedNaryUntil.h b/src/formula/Prctl/BoundedNaryUntil.h
index 19e2a8f9c..ad0d73ebc 100644
--- a/src/formula/Prctl/BoundedNaryUntil.h
+++ b/src/formula/Prctl/BoundedNaryUntil.h
@@ -16,7 +16,7 @@
 #include <vector>
 #include <tuple>
 #include <sstream>
-#include "src/modelchecker/ForwardDeclarations.h"
+#include "src/modelchecker/prctl/ForwardDeclarations.h"
 
 namespace storm {
 namespace property {
@@ -128,7 +128,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+	virtual std::vector<T> *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
 		return modelChecker.template as<IBoundedNaryUntilModelChecker>()->checkBoundedNaryUntil(*this, qualitative);
 	}
 
diff --git a/src/formula/Prctl/BoundedUntil.h b/src/formula/Prctl/BoundedUntil.h
index ed5aece6e..cfa951bf5 100644
--- a/src/formula/Prctl/BoundedUntil.h
+++ b/src/formula/Prctl/BoundedUntil.h
@@ -13,7 +13,7 @@
 #include "src/formula/Prctl/AbstractStateFormula.h"
 #include "boost/integer/integer_mask.hpp"
 #include <string>
-#include "src/modelchecker/ForwardDeclarations.h"
+#include "src/modelchecker/prctl/ForwardDeclarations.h"
 
 namespace storm {
 namespace property {
@@ -119,7 +119,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+	virtual std::vector<T> *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
 		return modelChecker.template as<IBoundedUntilModelChecker>()->checkBoundedUntil(*this, qualitative);
 	}
 };
diff --git a/src/formula/Prctl/CumulativeReward.h b/src/formula/Prctl/CumulativeReward.h
index d008e0aa8..382d31c80 100644
--- a/src/formula/Prctl/CumulativeReward.h
+++ b/src/formula/Prctl/CumulativeReward.h
@@ -98,7 +98,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+	virtual std::vector<T> *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
 		return modelChecker.template as<ICumulativeRewardModelChecker>()->checkCumulativeReward(*this, qualitative);
 	}
 };
diff --git a/src/formula/Prctl/Eventually.h b/src/formula/Prctl/Eventually.h
index 3775191bd..083d1bf79 100644
--- a/src/formula/Prctl/Eventually.h
+++ b/src/formula/Prctl/Eventually.h
@@ -11,7 +11,7 @@
 #include "src/formula/abstract/Eventually.h"
 #include "src/formula/Prctl/AbstractPathFormula.h"
 #include "src/formula/Prctl/AbstractStateFormula.h"
-#include "src/modelchecker/ForwardDeclarations.h"
+#include "src/modelchecker/prctl/ForwardDeclarations.h"
 
 namespace storm {
 namespace property {
@@ -108,7 +108,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+	virtual std::vector<T> *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
 		return modelChecker.template as<IEventuallyModelChecker>()->checkEventually(*this, qualitative);
 	}
 };
diff --git a/src/formula/Prctl/Globally.h b/src/formula/Prctl/Globally.h
index 2b11cf500..38b2fcb4c 100644
--- a/src/formula/Prctl/Globally.h
+++ b/src/formula/Prctl/Globally.h
@@ -12,7 +12,7 @@
 #include "AbstractPathFormula.h"
 #include "AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
-#include "src/modelchecker/ForwardDeclarations.h"
+#include "src/modelchecker/prctl/ForwardDeclarations.h"
 
 namespace storm {
 namespace property {
@@ -110,7 +110,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+	virtual std::vector<T> *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
 		return modelChecker.template as<IGloballyModelChecker>()->checkGlobally(*this, qualitative);
 	}
 };
diff --git a/src/formula/Prctl/InstantaneousReward.h b/src/formula/Prctl/InstantaneousReward.h
index 8a91afe45..bd54ef289 100644
--- a/src/formula/Prctl/InstantaneousReward.h
+++ b/src/formula/Prctl/InstantaneousReward.h
@@ -99,7 +99,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+	virtual std::vector<T> *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
 		return modelChecker.template as<IInstantaneousRewardModelChecker>()->checkInstantaneousReward(*this, qualitative);
 	}
 };
diff --git a/src/formula/Prctl/Next.h b/src/formula/Prctl/Next.h
index aa42d2580..5700f5a42 100644
--- a/src/formula/Prctl/Next.h
+++ b/src/formula/Prctl/Next.h
@@ -108,7 +108,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+	virtual std::vector<T> *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
 		return modelChecker.template as<INextModelChecker>()->checkNext(*this, qualitative);
 	}
 };
diff --git a/src/formula/Prctl/Not.h b/src/formula/Prctl/Not.h
index 860a2d338..8b60807db 100644
--- a/src/formula/Prctl/Not.h
+++ b/src/formula/Prctl/Not.h
@@ -11,7 +11,7 @@
 #include "AbstractStateFormula.h"
 #include "src/formula/abstract/Not.h"
 #include "src/formula/AbstractFormulaChecker.h"
-#include "src/modelchecker/ForwardDeclarations.h"
+#include "src/modelchecker/prctl/ForwardDeclarations.h"
 
 namespace storm {
 namespace property {
@@ -104,7 +104,7 @@ public:
 	 *
 	 * @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 {
+	virtual storm::storage::BitVector *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<INotModelChecker>()->checkNot(*this);  
 	}
 };
diff --git a/src/formula/Prctl/Or.h b/src/formula/Prctl/Or.h
index a77aafede..6a9159c7a 100644
--- a/src/formula/Prctl/Or.h
+++ b/src/formula/Prctl/Or.h
@@ -113,7 +113,7 @@ public:
 	 *
 	 * @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 {
+	virtual storm::storage::BitVector *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<IOrModelChecker>()->checkOr(*this);
 	}
 };
diff --git a/src/formula/Prctl/ProbabilisticBoundOperator.h b/src/formula/Prctl/ProbabilisticBoundOperator.h
index 823b4ec10..08c94398d 100644
--- a/src/formula/Prctl/ProbabilisticBoundOperator.h
+++ b/src/formula/Prctl/ProbabilisticBoundOperator.h
@@ -127,7 +127,7 @@ public:
 	 *
 	 * @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 {
+	virtual storm::storage::BitVector* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<IProbabilisticBoundOperatorModelChecker>()->checkProbabilisticBoundOperator(*this);
 	}
 };
diff --git a/src/formula/Prctl/ProbabilisticNoBoundOperator.h b/src/formula/Prctl/ProbabilisticNoBoundOperator.h
index c8e6b12e3..b50060ec4 100644
--- a/src/formula/Prctl/ProbabilisticNoBoundOperator.h
+++ b/src/formula/Prctl/ProbabilisticNoBoundOperator.h
@@ -103,7 +103,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const {
+	virtual std::vector<T>* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const {
 		return this->getPathFormula().check(modelChecker, qualitative);
 	}
 };
diff --git a/src/formula/Prctl/ReachabilityReward.h b/src/formula/Prctl/ReachabilityReward.h
index b65af73f3..a155c2835 100644
--- a/src/formula/Prctl/ReachabilityReward.h
+++ b/src/formula/Prctl/ReachabilityReward.h
@@ -105,7 +105,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+	virtual std::vector<T> *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
 		return modelChecker.template as<IReachabilityRewardModelChecker>()->checkReachabilityReward(*this, qualitative);
 	}
 };
diff --git a/src/formula/Prctl/RewardBoundOperator.h b/src/formula/Prctl/RewardBoundOperator.h
index 2a393c36c..572364b88 100644
--- a/src/formula/Prctl/RewardBoundOperator.h
+++ b/src/formula/Prctl/RewardBoundOperator.h
@@ -120,7 +120,7 @@ public:
 	 *
 	 * @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 {
+	virtual storm::storage::BitVector* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker) const {
 		return modelChecker.template as<IRewardBoundOperatorModelChecker>()->checkRewardBoundOperator(*this);
 	}
 };
diff --git a/src/formula/Prctl/RewardNoBoundOperator.h b/src/formula/Prctl/RewardNoBoundOperator.h
index fa198bded..108c1f14c 100644
--- a/src/formula/Prctl/RewardNoBoundOperator.h
+++ b/src/formula/Prctl/RewardNoBoundOperator.h
@@ -96,7 +96,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T>* check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const {
+	virtual std::vector<T>* check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative=false) const {
 		return this->getPathFormula().check(modelChecker, qualitative);
 	}
 };
diff --git a/src/formula/Prctl/SteadyStateReward.h b/src/formula/Prctl/SteadyStateReward.h
index a736b1bb0..df9f0a6f1 100644
--- a/src/formula/Prctl/SteadyStateReward.h
+++ b/src/formula/Prctl/SteadyStateReward.h
@@ -80,7 +80,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+	virtual std::vector<T> *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
 		return modelChecker.template as<ISteadyStateRewardModelChecker>()->checkSteadyStateReward(*this, qualitative);
 	}
 };
diff --git a/src/formula/Prctl/Until.h b/src/formula/Prctl/Until.h
index 338b776d5..75e27eb33 100644
--- a/src/formula/Prctl/Until.h
+++ b/src/formula/Prctl/Until.h
@@ -113,7 +113,7 @@ public:
 	 *
 	 * @returns A vector indicating the probability that the formula holds for each state.
 	 */
-	virtual std::vector<T> *check(const storm::modelchecker::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
+	virtual std::vector<T> *check(const storm::modelchecker::prctl::AbstractModelChecker<T>& modelChecker, bool qualitative) const {
 		return modelChecker.template as<IUntilModelChecker>()->checkUntil(*this, qualitative);
 	}
 };
diff --git a/src/formula/abstract/AbstractFormula.h b/src/formula/abstract/AbstractFormula.h
index 558c3ce5d..ad8122b52 100644
--- a/src/formula/abstract/AbstractFormula.h
+++ b/src/formula/abstract/AbstractFormula.h
@@ -18,7 +18,7 @@ template <class T> class AbstractFormula;
 } //namespace property
 } //namespace storm
 
-#include "src/modelchecker/ForwardDeclarations.h"
+
 #include "src/formula/AbstractFormulaChecker.h"
 
 namespace storm {
diff --git a/src/formula/abstract/And.h b/src/formula/abstract/And.h
index 3442d62a9..4837562da 100644
--- a/src/formula/abstract/And.h
+++ b/src/formula/abstract/And.h
@@ -10,7 +10,6 @@
 
 #include "src/formula/abstract/AbstractFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
-#include "src/modelchecker/ForwardDeclarations.h"
 #include <string>
 
 namespace storm {
diff --git a/src/formula/abstract/Ap.h b/src/formula/abstract/Ap.h
index bc5027ef1..47abc09ea 100644
--- a/src/formula/abstract/Ap.h
+++ b/src/formula/abstract/Ap.h
@@ -10,7 +10,6 @@
 
 #include "src/formula/abstract/AbstractFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
-#include "src/modelchecker/ForwardDeclarations.h"
 
 namespace storm {
 namespace property {
diff --git a/src/formula/abstract/BoundedEventually.h b/src/formula/abstract/BoundedEventually.h
index 420dbfff4..3b4bd8f34 100644
--- a/src/formula/abstract/BoundedEventually.h
+++ b/src/formula/abstract/BoundedEventually.h
@@ -12,7 +12,6 @@
 #include "src/formula/AbstractFormulaChecker.h"
 #include "boost/integer/integer_mask.hpp"
 #include <string>
-#include "src/modelchecker/ForwardDeclarations.h"
 
 namespace storm {
 
diff --git a/src/formula/abstract/BoundedNaryUntil.h b/src/formula/abstract/BoundedNaryUntil.h
index ccfe2ab17..08e640dbe 100644
--- a/src/formula/abstract/BoundedNaryUntil.h
+++ b/src/formula/abstract/BoundedNaryUntil.h
@@ -14,7 +14,6 @@
 #include <vector>
 #include <tuple>
 #include <sstream>
-#include "src/modelchecker/ForwardDeclarations.h"
 
 namespace storm {
 namespace property {
diff --git a/src/formula/abstract/BoundedUntil.h b/src/formula/abstract/BoundedUntil.h
index 33cc4f87a..9d7ea0ab1 100644
--- a/src/formula/abstract/BoundedUntil.h
+++ b/src/formula/abstract/BoundedUntil.h
@@ -11,7 +11,6 @@
 #include "src/formula/abstract/AbstractFormula.h"
 #include "boost/integer/integer_mask.hpp"
 #include <string>
-#include "src/modelchecker/ForwardDeclarations.h"
 
 namespace storm {
 namespace property {
diff --git a/src/formula/abstract/Eventually.h b/src/formula/abstract/Eventually.h
index aa706c311..fa6ca745f 100644
--- a/src/formula/abstract/Eventually.h
+++ b/src/formula/abstract/Eventually.h
@@ -9,7 +9,6 @@
 #define STORM_FORMULA_ABSTRACT_EVENTUALLY_H_
 
 #include "src/formula/abstract/AbstractFormula.h"
-#include "src/modelchecker/ForwardDeclarations.h"
 
 namespace storm {
 
diff --git a/src/formula/abstract/Globally.h b/src/formula/abstract/Globally.h
index 4e0ab0f22..b2b920714 100644
--- a/src/formula/abstract/Globally.h
+++ b/src/formula/abstract/Globally.h
@@ -10,7 +10,6 @@
 
 #include "src/formula/abstract/AbstractFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
-#include "src/modelchecker/ForwardDeclarations.h"
 
 namespace storm {
 
diff --git a/src/formula/abstract/Not.h b/src/formula/abstract/Not.h
index 6c92e7672..2c6e5f48d 100644
--- a/src/formula/abstract/Not.h
+++ b/src/formula/abstract/Not.h
@@ -10,7 +10,6 @@
 
 #include "src/formula/abstract/AbstractFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
-#include "src/modelchecker/ForwardDeclarations.h"
 
 namespace storm {
 
diff --git a/src/formula/abstract/PathBoundOperator.h b/src/formula/abstract/PathBoundOperator.h
index 34a6f0732..0a2a32777 100644
--- a/src/formula/abstract/PathBoundOperator.h
+++ b/src/formula/abstract/PathBoundOperator.h
@@ -15,7 +15,6 @@
 
 #include "src/formula/abstract/OptimizingOperator.h"
 
-#include "src/modelchecker/ForwardDeclarations.h"
 #include "src/utility/ConstTemplates.h"
 
 namespace storm {
diff --git a/src/formula/abstract/PathNoBoundOperator.h b/src/formula/abstract/PathNoBoundOperator.h
index 827b6cfa1..0ab6d29e7 100644
--- a/src/formula/abstract/PathNoBoundOperator.h
+++ b/src/formula/abstract/PathNoBoundOperator.h
@@ -12,7 +12,6 @@
 #include "src/formula/AbstractFormulaChecker.h"
 #include "src/formula/abstract/OptimizingOperator.h"
 
-#include "src/modelchecker/ForwardDeclarations.h"
 
 namespace storm {
 
diff --git a/src/formula/abstract/StateBoundOperator.h b/src/formula/abstract/StateBoundOperator.h
index c2f869b9e..a9615cfe7 100644
--- a/src/formula/abstract/StateBoundOperator.h
+++ b/src/formula/abstract/StateBoundOperator.h
@@ -12,7 +12,6 @@
 #include "src/formula/abstract/AbstractFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 #include "src/formula/ComparisonType.h"
-#include "src/modelchecker/AbstractModelChecker.h"
 #include "src/utility/ConstTemplates.h"
 
 namespace storm {
diff --git a/src/formula/abstract/StateNoBoundOperator.h b/src/formula/abstract/StateNoBoundOperator.h
index 9696f597d..2ad6aaaee 100644
--- a/src/formula/abstract/StateNoBoundOperator.h
+++ b/src/formula/abstract/StateNoBoundOperator.h
@@ -11,7 +11,6 @@
 #include "AbstractFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
 
-#include "src/modelchecker/ForwardDeclarations.h"
 
 namespace storm {
 namespace property {
diff --git a/src/modelchecker/csl/AbstractModelChecker.h b/src/modelchecker/csl/AbstractModelChecker.h
new file mode 100644
index 000000000..eed4aea0b
--- /dev/null
+++ b/src/modelchecker/csl/AbstractModelChecker.h
@@ -0,0 +1,287 @@
+/*
+ * AbstractModelChecker.h
+ *
+ *  Created on: 22.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef STORM_MODELCHECKER_CSL_ABSTRACTMODELCHECKER_H_
+#define STORM_MODELCHECKER_CSL_ABSTRACTMODELCHECKER_H_
+
+#include "src/exceptions/InvalidPropertyException.h"
+#include "src/formula/Csl.h"
+#include "src/storage/BitVector.h"
+#include "src/models/AbstractModel.h"
+
+#include "log4cplus/logger.h"
+#include "log4cplus/loggingmacros.h"
+
+#include <iostream>
+
+extern log4cplus::Logger logger;
+
+namespace storm {
+namespace modelchecker {
+namespace csl {
+
+/*!
+ * @brief
+ * (Abstract) interface for all model checker classes.
+ *
+ * This class provides basic functions that are common to all model checkers (i.e. subclasses). It mainly declares
+ * abstract methods that are implemented in the concrete subclasses, but also covers checking procedures that are common
+ * to all model checkers for state-based models.
+ */
+template<class Type>
+class AbstractModelChecker :
+	// A list of interfaces the model checker supports. Typically, for each of the interfaces, a check method needs to
+	// be implemented that performs the corresponding check.
+	public virtual storm::property::csl::IApModelChecker<Type>,
+	public virtual storm::property::csl::IAndModelChecker<Type>,
+	public virtual storm::property::csl::IOrModelChecker<Type>,
+	public virtual storm::property::csl::INotModelChecker<Type>,
+	public virtual storm::property::csl::IUntilModelChecker<Type>,
+	public virtual storm::property::csl::IEventuallyModelChecker<Type>,
+	public virtual storm::property::csl::IGloballyModelChecker<Type>,
+	public virtual storm::property::csl::INextModelChecker<Type>,
+	public virtual storm::property::csl::ITimeBoundedUntilModelChecker<Type>,
+	public virtual storm::property::csl::ITimeBoundedEventuallyModelChecker<Type>,
+	public virtual storm::property::csl::INoBoundOperatorModelChecker<Type>,
+	public virtual storm::property::csl::IProbabilisticBoundOperatorModelChecker<Type> {
+	
+public:
+	/*!
+	 * Constructs an AbstractModelChecker with the given model.
+	 */
+	explicit AbstractModelChecker(storm::models::AbstractModel<Type> const& model) : model(model) {
+		// Intentionally left empty.
+	}
+	/*!
+	 * Copy constructs an AbstractModelChecker from the given model checker. In particular, this means that the newly
+	 * constructed model checker will have the model of the given model checker as its associated model.
+	 */
+	explicit AbstractModelChecker(AbstractModelChecker<Type> const& modelchecker) : model(modelchecker.model) {
+		// Intentionally left empty.
+	}
+	
+	/*!
+	 * Virtual destructor. Needs to be virtual, because this class has virtual methods.
+	 */
+	virtual ~AbstractModelChecker() {
+		// Intentionally left empty.
+	}
+
+	/*!
+	 * Returns a pointer to the model checker object that is of the requested type as given by the template parameters.
+	 * @returns A pointer to the model checker object that is of the requested type as given by the template parameters.
+	 * If the model checker is not of the requested type, type casting will fail and result in an exception.
+	 */
+	template <template <class T> class Target>
+	const Target<Type>* as() const {
+		try {
+			const Target<Type>* target = dynamic_cast<const Target<Type>*>(this);
+			return target;
+		} catch (std::bad_cast& bc) {
+			LOG4CPLUS_ERROR(logger, "Bad cast: tried to cast " << typeid(*this).name() << " to " << typeid(Target<Type>).name() << ".");
+			throw bc;
+		}
+		return nullptr;
+	}
+
+	/*!
+	 * Retrieves the model associated with this model checker as a constant reference to an object of the type given
+	 * by the template parameter.
+	 *
+	 * @returns A constant reference of the specified type to the model associated with this model checker. If the model
+	 * is not of the requested type, type casting will fail and result in an exception.
+	 */
+	template <class Model>
+	Model const& getModel() const {
+		try {
+			Model const& target = dynamic_cast<Model const&>(this->model);
+			return target;
+		} catch (std::bad_cast& bc) {
+			LOG4CPLUS_ERROR(logger, "Bad cast: tried to cast " << typeid(this->model).name() << " to " << typeid(Model).name() << ".");
+			throw bc;
+		}
+	}
+
+	/*!
+	 * Checks the given abstract prctl formula on the model and prints the result (depending on the actual type of the formula)
+	 * for all initial states, i.e. states that carry the atomic proposition "init".
+	 *
+	 * @param formula The formula to be checked.
+	 */
+	void check(storm::property::csl::AbstractCslFormula<Type> const& formula) const {
+		if (dynamic_cast<storm::property::csl::AbstractStateFormula<Type> const*>(&formula) != nullptr) {
+			this->check(static_cast<storm::property::csl::AbstractStateFormula<Type> const&>(formula));
+		} else if (dynamic_cast<storm::property::csl::AbstractNoBoundOperator<Type> const*>(&formula) != nullptr) {
+			this->check(static_cast<storm::property::csl::AbstractNoBoundOperator<Type> const&>(formula));
+		}
+	}
+
+	/*!
+	 * Checks the given state formula on the model and prints the result (true/false) for all initial states, i.e.
+	 * states that carry the atomic proposition "init".
+	 *
+	 * @param stateFormula The formula to be checked.
+	 */
+	void check(storm::property::csl::AbstractStateFormula<Type> const& stateFormula) const {
+		std::cout << std::endl;
+		LOG4CPLUS_INFO(logger, "Model checking formula\t" << stateFormula.toString());
+		std::cout << "Model checking formula:\t" << stateFormula.toString() << std::endl;
+		storm::storage::BitVector* result = nullptr;
+		try {
+			result = stateFormula.check(*this);
+			LOG4CPLUS_INFO(logger, "Result for initial states:");
+			std::cout << "Result for initial states:" << std::endl;
+			for (auto initialState : model.getLabeledStates("init")) {
+				LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result->get(initialState) ? "satisfied" : "not satisfied"));
+				std::cout << "\t" << initialState << ": " << result->get(initialState) << std::endl;
+			}
+			delete result;
+		} catch (std::exception& e) {
+			std::cout << "Error during computation: " << e.what() << "Skipping property." << std::endl;
+			LOG4CPLUS_ERROR(logger, "Error during computation: " << e.what() << "Skipping property.");
+			if (result != nullptr) {
+				delete result;
+			}
+		}
+		std::cout << std::endl;
+		storm::utility::printSeparationLine(std::cout);
+	}
+
+	/*!
+	 * Checks the given formula (with no bound) on the model and prints the result (probability/rewards) for all
+	 * initial states, i.e. states that carry the atomic proposition "init".
+	 *
+	 * @param noBoundFormula The formula to be checked.
+	 */
+	void check(storm::property::csl::AbstractNoBoundOperator<Type> const& noBoundFormula) const {
+		std::cout << std::endl;
+		LOG4CPLUS_INFO(logger, "Model checking formula\t" << noBoundFormula.toString());
+		std::cout << "Model checking formula:\t" << noBoundFormula.toString() << std::endl;
+		std::vector<Type>* result = nullptr;
+		try {
+			result = this->checkNoBoundOperator(noBoundFormula);
+			LOG4CPLUS_INFO(logger, "Result for initial states:");
+			std::cout << "Result for initial states:" << std::endl;
+			for (auto initialState : model.getLabeledStates("init")) {
+				LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (*result)[initialState]);
+				std::cout << "\t" << initialState << ": " << (*result)[initialState] << std::endl;
+			}
+			delete result;
+		} catch (std::exception& e) {
+			std::cout << "Error during computation: " << e.what() << " Skipping property." << std::endl;
+			if (result != nullptr) {
+				delete result;
+			}
+		}
+		std::cout << std::endl;
+		storm::utility::printSeparationLine(std::cout);
+	}
+
+	/*!
+	 * Checks the given formula consisting of a single atomic proposition.
+	 *
+	 * @param formula The formula to be checked.
+	 * @returns The set of states satisfying the formula represented by a bit vector.
+	 */
+	storm::storage::BitVector* checkAp(storm::property::csl::Ap<Type> const& formula) const {
+		if (formula.getAp() == "true") {
+			return new storm::storage::BitVector(model.getNumberOfStates(), true);
+		} else if (formula.getAp() == "false") {
+			return new storm::storage::BitVector(model.getNumberOfStates());
+		}
+
+		if (!model.hasAtomicProposition(formula.getAp())) {
+			LOG4CPLUS_ERROR(logger, "Atomic proposition '" << formula.getAp() << "' is invalid.");
+			throw storm::exceptions::InvalidPropertyException() << "Atomic proposition '" << formula.getAp() << "' is invalid.";
+		}
+
+		return new storm::storage::BitVector(model.getLabeledStates(formula.getAp()));
+	}
+
+	/*!
+	 * Checks the given formula that is a logical "and" of two formulae.
+	 *
+	 * @param formula The formula to be checked.
+	 * @returns The set of states satisfying the formula represented by a bit vector.
+	 */
+	storm::storage::BitVector* checkAnd(storm::property::csl::And<Type> const& formula) const {
+		storm::storage::BitVector* result = formula.getLeft().check(*this);
+		storm::storage::BitVector* right = formula.getRight().check(*this);
+		(*result) &= (*right);
+		delete right;
+		return result;
+	}
+
+	/*!
+	 * Checks the given formula that is a logical "or" of two formulae.
+	 *
+	 * @param formula The formula to check.
+	 * @returns The set of states satisfying the formula represented by a bit vector.
+	 */
+	virtual storm::storage::BitVector* checkOr(storm::property::csl::Or<Type> const& formula) const {
+		storm::storage::BitVector* result = formula.getLeft().check(*this);
+		storm::storage::BitVector* right = formula.getRight().check(*this);
+		(*result) |= (*right);
+		delete right;
+		return result;
+	}
+
+	/*!
+	 * Checks the given formula that is a logical "not" of a sub-formula.
+	 *
+	 * @param formula The formula to check.
+	 * @returns The set of states satisfying the formula represented by a bit vector.
+	 */
+	storm::storage::BitVector* checkNot(const storm::property::csl::Not<Type>& formula) const {
+		storm::storage::BitVector* result = formula.getChild().check(*this);
+		result->complement();
+		return result;
+	}
+
+
+	/*!
+	 * Checks the given formula that is a P operator over a path formula featuring a value bound.
+	 *
+	 * @param formula The formula to check.
+	 * @returns The set of states satisfying the formula represented by a bit vector.
+	 */
+	storm::storage::BitVector* checkProbabilisticBoundOperator(storm::property::csl::ProbabilisticBoundOperator<Type> const& formula) const {
+		// First, we need to compute the probability for satisfying the path formula for each state.
+		std::vector<Type>* quantitativeResult = formula.getPathFormula().check(*this, false);
+
+		// Create resulting bit vector that will hold the yes/no-answer for every state.
+		storm::storage::BitVector* result = new storm::storage::BitVector(quantitativeResult->size());
+
+		// Now, we can compute which states meet the bound specified in this operator and set the
+		// corresponding bits to true in the resulting vector.
+		for (uint_fast64_t i = 0; i < quantitativeResult->size(); ++i) {
+			if (formula.meetsBound((*quantitativeResult)[i])) {
+				result->set(i, true);
+			}
+		}
+
+		// Delete the probabilities computed for the states and return result.
+		delete quantitativeResult;
+		return result;
+	}
+
+private:
+
+	/*!
+	 * A constant reference to the model associated with this model checker.
+	 *
+	 * @note that we do not own this object, but merely have a constant reference to  it. That means that using the
+	 * model checker object is unsafe after the object has been destroyed.
+	 */
+	storm::models::AbstractModel<Type> const& model;
+};
+
+} // namespace csl
+} // namespace modelchecker
+} // namespace storm
+
+#endif /* STORM_MODELCHECKER_CSL_DTMCPRCTLMODELCHECKER_H_ */
diff --git a/src/modelchecker/ForwardDeclarations.h b/src/modelchecker/csl/ForwardDeclarations.h
similarity index 94%
rename from src/modelchecker/ForwardDeclarations.h
rename to src/modelchecker/csl/ForwardDeclarations.h
index 014d5eec0..45d6aba8a 100644
--- a/src/modelchecker/ForwardDeclarations.h
+++ b/src/modelchecker/csl/ForwardDeclarations.h
@@ -12,10 +12,12 @@
 // the callback methods (i.e., the check methods).
 namespace storm {
 namespace modelchecker {
+namespace csl {
 
 template <class Type>
 class AbstractModelChecker;
 
+} //namespace csl
 } //namespace modelchecker
 } //namespace storm
 
diff --git a/src/modelchecker/ltl/AbstractModelChecker.h b/src/modelchecker/ltl/AbstractModelChecker.h
new file mode 100644
index 000000000..14f42553a
--- /dev/null
+++ b/src/modelchecker/ltl/AbstractModelChecker.h
@@ -0,0 +1,193 @@
+/*
+ * AbstractModelChecker.h
+ *
+ *  Created on: 22.10.2012
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef STORM_MODELCHECKER_LTL_ABSTRACTMODELCHECKER_H_
+#define STORM_MODELCHECKER_LTL_ABSTRACTMODELCHECKER_H_
+
+#include "src/exceptions/InvalidPropertyException.h"
+#include "src/formula/Ltl.h"
+#include "src/storage/BitVector.h"
+#include "src/models/AbstractModel.h"
+
+#include "log4cplus/logger.h"
+#include "log4cplus/loggingmacros.h"
+
+#include <iostream>
+
+extern log4cplus::Logger logger;
+
+namespace storm {
+namespace modelchecker {
+namespace ltl {
+
+/*!
+ * @brief
+ * (Abstract) interface for all model checker classes.
+ *
+ * This class provides basic functions that are common to all model checkers (i.e. subclasses). It mainly declares
+ * abstract methods that are implemented in the concrete subclasses, but also covers checking procedures that are common
+ * to all model checkers for state-based models.
+ */
+template<class Type>
+class AbstractModelChecker :
+	// A list of interfaces the model checker supports. Typically, for each of the interfaces, a check method needs to
+	// be implemented that performs the corresponding check.
+	public virtual storm::property::ltl::IApModelChecker<Type>,
+	public virtual storm::property::ltl::IAndModelChecker<Type>,
+	public virtual storm::property::ltl::IOrModelChecker<Type>,
+	public virtual storm::property::ltl::INotModelChecker<Type>,
+	public virtual storm::property::ltl::IUntilModelChecker<Type>,
+	public virtual storm::property::ltl::IEventuallyModelChecker<Type>,
+	public virtual storm::property::ltl::IGloballyModelChecker<Type>,
+	public virtual storm::property::ltl::INextModelChecker<Type>,
+	public virtual storm::property::ltl::IBoundedUntilModelChecker<Type>,
+	public virtual storm::property::ltl::IBoundedEventuallyModelChecker<Type> {
+	
+public:
+	/*!
+	 * Constructs an AbstractModelChecker with the given model.
+	 */
+	explicit AbstractModelChecker(storm::models::AbstractModel<Type> const& model) : model(model) {
+		// Intentionally left empty.
+	}
+	/*!
+	 * Copy constructs an AbstractModelChecker from the given model checker. In particular, this means that the newly
+	 * constructed model checker will have the model of the given model checker as its associated model.
+	 */
+	explicit AbstractModelChecker(AbstractModelChecker<Type> const& modelchecker) : model(modelchecker.model) {
+		// Intentionally left empty.
+	}
+	
+	/*!
+	 * Virtual destructor. Needs to be virtual, because this class has virtual methods.
+	 */
+	virtual ~AbstractModelChecker() {
+		// Intentionally left empty.
+	}
+
+	/*!
+	 * Returns a pointer to the model checker object that is of the requested type as given by the template parameters.
+	 * @returns A pointer to the model checker object that is of the requested type as given by the template parameters.
+	 * If the model checker is not of the requested type, type casting will fail and result in an exception.
+	 */
+	template <template <class T> class Target>
+	const Target<Type>* as() const {
+		try {
+			const Target<Type>* target = dynamic_cast<const Target<Type>*>(this);
+			return target;
+		} catch (std::bad_cast& bc) {
+			LOG4CPLUS_ERROR(logger, "Bad cast: tried to cast " << typeid(*this).name() << " to " << typeid(Target<Type>).name() << ".");
+			throw bc;
+		}
+		return nullptr;
+	}
+
+	/*!
+	 * Retrieves the model associated with this model checker as a constant reference to an object of the type given
+	 * by the template parameter.
+	 *
+	 * @returns A constant reference of the specified type to the model associated with this model checker. If the model
+	 * is not of the requested type, type casting will fail and result in an exception.
+	 */
+	template <class Model>
+	Model const& getModel() const {
+		try {
+			Model const& target = dynamic_cast<Model const&>(this->model);
+			return target;
+		} catch (std::bad_cast& bc) {
+			LOG4CPLUS_ERROR(logger, "Bad cast: tried to cast " << typeid(this->model).name() << " to " << typeid(Model).name() << ".");
+			throw bc;
+		}
+	}
+
+	/*!
+	 * Checks the given state formula on the model and prints the result (true/false) for all initial states, i.e.
+	 * states that carry the atomic proposition "init".
+	 *
+	 * @param stateFormula The formula to be checked.
+	 */
+	void check(storm::property::ltl::AbstractLtlFormula<Type> const& ltlFormula) const {
+		std::cout << std::endl;
+		LOG4CPLUS_INFO(logger, "Model checking formula\t" << ltlFormula.toString());
+		std::cout << "Model checking formula:\t" << ltlFormula.toString() << std::endl;
+		storm::storage::BitVector* result = nullptr;
+		try {
+			result = ltlFormula.check(*this);
+			LOG4CPLUS_INFO(logger, "Result for initial states:");
+			std::cout << "Result for initial states:" << std::endl;
+			for (auto initialState : model.getLabeledStates("init")) {
+				LOG4CPLUS_INFO(logger, "\t" << initialState << ": " << (result->get(initialState) ? "satisfied" : "not satisfied"));
+				std::cout << "\t" << initialState << ": " << result->get(initialState) << std::endl;
+			}
+			delete result;
+		} catch (std::exception& e) {
+			std::cout << "Error during computation: " << e.what() << "Skipping property." << std::endl;
+			LOG4CPLUS_ERROR(logger, "Error during computation: " << e.what() << "Skipping property.");
+			if (result != nullptr) {
+				delete result;
+			}
+		}
+		std::cout << std::endl;
+		storm::utility::printSeparationLine(std::cout);
+	}
+
+	/*!
+	 * Checks the given formula consisting of a single atomic proposition.
+	 *
+	 * @param formula The formula to be checked.
+	 * @returns The set of states satisfying the formula represented by a bit vector.
+	 */
+	virtual std::vector<Type>* checkAp(storm::property::ltl::Ap<Type> const& formula) const {
+		return nullptr;
+	}
+
+	/*!
+	 * Checks the given formula that is a logical "and" of two formulae.
+	 *
+	 * @param formula The formula to be checked.
+	 * @returns The set of states satisfying the formula represented by a bit vector.
+	 */
+	virtual std::vector<Type>* checkAnd(storm::property::ltl::And<Type> const& formula) const {
+		return nullptr;
+	}
+
+	/*!
+	 * Checks the given formula that is a logical "or" of two formulae.
+	 *
+	 * @param formula The formula to check.
+	 * @returns The set of states satisfying the formula represented by a bit vector.
+	 */
+	virtual std::vector<Type>* checkOr(storm::property::ltl::Or<Type> const& formula) const {
+		return nullptr;
+	}
+
+	/*!
+	 * Checks the given formula that is a logical "not" of a sub-formula.
+	 *
+	 * @param formula The formula to check.
+	 * @returns The set of states satisfying the formula represented by a bit vector.
+	 */
+	virtual std::vector<Type>* checkNot(const storm::property::ltl::Not<Type>& formula) const {
+		return nullptr;
+	}
+
+private:
+
+	/*!
+	 * A constant reference to the model associated with this model checker.
+	 *
+	 * @note that we do not own this object, but merely have a constant reference to  it. That means that using the
+	 * model checker object is unsafe after the object has been destroyed.
+	 */
+	storm::models::AbstractModel<Type> const& model;
+};
+
+} // namespace ltl
+} // namespace modelchecker
+} // namespace storm
+
+#endif /* STORM_MODELCHECKER_LTL_ABSTRACTMODELCHECKER_H_ */
diff --git a/src/modelchecker/ltl/ForwardDeclarations.h b/src/modelchecker/ltl/ForwardDeclarations.h
new file mode 100644
index 000000000..e8591fd46
--- /dev/null
+++ b/src/modelchecker/ltl/ForwardDeclarations.h
@@ -0,0 +1,24 @@
+/*
+ * ForwardDeclarations.h
+ *
+ *  Created on: 14.01.2013
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef STORM_MODELCHECKER_LTL_FORWARDDECLARATIONS_H_
+#define STORM_MODELCHECKER_LTL_FORWARDDECLARATIONS_H_
+
+// Forward declare the abstract model checker. This is used by the formula classes that need this declaration for
+// the callback methods (i.e., the check methods).
+namespace storm {
+namespace modelchecker {
+namespace ltl {
+
+template <class Type>
+class AbstractModelChecker;
+
+} //namespace ltl
+} //namespace modelchecker
+} //namespace storm
+
+#endif /* STORM_MODELCHECKER_LTL_FORWARDDECLARATIONS_H_ */
diff --git a/src/modelchecker/AbstractModelChecker.h b/src/modelchecker/prctl/AbstractModelChecker.h
similarity index 97%
rename from src/modelchecker/AbstractModelChecker.h
rename to src/modelchecker/prctl/AbstractModelChecker.h
index 2de2bfb28..080d6198b 100644
--- a/src/modelchecker/AbstractModelChecker.h
+++ b/src/modelchecker/prctl/AbstractModelChecker.h
@@ -5,15 +5,8 @@
  *      Author: Thomas Heinemann
  */
 
-#ifndef STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_
-#define STORM_MODELCHECKER_ABSTRACTMODELCHECKER_H_
-
-// Forward declaration of abstract model checker class needed by the formula classes.
-namespace storm {
-namespace modelchecker {
-	template <class Type> class AbstractModelChecker;
-}
-}
+#ifndef STORM_MODELCHECKER_PRCTL_ABSTRACTMODELCHECKER_H_
+#define STORM_MODELCHECKER_PRCTL_ABSTRACTMODELCHECKER_H_
 
 #include "src/exceptions/InvalidPropertyException.h"
 #include "src/formula/Prctl.h"
@@ -29,6 +22,7 @@ extern log4cplus::Logger logger;
 
 namespace storm {
 namespace modelchecker {
+namespace prctl {
 
 /*!
  * @brief
@@ -316,7 +310,8 @@ private:
 	storm::models::AbstractModel<Type> const& model;
 };
 
+} // namespace prctl
 } // namespace modelchecker
 } // namespace storm
 
-#endif /* STORM_MODELCHECKER_DTMCPRCTLMODELCHECKER_H_ */
+#endif /* STORM_MODELCHECKER_PRCTL_DTMCPRCTLMODELCHECKER_H_ */
diff --git a/src/modelchecker/EigenDtmcPrctlModelChecker.h b/src/modelchecker/prctl/EigenDtmcPrctlModelChecker.h
similarity index 94%
rename from src/modelchecker/EigenDtmcPrctlModelChecker.h
rename to src/modelchecker/prctl/EigenDtmcPrctlModelChecker.h
index 7c5b06ad0..e9dfe74d3 100644
--- a/src/modelchecker/EigenDtmcPrctlModelChecker.h
+++ b/src/modelchecker/prctl/EigenDtmcPrctlModelChecker.h
@@ -5,13 +5,13 @@
  *      Author: 
  */
 
-#ifndef STORM_MODELCHECKER_EIGENDTMCPRCTLMODELCHECKER_H_
-#define STORM_MODELCHECKER_EIGENDTMCPRCTLMODELCHECKER_H_
+#ifndef STORM_MODELCHECKER_PRCTL_EIGENDTMCPRCTLMODELCHECKER_H_
+#define STORM_MODELCHECKER_PRCTL_EIGENDTMCPRCTLMODELCHECKER_H_
 
 #include "src/utility/Vector.h"
 
 #include "src/models/Dtmc.h"
-#include "src/modelchecker/SparseDtmcPrctlModelChecker.h"
+#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
 #include "src/utility/GraphAnalyzer.h"
 #include "src/utility/ConstTemplates.h"
 #include "src/exceptions/NoConvergenceException.h"
@@ -30,6 +30,7 @@ extern log4cplus::Logger logger;
 
 namespace storm {
 namespace modelchecker {
+namespace prctl {
 
 /*
  * A model checking engine that makes use of the eigen backend.
@@ -135,7 +136,8 @@ private:
 	}
 };
 
+} //namespace prctl
 } //namespace modelchecker
 } //namespace storm
 
-#endif /* STORM_MODELCHECKER_EIGENDTMCPRCTLMODELCHECKER_H_ */
+#endif /* STORM_MODELCHECKER_PRCTL_EIGENDTMCPRCTLMODELCHECKER_H_ */
diff --git a/src/modelchecker/prctl/ForwardDeclarations.h b/src/modelchecker/prctl/ForwardDeclarations.h
new file mode 100644
index 000000000..c12ca6adb
--- /dev/null
+++ b/src/modelchecker/prctl/ForwardDeclarations.h
@@ -0,0 +1,24 @@
+/*
+ * ForwardDeclarations.h
+ *
+ *  Created on: 14.01.2013
+ *      Author: Thomas Heinemann
+ */
+
+#ifndef STORM_MODELCHECKER_PRCTL_FORWARDDECLARATIONS_H_
+#define STORM_MODELCHECKER_PRCTL_FORWARDDECLARATIONS_H_
+
+// Forward declare the abstract model checker. This is used by the formula classes that need this declaration for
+// the callback methods (i.e., the check methods).
+namespace storm {
+namespace modelchecker {
+namespace prctl {
+
+template <class Type>
+class AbstractModelChecker;
+
+} //namespace prctl
+} //namespace modelchecker
+} //namespace storm
+
+#endif /* STORM_MODELCHECKER_PRCTL_FORWARDDECLARATIONS_H_ */
diff --git a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h b/src/modelchecker/prctl/GmmxxDtmcPrctlModelChecker.h
similarity index 96%
rename from src/modelchecker/GmmxxDtmcPrctlModelChecker.h
rename to src/modelchecker/prctl/GmmxxDtmcPrctlModelChecker.h
index e7b24188e..4b4c31c82 100644
--- a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h
+++ b/src/modelchecker/prctl/GmmxxDtmcPrctlModelChecker.h
@@ -5,10 +5,10 @@
  *      Author: Christian Dehnert
  */
 
-#ifndef STORM_MODELCHECKER_GMMXXDTMCPRCTLMODELCHECKER_H_
-#define STORM_MODELCHECKER_GMMXXDTMCPRCTLMODELCHECKER_H_
+#ifndef STORM_MODELCHECKER_PRCTL_GMMXXDTMCPRCTLMODELCHECKER_H_
+#define STORM_MODELCHECKER_PRCTL_GMMXXDTMCPRCTLMODELCHECKER_H_
 
-#include "src/modelchecker/SparseDtmcPrctlModelChecker.h"
+#include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
 #include "src/adapters/GmmxxAdapter.h"
 #include "src/storage/JacobiDecomposition.h"
 #include "src/utility/ConstTemplates.h"
@@ -21,6 +21,7 @@
 
 namespace storm {
 namespace modelchecker {
+namespace prctl {
 
 /*
  * An implementation of the SparseDtmcPrctlModelChecker interface that uses gmm++ as the solving backend.
@@ -42,7 +43,7 @@ public:
 	 * Copy constructs a GmmxxDtmcPrctlModelChecker from the given model checker. In particular, this means that the newly
 	 * constructed model checker will have the model of the given model checker as its associated model.
 	 */
-	explicit GmmxxDtmcPrctlModelChecker(storm::modelchecker::GmmxxDtmcPrctlModelChecker<Type> const& modelchecker) : SparseDtmcPrctlModelChecker<Type>(modelchecker) {
+	explicit GmmxxDtmcPrctlModelChecker(storm::modelchecker::prctl::GmmxxDtmcPrctlModelChecker<Type> const& modelchecker) : SparseDtmcPrctlModelChecker<Type>(modelchecker) {
 		// Intentionally left empty.
 	}
 
@@ -302,7 +303,8 @@ private:
 	}
 };
 
+} // namespace prctl
 } // namespace modelchecker
 } // namespace storm
 
-#endif /* STORM_MODELCHECKER_GMMXXDTMCPRCTLMODELCHECKER_H_ */
+#endif /* STORM_MODELCHECKER_PRCTL_GMMXXDTMCPRCTLMODELCHECKER_H_ */
diff --git a/src/modelchecker/GmmxxMdpPrctlModelChecker.h b/src/modelchecker/prctl/GmmxxMdpPrctlModelChecker.h
similarity index 92%
rename from src/modelchecker/GmmxxMdpPrctlModelChecker.h
rename to src/modelchecker/prctl/GmmxxMdpPrctlModelChecker.h
index 48c4c6304..a1a4e3e1a 100644
--- a/src/modelchecker/GmmxxMdpPrctlModelChecker.h
+++ b/src/modelchecker/prctl/GmmxxMdpPrctlModelChecker.h
@@ -5,10 +5,10 @@
  *      Author: Christian Dehnert
  */
 
-#ifndef STORM_MODELCHECKER_GMMXXMDPPRCTLMODELCHECKER_H_
-#define STORM_MODELCHECKER_GMMXXMDPPRCTLMODELCHECKER_H_
+#ifndef STORM_MODELCHECKER_PRCTL_GMMXXMDPPRCTLMODELCHECKER_H_
+#define STORM_MODELCHECKER_PRCTL_GMMXXMDPPRCTLMODELCHECKER_H_
 
-#include "src/modelchecker/SparseMdpPrctlModelChecker.h"
+#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
 #include "src/adapters/GmmxxAdapter.h"
 
 #include "gmm/gmm_matrix.h"
@@ -18,6 +18,7 @@
 
 namespace storm {
 namespace modelchecker {
+namespace prctl {
 
 /*
  * An implementation of the SparseMdpPrctlModelChecker interface that uses gmm++ as the solving backend.
@@ -39,7 +40,7 @@ public:
 	 * Copy constructs a GmmxxDtmcPrctlModelChecker from the given model checker. In particular, this means that the newly
 	 * constructed model checker will have the model of the given model checker as its associated model.
 	 */
-	explicit GmmxxMdpPrctlModelChecker(storm::modelchecker::GmmxxMdpPrctlModelChecker<Type> const& modelchecker) : SparseMdpPrctlModelChecker<Type>(modelchecker) {
+	explicit GmmxxMdpPrctlModelChecker(storm::modelchecker::prctl::GmmxxMdpPrctlModelChecker<Type> const& modelchecker) : SparseMdpPrctlModelChecker<Type>(modelchecker) {
 		// Intentionally left empty.
 	}
 
@@ -156,7 +157,8 @@ private:
 	}
 };
 
+} //namespace prctl
 } //namespace modelchecker
 } //namespace storm
 
-#endif /* STORM_MODELCHECKER_GMMXXMDPPRCTLMODELCHECKER_H_ */
+#endif /* STORM_MODELCHECKER_PRCTL_GMMXXMDPPRCTLMODELCHECKER_H_ */
diff --git a/src/modelchecker/SparseDtmcPrctlModelChecker.h b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
similarity index 98%
rename from src/modelchecker/SparseDtmcPrctlModelChecker.h
rename to src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
index 6cbdd5aa3..6f0becc01 100644
--- a/src/modelchecker/SparseDtmcPrctlModelChecker.h
+++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h
@@ -5,10 +5,10 @@
  *      Author: Thomas Heinemann
  */
 
-#ifndef STORM_MODELCHECKER_SPARSEDTMCPRCTLMODELCHECKER_H_
-#define STORM_MODELCHECKER_SPARSEDTMCPRCTLMODELCHECKER_H_
+#ifndef STORM_MODELCHECKER_PRCTL_SPARSEDTMCPRCTLMODELCHECKER_H_
+#define STORM_MODELCHECKER_PRCTL_SPARSEDTMCPRCTLMODELCHECKER_H_
 
-#include "src/modelchecker/AbstractModelChecker.h"
+#include "src/modelchecker/prctl/AbstractModelChecker.h"
 #include "src/models/Dtmc.h"
 #include "src/utility/Vector.h"
 #include "src/utility/GraphAnalyzer.h"
@@ -17,6 +17,7 @@
 
 namespace storm {
 namespace modelchecker {
+namespace prctl {
 
 /*!
  * @brief
@@ -39,7 +40,7 @@ public:
 	 * Copy constructs a SparseDtmcPrctlModelChecker from the given model checker. In particular, this means that the newly
 	 * constructed model checker will have the model of the given model checker as its associated model.
 	 */
-	explicit SparseDtmcPrctlModelChecker(storm::modelchecker::SparseDtmcPrctlModelChecker<Type> const& modelChecker) : AbstractModelChecker<Type>(modelChecker) {
+	explicit SparseDtmcPrctlModelChecker(storm::modelchecker::prctl::SparseDtmcPrctlModelChecker<Type> const& modelChecker) : AbstractModelChecker<Type>(modelChecker) {
 		// Intentionally left empty.
 	}
 
@@ -448,7 +449,8 @@ private:
 	virtual void solveEquationSystem(storm::storage::SparseMatrix<Type> const& A, std::vector<Type>& x, std::vector<Type> const& b) const = 0;
 };
 
+} // namespace prctl
 } // namespace modelchecker
 } // namespace storm
 
-#endif /* STORM_MODELCHECKER_SPARSEDTMCPRCTLMODELCHECKER_H_ */
+#endif /* STORM_MODELCHECKER_PRCTL_SPARSEDTMCPRCTLMODELCHECKER_H_ */
diff --git a/src/modelchecker/SparseMdpPrctlModelChecker.h b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
similarity index 98%
rename from src/modelchecker/SparseMdpPrctlModelChecker.h
rename to src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
index e31212e36..11a602a75 100644
--- a/src/modelchecker/SparseMdpPrctlModelChecker.h
+++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.h
@@ -5,10 +5,10 @@
  *      Author: Christian Dehnert
  */
 
-#ifndef STORM_MODELCHECKER_SPARSEMDPPRCTLMODELCHECKER_H_
-#define STORM_MODELCHECKER_SPARSEMDPPRCTLMODELCHECKER_H_
+#ifndef STORM_MODELCHECKER_PRCTL_SPARSEMDPPRCTLMODELCHECKER_H_
+#define STORM_MODELCHECKER_PRCTL_SPARSEMDPPRCTLMODELCHECKER_H_
 
-#include "src/modelchecker/AbstractModelChecker.h"
+#include "src/modelchecker/prctl/AbstractModelChecker.h"
 #include "src/models/Mdp.h"
 #include "src/utility/Vector.h"
 #include "src/utility/GraphAnalyzer.h"
@@ -18,6 +18,7 @@
 
 namespace storm {
 namespace modelchecker {
+namespace prctl {
 
 /*!
  * @brief
@@ -40,7 +41,7 @@ public:
 	 * Copy constructs a SparseMdpPrctlModelChecker from the given model checker. In particular, this means that the newly
 	 * constructed model checker will have the model of the given model checker as its associated model.
 	 */
-	explicit SparseMdpPrctlModelChecker(storm::modelchecker::SparseMdpPrctlModelChecker<Type> const& modelchecker)
+	explicit SparseMdpPrctlModelChecker(storm::modelchecker::prctl::SparseMdpPrctlModelChecker<Type> const& modelchecker)
 		: AbstractModelChecker<Type>(modelchecker),  minimumOperatorStack() {
 		// Intentionally left empty.
 	}
@@ -580,7 +581,8 @@ private:
 	}
 };
 
+} // namespace prctl
 } // namespace modelchecker
 } // namespace storm
 
-#endif /* STORM_MODELCHECKER_SPARSEMDPPRCTLMODELCHECKER_H_ */
+#endif /* STORM_MODELCHECKER_PRCTL_SPARSEMDPPRCTLMODELCHECKER_H_ */
diff --git a/src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h b/src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h
similarity index 94%
rename from src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h
rename to src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h
index 248749624..45c9a9952 100644
--- a/src/modelchecker/TopologicalValueIterationMdpPrctlModelChecker.h
+++ b/src/modelchecker/prctl/TopologicalValueIterationMdpPrctlModelChecker.h
@@ -5,15 +5,16 @@
  *      Author: Christian Dehnert
  */
 
-#ifndef STORM_MODELCHECKER_TOPOLOGICALVALUEITERATIONSMDPPRCTLMODELCHECKER_H_
-#define STORM_MODELCHECKER_TOPOLOGICALVALUEITERATIONSMDPPRCTLMODELCHECKER_H_
+#ifndef STORM_MODELCHECKER_PRCTL_TOPOLOGICALVALUEITERATIONSMDPPRCTLMODELCHECKER_H_
+#define STORM_MODELCHECKER_PRCTL_TOPOLOGICALVALUEITERATIONSMDPPRCTLMODELCHECKER_H_
 
-#include "src/modelchecker/SparseMdpPrctlModelChecker.h"
+#include "src/modelchecker/prctl/SparseMdpPrctlModelChecker.h"
 #include "src/exceptions/InvalidPropertyException.h"
 #include <cmath>
 
 namespace storm {
 namespace modelchecker {
+namespace prctl {
 
 /*
  * An implementation of the SparseMdpPrctlModelChecker interface that uses topoligical value iteration for solving
@@ -143,7 +144,8 @@ private:
 	}
 };
 
+} // namespace prctl
 } // namespace modelchecker
 } // namespace storm
 
-#endif /* STORM_MODELCHECKER_TOPOLOGICALVALUEITERATIONSMDPPRCTLMODELCHECKER_H_ */
+#endif /* STORM_MODELCHECKER_PRCTL_TOPOLOGICALVALUEITERATIONSMDPPRCTLMODELCHECKER_H_ */
diff --git a/src/parser/LtlFileParser.cpp b/src/parser/LtlFileParser.cpp
new file mode 100644
index 000000000..e50e5411c
--- /dev/null
+++ b/src/parser/LtlFileParser.cpp
@@ -0,0 +1,49 @@
+/*
+ * LtlFileParser.cpp
+ *
+ *  Created on: 13.05.2013
+ *      Author: thomas
+ */
+
+#include "LtlFileParser.h"
+#include "LtlParser.h"
+
+namespace storm {
+namespace parser {
+
+LtlFileParser::LtlFileParser() {
+	// TODO Auto-generated constructor stub
+
+}
+
+LtlFileParser::~LtlFileParser() {
+	// TODO Auto-generated destructor stub
+}
+
+std::list<storm::property::ltl::AbstractLtlFormula<double>*> LtlFileParser::parseFormulas(std::string filename) {
+	// Open file
+	std::ifstream inputFileStream(filename, std::ios::in);
+
+	if (!inputFileStream.is_open()) {
+		std::string message = "Error while opening file ";
+		throw storm::exceptions::FileIoException() << message << filename;
+	}
+
+	std::list<storm::property::ltl::AbstractLtlFormula<double>*> result;
+
+	while(!inputFileStream.eof()) {
+		std::string line;
+		//The while loop reads the input file line by line
+		while (std::getline(inputFileStream, line)) {
+			LtlParser parser(line);
+			result.push_back(parser.getFormula());
+		}
+	}
+
+	return result;
+}
+
+} //namespace parser
+} //namespace storm
+
+
diff --git a/src/parser/LtlFileParser.h b/src/parser/LtlFileParser.h
new file mode 100644
index 000000000..ff8162df4
--- /dev/null
+++ b/src/parser/LtlFileParser.h
@@ -0,0 +1,42 @@
+/*
+ * LtlFileParser.h
+ *
+ *  Created on: 13.05.2013
+ *      Author: Thonas Heinemann
+ */
+
+#ifndef LTLFILEPARSER_H_
+#define LTLFILEPARSER_H_
+
+#include "formula/Ltl.h"
+
+#include <list>
+
+namespace storm {
+namespace parser {
+
+class LtlFileParser {
+public:
+	/*!
+	 * Constructor
+	 */
+	LtlFileParser();
+
+	/*!
+	 * Destructor
+	 */
+	~LtlFileParser();
+
+	/*!
+	 * Parses each line of a given file as prctl formula and returns a list containing the results of the parsing.
+	 *
+	 * @param filename
+	 * @return The list of parsed formulas
+	 */
+	std::list<storm::property::ltl::AbstractLtlFormula<double>*> parseFormulas(std::string filename);
+};
+
+} //namespace parser
+} //namespace storm
+
+#endif /* LTLFILEPARSER_H_ */
diff --git a/src/parser/PrctlFileParser.cpp b/src/parser/PrctlFileParser.cpp
index ed5f15a2b..29ee31349 100644
--- a/src/parser/PrctlFileParser.cpp
+++ b/src/parser/PrctlFileParser.cpp
@@ -9,9 +9,6 @@
 
 #include "PrctlFileParser.h"
 #include "PrctlParser.h"
-#include "modelchecker/EigenDtmcPrctlModelChecker.h"
-#include "modelchecker/GmmxxDtmcPrctlModelChecker.h"
-#include "modelchecker/GmmxxMdpPrctlModelChecker.h"
 
 namespace storm {
 namespace parser {
diff --git a/src/parser/PrctlFileParser.h b/src/parser/PrctlFileParser.h
index ee0987cfe..0ddb7fc4f 100644
--- a/src/parser/PrctlFileParser.h
+++ b/src/parser/PrctlFileParser.h
@@ -34,7 +34,7 @@ public:
 	 * At this time, empty
 	 *
 	 */
-	virtual ~PrctlFileParser();
+	~PrctlFileParser();
 
 	/*!
 	 * Parses each line of a given file as prctl formula and returns a list containing the results of the parsing.
diff --git a/src/parser/PrctlParser.cpp b/src/parser/PrctlParser.cpp
index c79485dc0..d98ae7a20 100644
--- a/src/parser/PrctlParser.cpp
+++ b/src/parser/PrctlParser.cpp
@@ -35,7 +35,7 @@ namespace parser {
 template<typename Iterator, typename Skipper>
 struct PrctlParser::PrctlGrammar : qi::grammar<Iterator, storm::property::prctl::AbstractPrctlFormula<double>*(), Skipper > {
 	PrctlGrammar() : PrctlGrammar::base_type(start) {
-		freeIdentifierName = qi::lexeme[+(qi::alpha | qi::char_('_'))];
+		freeIdentifierName = qi::lexeme[qi::alpha >> *(qi::alnum | qi::char_('_'))];
 
 		//This block defines rules for parsing state formulas
 		stateFormula %= orFormula;
diff --git a/src/storm.cpp b/src/storm.cpp
index f02783319..51f15519d 100644
--- a/src/storm.cpp
+++ b/src/storm.cpp
@@ -22,9 +22,9 @@
 #include "src/models/Dtmc.h"
 #include "src/storage/SparseMatrix.h"
 #include "src/models/AtomicPropositionsLabeling.h"
-#include "src/modelchecker/EigenDtmcPrctlModelChecker.h"
-#include "src/modelchecker/GmmxxDtmcPrctlModelChecker.h"
-#include "src/modelchecker/GmmxxMdpPrctlModelChecker.h"
+#include "src/modelchecker/prctl/EigenDtmcPrctlModelChecker.h"
+#include "src/modelchecker/prctl/GmmxxDtmcPrctlModelChecker.h"
+#include "src/modelchecker/prctl/GmmxxMdpPrctlModelChecker.h"
 #include "src/parser/AutoParser.h"
 #include "src/parser/PrctlParser.h"
 #include "src/utility/Settings.h"
@@ -32,6 +32,7 @@
 #include "src/formula/Prctl.h"
 
 #include "src/parser/PrctlFileParser.h"
+#include "src/parser/LtlFileParser.h"
 
 #include "log4cplus/logger.h"
 #include "log4cplus/loggingmacros.h"
@@ -98,7 +99,7 @@ void printFooter() {
 bool parseOptions(const int argc, const char* argv[]) {
 	storm::settings::Settings* s = nullptr;
 	try {
-		storm::settings::Settings::registerModule<storm::modelchecker::GmmxxDtmcPrctlModelChecker<double>>();
+		storm::settings::Settings::registerModule<storm::modelchecker::prctl::GmmxxDtmcPrctlModelChecker<double>>();
 		s = storm::settings::newInstance(argc, argv, nullptr);
 	} catch (storm::exceptions::InvalidSettingsException& e) {
 		std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl;
@@ -142,10 +143,10 @@ void cleanUp() {
  * @param dtmc The Dtmc that the model checker will check
  * @return
  */
-storm::modelchecker::AbstractModelChecker<double>* createPrctlModelChecker(storm::models::Dtmc<double>& dtmc) {
+storm::modelchecker::prctl::AbstractModelChecker<double>* createPrctlModelChecker(storm::models::Dtmc<double>& dtmc) {
 	storm::settings::Settings* s = storm::settings::instance();
 	if (s->getString("matrixlib") == "gmm++") {
-		return new storm::modelchecker::GmmxxDtmcPrctlModelChecker<double>(dtmc);
+		return new storm::modelchecker::prctl::GmmxxDtmcPrctlModelChecker<double>(dtmc);
 	}
 	// The control flow should never reach this point, as there is a default setting for matrixlib (gmm++)
 	std::string message = "No matrix library suitable for DTMC model checking has been set";
@@ -158,10 +159,10 @@ storm::modelchecker::AbstractModelChecker<double>* createPrctlModelChecker(storm
  * @param mdp The Dtmc that the model checker will check
  * @return
  */
-storm::modelchecker::AbstractModelChecker<double>* createPrctlModelChecker(storm::models::Mdp<double>& mdp) {
+storm::modelchecker::prctl::AbstractModelChecker<double>* createPrctlModelChecker(storm::models::Mdp<double>& mdp) {
 	storm::settings::Settings* s = storm::settings::instance();
 	if (s->getString("matrixlib") == "gmm++") {
-		return new storm::modelchecker::GmmxxMdpPrctlModelChecker<double>(mdp);
+		return new storm::modelchecker::prctl::GmmxxMdpPrctlModelChecker<double>(mdp);
 	}
 	// The control flow should never reach this point, as there is a default setting for matrixlib (gmm++)
 	std::string message = "No matrix library suitable for MDP model checking has been set";
@@ -176,7 +177,7 @@ storm::modelchecker::AbstractModelChecker<double>* createPrctlModelChecker(storm
  * @param mc the model checker
  */
 void checkPrctlFormulasAgainstModel(std::list<storm::property::prctl::AbstractPrctlFormula<double>*>& formulaList,
-									storm::modelchecker::AbstractModelChecker<double> const& mc) {
+									storm::modelchecker::prctl::AbstractModelChecker<double> const& mc) {
 	for ( auto formula : formulaList ) {
 		mc.check(*formula);
 
@@ -198,7 +199,7 @@ void checkMdp(std::shared_ptr<storm::models::Mdp<double>> mdp) {
 		storm::parser::PrctlFileParser fileParser;
 		std::list<storm::property::prctl::AbstractPrctlFormula<double>*> formulaList = fileParser.parseFormulas(s->getString("prctl"));
 
-		storm::modelchecker::AbstractModelChecker<double>* mc = createPrctlModelChecker(*mdp);
+		storm::modelchecker::prctl::AbstractModelChecker<double>* mc = createPrctlModelChecker(*mdp);
 
 		checkPrctlFormulasAgainstModel(formulaList, *mc);
 
@@ -222,13 +223,28 @@ void checkDtmc(std::shared_ptr<storm::models::Dtmc<double>> dtmc) {
 		storm::parser::PrctlFileParser fileParser;
 		std::list<storm::property::prctl::AbstractPrctlFormula<double>*> formulaList = fileParser.parseFormulas(s->getString("prctl"));
 
-		storm::modelchecker::AbstractModelChecker<double>* mc = createPrctlModelChecker(*dtmc);
+		storm::modelchecker::prctl::AbstractModelChecker<double>* mc = createPrctlModelChecker(*dtmc);
 
 		checkPrctlFormulasAgainstModel(formulaList, *mc);
 
 		delete mc;
 	}
 
+	if (s->isSet("ltl")) {
+		LOG4CPLUS_INFO(logger, "Parsing ltl file"+ s->getString("ltl"));
+		storm::parser::LtlFileParser fileParser;
+		std::list<storm::property::ltl::AbstractLtlFormula<double>*> formulaList = fileParser.parseFormulas(s->getString("ltl"));
+
+		LOG4CPLUS_ERROR(logger, "LTL model checking is not implemented yet.");
+
+		//Debug output while LTL formulas cannot be checked
+		for (auto formula : formulaList) {
+			LOG4CPLUS_DEBUG(logger, formula->toString());
+		}
+
+
+	}
+
 	if(s->isSet("csl")) {
 		LOG4CPLUS_ERROR(logger, "CSL properties cannot be checked on DTMCs.");
 	}
diff --git a/test/functional/GmmxxDtmcPrctModelCheckerTest.cpp b/test/functional/GmmxxDtmcPrctModelCheckerTest.cpp
index aa2a014fa..0c0be908b 100644
--- a/test/functional/GmmxxDtmcPrctModelCheckerTest.cpp
+++ b/test/functional/GmmxxDtmcPrctModelCheckerTest.cpp
@@ -2,7 +2,7 @@
 #include "storm-config.h"
 
 #include "src/utility/Settings.h"
-#include "src/modelchecker/GmmxxDtmcPrctlModelChecker.h"
+#include "src/modelchecker/prctl/GmmxxDtmcPrctlModelChecker.h"
 #include "src/parser/AutoParser.h"
 
 TEST(GmmxxDtmcPrctModelCheckerTest, Die) {
@@ -17,7 +17,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Die) {
 	ASSERT_EQ(dtmc->getNumberOfStates(), 13u);
 	ASSERT_EQ(dtmc->getNumberOfTransitions(), 27u);
 
-	storm::modelchecker::GmmxxDtmcPrctlModelChecker<double> mc(*dtmc);
+	storm::modelchecker::prctl::GmmxxDtmcPrctlModelChecker<double> mc(*dtmc);
 
 	storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("one");
 	storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
@@ -84,7 +84,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, Crowds) {
 	ASSERT_EQ(dtmc->getNumberOfStates(), 8607u);
 	ASSERT_EQ(dtmc->getNumberOfTransitions(), 22460u);
 
-	storm::modelchecker::GmmxxDtmcPrctlModelChecker<double> mc(*dtmc);
+	storm::modelchecker::prctl::GmmxxDtmcPrctlModelChecker<double> mc(*dtmc);
 
 	storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("observe0Greater1");
 	storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
@@ -138,7 +138,7 @@ TEST(GmmxxDtmcPrctModelCheckerTest, SynchronousLeader) {
 	ASSERT_EQ(dtmc->getNumberOfStates(), 12400u);
 	ASSERT_EQ(dtmc->getNumberOfTransitions(), 28894u);
 
-	storm::modelchecker::GmmxxDtmcPrctlModelChecker<double> mc(*dtmc);
+	storm::modelchecker::prctl::GmmxxDtmcPrctlModelChecker<double> mc(*dtmc);
 
 	storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("elected");
 	storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
diff --git a/test/functional/GmmxxMdpPrctModelCheckerTest.cpp b/test/functional/GmmxxMdpPrctModelCheckerTest.cpp
index 13136cc69..ff622a644 100644
--- a/test/functional/GmmxxMdpPrctModelCheckerTest.cpp
+++ b/test/functional/GmmxxMdpPrctModelCheckerTest.cpp
@@ -2,7 +2,7 @@
 #include "storm-config.h"
 
 #include "src/utility/Settings.h"
-#include "src/modelchecker/GmmxxMdpPrctlModelChecker.h"
+#include "src/modelchecker/prctl/GmmxxMdpPrctlModelChecker.h"
 #include "src/parser/AutoParser.h"
 
 TEST(GmmxxMdpPrctModelCheckerTest, Dice) {
@@ -16,7 +16,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) {
 	ASSERT_EQ(mdp->getNumberOfStates(), 169u);
 	ASSERT_EQ(mdp->getNumberOfTransitions(), 436u);
 
-	storm::modelchecker::GmmxxMdpPrctlModelChecker<double> mc(*mdp);
+	storm::modelchecker::prctl::GmmxxMdpPrctlModelChecker<double> mc(*mdp);
 
 	storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("two");
 	storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
@@ -114,7 +114,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) {
 
 	std::shared_ptr<storm::models::Mdp<double>> stateRewardMdp = stateRewardParser.getModel<storm::models::Mdp<double>>();
 
-	storm::modelchecker::GmmxxMdpPrctlModelChecker<double> stateRewardModelChecker(*stateRewardMdp);
+	storm::modelchecker::prctl::GmmxxMdpPrctlModelChecker<double> stateRewardModelChecker(*stateRewardMdp);
 
 	apFormula = new storm::property::prctl::Ap<double>("done");
 	reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
@@ -144,7 +144,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, Dice) {
 
 	std::shared_ptr<storm::models::Mdp<double>> stateAndTransitionRewardMdp = stateAndTransitionRewardParser.getModel<storm::models::Mdp<double>>();
 
-	storm::modelchecker::GmmxxMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp);
+	storm::modelchecker::prctl::GmmxxMdpPrctlModelChecker<double> stateAndTransitionRewardModelChecker(*stateAndTransitionRewardMdp);
 
 	apFormula = new storm::property::prctl::Ap<double>("done");
 	reachabilityRewardFormula = new storm::property::prctl::ReachabilityReward<double>(apFormula);
@@ -180,7 +180,7 @@ TEST(GmmxxMdpPrctModelCheckerTest, AsynchronousLeader) {
 	ASSERT_EQ(mdp->getNumberOfStates(), 3172u);
 	ASSERT_EQ(mdp->getNumberOfTransitions(), 7144u);
 
-	storm::modelchecker::GmmxxMdpPrctlModelChecker<double> mc(*mdp);
+	storm::modelchecker::prctl::GmmxxMdpPrctlModelChecker<double> mc(*mdp);
 
 	storm::property::prctl::Ap<double>* apFormula = new storm::property::prctl::Ap<double>("elected");
 	storm::property::prctl::Eventually<double>* eventuallyFormula = new storm::property::prctl::Eventually<double>(apFormula);
diff --git a/test/storm-tests.cpp b/test/storm-tests.cpp
index e5d78bb5e..f4cbe225c 100644
--- a/test/storm-tests.cpp
+++ b/test/storm-tests.cpp
@@ -7,7 +7,7 @@
 #include "log4cplus/fileappender.h"
 
 #include "src/utility/Settings.h"
-#include "src/modelchecker/GmmxxDtmcPrctlModelChecker.h"
+#include "src/modelchecker/prctl/GmmxxDtmcPrctlModelChecker.h"
 
 log4cplus::Logger logger;
 
@@ -37,7 +37,7 @@ void setUpLogging() {
 bool parseOptions(int const argc, char const * const argv[]) {
     storm::settings::Settings* s = nullptr;
     try {
-        storm::settings::Settings::registerModule<storm::modelchecker::GmmxxDtmcPrctlModelChecker<double>>();
+        storm::settings::Settings::registerModule<storm::modelchecker::prctl::GmmxxDtmcPrctlModelChecker<double>>();
         s = storm::settings::newInstance(argc, argv, nullptr, true);
     } catch (storm::exceptions::InvalidSettingsException& e) {
         std::cout << "Could not recover from settings error: " << e.what() << "." << std::endl;