diff --git a/CMakeLists.txt b/CMakeLists.txt
index b19636778..8cf280117 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -50,13 +50,13 @@ option(USE_POPCNT "Sets whether the popcnt instruction is going to be used." ON)
 option(USE_BOOST_STATIC_LIBRARIES "Sets whether the Boost libraries should be linked statically." ON)
 
 # If the DEBUG option was turned on, we will target a debug version and a release version otherwise
-#if (DEBUG)
-#    set (CMAKE_BUILD_TYPE "DEBUG")
-#    message(STATUS "Building DEBUG version.")
-#else()
-#    set (CMAKE_BUILD_TYPE "RELEASE")
-#    message(STATUS "Building RELEASE version.")
-#endif()
+if (DEBUG)
+    set (CMAKE_BUILD_TYPE "DEBUG")
+    message(STATUS "Building DEBUG version.")
+else()
+    set (CMAKE_BUILD_TYPE "RELEASE")
+    message(STATUS "Building RELEASE version.")
+endif()
 
 message(STATUS "CMAKE_BUILD_TYPE: ${CMAKE_BUILD_TYPE}")
 message(STATUS "CMAKE_BUILD_TYPE (ENV): $ENV{CMAKE_BUILD_TYPE}")
@@ -152,14 +152,24 @@ add_executable(storm-tests ${STORM_TEST_SOURCES} ${STORM_TEST_HEADERS})
 target_link_libraries(storm ${Boost_LIBRARIES})   
 target_link_libraries(storm-tests ${Boost_LIBRARIES})
 
-# Include Cotire for PCH Generation
-set (CMAKE_MODULE_PATH "${CMAKE_SOURCE_DIR}/resources/cmake")
-include(cotire)
+set (STORM_USE_COTIRE ON)
+if (APPLE)
+	set(STORM_USE_COTIRE OFF)
+endif(APPLE)
+
+# Print Cotire Usage Status
+message (STATUS "Using Cotire: ${STORM_USE_COTIRE}")
 
-cotire(storm)
-target_link_libraries(storm_unity ${Boost_LIBRARIES})
-#cotire(storm-tests)
+if (STORM_USE_COTIRE)
+	# Include Cotire for PCH Generation
+	set (CMAKE_MODULE_PATH "${CMAKE_SOURCE_DIR}/resources/cmake")
+	include(cotire)
 
+	cotire(storm)
+	target_link_libraries(storm_unity ${Boost_LIBRARIES})
+	#cotire(storm-tests)
+endif()
+	
 # Add a target to generate API documentation with Doxygen
 if(DOXYGEN_FOUND)
     set(CMAKE_DOXYGEN_OUTPUT_DIR "${CMAKE_CURRENT_BINARY_DIR}/doc")
@@ -187,27 +197,33 @@ endif(GTEST_INCLUDE_DIR)
 if (LOG4CPLUS_INCLUDE_DIR)
     include_directories(${LOG4CPLUS_INCLUDE_DIR})
     target_link_libraries(storm ${LOG4CPLUS_LIBRARIES}) 
-	target_link_libraries(storm_unity ${LOG4CPLUS_LIBRARIES})
+	if (STORM_USE_COTIRE)
+		target_link_libraries(storm_unity ${LOG4CPLUS_LIBRARIES})
+	endif(STORM_USE_COTIRE)
     target_link_libraries(storm-tests ${LOG4CPLUS_LIBRARIES})
     # On Linux, we have to link against librt
     if (UNIX AND NOT APPLE)
-	   target_link_libraries(storm rt)
-	   target_link_libraries(storm_unity rt)
-	   target_link_libraries(storm-tests rt)
+		target_link_libraries(storm rt)
+		if (STORM_USE_COTIRE)
+			target_link_libraries(storm_unity rt)
+		endif(STORM_USE_COTIRE)
+		target_link_libraries(storm-tests rt)
     endif(UNIX AND NOT APPLE)
 endif(LOG4CPLUS_INCLUDE_DIR)
 
 if (THREADS_FOUND)
 	include_directories(${THREADS_INCLUDE_DIRS})
-    target_link_libraries(storm ${CMAKE_THREAD_LIBS_INIT})
-	target_link_libraries(storm_unity ${CMAKE_THREAD_LIBS_INIT})
+	target_link_libraries(storm ${CMAKE_THREAD_LIBS_INIT})
+	if (STORM_USE_COTIRE)
+		target_link_libraries(storm_unity ${CMAKE_THREAD_LIBS_INIT})
+	endif(STORM_USE_COTIRE)
 	target_link_libraries(storm-tests ${CMAKE_THREAD_LIBS_INIT})
 endif(THREADS_FOUND)
 
 # Configure a header file to pass some of the CMake settings to the source code
 configure_file (
-  "${PROJECT_SOURCE_DIR}/storm-config.h.in"
-  "${PROJECT_BINARY_DIR}/storm-config.h"
+	"${PROJECT_SOURCE_DIR}/storm-config.h.in"
+	"${PROJECT_BINARY_DIR}/storm-config.h"
 )
 
 add_custom_target(memcheck valgrind --leak-check=full --show-reachable=yes ${PROJECT_BINARY_DIR}/storm -v --fix-deadlocks ${PROJECT_SOURCE_DIR}/examples/dtmc/crowds/crowds5_5.tra examples/dtmc/crowds/crowds5_5.lab
diff --git a/src/formula/ReachabilityReward.h b/src/formula/ReachabilityReward.h
index ad8171642..a725e202a 100644
--- a/src/formula/ReachabilityReward.h
+++ b/src/formula/ReachabilityReward.h
@@ -11,7 +11,6 @@
 #include "src/formula/AbstractPathFormula.h"
 #include "src/formula/AbstractStateFormula.h"
 #include "src/formula/AbstractFormulaChecker.h"
-#include "src/modelchecker/AbstractModelChecker.h"
 
 namespace storm {
 namespace formula {
diff --git a/src/modelchecker/AbstractModelChecker.h b/src/modelchecker/AbstractModelChecker.h
index 5e0920231..69bbeb9da 100644
--- a/src/modelchecker/AbstractModelChecker.h
+++ b/src/modelchecker/AbstractModelChecker.h
@@ -33,12 +33,19 @@ template<class Type>
 class AbstractModelChecker :
 	public virtual storm::formula::IApModelChecker<Type>,
 	public virtual storm::formula::IAndModelChecker<Type>,
+	public virtual storm::formula::IOrModelChecker<Type>,
+	public virtual storm::formula::INotModelChecker<Type>,
+	public virtual storm::formula::IUntilModelChecker<Type>,
 	public virtual storm::formula::IEventuallyModelChecker<Type>,
 	public virtual storm::formula::IGloballyModelChecker<Type>,
 	public virtual storm::formula::INextModelChecker<Type>,
-	public virtual storm::formula::INotModelChecker<Type>,
-	public virtual storm::formula::IOrModelChecker<Type>
-	{
+	public virtual storm::formula::IBoundedUntilModelChecker<Type>,
+	public virtual storm::formula::IBoundedEventuallyModelChecker<Type>,
+	public virtual storm::formula::INoBoundOperatorModelChecker<Type>,
+	public virtual storm::formula::IPathBoundOperatorModelChecker<Type>,
+	public virtual storm::formula::IReachabilityRewardModelChecker<Type>,
+	public virtual storm::formula::ICumulativeRewardModelChecker<Type>,
+	public virtual storm::formula::IInstantaneousRewardModelChecker<Type> {
 	
 public:
 	template <template <class T> class Target>
diff --git a/src/modelchecker/DtmcPrctlModelChecker.h b/src/modelchecker/DtmcPrctlModelChecker.h
index 90f1672e0..48b10d54b 100644
--- a/src/modelchecker/DtmcPrctlModelChecker.h
+++ b/src/modelchecker/DtmcPrctlModelChecker.h
@@ -39,10 +39,7 @@ namespace modelChecker {
  */
 template<class Type>
 class DtmcPrctlModelChecker : 
-	public virtual AbstractModelChecker<Type>, 
-	public virtual storm::formula::INoBoundOperatorModelChecker<Type>,
-	public virtual storm::formula::IReachabilityRewardModelChecker<Type>
-	{
+	public virtual AbstractModelChecker<Type> {
 public:
 	/*!
 	 * Constructor
diff --git a/src/modelchecker/EigenDtmcPrctlModelChecker.h b/src/modelchecker/EigenDtmcPrctlModelChecker.h
index a7b749129..6965b3a0c 100644
--- a/src/modelchecker/EigenDtmcPrctlModelChecker.h
+++ b/src/modelchecker/EigenDtmcPrctlModelChecker.h
@@ -12,7 +12,7 @@
 
 #include "src/models/Dtmc.h"
 #include "src/modelchecker/DtmcPrctlModelChecker.h"
-#include "src/solver/GraphAnalyzer.h"
+#include "src/utility/GraphAnalyzer.h"
 #include "src/utility/ConstTemplates.h"
 #include "src/exceptions/NoConvergenceException.h"
 
@@ -126,17 +126,16 @@ public:
 
 		// Then, we need to identify the states which have to be taken out of the matrix, i.e.
 		// all states that have probability 0 and 1 of satisfying the until-formula.
-		storm::storage::BitVector notExistsPhiUntilPsiStates(this->getModel().getNumberOfStates());
-		storm::storage::BitVector alwaysPhiUntilPsiStates(this->getModel().getNumberOfStates());
-		storm::solver::GraphAnalyzer::getPhiUntilPsiStates<double>(this->getModel(), *leftStates, *rightStates, &notExistsPhiUntilPsiStates, &alwaysPhiUntilPsiStates);
-		notExistsPhiUntilPsiStates.complement();
+		storm::storage::BitVector statesWithProbability0(this->getModel().getNumberOfStates());
+		storm::storage::BitVector statesWithProbability1(this->getModel().getNumberOfStates());
+		storm::utility::GraphAnalyzer::performProb01(this->getModel(), *leftStates, *rightStates, &statesWithProbability0, &statesWithProbability1);
 
 		delete leftStates;
 		delete rightStates;
 
-		LOG4CPLUS_INFO(logger, "Found " << notExistsPhiUntilPsiStates.getNumberOfSetBits() << " 'no' states.");
-		LOG4CPLUS_INFO(logger, "Found " << alwaysPhiUntilPsiStates.getNumberOfSetBits() << " 'yes' states.");
-		storm::storage::BitVector maybeStates = ~(notExistsPhiUntilPsiStates | alwaysPhiUntilPsiStates);
+		LOG4CPLUS_INFO(logger, "Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states.");
+		LOG4CPLUS_INFO(logger, "Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states.");
+		storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1);
 		LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
 
 		// Create resulting vector and set values accordingly.
@@ -175,7 +174,7 @@ public:
 			Type *pb = &(b[0]); // get the address storing the data for b
 			MapType vectorB(pb, b.size()); // vectorB shares data 
 
-			this->getModel().getTransitionProbabilityMatrix()->getConstrainedRowCountVector(maybeStates, alwaysPhiUntilPsiStates, &x);
+			this->getModel().getTransitionProbabilityMatrix()->getConstrainedRowCountVector(maybeStates, statesWithProbability1, &x);
 
 			Eigen::BiCGSTAB<Eigen::SparseMatrix<Type, 1, int_fast32_t>> solver;
 			solver.compute(*eigenSubMatrix);
@@ -212,8 +211,8 @@ public:
 			delete eigenSubMatrix;
 		}
 
-		storm::utility::setVectorValues<Type>(result, notExistsPhiUntilPsiStates, storm::utility::constGetZero<Type>());
-		storm::utility::setVectorValues<Type>(result, alwaysPhiUntilPsiStates, storm::utility::constGetOne<Type>());
+		storm::utility::setVectorValues<Type>(result, statesWithProbability0, storm::utility::constGetZero<Type>());
+		storm::utility::setVectorValues<Type>(result, statesWithProbability1, storm::utility::constGetOne<Type>());
 
 		return result;
 	}
diff --git a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h
index 009ecd678..359462c1f 100644
--- a/src/modelchecker/GmmxxDtmcPrctlModelChecker.h
+++ b/src/modelchecker/GmmxxDtmcPrctlModelChecker.h
@@ -12,7 +12,7 @@
 
 #include "src/models/Dtmc.h"
 #include "src/modelchecker/DtmcPrctlModelChecker.h"
-#include "src/solver/GraphAnalyzer.h"
+#include "src/utility/GraphAnalyzer.h"
 #include "src/utility/Vector.h"
 #include "src/utility/ConstTemplates.h"
 #include "src/utility/Settings.h"
@@ -49,7 +49,7 @@ public:
 		storm::storage::BitVector* rightStates = this->checkStateFormula(formula.getRight());
 
 		// Copy the matrix before we make any changes.
-		storm::storage::SparseMatrix<Type> tmpMatrix(*this->getModel().getTransitionProbabilityMatrix());
+		storm::storage::SparseMatrix<Type> tmpMatrix(*this->getModel().getTransitionMatrix());
 
 		// Make all rows absorbing that violate both sub-formulas or satisfy the second sub-formula.
 		tmpMatrix.makeRowsAbsorbing(~(*leftStates | *rightStates) | *rightStates);
@@ -84,7 +84,7 @@ public:
 		storm::storage::BitVector* nextStates = this->checkStateFormula(formula.getChild());
 
 		// Transform the transition probability matrix to the gmm++ format to use its arithmetic.
-		gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*this->getModel().getTransitionProbabilityMatrix());
+		gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*this->getModel().getTransitionMatrix());
 
 		// Create the vector with which to multiply and initialize it correctly.
 		std::vector<Type> x(this->getModel().getNumberOfStates());
@@ -111,18 +111,17 @@ public:
 
 		// Then, we need to identify the states which have to be taken out of the matrix, i.e.
 		// all states that have probability 0 and 1 of satisfying the until-formula.
-		storm::storage::BitVector notExistsPhiUntilPsiStates(this->getModel().getNumberOfStates());
-		storm::storage::BitVector alwaysPhiUntilPsiStates(this->getModel().getNumberOfStates());
-		storm::solver::GraphAnalyzer::getPhiUntilPsiStates(this->getModel(), *leftStates, *rightStates, &notExistsPhiUntilPsiStates, &alwaysPhiUntilPsiStates);
-		notExistsPhiUntilPsiStates.complement();
+		storm::storage::BitVector statesWithProbability0(this->getModel().getNumberOfStates());
+		storm::storage::BitVector statesWithProbability1(this->getModel().getNumberOfStates());
+		storm::utility::GraphAnalyzer::performProb01(this->getModel(), *leftStates, *rightStates, &statesWithProbability0, &statesWithProbability1);
 
 		// Delete sub-results that are obsolete now.
 		delete leftStates;
 		delete rightStates;
 
-		LOG4CPLUS_INFO(logger, "Found " << notExistsPhiUntilPsiStates.getNumberOfSetBits() << " 'no' states.");
-		LOG4CPLUS_INFO(logger, "Found " << alwaysPhiUntilPsiStates.getNumberOfSetBits() << " 'yes' states.");
-		storm::storage::BitVector maybeStates = ~(notExistsPhiUntilPsiStates | alwaysPhiUntilPsiStates);
+		LOG4CPLUS_INFO(logger, "Found " << statesWithProbability0.getNumberOfSetBits() << " 'no' states.");
+		LOG4CPLUS_INFO(logger, "Found " << statesWithProbability1.getNumberOfSetBits() << " 'yes' states.");
+		storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1);
 		LOG4CPLUS_INFO(logger, "Found " << maybeStates.getNumberOfSetBits() << " 'maybe' states.");
 
 		// Create resulting vector.
@@ -132,7 +131,7 @@ public:
 		uint_fast64_t mayBeStatesSetBitCount = maybeStates.getNumberOfSetBits();
 		if (mayBeStatesSetBitCount > 0) {
 			// Now we can eliminate the rows and columns from the original transition probability matrix.
-			storm::storage::SparseMatrix<Type>* submatrix = this->getModel().getTransitionProbabilityMatrix()->getSubmatrix(maybeStates);
+			storm::storage::SparseMatrix<Type>* submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates);
 			// Converting the matrix from the fixpoint notation to the form needed for the equation
 			// system. That is, we go from x = A*x + b to (I-A)x = b.
 			submatrix->convertToEquationSystem();
@@ -149,7 +148,7 @@ public:
 			// Prepare the right-hand side of the equation system. For entry i this corresponds to
 			// the accumulated probability of going from state i to some 'yes' state.
 			std::vector<Type> b(mayBeStatesSetBitCount);
-			this->getModel().getTransitionProbabilityMatrix()->getConstrainedRowCountVector(maybeStates, alwaysPhiUntilPsiStates, &b);
+			this->getModel().getTransitionMatrix()->getConstrainedRowCountVector(maybeStates, statesWithProbability1, &b);
 
 			// Solve the corresponding system of linear equations.
 			this->solveLinearEquationSystem(*gmmxxMatrix, x, b);
@@ -162,8 +161,8 @@ public:
 		}
 
 		// Set values of resulting vector that are known exactly.
-		storm::utility::setVectorValues<Type>(result, notExistsPhiUntilPsiStates, storm::utility::constGetZero<Type>());
-		storm::utility::setVectorValues<Type>(result, alwaysPhiUntilPsiStates, storm::utility::constGetOne<Type>());
+		storm::utility::setVectorValues<Type>(result, statesWithProbability0, storm::utility::constGetZero<Type>());
+		storm::utility::setVectorValues<Type>(result, statesWithProbability1, storm::utility::constGetOne<Type>());
 
 		return result;
 	}
@@ -176,10 +175,10 @@ public:
 		}
 
 		// Transform the transition probability matrix to the gmm++ format to use its arithmetic.
-		gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*this->getModel().getTransitionProbabilityMatrix());
+		gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*this->getModel().getTransitionMatrix());
 
 		// Initialize result to state rewards of the model.
-		std::vector<Type>* result = new std::vector<Type>(*this->getModel().getStateRewards());
+		std::vector<Type>* result = new std::vector<Type>(*this->getModel().getStateRewardVector());
 
 		// Now perform matrix-vector multiplication as long as we meet the bound of the formula.
 		std::vector<Type>* swap = nullptr;
@@ -205,17 +204,17 @@ public:
 		}
 
 		// Transform the transition probability matrix to the gmm++ format to use its arithmetic.
-		gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*this->getModel().getTransitionProbabilityMatrix());
+		gmm::csr_matrix<Type>* gmmxxMatrix = storm::adapters::GmmxxAdapter::toGmmxxSparseMatrix<Type>(*this->getModel().getTransitionMatrix());
 
 		// Compute the reward vector to add in each step based on the available reward models.
 		std::vector<Type>* totalRewardVector = nullptr;
 		if (this->getModel().hasTransitionRewards()) {
-			totalRewardVector = this->getModel().getTransitionProbabilityMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix());
+			totalRewardVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix());
 			if (this->getModel().hasStateRewards()) {
-				gmm::add(*this->getModel().getStateRewards(), *totalRewardVector);
+				gmm::add(*this->getModel().getStateRewardVector(), *totalRewardVector);
 			}
 		} else {
-			totalRewardVector = new std::vector<Type>(*this->getModel().getStateRewards());
+			totalRewardVector = new std::vector<Type>(*this->getModel().getStateRewardVector());
 		}
 
 		std::vector<Type>* result = new std::vector<Type>(this->getModel().getNumberOfStates());
@@ -253,7 +252,7 @@ public:
 		// Determine which states have a reward of infinity by definition.
 		storm::storage::BitVector infinityStates(this->getModel().getNumberOfStates());
 		storm::storage::BitVector trueStates(this->getModel().getNumberOfStates(), true);
-		storm::solver::GraphAnalyzer::getAlwaysPhiUntilPsiStates(this->getModel(), trueStates, *targetStates, &infinityStates);
+		storm::utility::GraphAnalyzer::performProb1(this->getModel(), trueStates, *targetStates, &infinityStates);
 		infinityStates.complement();
 
 		// Create resulting vector.
@@ -264,7 +263,7 @@ public:
 		const int maybeStatesSetBitCount = maybeStates.getNumberOfSetBits();
 		if (maybeStatesSetBitCount > 0) {
 			// Now we can eliminate the rows and columns from the original transition probability matrix.
-			storm::storage::SparseMatrix<Type>* submatrix = this->getModel().getTransitionProbabilityMatrix()->getSubmatrix(maybeStates);
+			storm::storage::SparseMatrix<Type>* submatrix = this->getModel().getTransitionMatrix()->getSubmatrix(maybeStates);
 			// Converting the matrix from the fixpoint notation to the form needed for the equation
 			// system. That is, we go from x = A*x + b to (I-A)x = b.
 			submatrix->convertToEquationSystem();
@@ -283,7 +282,7 @@ public:
 				// If a transition-based reward model is available, we initialize the right-hand
 				// side to the vector resulting from summing the rows of the pointwise product
 				// of the transition probability matrix and the transition reward matrix.
-				std::vector<Type>* pointwiseProductRowSumVector = this->getModel().getTransitionProbabilityMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix());
+				std::vector<Type>* pointwiseProductRowSumVector = this->getModel().getTransitionMatrix()->getPointwiseProductRowSumVector(*this->getModel().getTransitionRewardMatrix());
 				storm::utility::selectVectorValues(b, maybeStates, *pointwiseProductRowSumVector);
 				delete pointwiseProductRowSumVector;
 
@@ -293,7 +292,7 @@ public:
 					// that we still consider (i.e. maybeStates), we need to extract these values
 					// first.
 					std::vector<Type>* subStateRewards = new std::vector<Type>(maybeStatesSetBitCount);
-					storm::utility::setVectorValues(subStateRewards, maybeStates, *this->getModel().getStateRewards());
+					storm::utility::setVectorValues(subStateRewards, maybeStates, *this->getModel().getStateRewardVector());
 					gmm::add(*subStateRewards, *b);
 					delete subStateRewards;
 				}
@@ -302,7 +301,7 @@ public:
 				// right-hand side. As the state reward vector contains entries not just for the
 				// states that we still consider (i.e. maybeStates), we need to extract these values
 				// first.
-				storm::utility::setVectorValues(b, maybeStates, *this->getModel().getStateRewards());
+				storm::utility::setVectorValues(b, maybeStates, *this->getModel().getStateRewardVector());
 			}
 
 			// Solve the corresponding system of linear equations.
diff --git a/src/models/AbstractDeterministicModel.h b/src/models/AbstractDeterministicModel.h
new file mode 100644
index 000000000..aa44ba736
--- /dev/null
+++ b/src/models/AbstractDeterministicModel.h
@@ -0,0 +1,54 @@
+#ifndef STORM_MODELS_ABSTRACTDETERMINISTICMODEL_H_
+#define STORM_MODELS_ABSTRACTDETERMINISTICMODEL_H_
+
+#include "AbstractModel.h"
+#include "GraphTransitions.h"
+
+#include <memory>
+
+namespace storm {
+
+namespace models {
+
+/*!
+ *	@brief	Base class for all deterministic model classes.
+ *
+ *	This is base class defines a common interface for all deterministic models.
+ */
+template<class T>
+class AbstractDeterministicModel: public AbstractModel<T> {
+
+	public:
+		/*! Constructs an abstract determinstic model from the given parameters.
+		 * @param transitionMatrix The matrix representing the transitions in the model.
+		 * @param stateLabeling The labeling that assigns a set of atomic
+		 * propositions to each state.
+		 * @param stateRewardVector The reward values associated with the states.
+		 * @param transitionRewardMatrix The reward values associated with the transitions of the model.
+		 */
+		AbstractDeterministicModel(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix,
+			std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling,
+			std::shared_ptr<std::vector<T>> stateRewardVector, std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix)
+			: AbstractModel<T>(transitionMatrix, stateLabeling, stateRewardVector, transitionRewardMatrix) {
+		}
+
+		/*!
+		 * Destructor.
+		 */
+		virtual ~AbstractDeterministicModel() {
+			// Intentionally left empty.
+		}
+
+		/*!
+		 * Copy Constructor.
+		 */
+		AbstractDeterministicModel(AbstractDeterministicModel const& other) : AbstractModel<T>(other) {
+			// Intentionally left empty.
+		}
+};
+
+} // namespace models
+
+} // namespace storm
+
+#endif /* STORM_MODELS_ABSTRACTDETERMINISTICMODEL_H_ */
diff --git a/src/models/AbstractModel.h b/src/models/AbstractModel.h
index c35ecd3cc..0f830b6fc 100644
--- a/src/models/AbstractModel.h
+++ b/src/models/AbstractModel.h
@@ -1,7 +1,13 @@
 #ifndef STORM_MODELS_ABSTRACTMODEL_H_
 #define STORM_MODELS_ABSTRACTMODEL_H_
 
+#include "src/models/AtomicPropositionsLabeling.h"
+#include "src/storage/BitVector.h"
+#include "src/storage/SparseMatrix.h"
+#include "src/utility/CommandLine.h"
+
 #include <memory>
+#include <vector>
 
 namespace storm {
 namespace models {
@@ -24,9 +30,32 @@ std::ostream& operator<<(std::ostream& os, ModelType const type);
  *	This is base class defines a common interface for all models to identify
  *	their type and obtain the special model.
  */
-class AbstractModel: public std::enable_shared_from_this<AbstractModel> {
+template<class T>
+class AbstractModel: public std::enable_shared_from_this<AbstractModel<T>> {
 
 	public:
+		/*! Constructs an abstract model from the given transition matrix and
+		 * the given labeling of the states.
+		 * @param transitionMatrix The matrix representing the transitions in the model.
+		 * @param stateLabeling The labeling that assigns a set of atomic
+		 * propositions to each state.
+		 * @param stateRewardVector The reward values associated with the states.
+		 * @param transitionRewardMatrix The reward values associated with the transitions of the model.
+		 */
+		AbstractModel(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix,
+				std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling,
+				std::shared_ptr<std::vector<T>> stateRewardVector, std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix)
+				: transitionMatrix(transitionMatrix), stateLabeling(stateLabeling), stateRewardVector(stateRewardVector), transitionRewardMatrix(transitionRewardMatrix) {
+			// Intentionally left empty.
+		}
+
+		/*!
+		 * Destructor.
+		 */
+		virtual ~AbstractModel() {
+			// Intentionally left empty.
+		}
+
 		/*!
 		 *	@brief Casts the model to the model type that was actually
 		 *	created.
@@ -44,7 +73,7 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel> {
 		 */
 		template <typename Model>
 		std::shared_ptr<Model> as() {
-			return std::dynamic_pointer_cast<Model>(shared_from_this());
+			return std::dynamic_pointer_cast<Model>(this->shared_from_this());
 		}
 		
 		/*!
@@ -54,8 +83,147 @@ class AbstractModel: public std::enable_shared_from_this<AbstractModel> {
 		 *
 		 *	@return	Type of the model.
 		 */
-		virtual ModelType getType() = 0;
-		
+		virtual ModelType getType() const = 0;
+
+		/*!
+		 * Returns the state space size of the model.
+		 * @return The size of the state space of the model.
+		 */
+		virtual uint_fast64_t getNumberOfStates() const {
+			return this->getTransitionMatrix()->getColumnCount();
+		}
+
+		/*!
+		 * Returns the number of (non-zero) transitions of the model.
+		 * @return The number of (non-zero) transitions of the model.
+		 */
+		virtual uint_fast64_t getNumberOfTransitions() const {
+			return this->getTransitionMatrix()->getNonZeroEntryCount();
+		}
+
+		/*!
+		 * Returns a bit vector in which exactly those bits are set to true that
+		 * correspond to a state labeled with the given atomic proposition.
+		 * @param ap The atomic proposition for which to get the bit vector.
+		 * @return A bit vector in which exactly those bits are set to true that
+		 * correspond to a state labeled with the given atomic proposition.
+		 */
+		storm::storage::BitVector* getLabeledStates(std::string ap) const {
+			return stateLabeling->getAtomicProposition(ap);
+		}
+
+		/*!
+		 * Retrieves whether the given atomic proposition is a valid atomic proposition in this model.
+		 * @param atomicProposition The atomic proposition to be checked for validity.
+		 * @return True if the given atomic proposition is valid in this model.
+		 */
+		bool hasAtomicProposition(std::string const& atomicProposition) const {
+			return stateLabeling->containsAtomicProposition(atomicProposition);
+		}
+
+		/*!
+		 * Returns a pointer to the matrix representing the transition probability
+		 * function.
+		 * @return A pointer to the matrix representing the transition probability
+		 * function.
+		 */
+		std::shared_ptr<storm::storage::SparseMatrix<T>> getTransitionMatrix() const {
+			return transitionMatrix;
+		}
+
+		/*!
+		 * Returns a pointer to the matrix representing the transition rewards.
+		 * @return A pointer to the matrix representing the transition rewards.
+		 */
+		std::shared_ptr<storm::storage::SparseMatrix<T>> getTransitionRewardMatrix() const {
+			return transitionRewardMatrix;
+		}
+
+		/*!
+		 * Returns a pointer to the vector representing the state rewards.
+		 * @return A pointer to the vector representing the state rewards.
+		 */
+		std::shared_ptr<std::vector<T>> getStateRewardVector() const {
+			return stateRewardVector;
+		}
+
+		/*!
+		 * Returns the set of states with which the given state is labeled.
+		 * @return The set of states with which the given state is labeled.
+		 */
+		std::set<std::string> const getPropositionsForState(uint_fast64_t const &state) const {
+			return stateLabeling->getPropositionsForState(state);
+		}
+
+		/*!
+		 * Returns the state labeling associated with this model.
+		 * @return The state labeling associated with this model.
+		 */
+		std::shared_ptr<storm::models::AtomicPropositionsLabeling> getStateLabeling() const {
+			return stateLabeling;
+		}
+
+		/*!
+		 * Retrieves whether this model has a state reward model.
+		 * @return True if this model has a state reward model.
+		 */
+		bool hasStateRewards() const {
+			return stateRewardVector != nullptr;
+		}
+
+		/*!
+		 * Retrieves whether this model has a transition reward model.
+		 * @return True if this model has a transition reward model.
+		 */
+		bool hasTransitionRewards() const {
+			return transitionRewardMatrix != nullptr;
+		}
+
+		/*!
+		 * Retrieves the size of the internal representation of the model in memory.
+		 * @return the size of the internal representation of the model in memory
+		 * measured in bytes.
+		 */
+		virtual uint_fast64_t getSizeInMemory() const {
+			uint_fast64_t result = transitionMatrix->getSizeInMemory() + stateLabeling->getSizeInMemory();
+			if (stateRewardVector != nullptr) {
+				result += stateRewardVector->size() * sizeof(T);
+			}
+			if (transitionRewardMatrix != nullptr) {
+				result += transitionRewardMatrix->getSizeInMemory();
+			}
+			return result;
+		}
+
+		/*!
+		 * Prints information about the model to the specified stream.
+		 * @param out The stream the information is to be printed to.
+		 */
+		void printModelInformationToStream(std::ostream& out) const {
+			out << "-------------------------------------------------------------- "
+				<< std::endl;
+			out << "Model type: \t\t" << this->getType() << std::endl;
+			out << "States: \t\t" << this->getNumberOfStates() << std::endl;
+			out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl;
+			this->getStateLabeling()->printAtomicPropositionsInformationToStream(out);
+			out << "Size in memory: \t"
+				<< (this->getSizeInMemory())/1024 << " kbytes" << std::endl;
+			out << "-------------------------------------------------------------- "
+				<< std::endl;
+		}
+
+	private:
+		/*! A matrix representing the likelihoods of moving between states. */
+		std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix;
+
+		/*! The labeling of the states of the model. */
+		std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling;
+
+		/*! The state-based rewards of the model. */
+		std::shared_ptr<std::vector<T>> stateRewardVector;
+
+		/*! The transition-based rewards of the model. */
+		std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix;
 };
 
 } // namespace models
diff --git a/src/models/AbstractNondeterministicModel.h b/src/models/AbstractNondeterministicModel.h
new file mode 100644
index 000000000..0ca1dea37
--- /dev/null
+++ b/src/models/AbstractNondeterministicModel.h
@@ -0,0 +1,82 @@
+#ifndef STORM_MODELS_ABSTRACTNONDETERMINISTICMODEL_H_
+#define STORM_MODELS_ABSTRACTNONDETERMINISTICMODEL_H_
+
+#include "AbstractModel.h"
+#include "GraphTransitions.h"
+
+#include <memory>
+
+namespace storm {
+
+namespace models {
+
+/*!
+ *	@brief	Base class for all non-deterministic model classes.
+ *
+ *	This is base class defines a common interface for all non-deterministic models.
+ */
+template<class T>
+class AbstractNondeterministicModel: public AbstractModel<T> {
+
+	public:
+		/*! Constructs an abstract non-determinstic model from the given parameters.
+		 * @param transitionMatrix The matrix representing the transitions in the model.
+		 * @param stateLabeling The labeling that assigns a set of atomic
+		 * propositions to each state.
+		 * @param choiceIndices A mapping from states to rows in the transition matrix.
+		 * @param stateRewardVector The reward values associated with the states.
+		 * @param transitionRewardMatrix The reward values associated with the transitions of the model.
+		 */
+		AbstractNondeterministicModel(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix,
+			std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling,
+			std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices,
+			std::shared_ptr<std::vector<T>> stateRewardVector,
+			std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix)
+			: AbstractModel<T>(transitionMatrix, stateLabeling, stateRewardVector, transitionRewardMatrix),
+			  nondeterministicChoiceIndices(nondeterministicChoiceIndices) {
+		}
+
+		/*!
+		 * Destructor.
+		 */
+		virtual ~AbstractNondeterministicModel() {
+			// Intentionally left empty.
+		}
+
+		/*!
+		 * Copy Constructor.
+		 */
+		AbstractNondeterministicModel(AbstractNondeterministicModel const& other) : AbstractModel<T>(other),
+				nondeterministicChoiceIndices(other.nondeterministicChoiceIndices) {
+			// Intentionally left empty.
+		}
+
+		/*!
+		 * Retrieves the size of the internal representation of the model in memory.
+		 * @return the size of the internal representation of the model in memory
+		 * measured in bytes.
+		 */
+		virtual uint_fast64_t getSizeInMemory() const {
+			return AbstractModel<T>::getSizeInMemory() + nondeterministicChoiceIndices->size() * sizeof(uint_fast64_t);
+		}
+
+		/*!
+		 * Retrieves the vector indicating which matrix rows represent non-deterministic choices
+		 * of a certain state.
+		 * @param the vector indicating which matrix rows represent non-deterministic choices
+		 * of a certain state.
+		 */
+		std::shared_ptr<std::vector<uint_fast64_t>> getNondeterministicChoiceIndices() const {
+			return nondeterministicChoiceIndices;
+		}
+
+	private:
+		/*! A vector of indices mapping states to the choices (rows) in the transition matrix. */
+		std::shared_ptr<std::vector<uint_fast64_t>> nondeterministicChoiceIndices;
+};
+
+} // namespace models
+
+} // namespace storm
+
+#endif /* STORM_MODELS_ABSTRACTDETERMINISTICMODEL_H_ */
diff --git a/src/models/Ctmc.h b/src/models/Ctmc.h
index 263a62fe9..0b8eff5fd 100644
--- a/src/models/Ctmc.h
+++ b/src/models/Ctmc.h
@@ -8,28 +8,23 @@
 #ifndef STORM_MODELS_CTMC_H_
 #define STORM_MODELS_CTMC_H_
 
-#include <ostream>
-#include <iostream>
 #include <memory>
-#include <cstdlib>
+#include <vector>
 
+#include "AbstractDeterministicModel.h"
 #include "AtomicPropositionsLabeling.h"
-#include "GraphTransitions.h"
 #include "src/storage/SparseMatrix.h"
-#include "src/exceptions/InvalidArgumentException.h"
-
-#include "src/models/AbstractModel.h"
 
 namespace storm {
 
 namespace models {
 
 /*!
- * This class represents a discrete-time Markov chain (DTMC) whose states are
+ * This class represents a continuous-time Markov chain (CTMC) whose states are
  * labeled with atomic propositions.
  */
 template <class T>
-class Ctmc : public storm::models::AbstractModel {
+class Ctmc : public storm::models::AbstractDeterministicModel<T> {
 
 public:
 	//! Constructor
@@ -43,11 +38,9 @@ public:
 	 */
 	Ctmc(std::shared_ptr<storm::storage::SparseMatrix<T>> rateMatrix,
 			std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling,
-			std::shared_ptr<std::vector<T>> stateRewards = nullptr,
+			std::shared_ptr<std::vector<T>> stateRewardVector = nullptr,
 			std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix = nullptr)
-			: rateMatrix(rateMatrix), stateLabeling(stateLabeling),
-			  stateRewards(stateRewards), transitionRewardMatrix(transitionRewardMatrix),
-			  backwardTransitions(nullptr) {
+			: AbstractDeterministicModel<T>(rateMatrix, stateLabeling, stateRewardVector, transitionRewardMatrix) {
 	}
 
 	//! Copy Constructor
@@ -55,137 +48,13 @@ public:
 	 * Copy Constructor. Performs a deep copy of the given CTMC.
 	 * @param ctmc A reference to the CTMC that is to be copied.
 	 */
-	Ctmc(const Ctmc<T> &ctmc) : rateMatrix(ctmc.rateMatrix),
-			stateLabeling(ctmc.stateLabeling), stateRewards(ctmc.stateRewards),
-			transitionRewardMatrix(ctmc.transitionRewardMatrix) {
-		if (ctmc.backwardTransitions != nullptr) {
-			this->backwardTransitions = new storm::models::GraphTransitions<T>(*ctmc.backwardTransitions);
-		}
-	}
-
-	//! Destructor
-	/*!
-	 * Destructor. Frees the matrix and labeling associated with this CTMC.
-	 */
-	~Ctmc() {
-		if (this->backwardTransitions != nullptr) {
-			delete this->backwardTransitions;
-		}
-	}
-	
-	/*!
-	 * Returns the state space size of the CTMC.
-	 * @return The size of the state space of the CTMC.
-	 */
-	uint_fast64_t getNumberOfStates() const {
-		return this->rateMatrix->getRowCount();
-	}
-
-	/*!
-	 * Returns the number of (non-zero) transitions of the CTMC.
-	 * @return The number of (non-zero) transitions of the CTMC.
-	 */
-	uint_fast64_t getNumberOfTransitions() const {
-		return this->rateMatrix->getNonZeroEntryCount();
-	}
-
-	/*!
-	 * Returns a bit vector in which exactly those bits are set to true that
-	 * correspond to a state labeled with the given atomic proposition.
-	 * @param ap The atomic proposition for which to get the bit vector.
-	 * @return A bit vector in which exactly those bits are set to true that
-	 * correspond to a state labeled with the given atomic proposition.
-	 */
-	storm::storage::BitVector* getLabeledStates(std::string ap) const {
-		return this->stateLabeling->getAtomicProposition(ap);
-	}
-
-	/*!
-	 * Returns a pointer to the matrix representing the transition probability
-	 * function.
-	 * @return A pointer to the matrix representing the transition probability
-	 * function.
-	 */
-	std::shared_ptr<storm::storage::SparseMatrix<T>> getTransitionRateMatrix() const {
-		return this->rateMatrix;
-	}
-
-	/*!
-	 * Returns a pointer to the matrix representing the transition rewards.
-	 * @return A pointer to the matrix representing the transition rewards.
-	 */
-	std::shared_ptr<storm::storage::SparseMatrix<T>> getTransitionRewardMatrix() const {
-		return this->transitionRewardMatrix;
+	Ctmc(const Ctmc<T> &ctmc) : AbstractDeterministicModel<T>(ctmc) {
+		// Intentionally left empty.
 	}
 
-	/*!
-	 * Returns a pointer to the vector representing the state rewards.
-	 * @return A pointer to the vector representing the state rewards.
-	 */
-	std::shared_ptr<std::vector<T>> getStateRewards() const {
-		return this->stateRewards;
-	}
-
-	/*!
-	 *
-	 */
-	std::set<std::string> const getPropositionsForState(uint_fast64_t const &state) const {
-		return stateLabeling->getPropositionsForState(state);
-	}
-
-	/*!
-	 * Retrieves a reference to the backwards transition relation.
-	 * @return A reference to the backwards transition relation.
-	 */
-	storm::models::GraphTransitions<T>& getBackwardTransitions() {
-		if (this->backwardTransitions == nullptr) {
-			this->backwardTransitions = new storm::models::GraphTransitions<T>(this->probabilityMatrix, false);
-		}
-		return *this->backwardTransitions;
-	}
-
-	/*!
-	 * Prints information about the model to the specified stream.
-	 * @param out The stream the information is to be printed to.
-	 */
-	void printModelInformationToStream(std::ostream& out) const {
-		out << "-------------------------------------------------------------- "
-			<< std::endl;
-		out << "Model type: \t\tCTMC" << std::endl;
-		out << "States: \t\t" << this->getNumberOfStates() << std::endl;
-		out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl;
-		this->stateLabeling->printAtomicPropositionsInformationToStream(out);
-		out << "Size in memory: \t"
-			<< (this->rateMatrix->getSizeInMemory() +
-				this->stateLabeling->getSizeInMemory() +
-				sizeof(*this))/1024 << " kbytes" << std::endl;
-		out << "-------------------------------------------------------------- "
-			<< std::endl;
-	}
-
-	storm::models::ModelType getType() {
+	storm::models::ModelType getType() const {
 		return CTMC;
 	}
-
-private:
-
-	/*! A matrix representing the transition rate function of the CTMC. */
-	std::shared_ptr<storm::storage::SparseMatrix<T>> rateMatrix;
-
-	/*! The labeling of the states of the CTMC. */
-	std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling;
-
-	/*! The state-based rewards of the CTMC. */
-	std::shared_ptr<std::vector<T>> stateRewards;
-
-	/*! The transition-based rewards of the CTMC. */
-	std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix;
-
-	/*!
-	 * A data structure that stores the predecessors for all states. This is
-	 * needed for backwards directed searches.
-	 */
-	storm::models::GraphTransitions<T>* backwardTransitions;
 };
 
 } // namespace models
diff --git a/src/models/Ctmdp.h b/src/models/Ctmdp.h
index 137095e9f..e693c70a1 100644
--- a/src/models/Ctmdp.h
+++ b/src/models/Ctmdp.h
@@ -8,19 +8,13 @@
 #ifndef STORM_MODELS_CTMDP_H_
 #define STORM_MODELS_CTMDP_H_
 
-#include <ostream>
-#include <iostream>
 #include <memory>
-#include <cstdlib>
+#include <vector>
 
 #include "AtomicPropositionsLabeling.h"
-#include "GraphTransitions.h"
+#include "AbstractNondeterministicModel.h"
 #include "src/storage/SparseMatrix.h"
-#include "src/exceptions/InvalidArgumentException.h"
-#include "src/utility/CommandLine.h"
 #include "src/utility/Settings.h"
-#include "src/models/AbstractModel.h"
-#include "src/parser/NonDeterministicSparseTransitionParser.h"
 
 namespace storm {
 
@@ -31,7 +25,7 @@ namespace models {
  * labeled with atomic propositions.
  */
 template <class T>
-class Ctmdp : public storm::models::AbstractModel {
+class Ctmdp : public storm::models::AbstractNondeterministicModel<T> {
 
 public:
 	//! Constructor
@@ -45,12 +39,10 @@ public:
 	 */
 	Ctmdp(std::shared_ptr<storm::storage::SparseMatrix<T>> probabilityMatrix,
 			std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling,
-			std::shared_ptr<std::vector<uint_fast64_t>> rowMapping,
-			std::shared_ptr<std::vector<T>> stateRewards = nullptr,
+			std::shared_ptr<std::vector<uint_fast64_t>> choiceIndices,
+			std::shared_ptr<std::vector<T>> stateRewardVector = nullptr,
 			std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix = nullptr)
-			: probabilityMatrix(probabilityMatrix), stateLabeling(stateLabeling), rowMapping(rowMapping),
-			  stateRewards(stateRewards), transitionRewardMatrix(transitionRewardMatrix),
-			  backwardTransitions(nullptr) {
+			: AbstractNondeterministicModel<T>(probabilityMatrix, stateLabeling, choiceIndices, stateRewardVector, transitionRewardMatrix) {
 		if (!this->checkValidityOfProbabilityMatrix()) {
 			LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
 			throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
@@ -62,12 +54,7 @@ public:
 	 * Copy Constructor. Performs a deep copy of the given CTMDP.
 	 * @param ctmdp A reference to the CTMDP that is to be copied.
 	 */
-	Ctmdp(const Ctmdp<T> &ctmdp) : probabilityMatrix(ctmdp.probabilityMatrix),
-			stateLabeling(ctmdp.stateLabeling), rowMapping(ctmdp.rowMapping), stateRewards(ctmdp.stateRewards),
-			transitionRewardMatrix(ctmdp.transitionRewardMatrix) {
-		if (ctmdp.backwardTransitions != nullptr) {
-			this->backwardTransitions = new storm::models::GraphTransitions<T>(*ctmdp.backwardTransitions);
-		}
+	Ctmdp(const Ctmdp<T> &ctmdp) : AbstractNondeterministicModel<T>(ctmdp) {
 		if (!this->checkValidityOfProbabilityMatrix()) {
 			LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
 			throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
@@ -76,130 +63,13 @@ public:
 
 	//! Destructor
 	/*!
-	 * Destructor. Frees the matrix and labeling associated with this CTMDP.
+	 * Destructor.
 	 */
 	~Ctmdp() {
-		if (this->backwardTransitions != nullptr) {
-			delete this->backwardTransitions;
-		}
-	}
-	
-	/*!
-	 * Returns the state space size of the CTMDP.
-	 * @return The size of the state space of the CTMDP.
-	 */
-	uint_fast64_t getNumberOfStates() const {
-		return this->probabilityMatrix->getColumnCount();
+		// Intentionally left empty.
 	}
 
-	/*!
-	 * Returns the number of (non-zero) transitions of the CTMDP.
-	 * @return The number of (non-zero) transitions of the CTMDP.
-	 */
-	uint_fast64_t getNumberOfTransitions() const {
-		return this->probabilityMatrix->getNonZeroEntryCount();
-	}
-
-	/*!
-	 * Returns a bit vector in which exactly those bits are set to true that
-	 * correspond to a state labeled with the given atomic proposition.
-	 * @param ap The atomic proposition for which to get the bit vector.
-	 * @return A bit vector in which exactly those bits are set to true that
-	 * correspond to a state labeled with the given atomic proposition.
-	 */
-	storm::storage::BitVector* getLabeledStates(std::string ap) const {
-		return this->stateLabeling->getAtomicProposition(ap);
-	}
-
-	/*!
-	 * Returns a pointer to the matrix representing the transition probability
-	 * function.
-	 * @return A pointer to the matrix representing the transition probability
-	 * function.
-	 */
-	std::shared_ptr<storm::storage::SparseMatrix<T>> getTransitionProbabilityMatrix() const {
-		return this->probabilityMatrix;
-	}
-
-	/*!
-	 * Returns a pointer to the matrix representing the transition rewards.
-	 * @return A pointer to the matrix representing the transition rewards.
-	 */
-	std::shared_ptr<storm::storage::SparseMatrix<T>> getTransitionRewardMatrix() const {
-		return this->transitionRewardMatrix;
-	}
-
-	/*!
-	 * Returns a pointer to the vector representing the state rewards.
-	 * @return A pointer to the vector representing the state rewards.
-	 */
-	std::shared_ptr<std::vector<T>> getStateRewards() const {
-		return this->stateRewards;
-	}
-
-	/*!
-	 *
-	 */
-	std::set<std::string> const getPropositionsForState(uint_fast64_t const &state) const {
-		return stateLabeling->getPropositionsForState(state);
-	}
-
-	/*!
-	 * Retrieves a reference to the backwards transition relation.
-	 * @return A reference to the backwards transition relation.
-	 */
-	storm::models::GraphTransitions<T>& getBackwardTransitions() {
-		if (this->backwardTransitions == nullptr) {
-			this->backwardTransitions = new storm::models::GraphTransitions<T>(this->probabilityMatrix, false);
-		}
-		return *this->backwardTransitions;
-	}
-
-	/*!
-	 * Retrieves whether this CTMDP has a state reward model.
-	 * @return True if this CTMDP has a state reward model.
-	 */
-	bool hasStateRewards() {
-		return this->stateRewards != nullptr;
-	}
-
-	/*!
-	 * Retrieves whether this CTMDP has a transition reward model.
-	 * @return True if this CTMDP has a transition reward model.
-	 */
-	bool hasTransitionRewards() {
-		return this->transitionRewardMatrix != nullptr;
-	}
-
-	/*!
-	 * Retrieves whether the given atomic proposition is a valid atomic proposition in this model.
-	 * @param atomicProposition The atomic proposition to be checked for validity.
-	 * @return True if the given atomic proposition is valid in this model.
-	 */
-	bool hasAtomicProposition(std::string const& atomicProposition) {
-		return this->stateLabeling->containsAtomicProposition(atomicProposition);
-	}
-
-	/*!
-	 * Prints information about the model to the specified stream.
-	 * @param out The stream the information is to be printed to.
-	 */
-	void printModelInformationToStream(std::ostream& out) const {
-		storm::utility::printSeparationLine(out);
-		out << std::endl;
-		out << "Model type: \t\tCTMDP" << std::endl;
-		out << "States: \t\t" << this->getNumberOfStates() << std::endl;
-		out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl;
-		this->stateLabeling->printAtomicPropositionsInformationToStream(out);
-		out << "Size in memory: \t"
-			<< (this->probabilityMatrix->getSizeInMemory() +
-				this->stateLabeling->getSizeInMemory() +
-				sizeof(*this))/1024 << " kbytes" << std::endl;
-		out << std::endl;
-		storm::utility::printSeparationLine(out);
-	}
-	
-	storm::models::ModelType getType() {
+	storm::models::ModelType getType() const {
 		return CTMDP;
 	}
 
@@ -214,34 +84,13 @@ private:
 		// Get the settings object to customize linear solving.
 		storm::settings::Settings* s = storm::settings::instance();
 		double precision = s->get<double>("precision");
-		for (uint_fast64_t row = 0; row < this->probabilityMatrix->getRowCount(); row++) {
-			T sum = this->probabilityMatrix->getRowSum(row);
+		for (uint_fast64_t row = 0; row < this->getTransitionMatrix()->getRowCount(); row++) {
+			T sum = this->getTransitionMatrix()->getRowSum(row);
 			if (sum == 0) continue;
 			if (std::abs(sum - 1) > precision) return false;
 		}
 		return true;
 	}
-
-	/*! A matrix representing the transition probability function of the CTMDP. */
-	std::shared_ptr<storm::storage::SparseMatrix<T>> probabilityMatrix;
-
-	/*! The labeling of the states of the CTMDP. */
-	std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling;
-	
-	/*! The mapping from states to rows. */
-	std::shared_ptr<std::vector<uint_fast64_t>> rowMapping;
-
-	/*! The state-based rewards of the CTMDP. */
-	std::shared_ptr<std::vector<T>> stateRewards;
-
-	/*! The transition-based rewards of the CTMDP. */
-	std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix;
-
-	/*!
-	 * A data structure that stores the predecessors for all states. This is
-	 * needed for backwards directed searches.
-	 */
-	storm::models::GraphTransitions<T>* backwardTransitions;
 };
 
 } // namespace models
diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h
index c19208543..eefcc2ab5 100644
--- a/src/models/Dtmc.h
+++ b/src/models/Dtmc.h
@@ -13,13 +13,11 @@
 #include <memory>
 #include <cstdlib>
 
+#include "AbstractDeterministicModel.h"
 #include "AtomicPropositionsLabeling.h"
-#include "GraphTransitions.h"
 #include "src/storage/SparseMatrix.h"
 #include "src/exceptions/InvalidArgumentException.h"
-#include "src/utility/CommandLine.h"
 #include "src/utility/Settings.h"
-#include "src/models/AbstractModel.h"
 
 namespace storm {
 
@@ -30,7 +28,7 @@ namespace models {
  * labeled with atomic propositions.
  */
 template <class T>
-class Dtmc : public storm::models::AbstractModel {
+class Dtmc : public storm::models::AbstractDeterministicModel<T> {
 
 public:
 	//! Constructor
@@ -44,17 +42,15 @@ public:
 	 */
 	Dtmc(std::shared_ptr<storm::storage::SparseMatrix<T>> probabilityMatrix,
 			std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling,
-			std::shared_ptr<std::vector<T>> stateRewards = nullptr,
+			std::shared_ptr<std::vector<T>> stateRewardVector = nullptr,
 			std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix = nullptr)
-			: probabilityMatrix(probabilityMatrix), stateLabeling(stateLabeling),
-			  stateRewards(stateRewards), transitionRewardMatrix(transitionRewardMatrix),
-			  backwardTransitions(nullptr) {
+			: AbstractDeterministicModel<T>(probabilityMatrix, stateLabeling, stateRewardVector, transitionRewardMatrix) {
 		if (!this->checkValidityOfProbabilityMatrix()) {
 			LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
 			throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
 		}
-		if (this->transitionRewardMatrix != nullptr) {
-			if (!this->transitionRewardMatrix->isSubmatrixOf(*(this->probabilityMatrix))) {
+		if (this->getTransitionRewardMatrix() != nullptr) {
+			if (!this->getTransitionRewardMatrix()->isSubmatrixOf(*(this->getTransitionMatrix()))) {
 				LOG4CPLUS_ERROR(logger, "Transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist.");
 				throw storm::exceptions::InvalidArgumentException() << "There are transition rewards for nonexistent transitions.";
 			}
@@ -66,146 +62,23 @@ public:
 	 * Copy Constructor. Performs a deep copy of the given DTMC.
 	 * @param dtmc A reference to the DTMC that is to be copied.
 	 */
-	Dtmc(const Dtmc<T> &dtmc) : probabilityMatrix(dtmc.probabilityMatrix),
-			stateLabeling(dtmc.stateLabeling), stateRewards(dtmc.stateRewards),
-			transitionRewardMatrix(dtmc.transitionRewardMatrix) {
-		if (dtmc.backwardTransitions != nullptr) {
-			this->backwardTransitions = new storm::models::GraphTransitions<T>(*dtmc.backwardTransitions);
-		}
-		// no checks here, as they have already been performed for dtmc.
+	Dtmc(const Dtmc<T> &dtmc) : AbstractDeterministicModel<T>(dtmc) {
+		// Intentionally left empty.
 	}
 
 	//! Destructor
 	/*!
-	 * Destructor. Frees the matrix and labeling associated with this DTMC.
+	 * Destructor.
 	 */
 	~Dtmc() {
-		if (this->backwardTransitions != nullptr) {
-			delete this->backwardTransitions;
-		}
-	}
-	
-	/*!
-	 * Returns the state space size of the DTMC.
-	 * @return The size of the state space of the DTMC.
-	 */
-	uint_fast64_t getNumberOfStates() const {
-		return this->probabilityMatrix->getRowCount();
-	}
-
-	/*!
-	 * Returns the number of (non-zero) transitions of the DTMC.
-	 * @return The number of (non-zero) transitions of the DTMC.
-	 */
-	uint_fast64_t getNumberOfTransitions() const {
-		return this->probabilityMatrix->getNonZeroEntryCount();
-	}
-
-	/*!
-	 * Returns a bit vector in which exactly those bits are set to true that
-	 * correspond to a state labeled with the given atomic proposition.
-	 * @param ap The atomic proposition for which to get the bit vector.
-	 * @return A bit vector in which exactly those bits are set to true that
-	 * correspond to a state labeled with the given atomic proposition.
-	 */
-	storm::storage::BitVector* getLabeledStates(std::string ap) const {
-		return this->stateLabeling->getAtomicProposition(ap);
-	}
-
-	/*!
-	 * Returns a pointer to the matrix representing the transition probability
-	 * function.
-	 * @return A pointer to the matrix representing the transition probability
-	 * function.
-	 */
-	std::shared_ptr<storm::storage::SparseMatrix<T>> getTransitionProbabilityMatrix() const {
-		return this->probabilityMatrix;
-	}
-
-	/*!
-	 * Returns a pointer to the matrix representing the transition rewards.
-	 * @return A pointer to the matrix representing the transition rewards.
-	 */
-	std::shared_ptr<storm::storage::SparseMatrix<T>> getTransitionRewardMatrix() const {
-		return this->transitionRewardMatrix;
-	}
-
-	/*!
-	 * Returns a pointer to the vector representing the state rewards.
-	 * @return A pointer to the vector representing the state rewards.
-	 */
-	std::shared_ptr<std::vector<T>> getStateRewards() const {
-		return this->stateRewards;
-	}
-
-	/*!
-	 *
-	 */
-	std::set<std::string> const getPropositionsForState(uint_fast64_t const &state) const {
-		return stateLabeling->getPropositionsForState(state);
-	}
-
-	/*!
-	 * Retrieves a reference to the backwards transition relation.
-	 * @return A reference to the backwards transition relation.
-	 */
-	storm::models::GraphTransitions<T>& getBackwardTransitions() {
-		if (this->backwardTransitions == nullptr) {
-			this->backwardTransitions = new storm::models::GraphTransitions<T>(this->probabilityMatrix, false);
-		}
-		return *this->backwardTransitions;
-	}
-
-	/*!
-	 * Retrieves whether this DTMC has a state reward model.
-	 * @return True if this DTMC has a state reward model.
-	 */
-	bool hasStateRewards() {
-		return this->stateRewards != nullptr;
-	}
-
-	/*!
-	 * Retrieves whether this DTMC has a transition reward model.
-	 * @return True if this DTMC has a transition reward model.
-	 */
-	bool hasTransitionRewards() {
-		return this->transitionRewardMatrix != nullptr;
-	}
-
-	/*!
-	 * Retrieves whether the given atomic proposition is a valid atomic proposition in this model.
-	 * @param atomicProposition The atomic proposition to be checked for validity.
-	 * @return True if the given atomic proposition is valid in this model.
-	 */
-	bool hasAtomicProposition(std::string const& atomicProposition) {
-		return this->stateLabeling->containsAtomicProposition(atomicProposition);
-	}
-
-	/*!
-	 * Prints information about the model to the specified stream.
-	 * @param out The stream the information is to be printed to.
-	 */
-	void printModelInformationToStream(std::ostream& out) const {
-		storm::utility::printSeparationLine(out);
-		out << std::endl;
-		out << "Model type: \t\tDTMC" << std::endl;
-		out << "States: \t\t" << this->getNumberOfStates() << std::endl;
-		out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl;
-		this->stateLabeling->printAtomicPropositionsInformationToStream(out);
-		out << "Size in memory: \t"
-			<< (this->probabilityMatrix->getSizeInMemory() +
-				this->stateLabeling->getSizeInMemory() +
-				sizeof(*this))/1024 << " kbytes" << std::endl;
-		out << std::endl;
-		storm::utility::printSeparationLine(out);
+		// Intentionally left empty.
 	}
 	
-	storm::models::ModelType getType() {
+	storm::models::ModelType getType() const {
 		return DTMC;
 	}
 
 private:
-
 	/*!
 	 *	@brief Perform some sanity checks.
 	 *
@@ -216,14 +89,14 @@ private:
 		storm::settings::Settings* s = storm::settings::instance();
 		double precision = s->get<double>("precision");
 
-		if (this->probabilityMatrix->getRowCount() != this->probabilityMatrix->getColumnCount()) {
+		if (this->getTransitionMatrix()->getRowCount() != this->getTransitionMatrix()->getColumnCount()) {
 			// not square
 			LOG4CPLUS_ERROR(logger, "Probability matrix is not square.");
 			return false;
 		}
 
-		for (uint_fast64_t row = 0; row < this->probabilityMatrix->getRowCount(); row++) {
-			T sum = this->probabilityMatrix->getRowSum(row);
+		for (uint_fast64_t row = 0; row < this->getTransitionMatrix()->getRowCount(); row++) {
+			T sum = this->getTransitionMatrix()->getRowSum(row);
 			if (sum == 0) {
 				LOG4CPLUS_ERROR(logger, "Row " << row << " has sum 0");
 				return false;
@@ -235,24 +108,6 @@ private:
 		}
 		return true;
 	}
-
-	/*! A matrix representing the transition probability function of the DTMC. */
-	std::shared_ptr<storm::storage::SparseMatrix<T>> probabilityMatrix;
-
-	/*! The labeling of the states of the DTMC. */
-	std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling;
-
-	/*! The state-based rewards of the DTMC. */
-	std::shared_ptr<std::vector<T>> stateRewards;
-
-	/*! The transition-based rewards of the DTMC. */
-	std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix;
-
-	/*!
-	 * A data structure that stores the predecessors for all states. This is
-	 * needed for backwards directed searches.
-	 */
-	storm::models::GraphTransitions<T>* backwardTransitions;
 };
 
 } // namespace models
diff --git a/src/models/GraphTransitions.h b/src/models/GraphTransitions.h
index 579bf7832..6f4da36f1 100644
--- a/src/models/GraphTransitions.h
+++ b/src/models/GraphTransitions.h
@@ -40,7 +40,7 @@ public:
 	 * of the backwards transition relation.
 	 */
 	GraphTransitions(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix, bool forward)
-			: successorList(nullptr), stateIndications(nullptr), numberOfStates(transitionMatrix->getRowCount()), numberOfNonZeroTransitions(transitionMatrix->getNonZeroEntryCount()) {
+			: successorList(nullptr), stateIndications(nullptr), numberOfStates(transitionMatrix->getColumnCount()), numberOfTransitions(transitionMatrix->getNonZeroEntryCount()) {
 		if (forward) {
 			this->initializeForward(transitionMatrix);
 		} else {
@@ -48,6 +48,15 @@ public:
 		}
 	}
 
+	GraphTransitions(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix, std::shared_ptr<std::vector<uint_fast64_t>> choiceIndices, bool forward)
+		: successorList(nullptr), stateIndications(nullptr), numberOfStates(transitionMatrix->getColumnCount()), numberOfTransitions(transitionMatrix->getNonZeroEntryCount()) {
+		if (forward) {
+			this->initializeForward(transitionMatrix, choiceIndices);
+		} else {
+			this->initializeBackward(transitionMatrix, choiceIndices);
+		}
+	}
+
 	//! Destructor
 	/*!
 	 * Destructor. Frees the internal storage.
@@ -61,6 +70,16 @@ public:
 		}
 	}
 
+	/*!
+	 * Retrieves the size of the internal representation of the graph transitions in memory.
+	 * @return the size of the internal representation of the graph transitions in memory
+	 * measured in bytes.
+	 */
+	virtual uint_fast64_t getSizeInMemory() const {
+		uint_fast64_t result = sizeof(this) + (numberOfStates + numberOfTransitions + 1) * sizeof(uint_fast64_t);
+		return result;
+	}
+
 	/*!
 	 * Returns an iterator to the successors of the given state.
 	 * @param state The state for which to get the successor iterator.
@@ -88,18 +107,37 @@ private:
 	 * relation given by means of a sparse matrix.
 	 */
 	void initializeForward(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix) {
-		this->successorList = new uint_fast64_t[numberOfNonZeroTransitions];
+		this->successorList = new uint_fast64_t[numberOfTransitions];
 		this->stateIndications = new uint_fast64_t[numberOfStates + 1];
 
 		// First, we copy the index list from the sparse matrix as this will
 		// stay the same.
-		std::copy(transitionMatrix->getRowIndicationsPointer().begin(), transitionMatrix->getRowIndicationsPointer().end(), this->stateIndications);
+		std::copy(transitionMatrix->getRowIndications().begin(), transitionMatrix->getRowIndications().end(), this->stateIndications);
 
 		// Now we can iterate over all rows of the transition matrix and record
 		// the target state.
 		for (uint_fast64_t i = 0, currentNonZeroElement = 0; i < numberOfStates; i++) {
 			for (auto rowIt = transitionMatrix->beginConstColumnIterator(i); rowIt != transitionMatrix->endConstColumnIterator(i); ++rowIt) {
-				this->stateIndications[currentNonZeroElement++] = *rowIt;
+				this->successorList[currentNonZeroElement++] = *rowIt;
+			}
+		}
+	}
+
+	void initializeForward(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix, std::shared_ptr<std::vector<uint_fast64_t>> choiceIndices) {
+		this->successorList = new uint_fast64_t[numberOfTransitions];
+		this->stateIndications = new uint_fast64_t[numberOfStates + 1];
+
+		for (uint_fast64_t i = 0; i < numberOfStates; ++i) {
+			this->stateIndications[i] = transitionMatrix->getRowIndications().at(choiceIndices->at(i));
+		}
+
+		// Now we can iterate over all rows of the transition matrix and record
+		// the target state.
+		for (uint_fast64_t i = 0, currentNonZeroElement = 0; i < numberOfStates; i++) {
+			for (uint_fast64_t j = choiceIndices->at(i); j < choiceIndices->at(i + 1); ++j) {
+				for (auto rowIt = transitionMatrix->beginConstColumnIterator(j); rowIt != transitionMatrix->endConstColumnIterator(j); ++rowIt) {
+					this->successorList[currentNonZeroElement++] = *rowIt;
+				}
 			}
 		}
 	}
@@ -110,27 +148,25 @@ private:
 	 * matrix.
 	 */
 	void initializeBackward(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix) {
-		this->successorList = new uint_fast64_t[numberOfNonZeroTransitions];
-		this->stateIndications = new uint_fast64_t[numberOfStates + 1];
+		this->successorList = new uint_fast64_t[numberOfTransitions];
+		this->stateIndications = new uint_fast64_t[numberOfStates + 1]();
 
 		// First, we need to count how many backward transitions each state has.
-		// NOTE: We disregard the diagonal here, as we only consider "true"
-		// predecessors.
-		for (uint_fast64_t i = 0; i < numberOfStates; i++) {
+		for (uint_fast64_t i = 0; i < numberOfStates; ++i) {
 			for (auto rowIt = transitionMatrix->beginConstColumnIterator(i); rowIt != transitionMatrix->endConstColumnIterator(i); ++rowIt) {
 				this->stateIndications[*rowIt + 1]++;
 			}
 		}
 
 		// Now compute the accumulated offsets.
-		for (uint_fast64_t i = 1; i < numberOfStates; i++) {
+		for (uint_fast64_t i = 1; i < numberOfStates; ++i) {
 			this->stateIndications[i] = this->stateIndications[i - 1] + this->stateIndications[i];
 		}
 
 		// Put a sentinel element at the end of the indices list. This way,
 		// for each state i the range of indices can be read off between
 		// state_indices_list[i] and state_indices_list[i + 1].
-		this->stateIndications[numberOfStates] = numberOfNonZeroTransitions;
+		this->stateIndications[numberOfStates] = numberOfTransitions;
 
 		// Create an array that stores the next index for each state. Initially
 		// this corresponds to the previously computed accumulated offsets.
@@ -139,7 +175,7 @@ private:
 
 		// Now we are ready to actually fill in the list of predecessors for
 		// every state. Again, we start by considering all but the last row.
-		for (uint_fast64_t i = 0; i < numberOfStates; i++) {
+		for (uint_fast64_t i = 0; i < numberOfStates; ++i) {
 			for (auto rowIt = transitionMatrix->beginConstColumnIterator(i); rowIt != transitionMatrix->endConstColumnIterator(i); ++rowIt) {
 				this->successorList[nextIndicesList[*rowIt]++] = i;
 			}
@@ -149,6 +185,48 @@ private:
 		delete[] nextIndicesList;
 	}
 
+	void initializeBackward(std::shared_ptr<storm::storage::SparseMatrix<T>> transitionMatrix, std::shared_ptr<std::vector<uint_fast64_t>> choiceIndices) {
+		this->successorList = new uint_fast64_t[numberOfTransitions];
+		this->stateIndications = new uint_fast64_t[numberOfStates + 1]();
+
+		// First, we need to count how many backward transitions each state has.
+		for (uint_fast64_t i = 0; i < numberOfStates; ++i) {
+			for (uint_fast64_t j = choiceIndices->at(i); j < choiceIndices->at(i + 1); ++j) {
+				for (auto rowIt = transitionMatrix->beginConstColumnIterator(j); rowIt != transitionMatrix->endConstColumnIterator(j); ++rowIt) {
+					this->stateIndications[*rowIt + 1]++;
+				}
+			}
+		}
+
+		// Now compute the accumulated offsets.
+		for (uint_fast64_t i = 1; i < numberOfStates; i++) {
+			this->stateIndications[i] = this->stateIndications[i - 1] + this->stateIndications[i];
+		}
+
+		// Put a sentinel element at the end of the indices list. This way,
+		// for each state i the range of indices can be read off between
+		// state_indices_list[i] and state_indices_list[i + 1].
+		this->stateIndications[numberOfStates] = numberOfTransitions;
+
+		// Create an array that stores the next index for each state. Initially
+		// this corresponds to the previously computed accumulated offsets.
+		uint_fast64_t* nextIndicesList = new uint_fast64_t[numberOfStates];
+		std::copy(stateIndications, stateIndications + numberOfStates, nextIndicesList);
+
+		// Now we are ready to actually fill in the list of predecessors for
+		// every state. Again, we start by considering all but the last row.
+		for (uint_fast64_t i = 0; i < numberOfStates; i++) {
+			for (uint_fast64_t j = choiceIndices->at(i); j < choiceIndices->at(i + 1); ++j) {
+				for (auto rowIt = transitionMatrix->beginConstColumnIterator(j); rowIt != transitionMatrix->endConstColumnIterator(j); ++rowIt) {
+					this->successorList[nextIndicesList[*rowIt]++] = i;
+				}
+			}
+		}
+
+		// Now we can dispose of the auxiliary array.
+		delete[] nextIndicesList;
+	}
+
 	/*! A list of successors for *all* states. */
 	uint_fast64_t* successorList;
 
@@ -168,7 +246,7 @@ private:
 	 * Store the number of non-zero transition entries to determine the highest
 	 * index at which the predecessor_list may be accessed.
 	 */
-	uint_fast64_t numberOfNonZeroTransitions;
+	uint_fast64_t numberOfTransitions;
 };
 
 } // namespace models
diff --git a/src/models/Mdp.h b/src/models/Mdp.h
index 5b9d0157f..515a1842e 100644
--- a/src/models/Mdp.h
+++ b/src/models/Mdp.h
@@ -14,13 +14,9 @@
 #include <cstdlib>
 
 #include "AtomicPropositionsLabeling.h"
-#include "GraphTransitions.h"
 #include "src/storage/SparseMatrix.h"
-#include "src/exceptions/InvalidArgumentException.h"
-#include "src/utility/CommandLine.h"
 #include "src/utility/Settings.h"
-#include "src/models/AbstractModel.h"
-#include "src/parser/NonDeterministicSparseTransitionParser.h"
+#include "src/models/AbstractNondeterministicModel.h"
 
 namespace storm {
 
@@ -31,7 +27,7 @@ namespace models {
  * labeled with atomic propositions.
  */
 template <class T>
-class Mdp : public storm::models::AbstractModel {
+class Mdp : public storm::models::AbstractNondeterministicModel<T> {
 
 public:
 	//! Constructor
@@ -45,12 +41,10 @@ public:
 	 */
 	Mdp(std::shared_ptr<storm::storage::SparseMatrix<T>> probabilityMatrix,
 			std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling,
-			std::shared_ptr<std::vector<uint_fast64_t>> rowMapping,
-			std::shared_ptr<std::vector<T>> stateRewards = nullptr,
+			std::shared_ptr<std::vector<uint_fast64_t>> choiceIndices,
+			std::shared_ptr<std::vector<T>> stateRewardVector = nullptr,
 			std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix = nullptr)
-			: probabilityMatrix(probabilityMatrix), stateLabeling(stateLabeling), rowMapping(rowMapping),
-			  stateRewards(stateRewards), transitionRewardMatrix(transitionRewardMatrix),
-			  backwardTransitions(nullptr) {
+			: AbstractNondeterministicModel<T>(probabilityMatrix, stateLabeling, choiceIndices, stateRewardVector, transitionRewardMatrix) {
 		if (!this->checkValidityOfProbabilityMatrix()) {
 			LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
 			throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
@@ -62,12 +56,7 @@ public:
 	 * Copy Constructor. Performs a deep copy of the given MDP.
 	 * @param mdp A reference to the MDP that is to be copied.
 	 */
-	Mdp(const Mdp<T> &mdp) : probabilityMatrix(mdp.probabilityMatrix),
-			stateLabeling(mdp.stateLabeling), rowMapping(mdp.rowMapping), stateRewards(mdp.stateRewards),
-			transitionRewardMatrix(mdp.transitionRewardMatrix) {
-		if (mdp.backwardTransitions != nullptr) {
-			this->backwardTransitions = new storm::models::GraphTransitions<T>(*mdp.backwardTransitions);
-		}
+	Mdp(const Mdp<T> &mdp) : AbstractNondeterministicModel<T>(mdp) {
 		if (!this->checkValidityOfProbabilityMatrix()) {
 			LOG4CPLUS_ERROR(logger, "Probability matrix is invalid.");
 			throw storm::exceptions::InvalidArgumentException() << "Probability matrix is invalid.";
@@ -76,130 +65,13 @@ public:
 
 	//! Destructor
 	/*!
-	 * Destructor. Frees the matrix and labeling associated with this MDP.
+	 * Destructor.
 	 */
 	~Mdp() {
-		if (this->backwardTransitions != nullptr) {
-			delete this->backwardTransitions;
-		}
-	}
-	
-	/*!
-	 * Returns the state space size of the MDP.
-	 * @return The size of the state space of the MDP.
-	 */
-	uint_fast64_t getNumberOfStates() const {
-		return this->probabilityMatrix->getColumnCount();
+		// Intentionally left empty.
 	}
 
-	/*!
-	 * Returns the number of (non-zero) transitions of the MDP.
-	 * @return The number of (non-zero) transitions of the MDP.
-	 */
-	uint_fast64_t getNumberOfTransitions() const {
-		return this->probabilityMatrix->getNonZeroEntryCount();
-	}
-
-	/*!
-	 * Returns a bit vector in which exactly those bits are set to true that
-	 * correspond to a state labeled with the given atomic proposition.
-	 * @param ap The atomic proposition for which to get the bit vector.
-	 * @return A bit vector in which exactly those bits are set to true that
-	 * correspond to a state labeled with the given atomic proposition.
-	 */
-	storm::storage::BitVector* getLabeledStates(std::string ap) const {
-		return this->stateLabeling->getAtomicProposition(ap);
-	}
-
-	/*!
-	 * Returns a pointer to the matrix representing the transition probability
-	 * function.
-	 * @return A pointer to the matrix representing the transition probability
-	 * function.
-	 */
-	std::shared_ptr<storm::storage::SparseMatrix<T>> getTransitionProbabilityMatrix() const {
-		return this->probabilityMatrix;
-	}
-
-	/*!
-	 * Returns a pointer to the matrix representing the transition rewards.
-	 * @return A pointer to the matrix representing the transition rewards.
-	 */
-	std::shared_ptr<storm::storage::SparseMatrix<T>> getTransitionRewardMatrix() const {
-		return this->transitionRewardMatrix;
-	}
-
-	/*!
-	 * Returns a pointer to the vector representing the state rewards.
-	 * @return A pointer to the vector representing the state rewards.
-	 */
-	std::shared_ptr<std::vector<T>> getStateRewards() const {
-		return this->stateRewards;
-	}
-
-	/*!
-	 *
-	 */
-	std::set<std::string> const getPropositionsForState(uint_fast64_t const &state) const {
-		return stateLabeling->getPropositionsForState(state);
-	}
-
-	/*!
-	 * Retrieves a reference to the backwards transition relation.
-	 * @return A reference to the backwards transition relation.
-	 */
-	storm::models::GraphTransitions<T>& getBackwardTransitions() {
-		if (this->backwardTransitions == nullptr) {
-			this->backwardTransitions = new storm::models::GraphTransitions<T>(this->probabilityMatrix, false);
-		}
-		return *this->backwardTransitions;
-	}
-
-	/*!
-	 * Retrieves whether this MDP has a state reward model.
-	 * @return True if this MDP has a state reward model.
-	 */
-	bool hasStateRewards() {
-		return this->stateRewards != nullptr;
-	}
-
-	/*!
-	 * Retrieves whether this MDP has a transition reward model.
-	 * @return True if this MDP has a transition reward model.
-	 */
-	bool hasTransitionRewards() {
-		return this->transitionRewardMatrix != nullptr;
-	}
-
-	/*!
-	 * Retrieves whether the given atomic proposition is a valid atomic proposition in this model.
-	 * @param atomicProposition The atomic proposition to be checked for validity.
-	 * @return True if the given atomic proposition is valid in this model.
-	 */
-	bool hasAtomicProposition(std::string const& atomicProposition) {
-		return this->stateLabeling->containsAtomicProposition(atomicProposition);
-	}
-
-	/*!
-	 * Prints information about the model to the specified stream.
-	 * @param out The stream the information is to be printed to.
-	 */
-	void printModelInformationToStream(std::ostream& out) const {
-		storm::utility::printSeparationLine(out);
-		out << std::endl;
-		out << "Model type: \t\tMDP" << std::endl;
-		out << "States: \t\t" << this->getNumberOfStates() << std::endl;
-		out << "Transitions: \t\t" << this->getNumberOfTransitions() << std::endl;
-		this->stateLabeling->printAtomicPropositionsInformationToStream(out);
-		out << "Size in memory: \t"
-			<< (this->probabilityMatrix->getSizeInMemory() +
-				this->stateLabeling->getSizeInMemory() +
-				sizeof(*this))/1024 << " kbytes" << std::endl;
-		out << std::endl;
-		storm::utility::printSeparationLine(out);
-	}
-	
-	storm::models::ModelType getType() {
+	storm::models::ModelType getType() const {
 		return MDP;
 	}
 
@@ -214,34 +86,13 @@ private:
 		// Get the settings object to customize linear solving.
 		storm::settings::Settings* s = storm::settings::instance();
 		double precision = s->get<double>("precision");
-		for (uint_fast64_t row = 0; row < this->probabilityMatrix->getRowCount(); row++) {
-			T sum = this->probabilityMatrix->getRowSum(row);
+		for (uint_fast64_t row = 0; row < this->getTransitionMatrix()->getRowCount(); row++) {
+			T sum = this->getTransitionMatrix()->getRowSum(row);
 			if (sum == 0) continue;
 			if (std::abs(sum - 1) > precision) return false;
 		}
 		return true;
 	}
-
-	/*! A matrix representing the transition probability function of the MDP. */
-	std::shared_ptr<storm::storage::SparseMatrix<T>> probabilityMatrix;
-
-	/*! The labeling of the states of the MDP. */
-	std::shared_ptr<storm::models::AtomicPropositionsLabeling> stateLabeling;
-	
-	/*! The mapping from states to rows. */
-	std::shared_ptr<std::vector<uint_fast64_t>> rowMapping;
-
-	/*! The state-based rewards of the MDP. */
-	std::shared_ptr<std::vector<T>> stateRewards;
-
-	/*! The transition-based rewards of the MDP. */
-	std::shared_ptr<storm::storage::SparseMatrix<T>> transitionRewardMatrix;
-
-	/*!
-	 * A data structure that stores the predecessors for all states. This is
-	 * needed for backwards directed searches.
-	 */
-	storm::models::GraphTransitions<T>* backwardTransitions;
 };
 
 } // namespace models
diff --git a/src/parser/AutoParser.cpp b/src/parser/AutoParser.cpp
deleted file mode 100644
index 6c0d5cc40..000000000
--- a/src/parser/AutoParser.cpp
+++ /dev/null
@@ -1,79 +0,0 @@
-#include "src/parser/AutoParser.h"
-
-#include <string>
-#include <cctype>
-
-#include "src/exceptions/WrongFileFormatException.h"
-#include "src/models/AbstractModel.h"
-#include "src/parser/DeterministicModelParser.h"
-#include "src/parser/NonDeterministicModelParser.h"
-
-namespace storm {
-namespace parser {
-
-AutoParser::AutoParser(std::string const & transitionSystemFile, std::string const & labelingFile,
-	std::string const & stateRewardFile, std::string const & transitionRewardFile)
-	: model(nullptr) {
-	storm::models::ModelType type = this->analyzeHint(transitionSystemFile);
-
-	if (type == storm::models::Unknown) {
-		LOG4CPLUS_ERROR(logger, "Could not determine file type of " << transitionSystemFile << ".");
-		LOG4CPLUS_ERROR(logger, "The first line of the file should contain a format hint. Please fix your file and try again.");
-		throw storm::exceptions::WrongFileFormatException() << "Could not determine type of file " << transitionSystemFile;
-	} else {
-		LOG4CPLUS_INFO(logger, "Model type seems to be " << type);
-	}
-
-	// Do actual parsing
-	switch (type) {
-		case storm::models::DTMC: {
-			DeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
-			this->model = parser.getDtmc();
-			break;
-		}
-		case storm::models::CTMC: {
-			DeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
-			this->model = parser.getCtmc();
-			break;
-		}
-		case storm::models::MDP: {
-			NonDeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
-			this->model = parser.getMdp();
-			break;
-		}
-		case storm::models::CTMDP: {
-			NonDeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
-			this->model = parser.getCtmdp();
-			break;
-		}
-		default: ;  // Unknown
-	}
-
-	
-	if (!this->model) {
-		LOG4CPLUS_WARN(logger, "Model is still null.");
-	}
-}
-
-storm::models::ModelType AutoParser::analyzeHint(const std::string& filename) {
-	storm::models::ModelType hintType = storm::models::Unknown;
-	// Open file
-	MappedFile file(filename.c_str());
-	char* buf = file.data;
-
-	// parse hint
-	char hint[128];
-	sscanf(buf, "%s\n", hint);
-	for (char* c = hint; *c != '\0'; c++) *c = toupper(*c);
-
-	// check hint
-	if (strncmp(hint, "DTMC", sizeof(hint)) == 0) hintType = storm::models::DTMC;
-	else if (strncmp(hint, "CTMC", sizeof(hint)) == 0) hintType = storm::models::CTMC;
-	else if (strncmp(hint, "MDP", sizeof(hint)) == 0) hintType = storm::models::MDP;
-	else if (strncmp(hint, "CTMDP", sizeof(hint)) == 0) hintType = storm::models::CTMDP;
-
-	return hintType;
-}
-
-}  // namespace parser
-}  // namespace storm
diff --git a/src/parser/AutoParser.h b/src/parser/AutoParser.h
index 1424cb9b7..f7331da7e 100644
--- a/src/parser/AutoParser.h
+++ b/src/parser/AutoParser.h
@@ -4,11 +4,19 @@
 #include "src/parser/Parser.h"
 #include "src/models/AbstractModel.h"
 
+#include "src/exceptions/WrongFileFormatException.h"
+#include "src/models/AbstractModel.h"
+#include "src/parser/DeterministicModelParser.h"
+#include "src/parser/NondeterministicModelParser.h"
+
 #include <memory>
 #include <iostream>
 #include <utility>
+#include <string>
+#include <cctype>
 
 namespace storm {
+
 namespace parser {
 
 /*!
@@ -21,10 +29,51 @@ namespace parser {
  *	When the files are parsed successfully, the parsed ModelType and Model
  *	can be obtained via getType() and getModel<ModelClass>().
  */
+template<class T>
 class AutoParser : Parser {
 	public:
 		AutoParser(std::string const & transitionSystemFile, std::string const & labelingFile,
-				std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "");
+				std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "") : model(nullptr) {
+			storm::models::ModelType type = this->analyzeHint(transitionSystemFile);
+
+			if (type == storm::models::Unknown) {
+				LOG4CPLUS_ERROR(logger, "Could not determine file type of " << transitionSystemFile << ".");
+				LOG4CPLUS_ERROR(logger, "The first line of the file should contain a format hint. Please fix your file and try again.");
+				throw storm::exceptions::WrongFileFormatException() << "Could not determine type of file " << transitionSystemFile;
+			} else {
+				LOG4CPLUS_INFO(logger, "Model type seems to be " << type);
+			}
+
+			// Do actual parsing
+			switch (type) {
+				case storm::models::DTMC: {
+					DeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
+					this->model = parser.getDtmc();
+					break;
+				}
+				case storm::models::CTMC: {
+					DeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
+					this->model = parser.getCtmc();
+					break;
+				}
+				case storm::models::MDP: {
+					NondeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
+					this->model = parser.getMdp();
+					break;
+				}
+				case storm::models::CTMDP: {
+					NondeterministicModelParser parser(transitionSystemFile, labelingFile, stateRewardFile, transitionRewardFile);
+					this->model = parser.getCtmdp();
+					break;
+				}
+				default: ;  // Unknown
+			}
+
+
+			if (!this->model) {
+				LOG4CPLUS_WARN(logger, "Model is still null.");
+			}
+		}
 		
 		/*!
 		 *	@brief 	Returns the type of model that was parsed.
@@ -39,7 +88,7 @@ class AutoParser : Parser {
 		 */
 		template <typename Model>
 		std::shared_ptr<Model> getModel() {
-			return this->model->as<Model>();
+			return this->model->template as<Model>();
 		}
 		
 	private:
@@ -47,15 +96,34 @@ class AutoParser : Parser {
 		/*!
 		 *	@brief	Open file and read file format hint.
 		 */
-		storm::models::ModelType analyzeHint(const std::string& filename);
+		storm::models::ModelType analyzeHint(const std::string& filename) {
+			storm::models::ModelType hintType = storm::models::Unknown;
+			// Open file
+			MappedFile file(filename.c_str());
+			char* buf = file.data;
+
+			// parse hint
+			char hint[128];
+			sscanf(buf, "%s\n", hint);
+			for (char* c = hint; *c != '\0'; c++) *c = toupper(*c);
+
+			// check hint
+			if (strncmp(hint, "DTMC", sizeof(hint)) == 0) hintType = storm::models::DTMC;
+			else if (strncmp(hint, "CTMC", sizeof(hint)) == 0) hintType = storm::models::CTMC;
+			else if (strncmp(hint, "MDP", sizeof(hint)) == 0) hintType = storm::models::MDP;
+			else if (strncmp(hint, "CTMDP", sizeof(hint)) == 0) hintType = storm::models::CTMDP;
+
+			return hintType;
+		}
 		
 		/*!
 		 *	@brief	Pointer to a parser that has parsed the given transition system.
 		 */
-		std::shared_ptr<storm::models::AbstractModel> model;
+		std::shared_ptr<storm::models::AbstractModel<T>> model;
 };
 
 } // namespace parser
+
 } // namespace storm
 
 #endif /* STORM_PARSER_AUTOPARSER_H_ */
diff --git a/src/parser/NonDeterministicModelParser.cpp b/src/parser/NondeterministicModelParser.cpp
similarity index 87%
rename from src/parser/NonDeterministicModelParser.cpp
rename to src/parser/NondeterministicModelParser.cpp
index 017d3b31e..036f0dc9b 100644
--- a/src/parser/NonDeterministicModelParser.cpp
+++ b/src/parser/NondeterministicModelParser.cpp
@@ -10,7 +10,7 @@
 #include <string>
 #include <vector>
 
-#include "src/parser/NonDeterministicSparseTransitionParser.h"
+#include "src/parser/NondeterministicSparseTransitionParser.h"
 #include "src/parser/AtomicPropositionLabelingParser.h"
 #include "src/parser/SparseStateRewardParser.h"
 
@@ -27,9 +27,9 @@ namespace parser {
  * @param stateRewardFile String containing the location of the state reward file (...srew)
  * @param transitionRewardFile String containing the location of the transition reward file (...trew)
  */
-NonDeterministicModelParser::NonDeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile,
+NondeterministicModelParser::NondeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile,
 		std::string const & stateRewardFile, std::string const & transitionRewardFile) {
-	storm::parser::NonDeterministicSparseTransitionParser tp(transitionSystemFile);
+	storm::parser::NondeterministicSparseTransitionParser tp(transitionSystemFile);
 	uint_fast64_t stateCount = tp.getMatrix()->getRowCount();
 
 	storm::parser::AtomicPropositionLabelingParser lp(stateCount, labelingFile);
@@ -38,7 +38,7 @@ NonDeterministicModelParser::NonDeterministicModelParser(std::string const & tra
 		this->stateRewards = srp.getStateRewards();
 	}
 	if (transitionRewardFile != "") {
-		storm::parser::NonDeterministicSparseTransitionParser trp(transitionRewardFile);
+		storm::parser::NondeterministicSparseTransitionParser trp(transitionRewardFile);
 		this->transitionRewardMatrix = trp.getMatrix();
 	}
 
diff --git a/src/parser/NonDeterministicModelParser.h b/src/parser/NondeterministicModelParser.h
similarity index 93%
rename from src/parser/NonDeterministicModelParser.h
rename to src/parser/NondeterministicModelParser.h
index 379fdf07c..bdc4c42d4 100644
--- a/src/parser/NonDeterministicModelParser.h
+++ b/src/parser/NondeterministicModelParser.h
@@ -13,6 +13,7 @@
 #include "src/models/Ctmdp.h"
 
 namespace storm {
+
 namespace parser {
 
 /*!
@@ -23,9 +24,9 @@ namespace parser {
  *
  *	@note The labeling representation in the file may use at most as much nodes as are specified in the mdp.
  */
-class NonDeterministicModelParser: public storm::parser::Parser {
+class NondeterministicModelParser: public storm::parser::Parser {
 public:
-	NonDeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile,
+	NondeterministicModelParser(std::string const & transitionSystemFile, std::string const & labelingFile,
 			std::string const & stateRewardFile = "", std::string const & transitionRewardFile = "");
 
 	std::shared_ptr<storm::models::Mdp<double>> getMdp() {
@@ -58,5 +59,7 @@ private:
 };
 
 } /* namespace parser */
+
 } /* namespace storm */
+
 #endif /* STORM_PARSER_NONDETERMINISTICMODELPARSER_H_ */
diff --git a/src/parser/NonDeterministicSparseTransitionParser.cpp b/src/parser/NondeterministicSparseTransitionParser.cpp
similarity index 96%
rename from src/parser/NonDeterministicSparseTransitionParser.cpp
rename to src/parser/NondeterministicSparseTransitionParser.cpp
index f6b70e719..a17f48552 100644
--- a/src/parser/NonDeterministicSparseTransitionParser.cpp
+++ b/src/parser/NondeterministicSparseTransitionParser.cpp
@@ -5,7 +5,7 @@
  *		Author: Gereon Kremer
  */
 
-#include "src/parser/NonDeterministicSparseTransitionParser.h"
+#include "src/parser/NondeterministicSparseTransitionParser.h"
 
 #include <errno.h>
 #include <time.h>
@@ -49,7 +49,7 @@ namespace parser {
  *	@param maxnode Is set to highest id of all nodes.
  *	@return The number of non-zero elements.
  */
-uint_fast64_t NonDeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode) {
+uint_fast64_t NondeterministicSparseTransitionParser::firstPass(char* buf, uint_fast64_t& choices, int_fast64_t& maxnode) {
 	/*
 	 *	Check file header and extract number of transitions.
 	 */
@@ -154,7 +154,7 @@ uint_fast64_t NonDeterministicSparseTransitionParser::firstPass(char* buf, uint_
  *	@return a pointer to the created sparse matrix.
  */
 
-NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(std::string const &filename)
+NondeterministicSparseTransitionParser::NondeterministicSparseTransitionParser(std::string const &filename)
 	: matrix(nullptr) {
 	/*
 	 *	Enforce locale where decimal point is '.'.
@@ -214,7 +214,7 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
 	/*
 	 *	Create row mapping.
 	 */
-	this->rowMapping = std::shared_ptr<std::vector<uint_fast64_t>>(new std::vector<uint_fast64_t>(maxnode+1,0));
+	this->rowMapping = std::shared_ptr<std::vector<uint_fast64_t>>(new std::vector<uint_fast64_t>(maxnode+2,0));
 
 	/*
 	 *	Parse file content.
@@ -288,6 +288,8 @@ NonDeterministicSparseTransitionParser::NonDeterministicSparseTransitionParser(s
 		curRow++;
 	}
 
+	this->rowMapping->at(maxnode+1) = curRow;
+
 	if (!fixDeadlocks && hadDeadlocks) throw storm::exceptions::WrongFileFormatException() << "Some of the nodes had deadlocks. You can use --fix-deadlocks to insert self-loops on the fly.";
 
 	/*
diff --git a/src/parser/NonDeterministicSparseTransitionParser.h b/src/parser/NondeterministicSparseTransitionParser.h
similarity index 88%
rename from src/parser/NonDeterministicSparseTransitionParser.h
rename to src/parser/NondeterministicSparseTransitionParser.h
index a0d9ea50a..209c0e7a0 100644
--- a/src/parser/NonDeterministicSparseTransitionParser.h
+++ b/src/parser/NondeterministicSparseTransitionParser.h
@@ -17,9 +17,9 @@ namespace parser {
  *	@brief	Load a nondeterministic transition system from file and create a
  *	sparse adjacency matrix whose entries represent the weights of the edges
  */
-class NonDeterministicSparseTransitionParser : public Parser {
+class NondeterministicSparseTransitionParser : public Parser {
 	public:
-		NonDeterministicSparseTransitionParser(std::string const &filename);
+		NondeterministicSparseTransitionParser(std::string const &filename);
 		
 		inline std::shared_ptr<storm::storage::SparseMatrix<double>> getMatrix() const {
 			return this->matrix;
diff --git a/src/solver/GraphAnalyzer.h b/src/solver/GraphAnalyzer.h
deleted file mode 100644
index 70b6b10f5..000000000
--- a/src/solver/GraphAnalyzer.h
+++ /dev/null
@@ -1,155 +0,0 @@
-/*
- * GraphAnalyzer.h
- *
- *  Created on: 28.11.2012
- *      Author: Christian Dehnert
- */
-
-#ifndef STORM_SOLVER_GRAPHANALYZER_H_
-#define STORM_SOLVER_GRAPHANALYZER_H_
-
-#include "src/models/Dtmc.h"
-#include "src/exceptions/InvalidArgumentException.h"
-
-#include "log4cplus/logger.h"
-#include "log4cplus/loggingmacros.h"
-
-extern log4cplus::Logger logger;
-
-namespace storm {
-
-namespace solver {
-
-class GraphAnalyzer {
-public:
-	/*!
-	 * Performs a backwards depth-first search trough the underlying graph structure
-	 * of the given model to determine which states of the model can reach one
-	 * of the given target states whilst always staying in the set of filter states
-	 * before. The resulting states are written to the given bit vector.
-	 * @param model The model whose graph structure to search.
-	 * @param phiStates A bit vector of all states satisfying phi.
-	 * @param psiStates A bit vector of all states satisfying psi.
-	 * @param existsPhiUntilPsiStates A pointer to the result of the search for states that possess
-	 * a paths satisfying phi until psi.
-	 */
-	template <class T>
-	static void getExistsPhiUntilPsiStates(storm::models::Dtmc<T>& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, storm::storage::BitVector* existsPhiUntilPsiStates) {
-		// Check for valid parameter.
-		if (existsPhiUntilPsiStates == nullptr) {
-			LOG4CPLUS_ERROR(logger, "Parameter 'existsPhiUntilPhiStates' must not be null.");
-			throw storm::exceptions::InvalidArgumentException("Parameter 'existsPhiUntilPhiStates' must not be null.");
-		}
-
-		// Get the backwards transition relation from the model to ease the search.
-		storm::models::GraphTransitions<T>& backwardTransitions = model.getBackwardTransitions();
-
-		// Add all psi states as the already satisfy the condition.
-		*existsPhiUntilPsiStates |= psiStates;
-
-		// Initialize the stack used for the DFS with the states
-		std::vector<uint_fast64_t> stack;
-		stack.reserve(model.getNumberOfStates());
-		psiStates.getList(stack);
-
-		// Perform the actual DFS.
-		while(!stack.empty()) {
-			uint_fast64_t currentState = stack.back();
-			stack.pop_back();
-
-			for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) {
-				if (phiStates.get(*it) && !existsPhiUntilPsiStates->get(*it)) {
-					existsPhiUntilPsiStates->set(*it, true);
-					stack.push_back(*it);
-				}
-			}
-		}
-	}
-
-	/*!
-	 * Computes the set of states of the given model for which all paths lead to
-	 * the given set of target states and only visit states from the filter set
-	 * before. In order to do this, it uses the given set of states that
-	 * characterizes the states that possess at least one path to a target state.
-	 * The results are written to the given bit vector.
-	 * @param model The model whose graph structure to search.
-	 * @param phiStates A bit vector of all states satisfying phi.
-	 * @param psiStates A bit vector of all states satisfying psi.
-	 * @param existsPhiUntilPsiStates A reference to a bit vector of states that possess a path
-	 * satisfying phi until psi.
-	 * @param alwaysPhiUntilPsiStates A pointer to the result of the search for states that only
-	 * have paths satisfying phi until psi.
-	 */
-	template <class T>
-	static void getAlwaysPhiUntilPsiStates(storm::models::Dtmc<T>& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, const storm::storage::BitVector& existsPhiUntilPsiStates, storm::storage::BitVector* alwaysPhiUntilPsiStates) {
-		// Check for valid parameter.
-		if (alwaysPhiUntilPsiStates == nullptr) {
-			LOG4CPLUS_ERROR(logger, "Parameter 'alwaysPhiUntilPhiStates' must not be null.");
-			throw storm::exceptions::InvalidArgumentException("Parameter 'alwaysPhiUntilPhiStates' must not be null.");
-		}
-
-		GraphAnalyzer::getExistsPhiUntilPsiStates(model, ~psiStates, ~existsPhiUntilPsiStates, alwaysPhiUntilPsiStates);
-		alwaysPhiUntilPsiStates->complement();
-	}
-
-	/*!
-	 * Computes the set of states of the given model for which all paths lead to
-	 * the given set of target states and only visit states from the filter set
-	 * before. The results are written to the given bit vector.
-	 * @param model The model whose graph structure to search.
-	 * @param phiStates A bit vector of all states satisfying phi.
-	 * @param psiStates A bit vector of all states satisfying psi.
-	 * @param alwaysPhiUntilPsiStates A pointer to the result of the search for states that only
-	 * have paths satisfying phi until psi.
-	 */
-	template <class T>
-	static void getAlwaysPhiUntilPsiStates(storm::models::Dtmc<T>& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, storm::storage::BitVector* alwaysPhiUntilPsiStates) {
-		// Check for valid parameter.
-		if (alwaysPhiUntilPsiStates == nullptr) {
-			LOG4CPLUS_ERROR(logger, "Parameter 'alwaysPhiUntilPhiStates' must not be null.");
-			throw storm::exceptions::InvalidArgumentException("Parameter 'alwaysPhiUntilPhiStates' must not be null.");
-		}
-
-		storm::storage::BitVector existsPhiUntilPsiStates(model.getNumberOfStates());
-		GraphAnalyzer::getExistsPhiUntilPsiStates(model, phiStates, psiStates, &existsPhiUntilPsiStates);
-		GraphAnalyzer::getExistsPhiUntilPsiStates(model, ~psiStates, ~existsPhiUntilPsiStates, alwaysPhiUntilPsiStates);
-		alwaysPhiUntilPsiStates->complement();
-	}
-
-
-	/*!
-	 * Computes the set of states of the given model for which all paths lead to
-	 * the given set of target states and only visit states from the filter set
-	 * before.
-	 * @param model The model whose graph structure to search.
-	 * @param phiStates A bit vector of all states satisfying phi.
-	 * @param psiStates A bit vector of all states satisfying psi.
-	 * @param existsPhiUntilPsiStates A pointer to the result of the search for states that possess
-	 * a path satisfying phi until psi.
-	 * @param alwaysPhiUntilPsiStates A pointer to the result of the search for states that only
-	 * have paths satisfying phi until psi.
-	 */
-	template <class T>
-	static void getPhiUntilPsiStates(storm::models::Dtmc<T>& model, const storm::storage::BitVector& phiStates, const storm::storage::BitVector& psiStates, storm::storage::BitVector* existsPhiUntilPsiStates, storm::storage::BitVector* alwaysPhiUntilPsiStates) {
-		// Check for valid parameters.
-		if (existsPhiUntilPsiStates == nullptr) {
-			LOG4CPLUS_ERROR(logger, "Parameter 'existsPhiUntilPhiStates' must not be null.");
-			throw storm::exceptions::InvalidArgumentException("Parameter 'existsPhiUntilPhiStates' must not be null.");
-		}
-		if (alwaysPhiUntilPsiStates == nullptr) {
-			LOG4CPLUS_ERROR(logger, "Parameter 'alwaysPhiUntilPhiStates' must not be null.");
-			throw storm::exceptions::InvalidArgumentException("Parameter 'alwaysPhiUntilPhiStates' must not be null.");
-		}
-
-		// Perform search.
-		GraphAnalyzer::getExistsPhiUntilPsiStates(model, phiStates, psiStates, existsPhiUntilPsiStates);
-		GraphAnalyzer::getAlwaysPhiUntilPsiStates(model, phiStates, psiStates, *existsPhiUntilPsiStates, alwaysPhiUntilPsiStates);
-	}
-
-};
-
-} // namespace solver
-
-} // namespace storm
-
-#endif /* STORM_SOLVER_GRAPHANALYZER_H_ */
diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h
index 94d663d3b..a35df8b47 100644
--- a/src/storage/SparseMatrix.h
+++ b/src/storage/SparseMatrix.h
@@ -476,7 +476,7 @@ public:
 	 * Returns a pointer to the value storage of the matrix.
 	 * @return A pointer to the value storage of the matrix.
 	 */
-	std::vector<T> const & getStoragePointer() const {
+	std::vector<T> const& getStorage() const {
 		return valueStorage;
 	}
 
@@ -486,7 +486,7 @@ public:
 	 * @return A pointer to the array that stores the start indices of non-zero
 	 * entries in the value storage for each row.
 	 */
-	std::vector<uint_fast64_t> const & getRowIndicationsPointer() const {
+	std::vector<uint_fast64_t> const& getRowIndications() const {
 		return rowIndications;
 	}
 
@@ -496,7 +496,7 @@ public:
 	 * @return A pointer to an array that stores the column of each non-zero
 	 * element.
 	 */
-	std::vector<uint_fast64_t> const & getColumnIndicationsPointer() const {
+	std::vector<uint_fast64_t> const& getColumnIndications() const {
 		return columnIndications;
 	}
 
diff --git a/src/storm.cpp b/src/storm.cpp
index 2015e85e4..26fe8d15a 100644
--- a/src/storm.cpp
+++ b/src/storm.cpp
@@ -26,7 +26,6 @@
 #include "src/modelchecker/GmmxxDtmcPrctlModelChecker.h"
 #include "src/parser/AutoParser.h"
 #include "src/parser/PrctlParser.h"
-#include "src/solver/GraphAnalyzer.h"
 #include "src/utility/Settings.h"
 #include "src/formula/Formulas.h"
 
@@ -211,7 +210,7 @@ void testCheckingSynchronousLeader(storm::models::Dtmc<double>& dtmc, uint_fast6
  */
 void testChecking() {
 	storm::settings::Settings* s = storm::settings::instance();
-	storm::parser::AutoParser parser(s->getString("trafile"), s->getString("labfile"), s->getString("staterew"), s->getString("transrew"));
+	storm::parser::AutoParser<double> parser(s->getString("trafile"), s->getString("labfile"), s->getString("staterew"), s->getString("transrew"));
 
 	if (parser.getType() == storm::models::DTMC) {
 		std::shared_ptr<storm::models::Dtmc<double>> dtmc = parser.getModel<storm::models::Dtmc<double>>();
diff --git a/src/utility/GraphAnalyzer.h b/src/utility/GraphAnalyzer.h
new file mode 100644
index 000000000..4b1db5178
--- /dev/null
+++ b/src/utility/GraphAnalyzer.h
@@ -0,0 +1,242 @@
+/*
+ * GraphAnalyzer.h
+ *
+ *  Created on: 28.11.2012
+ *      Author: Christian Dehnert
+ */
+
+#ifndef STORM_UTILITY_GRAPHANALYZER_H_
+#define STORM_UTILITY_GRAPHANALYZER_H_
+
+#include "src/models/AbstractDeterministicModel.h"
+#include "src/models/AbstractNondeterministicModel.h"
+#include "src/exceptions/InvalidArgumentException.h"
+
+#include "log4cplus/logger.h"
+#include "log4cplus/loggingmacros.h"
+
+extern log4cplus::Logger logger;
+
+namespace storm {
+
+namespace utility {
+
+class GraphAnalyzer {
+public:
+	/*!
+	 * Computes the sets of states that have probability 0 or 1, respectively, of satisfying phi until psi in a
+	 * deterministic model.
+	 * @param model The model whose graph structure to search.
+	 * @param phiStates The set of all states satisfying phi.
+	 * @param psiStates The set of all states satisfying psi.
+	 * @param statesWithProbability0 A pointer to a bit vector that is initially empty and will contain all states with
+	 * probability 0 after the invocation of the function.
+	 * @param statesWithProbability1 A pointer to a bit vector that is initially empty and will contain all states with
+	 * probability 1 after the invocation of the function.
+	 */
+	template <class T>
+	static void performProb01(storm::models::AbstractDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) {
+		// Check for valid parameters.
+		if (statesWithProbability0 == nullptr) {
+			LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability0' must not be null.");
+			throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability0' must not be null.");
+		}
+		if (statesWithProbability1 == nullptr) {
+			LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability1' must not be null.");
+			throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability1' must not be null.");
+		}
+
+		// Perform the actual search.
+		GraphAnalyzer::performProbGreater0(model, phiStates, psiStates, statesWithProbability0);
+		GraphAnalyzer::performProb1(model, phiStates, psiStates, *statesWithProbability0, statesWithProbability1);
+		statesWithProbability0->complement();
+	}
+
+	/*!
+	 * Performs a backwards depth-first search trough the underlying graph structure
+	 * of the given model to determine which states of the model have a positive probability
+	 * of satisfying phi until psi. The resulting states are written to the given bit vector.
+	 * @param model The model whose graph structure to search.
+	 * @param phiStates A bit vector of all states satisfying phi.
+	 * @param psiStates A bit vector of all states satisfying psi.
+	 * @param statesWithProbabilityGreater0 A pointer to the result of the search for states that possess
+	 * a positive probability of satisfying phi until psi.
+	 */
+	template <class T>
+	static void performProbGreater0(storm::models::AbstractDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbabilityGreater0) {
+		// Check for valid parameter.
+		if (statesWithProbabilityGreater0 == nullptr) {
+			LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbabilityGreater0' must not be null.");
+			throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbabilityGreater0' must not be null.");
+		}
+
+		// Get the backwards transition relation from the model to ease the search.
+		storm::models::GraphTransitions<T> backwardTransitions(model.getTransitionMatrix(), false);
+
+		// Add all psi states as the already satisfy the condition.
+		*statesWithProbabilityGreater0 |= psiStates;
+
+		// Initialize the stack used for the DFS with the states
+		std::vector<uint_fast64_t> stack;
+		stack.reserve(model.getNumberOfStates());
+		psiStates.getList(stack);
+
+		// Perform the actual DFS.
+		while(!stack.empty()) {
+			uint_fast64_t currentState = stack.back();
+			stack.pop_back();
+
+			for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) {
+				if (phiStates.get(*it) && !statesWithProbabilityGreater0->get(*it)) {
+					statesWithProbabilityGreater0->set(*it, true);
+					stack.push_back(*it);
+				}
+			}
+		}
+	}
+
+	/*!
+	 * Computes the set of states of the given model for which all paths lead to
+	 * the given set of target states and only visit states from the filter set
+	 * before. In order to do this, it uses the given set of states that
+	 * characterizes the states that possess at least one path to a target state.
+	 * The results are written to the given bit vector.
+	 * @param model The model whose graph structure to search.
+	 * @param phiStates A bit vector of all states satisfying phi.
+	 * @param psiStates A bit vector of all states satisfying psi.
+	 * @param statesWithProbabilityGreater0 A reference to a bit vector of states that possess a positive
+	 * probability mass of satisfying phi until psi.
+	 * @param alwaysPhiUntilPsiStates A pointer to the result of the search for states that only
+	 * have paths satisfying phi until psi.
+	 */
+	template <class T>
+	static void performProb1(storm::models::AbstractDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector const& statesWithProbabilityGreater0, storm::storage::BitVector* statesWithProbability1) {
+		// Check for valid parameter.
+		if (statesWithProbability1 == nullptr) {
+			LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability1' must not be null.");
+			throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability1' must not be null.");
+		}
+
+		GraphAnalyzer::performProbGreater0(model, ~psiStates, ~statesWithProbabilityGreater0, statesWithProbability1);
+		statesWithProbability1->complement();
+	}
+
+	/*!
+	 * Computes the set of states of the given model for which all paths lead to
+	 * the given set of target states and only visit states from the filter set
+	 * before. In order to do this, it uses the given set of states that
+	 * characterizes the states that possess at least one path to a target state.
+	 * The results are written to the given bit vector.
+	 * @param model The model whose graph structure to search.
+	 * @param phiStates A bit vector of all states satisfying phi.
+	 * @param psiStates A bit vector of all states satisfying psi.
+	 * @param alwaysPhiUntilPsiStates A pointer to the result of the search for states that only
+	 * have paths satisfying phi until psi.
+	 */
+	template <class T>
+	static void performProb1(storm::models::AbstractDeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) {
+		// Check for valid parameter.
+		if (statesWithProbability1 == nullptr) {
+			LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability1' must not be null.");
+			throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability1' must not be null.");
+		}
+
+		storm::storage::BitVector* statesWithProbabilityGreater0 = new storm::storage::BitVector(model.getNumberOfStates());
+		GraphAnalyzer::performProbGreater0(model, phiStates, psiStates, statesWithProbabilityGreater0);
+		GraphAnalyzer::performProbGreater0(model, ~psiStates, ~(*statesWithProbabilityGreater0), statesWithProbability1);
+		delete statesWithProbabilityGreater0;
+		statesWithProbability1->complement();
+	}
+
+	template <class T>
+	static void performProb01Max(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) {
+		// Check for valid parameters.
+		if (statesWithProbability0 == nullptr) {
+			LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability0' must not be null.");
+			throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability0' must not be null.");
+		}
+		if (statesWithProbability1 == nullptr) {
+			LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability1' must not be null.");
+			throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability1' must not be null.");
+		}
+
+		// Perform the actual search.
+		GraphAnalyzer::performProb0A(model, phiStates, psiStates, statesWithProbability0);
+		GraphAnalyzer::performProb1E(model, phiStates, psiStates, statesWithProbability1);
+	}
+
+	template <class T>
+	static void performProb0A(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) {
+		// Check for valid parameter.
+		if (statesWithProbability0 == nullptr) {
+			LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability0' must not be null.");
+			throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability0' must not be null.");
+		}
+
+		// Get the backwards transition relation from the model to ease the search.
+		storm::models::GraphTransitions<T> backwardTransitions(model.getTransitionMatrix(), model.getNondeterministicChoiceIndices(), false);
+
+		// Add all psi states as the already satisfy the condition.
+		*statesWithProbability0 |= psiStates;
+
+		// Initialize the stack used for the DFS with the states
+		std::vector<uint_fast64_t> stack;
+		stack.reserve(model.getNumberOfStates());
+		psiStates.getList(stack);
+
+		// Perform the actual DFS.
+		while(!stack.empty()) {
+			uint_fast64_t currentState = stack.back();
+			stack.pop_back();
+
+			for(auto it = backwardTransitions.beginStateSuccessorsIterator(currentState); it != backwardTransitions.endStateSuccessorsIterator(currentState); ++it) {
+				if (phiStates.get(*it) && !statesWithProbability0->get(*it)) {
+					statesWithProbability0->set(*it, true);
+					stack.push_back(*it);
+				}
+			}
+		}
+
+		statesWithProbability0->complement();
+	}
+
+	template <class T>
+	static void performProb1E(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) {
+
+	}
+
+	template <class T>
+	static void performProb01Min(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0, storm::storage::BitVector* statesWithProbability1) {
+		// Check for valid parameters.
+		if (statesWithProbability0 == nullptr) {
+			LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability0' must not be null.");
+			throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability0' must not be null.");
+		}
+		if (statesWithProbability1 == nullptr) {
+			LOG4CPLUS_ERROR(logger, "Parameter 'statesWithProbability1' must not be null.");
+			throw storm::exceptions::InvalidArgumentException("Parameter 'statesWithProbability1' must not be null.");
+		}
+
+		// Perform the actual search.
+		GraphAnalyzer::performProb0E(model, phiStates, psiStates, statesWithProbability0);
+		GraphAnalyzer::performProb1A(model, phiStates, psiStates, statesWithProbability1);
+	}
+
+	template <class T>
+	static void performProb0E(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability0) {
+
+	}
+
+	template <class T>
+	static void performProb1A(storm::models::AbstractNondeterministicModel<T>& model, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, storm::storage::BitVector* statesWithProbability1) {
+		// This result is a rough guess and does not compute all states with probability 1.
+		// TODO: Check whether it makes sense to implement the precise but complicated algorithm here.
+		*statesWithProbability1 = psiStates;
+	}
+};
+
+} // namespace utility
+
+} // namespace storm
+
+#endif /* STORM_UTILITY_GRAPHANALYZER_H_ */
diff --git a/src/utility/IoUtility.cpp b/src/utility/IoUtility.cpp
index 1c2f75c3c..92d682a7b 100644
--- a/src/utility/IoUtility.cpp
+++ b/src/utility/IoUtility.cpp
@@ -17,7 +17,7 @@ namespace storm {
 	namespace utility {
 
 		void dtmcToDot(storm::models::Dtmc<double> const &dtmc, std::string filename) {
-			std::shared_ptr<storm::storage::SparseMatrix<double>> matrix(dtmc.getTransitionProbabilityMatrix());
+			std::shared_ptr<storm::storage::SparseMatrix<double>> matrix(dtmc.getTransitionMatrix());
 			std::ofstream file;
 			file.open(filename);
 
diff --git a/test/parser/ParseMdpTest.cpp b/test/parser/ParseMdpTest.cpp
index 353b470c2..02302dc2a 100644
--- a/test/parser/ParseMdpTest.cpp
+++ b/test/parser/ParseMdpTest.cpp
@@ -8,17 +8,17 @@
 
 #include "gtest/gtest.h"
 #include "storm-config.h"
-#include "src/parser/NonDeterministicModelParser.h"
+#include "src/parser/NondeterministicModelParser.h"
 #include "src/utility/IoUtility.h"
 
 TEST(ParseMdpTest, parseAndOutput) {
-	storm::parser::NonDeterministicModelParser* mdpParser = nullptr;
-	ASSERT_NO_THROW(mdpParser = new storm::parser::NonDeterministicModelParser(
+	storm::parser::NondeterministicModelParser* mdpParser = nullptr;
+	ASSERT_NO_THROW(mdpParser = new storm::parser::NondeterministicModelParser(
 			STORM_CPP_TESTS_BASE_PATH "/parser/tra_files/mdp_general_input_01.tra",
 			STORM_CPP_TESTS_BASE_PATH "/parser/lab_files/pctl_general_input_01.lab"));
 
 	std::shared_ptr<storm::models::Mdp<double>> mdp = mdpParser->getMdp();
-	std::shared_ptr<storm::storage::SparseMatrix<double>> matrix = mdp->getTransitionProbabilityMatrix();
+	std::shared_ptr<storm::storage::SparseMatrix<double>> matrix = mdp->getTransitionMatrix();
 
 	ASSERT_EQ(mdp->getNumberOfStates(), (uint_fast64_t)3);
 	ASSERT_EQ(mdp->getNumberOfTransitions(), (uint_fast64_t)11);
diff --git a/test/storage/SparseMatrixTest.cpp b/test/storage/SparseMatrixTest.cpp
index 6a20050dd..69d11cc37 100644
--- a/test/storage/SparseMatrixTest.cpp
+++ b/test/storage/SparseMatrixTest.cpp
@@ -80,7 +80,7 @@ TEST(SparseMatrixTest, Test) {
 	int position_row[50] = {
 		2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
 		2, 2, 2, 2, 2, 2, 2, 2, 2, 2,
-		2, 2, 2, 2, /* first row empty, one full row ��������� 25 minus the diagonal entry */
+		2, 2, 2, 2, /* first row empty, one full row 25 minus the diagonal entry */
 		4, 4, /* one empty row, then first and last column */
 		13, 13, 13, 13, /* a few empty rows, middle columns */
 		24, 24, 24, 24, 24, 24, 24, 24, 24, 24,
@@ -288,9 +288,9 @@ TEST(SparseMatrixTest, ConversionFromSparseEigen_RowMajor_SparseMatrixTest) {
 
 	ASSERT_EQ(ssm->getState(), storm::storage::SparseMatrix<int>::MatrixStatus::ReadReady);
 	
-	const std::vector<uint_fast64_t> rowP = ssm->getRowIndicationsPointer();
-	const std::vector<uint_fast64_t> colP = ssm->getColumnIndicationsPointer();
-	const std::vector<int> valP = ssm->getStoragePointer();
+	const std::vector<uint_fast64_t> rowP = ssm->getRowIndications();
+	const std::vector<uint_fast64_t> colP = ssm->getColumnIndications();
+	const std::vector<int> valP = ssm->getStorage();
 
 	int target = -1;
 	for (auto &coeff: tripletList) {