diff --git a/CMakeLists.txt b/CMakeLists.txt
index 72fa4adef..a3c45d6eb 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -258,6 +258,7 @@ file(GLOB_RECURSE STORM_LOGIC_FILES ${PROJECT_SOURCE_DIR}/src/logic/*.h ${PROJEC
 file(GLOB STORM_MODELCHECKER_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/*.cpp)
 file(GLOB_RECURSE STORM_MODELCHECKER_PRCTL_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/prctl/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/prctl/*.cpp)
 file(GLOB_RECURSE STORM_MODELCHECKER_CSL_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/csl/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/csl/*.cpp)
+file(GLOB_RECURSE STORM_MODELCHECKER_REACHABILITY_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/reachability/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/reachability/*.cpp)
 file(GLOB_RECURSE STORM_COUNTEREXAMPLES_FILES ${PROJECT_SOURCE_DIR}/src/counterexamples/*.h ${PROJECT_SOURCE_DIR}/src/counterexamples/*.cpp)
 file(GLOB_RECURSE STORM_MODELS_FILES ${PROJECT_SOURCE_DIR}/src/models/*.h ${PROJECT_SOURCE_DIR}/src/models/*.cpp)
 file(GLOB STORM_PARSER_FILES ${PROJECT_SOURCE_DIR}/src/parser/*.h ${PROJECT_SOURCE_DIR}/src/parser/*.cpp)
@@ -292,6 +293,7 @@ source_group(generated FILES ${STORM_BUILD_HEADERS} ${STORM_BUILD_SOURCES})
 source_group(modelchecker FILES ${STORM_MODELCHECKER_FILES})
 source_group(modelchecker\\prctl FILES ${STORM_MODELCHECKER_PRCTL_FILES})
 source_group(modelchecker\\csl FILES ${STORM_MODELCHECKER_CSL_FILES})
+source_group(modelchecker\\reachability FILES ${STORM_MODELCHECKER_REACHABILITY_FILES})
 source_group(counterexamples FILES ${STORM_COUNTEREXAMPLES_FILES})
 source_group(models FILES ${STORM_MODELS_FILES})
 source_group(parser FILES ${STORM_PARSER_FILES})
diff --git a/src/counterexamples/MILPMinimalLabelSetGenerator.h b/src/counterexamples/MILPMinimalLabelSetGenerator.h
index 352534d8e..43694e74b 100644
--- a/src/counterexamples/MILPMinimalLabelSetGenerator.h
+++ b/src/counterexamples/MILPMinimalLabelSetGenerator.h
@@ -1000,8 +1000,8 @@ namespace storm {
                     storm::modelchecker::ExplicitQualitativeCheckResult const& leftQualitativeResult = leftResult->asExplicitQualitativeCheckResult();
                     storm::modelchecker::ExplicitQualitativeCheckResult const& rightQualitativeResult = rightResult->asExplicitQualitativeCheckResult();
                     
-                    phiStates = leftQualitativeResult.getTruthValues();
-                    psiStates = rightQualitativeResult.getTruthValues();
+                    phiStates = leftQualitativeResult.getTruthValuesVector();
+                    psiStates = rightQualitativeResult.getTruthValuesVector();
                 } else if (probabilityOperator.getSubformula().isEventuallyFormula()) {
                     storm::logic::EventuallyFormula const& eventuallyFormula = probabilityOperator.getSubformula().asEventuallyFormula();
                     
@@ -1010,7 +1010,7 @@ namespace storm {
                     storm::modelchecker::ExplicitQualitativeCheckResult const& subQualitativeResult = subResult->asExplicitQualitativeCheckResult();
                     
                     phiStates = storm::storage::BitVector(labeledMdp.getNumberOfStates(), true);
-                    psiStates = subQualitativeResult.getTruthValues();
+                    psiStates = subQualitativeResult.getTruthValuesVector();
                 }
                 
                 // Delegate the actual computation work to the function of equal name.
diff --git a/src/counterexamples/SMTMinimalCommandSetGenerator.h b/src/counterexamples/SMTMinimalCommandSetGenerator.h
index 8b161d372..501fc097c 100644
--- a/src/counterexamples/SMTMinimalCommandSetGenerator.h
+++ b/src/counterexamples/SMTMinimalCommandSetGenerator.h
@@ -1779,8 +1779,8 @@ namespace storm {
                     storm::modelchecker::ExplicitQualitativeCheckResult const& leftQualitativeResult = leftResult.asExplicitQualitativeCheckResult();
                     storm::modelchecker::ExplicitQualitativeCheckResult const& rightQualitativeResult = rightResult.asExplicitQualitativeCheckResult();
                     
-                    phiStates = leftQualitativeResult.getTruthValues();
-                    psiStates = rightQualitativeResult.getTruthValues();
+                    phiStates = leftQualitativeResult.getTruthValuesVector();
+                    psiStates = rightQualitativeResult.getTruthValuesVector();
                 } else if (probabilityOperator.getSubformula().isEventuallyFormula()) {
                     storm::logic::EventuallyFormula const& eventuallyFormula = probabilityOperator.getSubformula().asEventuallyFormula();
                     
@@ -1789,7 +1789,7 @@ namespace storm {
                     storm::modelchecker::ExplicitQualitativeCheckResult const& subQualitativeResult = subResult.asExplicitQualitativeCheckResult();
                     
                     phiStates = storm::storage::BitVector(labeledMdp.getNumberOfStates(), true);
-                    psiStates = subResult.getTruthValues();
+                    psiStates = subResult.getTruthValuesVector();
                 }
                 
                 // Delegate the actual computation work to the function of equal name.
diff --git a/src/logic/ExpectedTimeOperatorFormula.cpp b/src/logic/ExpectedTimeOperatorFormula.cpp
new file mode 100644
index 000000000..17128a837
--- /dev/null
+++ b/src/logic/ExpectedTimeOperatorFormula.cpp
@@ -0,0 +1,47 @@
+#include "src/logic/ExpectedTimeOperatorFormula.h"
+
+namespace storm {
+    namespace logic {
+        ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(std::shared_ptr<Formula const> const& subformula) : ExpectedTimeOperatorFormula(boost::optional<OptimalityType>(), boost::optional<ComparisonType>(), boost::optional<double>(), subformula) {
+            // Intentionally left empty.
+        }
+        
+        ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr<Formula const> const& subformula) : ExpectedTimeOperatorFormula(boost::optional<OptimalityType>(), boost::optional<ComparisonType>(comparisonType), boost::optional<double>(bound), subformula) {
+            // Intentionally left empty.
+        }
+        
+        ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(OptimalityType optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr<Formula const> const& subformula) : ExpectedTimeOperatorFormula(boost::optional<OptimalityType>(optimalityType), boost::optional<ComparisonType>(comparisonType), boost::optional<double>(bound), subformula) {
+            // Intentionally left empty.
+        }
+        
+        ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(OptimalityType optimalityType, std::shared_ptr<Formula const> const& subformula) : ExpectedTimeOperatorFormula(boost::optional<OptimalityType>(optimalityType), boost::optional<ComparisonType>(), boost::optional<double>(), subformula) {
+            // Intentionally left empty.
+        }
+        
+        bool ExpectedTimeOperatorFormula::isExpectedTimeOperatorFormula() const {
+            return true;
+        }
+        
+        bool ExpectedTimeOperatorFormula::isPctlStateFormula() const {
+            return this->getSubformula().isPctlStateFormula();
+        }
+        
+        bool ExpectedTimeOperatorFormula::hasProbabilityOperator() const {
+            return this->getSubformula().hasProbabilityOperator();
+        }
+        
+        bool ExpectedTimeOperatorFormula::hasNestedProbabilityOperators() const {
+            return this->getSubformula().hasNestedProbabilityOperators();
+        }
+        
+        ExpectedTimeOperatorFormula::ExpectedTimeOperatorFormula(boost::optional<OptimalityType> optimalityType, boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, std::shared_ptr<Formula const> const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula) {
+            // Intentionally left empty.
+        }
+        
+        std::ostream& ExpectedTimeOperatorFormula::writeToStream(std::ostream& out) const {
+            out << "ET";
+            OperatorFormula::writeToStream(out);
+            return out;
+        }
+    }
+}
\ No newline at end of file
diff --git a/src/logic/ExpectedTimeOperatorFormula.h b/src/logic/ExpectedTimeOperatorFormula.h
new file mode 100644
index 000000000..9ac29fb33
--- /dev/null
+++ b/src/logic/ExpectedTimeOperatorFormula.h
@@ -0,0 +1,31 @@
+#ifndef STORM_LOGIC_EXPECTEDTIMEOPERATORFORMULA_H_
+#define STORM_LOGIC_EXPECTEDTIMEOPERATORFORMULA_H_
+
+#include "src/logic/OperatorFormula.h"
+
+namespace storm {
+    namespace logic {
+        class ExpectedTimeOperatorFormula : public OperatorFormula {
+        public:
+            ExpectedTimeOperatorFormula(std::shared_ptr<Formula const> const& subformula);
+            ExpectedTimeOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr<Formula const> const& subformula);
+            ExpectedTimeOperatorFormula(OptimalityType optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr<Formula const> const& subformula);
+            ExpectedTimeOperatorFormula(OptimalityType optimalityType, std::shared_ptr<Formula const> const& subformula);
+            ExpectedTimeOperatorFormula(boost::optional<OptimalityType> optimalityType, boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, std::shared_ptr<Formula const> const& subformula);
+            
+            virtual ~ExpectedTimeOperatorFormula() {
+                // Intentionally left empty.
+            }
+            
+            virtual bool isExpectedTimeOperatorFormula() const override;
+            
+            virtual bool isPctlStateFormula() const override;
+            virtual bool hasProbabilityOperator() const override;
+            virtual bool hasNestedProbabilityOperators() const override;
+            
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
+        };
+    }
+}
+
+#endif /* STORM_LOGIC_EXPECTEDTIMEOPERATORFORMULA_H_ */
\ No newline at end of file
diff --git a/src/logic/Formula.cpp b/src/logic/Formula.cpp
index 309f02c32..e0e25c5ba 100644
--- a/src/logic/Formula.cpp
+++ b/src/logic/Formula.cpp
@@ -78,7 +78,11 @@ namespace storm {
             return false;
         }
         
-        bool Formula::isSteadyStateOperatorFormula() const {
+        bool Formula::isLongRunAverageOperatorFormula() const {
+            return false;
+        }
+        
+        bool Formula::isExpectedTimeOperatorFormula() const {
             return false;
         }
         
@@ -282,12 +286,20 @@ namespace storm {
             return dynamic_cast<NextFormula const&>(*this);
         }
         
-        SteadyStateOperatorFormula& Formula::asSteadyStateOperatorFormula() {
-            return dynamic_cast<SteadyStateOperatorFormula&>(*this);
+        LongRunAverageOperatorFormula& Formula::asLongRunAverageOperatorFormula() {
+            return dynamic_cast<LongRunAverageOperatorFormula&>(*this);
+        }
+        
+        LongRunAverageOperatorFormula const& Formula::asLongRunAverageOperatorFormula() const {
+            return dynamic_cast<LongRunAverageOperatorFormula const&>(*this);
+        }
+        
+        ExpectedTimeOperatorFormula& Formula::asExpectedTimeOperatorFormula() {
+            return dynamic_cast<ExpectedTimeOperatorFormula&>(*this);
         }
         
-        SteadyStateOperatorFormula const& Formula::asSteadyStateOperatorFormula() const {
-            return dynamic_cast<SteadyStateOperatorFormula const&>(*this);
+        ExpectedTimeOperatorFormula const& Formula::asExpectedTimeOperatorFormula() const {
+            return dynamic_cast<ExpectedTimeOperatorFormula const&>(*this);
         }
         
         RewardPathFormula& Formula::asRewardPathFormula() {
diff --git a/src/logic/Formula.h b/src/logic/Formula.h
index 75aafa543..ba0b240c3 100644
--- a/src/logic/Formula.h
+++ b/src/logic/Formula.h
@@ -26,7 +26,8 @@ namespace storm {
         class UnaryPathFormula;
         class ConditionalPathFormula;
         class NextFormula;
-        class SteadyStateOperatorFormula;
+        class LongRunAverageOperatorFormula;
+        class ExpectedTimeOperatorFormula;
         class RewardPathFormula;
         class CumulativeRewardFormula;
         class InstantaneousRewardFormula;
@@ -66,7 +67,8 @@ namespace storm {
             virtual bool isUnaryPathFormula() const;
             virtual bool isConditionalPathFormula() const;
             virtual bool isNextFormula() const;
-            virtual bool isSteadyStateOperatorFormula() const;
+            virtual bool isLongRunAverageOperatorFormula() const;
+            virtual bool isExpectedTimeOperatorFormula() const;
             virtual bool isRewardPathFormula() const;
             virtual bool isCumulativeRewardFormula() const;
             virtual bool isInstantaneousRewardFormula() const;
@@ -137,8 +139,11 @@ namespace storm {
             NextFormula& asNextFormula();
             NextFormula const& asNextFormula() const;
             
-            SteadyStateOperatorFormula& asSteadyStateOperatorFormula();
-            SteadyStateOperatorFormula const& asSteadyStateOperatorFormula() const;
+            LongRunAverageOperatorFormula& asLongRunAverageOperatorFormula();
+            LongRunAverageOperatorFormula const& asLongRunAverageOperatorFormula() const;
+
+            ExpectedTimeOperatorFormula& asExpectedTimeOperatorFormula();
+            ExpectedTimeOperatorFormula const& asExpectedTimeOperatorFormula() const;
             
             RewardPathFormula& asRewardPathFormula();
             RewardPathFormula const& asRewardPathFormula() const;
diff --git a/src/logic/Formulas.h b/src/logic/Formulas.h
index ee6355535..d3cfa605d 100644
--- a/src/logic/Formulas.h
+++ b/src/logic/Formulas.h
@@ -17,7 +17,8 @@
 #include "src/logic/ReachabilityRewardFormula.h"
 #include "src/logic/RewardOperatorFormula.h"
 #include "src/logic/StateFormula.h"
-#include "src/logic/SteadyStateOperatorFormula.h"
+#include "src/logic/LongRunAverageOperatorFormula.h"
+#include "src/logic/ExpectedTimeOperatorFormula.h"
 #include "src/logic/UnaryBooleanStateFormula.h"
 #include "src/logic/UnaryPathFormula.h"
 #include "src/logic/UnaryStateFormula.h"
diff --git a/src/logic/LongRunAverageOperatorFormula.cpp b/src/logic/LongRunAverageOperatorFormula.cpp
new file mode 100644
index 000000000..136bee98a
--- /dev/null
+++ b/src/logic/LongRunAverageOperatorFormula.cpp
@@ -0,0 +1,47 @@
+#include "src/logic/LongRunAverageOperatorFormula.h"
+
+namespace storm {
+    namespace logic {
+        LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(std::shared_ptr<Formula const> const& subformula) : LongRunAverageOperatorFormula(boost::optional<OptimalityType>(), boost::optional<ComparisonType>(), boost::optional<double>(), subformula) {
+            // Intentionally left empty.
+        }
+        
+        LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr<Formula const> const& subformula) : LongRunAverageOperatorFormula(boost::optional<OptimalityType>(), boost::optional<ComparisonType>(comparisonType), boost::optional<double>(bound), subformula) {
+            // Intentionally left empty.
+        }
+        
+        LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(OptimalityType optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr<Formula const> const& subformula) : LongRunAverageOperatorFormula(boost::optional<OptimalityType>(optimalityType), boost::optional<ComparisonType>(comparisonType), boost::optional<double>(bound), subformula) {
+            // Intentionally left empty.
+        }
+        
+        LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(OptimalityType optimalityType, std::shared_ptr<Formula const> const& subformula) : LongRunAverageOperatorFormula(boost::optional<OptimalityType>(optimalityType), boost::optional<ComparisonType>(), boost::optional<double>(), subformula) {
+            // Intentionally left empty.
+        }
+                
+        bool LongRunAverageOperatorFormula::isLongRunAverageOperatorFormula() const {
+            return true;
+        }
+        
+        bool LongRunAverageOperatorFormula::isPctlStateFormula() const {
+            return this->getSubformula().isPctlStateFormula();
+        }
+        
+        bool LongRunAverageOperatorFormula::hasProbabilityOperator() const {
+            return this->getSubformula().hasProbabilityOperator();
+        }
+        
+        bool LongRunAverageOperatorFormula::hasNestedProbabilityOperators() const {
+            return this->getSubformula().hasNestedProbabilityOperators();
+        }
+        
+        LongRunAverageOperatorFormula::LongRunAverageOperatorFormula(boost::optional<OptimalityType> optimalityType, boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, std::shared_ptr<Formula const> const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula) {
+            // Intentionally left empty.
+        }
+        
+        std::ostream& LongRunAverageOperatorFormula::writeToStream(std::ostream& out) const {
+            out << "LRA";
+            OperatorFormula::writeToStream(out);
+            return out;
+        }
+    }
+}
\ No newline at end of file
diff --git a/src/logic/LongRunAverageOperatorFormula.h b/src/logic/LongRunAverageOperatorFormula.h
new file mode 100644
index 000000000..2cbdef61b
--- /dev/null
+++ b/src/logic/LongRunAverageOperatorFormula.h
@@ -0,0 +1,31 @@
+#ifndef STORM_LOGIC_LONGRUNAVERAGEOPERATORFORMULA_H_
+#define STORM_LOGIC_LONGRUNAVERAGEOPERATORFORMULA_H_
+
+#include "src/logic/OperatorFormula.h"
+
+namespace storm {
+    namespace logic {
+        class LongRunAverageOperatorFormula : public OperatorFormula {
+        public:
+            LongRunAverageOperatorFormula(std::shared_ptr<Formula const> const& subformula);
+            LongRunAverageOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr<Formula const> const& subformula);
+            LongRunAverageOperatorFormula(OptimalityType optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr<Formula const> const& subformula);
+            LongRunAverageOperatorFormula(OptimalityType optimalityType, std::shared_ptr<Formula const> const& subformula);
+            LongRunAverageOperatorFormula(boost::optional<OptimalityType> optimalityType, boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, std::shared_ptr<Formula const> const& subformula);
+            
+            virtual ~LongRunAverageOperatorFormula() {
+                // Intentionally left empty.
+            }
+            
+            virtual bool isLongRunAverageOperatorFormula() const override;
+            
+            virtual bool isPctlStateFormula() const override;
+            virtual bool hasProbabilityOperator() const override;
+            virtual bool hasNestedProbabilityOperators() const override;
+            
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
+        };
+    }
+}
+
+#endif /* STORM_LOGIC_LONGRUNAVERAGEOPERATORFORMULA_H_ */
\ No newline at end of file
diff --git a/src/logic/SteadyStateOperatorFormula.cpp b/src/logic/SteadyStateOperatorFormula.cpp
deleted file mode 100644
index 0d4a110e2..000000000
--- a/src/logic/SteadyStateOperatorFormula.cpp
+++ /dev/null
@@ -1,47 +0,0 @@
-#include "src/logic/SteadyStateOperatorFormula.h"
-
-namespace storm {
-    namespace logic {
-        SteadyStateOperatorFormula::SteadyStateOperatorFormula(std::shared_ptr<Formula const> const& subformula) : SteadyStateOperatorFormula(boost::optional<OptimalityType>(), boost::optional<ComparisonType>(), boost::optional<double>(), subformula) {
-            // Intentionally left empty.
-        }
-        
-        SteadyStateOperatorFormula::SteadyStateOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr<Formula const> const& subformula) : SteadyStateOperatorFormula(boost::optional<OptimalityType>(), boost::optional<ComparisonType>(comparisonType), boost::optional<double>(bound), subformula) {
-            // Intentionally left empty.
-        }
-        
-        SteadyStateOperatorFormula::SteadyStateOperatorFormula(OptimalityType optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr<Formula const> const& subformula) : SteadyStateOperatorFormula(boost::optional<OptimalityType>(optimalityType), boost::optional<ComparisonType>(comparisonType), boost::optional<double>(bound), subformula) {
-            // Intentionally left empty.
-        }
-        
-        SteadyStateOperatorFormula::SteadyStateOperatorFormula(OptimalityType optimalityType, std::shared_ptr<Formula const> const& subformula) : SteadyStateOperatorFormula(boost::optional<OptimalityType>(optimalityType), boost::optional<ComparisonType>(), boost::optional<double>(), subformula) {
-            // Intentionally left empty.
-        }
-                
-        bool SteadyStateOperatorFormula::isSteadyStateOperatorFormula() const {
-            return true;
-        }
-        
-        bool SteadyStateOperatorFormula::isPctlStateFormula() const {
-            return this->getSubformula().isPctlStateFormula();
-        }
-        
-        bool SteadyStateOperatorFormula::hasProbabilityOperator() const {
-            return this->getSubformula().hasProbabilityOperator();
-        }
-        
-        bool SteadyStateOperatorFormula::hasNestedProbabilityOperators() const {
-            return this->getSubformula().hasNestedProbabilityOperators();
-        }
-        
-        SteadyStateOperatorFormula::SteadyStateOperatorFormula(boost::optional<OptimalityType> optimalityType, boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, std::shared_ptr<Formula const> const& subformula) : OperatorFormula(optimalityType, comparisonType, bound, subformula) {
-            // Intentionally left empty.
-        }
-        
-        std::ostream& SteadyStateOperatorFormula::writeToStream(std::ostream& out) const {
-            out << "S";
-            OperatorFormula::writeToStream(out);
-            return out;
-        }
-    }
-}
\ No newline at end of file
diff --git a/src/logic/SteadyStateOperatorFormula.h b/src/logic/SteadyStateOperatorFormula.h
deleted file mode 100644
index 978aaaeba..000000000
--- a/src/logic/SteadyStateOperatorFormula.h
+++ /dev/null
@@ -1,31 +0,0 @@
-#ifndef STORM_LOGIC_STEADYSTATEFORMULA_H_
-#define STORM_LOGIC_STEADYSTATEFORMULA_H_
-
-#include "src/logic/OperatorFormula.h"
-
-namespace storm {
-    namespace logic {
-        class SteadyStateOperatorFormula : public OperatorFormula {
-        public:
-            SteadyStateOperatorFormula(std::shared_ptr<Formula const> const& subformula);
-            SteadyStateOperatorFormula(ComparisonType comparisonType, double bound, std::shared_ptr<Formula const> const& subformula);
-            SteadyStateOperatorFormula(OptimalityType optimalityType, ComparisonType comparisonType, double bound, std::shared_ptr<Formula const> const& subformula);
-            SteadyStateOperatorFormula(OptimalityType optimalityType, std::shared_ptr<Formula const> const& subformula);
-            SteadyStateOperatorFormula(boost::optional<OptimalityType> optimalityType, boost::optional<ComparisonType> comparisonType, boost::optional<double> bound, std::shared_ptr<Formula const> const& subformula);
-            
-            virtual ~SteadyStateOperatorFormula() {
-                // Intentionally left empty.
-            }
-            
-            virtual bool isSteadyStateOperatorFormula() const override;
-            
-            virtual bool isPctlStateFormula() const override;
-            virtual bool hasProbabilityOperator() const override;
-            virtual bool hasNestedProbabilityOperators() const override;
-            
-            virtual std::ostream& writeToStream(std::ostream& out) const override;
-        };
-    }
-}
-
-#endif /* STORM_LOGIC_STEADYSTATEFORMULA_H_ */
\ No newline at end of file
diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp
index bb70df149..85b62563a 100644
--- a/src/modelchecker/AbstractModelChecker.cpp
+++ b/src/modelchecker/AbstractModelChecker.cpp
@@ -81,6 +81,14 @@ namespace storm {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << rewardPathFormula << ".");
         }
         
+        std::unique_ptr<CheckResult> AbstractModelChecker::computeLongRunAverage(storm::logic::StateFormula const& eventuallyFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the computation of long-run averages.");
+        }
+
+        std::unique_ptr<CheckResult> AbstractModelChecker::computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
+            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the computation of expected times.");
+        }
+        
         std::unique_ptr<CheckResult> AbstractModelChecker::checkStateFormula(storm::logic::StateFormula const& stateFormula) {
             if (stateFormula.isBinaryBooleanStateFormula()) {
                 return this->checkBinaryBooleanStateFormula(stateFormula.asBinaryBooleanStateFormula());
@@ -92,8 +100,10 @@ namespace storm {
                 return this->checkProbabilityOperatorFormula(stateFormula.asProbabilityOperatorFormula());
             } else if (stateFormula.isRewardOperatorFormula()) {
                 return this->checkRewardOperatorFormula(stateFormula.asRewardOperatorFormula());
-            } else if (stateFormula.isSteadyStateOperatorFormula()) {
-                return this->checkSteadyStateOperatorFormula(stateFormula.asSteadyStateOperatorFormula());
+            } else if (stateFormula.isExpectedTimeOperatorFormula()) {
+                return this->checkExpectedTimeOperatorFormula(stateFormula.asExpectedTimeOperatorFormula());
+            } else if (stateFormula.isLongRunAverageOperatorFormula()) {
+                return this->checkLongRunAverageOperatorFormula(stateFormula.asLongRunAverageOperatorFormula());
             } else if (stateFormula.isAtomicExpressionFormula()) {
                 return this->checkAtomicExpressionFormula(stateFormula.asAtomicExpressionFormula());
             } else if (stateFormula.isAtomicLabelFormula()) {
@@ -161,22 +171,68 @@ namespace storm {
         std::unique_ptr<CheckResult> AbstractModelChecker::checkRewardOperatorFormula(storm::logic::RewardOperatorFormula const& stateFormula) {
             STORM_LOG_THROW(stateFormula.getSubformula().isRewardPathFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
             
-            // If the probability bound is 0, is suffices to do qualitative model checking.
+            // If the reward bound is 0, is suffices to do qualitative model checking.
             bool qualitative = false;
             if (stateFormula.hasBound()) {
-                if (stateFormula.getBound() == storm::utility::zero<double>() || stateFormula.getBound() == storm::utility::one<double>()) {
+                if (stateFormula.getBound() == storm::utility::zero<double>()) {
                     qualitative = true;
                 }
             }
+            
+            std::unique_ptr<CheckResult> result;
             if (stateFormula.hasOptimalityType()) {
-                return this->computeRewards(stateFormula.getSubformula().asRewardPathFormula(), qualitative, stateFormula.getOptimalityType());
+                result = this->computeRewards(stateFormula.getSubformula().asRewardPathFormula(), qualitative, stateFormula.getOptimalityType());
+            } else {
+                result = this->computeRewards(stateFormula.getSubformula().asRewardPathFormula(), qualitative);
+            }
+            
+            if (stateFormula.hasBound()) {
+                return result->compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound());
             } else {
-                return this->computeRewards(stateFormula.getSubformula().asRewardPathFormula(), qualitative);
+                return result;
             }
         }
         
-        std::unique_ptr<CheckResult> AbstractModelChecker::checkSteadyStateOperatorFormula(storm::logic::SteadyStateOperatorFormula const& stateFormula) {
-            STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This model checker does not support the formula: " << stateFormula << ".");
+        std::unique_ptr<CheckResult> AbstractModelChecker::checkExpectedTimeOperatorFormula(storm::logic::ExpectedTimeOperatorFormula const& stateFormula) {
+            STORM_LOG_THROW(stateFormula.getSubformula().isStateFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
+            
+            // If the reward bound is 0, is suffices to do qualitative model checking.
+            bool qualitative = false;
+            if (stateFormula.hasBound()) {
+                if (stateFormula.getBound() == storm::utility::zero<double>()) {
+                    qualitative = true;
+                }
+            }
+            
+            std::unique_ptr<CheckResult> result;
+            if (stateFormula.hasOptimalityType()) {
+                result = this->computeExpectedTimes(stateFormula.getSubformula().asEventuallyFormula(), qualitative, stateFormula.getOptimalityType());
+            } else {
+                result = this->computeExpectedTimes(stateFormula.getSubformula().asEventuallyFormula(), qualitative);
+            }
+            
+            if (stateFormula.hasBound()) {
+                return result->compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound());
+            } else {
+                return result;
+            }
+        }
+        
+        std::unique_ptr<CheckResult> AbstractModelChecker::checkLongRunAverageOperatorFormula(storm::logic::LongRunAverageOperatorFormula const& stateFormula) {
+            STORM_LOG_THROW(stateFormula.getSubformula().isEventuallyFormula(), storm::exceptions::InvalidArgumentException, "The given formula is invalid.");
+            
+            if (stateFormula.hasOptimalityType()) {
+                return this->computeLongRunAverage(stateFormula.getSubformula().asStateFormula(), false, stateFormula.getOptimalityType());
+            } else {
+                return this->computeLongRunAverage(stateFormula.getSubformula().asStateFormula(), false);
+            }
+            
+            std::unique_ptr<CheckResult> result;
+            if (stateFormula.hasBound()) {
+                return result->compareAgainstBound(stateFormula.getComparisonType(), stateFormula.getBound());
+            } else {
+                return result;
+            }
         }
         
         std::unique_ptr<CheckResult> AbstractModelChecker::checkUnaryBooleanStateFormula(storm::logic::UnaryBooleanStateFormula const& stateFormula) {
diff --git a/src/modelchecker/AbstractModelChecker.h b/src/modelchecker/AbstractModelChecker.h
index 397995414..92434d18d 100644
--- a/src/modelchecker/AbstractModelChecker.h
+++ b/src/modelchecker/AbstractModelChecker.h
@@ -38,13 +38,17 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeGloballyProbabilities(storm::logic::GloballyFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>());
             virtual std::unique_ptr<CheckResult> computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>());
             virtual std::unique_ptr<CheckResult> computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>());
-
+            
             // The methods to compute the rewards for path formulas.
             virtual std::unique_ptr<CheckResult> computeRewards(storm::logic::RewardPathFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>());
             virtual std::unique_ptr<CheckResult> computeCumulativeRewards(storm::logic::CumulativeRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>());
             virtual std::unique_ptr<CheckResult> computeInstantaneousRewards(storm::logic::InstantaneousRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>());
             virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>());
             
+            // The methods to compute the long-run average and expected time.
+            virtual std::unique_ptr<CheckResult> computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>());
+            virtual std::unique_ptr<CheckResult> computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>());
+            
             // The methods to check state formulas.
             virtual std::unique_ptr<CheckResult> checkStateFormula(storm::logic::StateFormula const& stateFormula);
             virtual std::unique_ptr<CheckResult> checkAtomicExpressionFormula(storm::logic::AtomicExpressionFormula const& stateFormula);
@@ -53,7 +57,8 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula);
             virtual std::unique_ptr<CheckResult> checkProbabilityOperatorFormula(storm::logic::ProbabilityOperatorFormula const& stateFormula);
             virtual std::unique_ptr<CheckResult> checkRewardOperatorFormula(storm::logic::RewardOperatorFormula const& stateFormula);
-            virtual std::unique_ptr<CheckResult> checkSteadyStateOperatorFormula(storm::logic::SteadyStateOperatorFormula const& stateFormula);
+            virtual std::unique_ptr<CheckResult> checkExpectedTimeOperatorFormula(storm::logic::ExpectedTimeOperatorFormula const& stateFormula);
+            virtual std::unique_ptr<CheckResult> checkLongRunAverageOperatorFormula(storm::logic::LongRunAverageOperatorFormula const& stateFormula);
             virtual std::unique_ptr<CheckResult> checkUnaryBooleanStateFormula(storm::logic::UnaryBooleanStateFormula const& stateFormula);
         };
     }
diff --git a/src/modelchecker/CheckResult.cpp b/src/modelchecker/CheckResult.cpp
index 6b91ca464..c8743f966 100644
--- a/src/modelchecker/CheckResult.cpp
+++ b/src/modelchecker/CheckResult.cpp
@@ -52,7 +52,7 @@ namespace storm {
         bool CheckResult::isExplicitQuantitativeCheckResult() const {
             return false;
         }
-        
+                
         ExplicitQualitativeCheckResult& CheckResult::asExplicitQualitativeCheckResult() {
             return dynamic_cast<ExplicitQualitativeCheckResult&>(*this);
         }
diff --git a/src/modelchecker/CheckResult.h b/src/modelchecker/CheckResult.h
index 9e7c061e7..4e0754652 100644
--- a/src/modelchecker/CheckResult.h
+++ b/src/modelchecker/CheckResult.h
@@ -31,6 +31,7 @@ namespace storm {
             
             virtual bool isExplicitQualitativeCheckResult() const;
             virtual bool isExplicitQuantitativeCheckResult() const;
+            virtual bool isExplicitSingleStateQuantitativeCheckResult() const;
             
             ExplicitQualitativeCheckResult& asExplicitQualitativeCheckResult();
             ExplicitQualitativeCheckResult const& asExplicitQualitativeCheckResult() const;
diff --git a/src/modelchecker/ExplicitQualitativeCheckResult.cpp b/src/modelchecker/ExplicitQualitativeCheckResult.cpp
index e41ea1945..b688bb1d8 100644
--- a/src/modelchecker/ExplicitQualitativeCheckResult.cpp
+++ b/src/modelchecker/ExplicitQualitativeCheckResult.cpp
@@ -5,30 +5,90 @@
 
 namespace storm {
     namespace modelchecker {
+        ExplicitQualitativeCheckResult::ExplicitQualitativeCheckResult() : truthValues(map_type()) {
+            // Intentionally left empty.
+        }
+        
+        ExplicitQualitativeCheckResult::ExplicitQualitativeCheckResult(map_type const& map) : truthValues(map) {
+            // Intentionally left empty.
+        }
+        
+        ExplicitQualitativeCheckResult::ExplicitQualitativeCheckResult(map_type&& map) : truthValues(map) {
+            // Intentionally left empty.
+        }
+        
+        ExplicitQualitativeCheckResult::ExplicitQualitativeCheckResult(storm::storage::sparse::state_type state, bool value) : truthValues(map_type()) {
+            boost::get<map_type>(truthValues)[state] = value;
+        }
+        
+        ExplicitQualitativeCheckResult::ExplicitQualitativeCheckResult(storm::storage::BitVector const& truthValues) : truthValues(truthValues) {
+            // Intentionally left empty.
+        }
+        
+        ExplicitQualitativeCheckResult::ExplicitQualitativeCheckResult(storm::storage::BitVector&& truthValues) : truthValues(std::move(truthValues)) {
+            // Intentionally left empty.
+        }
+        
+        void ExplicitQualitativeCheckResult::performLogicalOperation(ExplicitQualitativeCheckResult& first, CheckResult const& second, std::function<bool (bool, bool)> const& function) {
+            STORM_LOG_THROW(typeid(second) == typeid(ExplicitQualitativeCheckResult), storm::exceptions::InvalidOperationException, "Cannot perform logical 'and' on check results of incompatible type.");
+            STORM_LOG_THROW(first.isResultForAllStates() == second.isResultForAllStates(), storm::exceptions::InvalidOperationException, "Cannot perform logical 'and' on check results of incompatible type.");
+            ExplicitQualitativeCheckResult const& secondCheckResult = static_cast<ExplicitQualitativeCheckResult const&>(second);
+            if (first.isResultForAllStates()) {
+                boost::get<vector_type>(first.truthValues) &= boost::get<vector_type>(secondCheckResult.truthValues);
+            } else {
+                map_type& map1 = boost::get<map_type>(first.truthValues);
+                map_type const& map2 = boost::get<map_type>(secondCheckResult.truthValues);
+                for (auto& element1 : map1) {
+                    auto const& keyValuePair = map2.find(element1.first);
+                    STORM_LOG_THROW(keyValuePair != map2.end(), storm::exceptions::InvalidOperationException, "Cannot perform logical 'and' on check results of incompatible type.");
+                    element1.second = function(element1.second, keyValuePair->second);
+                }
+                
+                // Double-check that there are no entries in map2 that the current result does not have.
+                for (auto const& element2 : map2) {
+                    auto const& keyValuePair = map1.find(element2.first);
+                    STORM_LOG_THROW(keyValuePair != map1.end(), storm::exceptions::InvalidOperationException, "Cannot perform logical 'and' on check results of incompatible type.");
+                }
+            }
+        }
+        
         CheckResult& ExplicitQualitativeCheckResult::operator&=(CheckResult const& other) {
-            STORM_LOG_THROW(typeid(other) == typeid(ExplicitQualitativeCheckResult), storm::exceptions::InvalidOperationException, "Cannot perform logical 'and' on check results of incompatible type.");
-            ExplicitQualitativeCheckResult const& otherCheckResult = static_cast<ExplicitQualitativeCheckResult const&>(other);
-            this->truthValues &= otherCheckResult.truthValues;
+            performLogicalOperation(*this, other, [] (bool a, bool b) { return a && b; });
             return *this;
         }
         
         CheckResult& ExplicitQualitativeCheckResult::operator|=(CheckResult const& other) {
-            STORM_LOG_THROW(typeid(other) == typeid(ExplicitQualitativeCheckResult), storm::exceptions::InvalidOperationException, "Cannot perform logical 'or' on check results of incompatible type.");
-            ExplicitQualitativeCheckResult const& otherCheckResult = static_cast<ExplicitQualitativeCheckResult const&>(other);
-            this->truthValues |= otherCheckResult.truthValues;
+            performLogicalOperation(*this, other, [] (bool a, bool b) { return a || b; });
             return *this;
         }
         
-        bool ExplicitQualitativeCheckResult::operator[](uint_fast64_t index) const {
-            return truthValues.get(index);
+        bool ExplicitQualitativeCheckResult::operator[](storm::storage::sparse::state_type state) const {
+            if (this->isResultForAllStates()) {
+                return boost::get<vector_type>(truthValues).get(state);
+            } else {
+                map_type const& map = boost::get<map_type>(truthValues);
+                auto const& keyValuePair = map.find(state);
+                STORM_LOG_THROW(keyValuePair != map.end(), storm::exceptions::InvalidOperationException, "Unknown key '" << state << "'.");
+                return keyValuePair->second;
+            }
         }
         
-        storm::storage::BitVector const& ExplicitQualitativeCheckResult::getTruthValues() const {
-            return truthValues;
+        ExplicitQualitativeCheckResult::vector_type const& ExplicitQualitativeCheckResult::getTruthValuesVector() const {
+            return boost::get<vector_type>(truthValues);
+        }
+        
+        ExplicitQualitativeCheckResult::map_type const& ExplicitQualitativeCheckResult::getTruthValuesVectorMap() const {
+            return boost::get<map_type>(truthValues);
         }
         
         void ExplicitQualitativeCheckResult::complement() {
-            truthValues.complement();
+            if (this->isResultForAllStates()) {
+                boost::get<vector_type>(truthValues).complement();
+            } else {
+                for (auto& element : boost::get<map_type>(truthValues)) {
+                    element.second = !element.second;
+                }
+            }
         }
         
         bool ExplicitQualitativeCheckResult::isExplicit() const {
@@ -36,7 +96,7 @@ namespace storm {
         }
         
         bool ExplicitQualitativeCheckResult::isResultForAllStates() const {
-            return true;
+            return truthValues.which() == 0;
         }
         
         bool ExplicitQualitativeCheckResult::isExplicitQualitativeCheckResult() const {
@@ -44,7 +104,26 @@ namespace storm {
         }
         
         std::ostream& ExplicitQualitativeCheckResult::writeToStream(std::ostream& out) const {
-            out << truthValues;
+            if (this->isResultForAllStates()) {
+                out << boost::get<vector_type>(truthValues);
+            } else {
+                std::ios::fmtflags oldflags(std::cout.flags());
+                out << std::boolalpha;
+
+                map_type const& map = boost::get<map_type>(truthValues);
+                typename map_type::const_iterator it = map.begin();
+                typename map_type::const_iterator itPlusOne = map.begin();
+                ++itPlusOne;
+                typename map_type::const_iterator ite = map.end();
+                
+                for (; it != ite; ++itPlusOne, ++it) {
+                    out << it->second;
+                    if (itPlusOne != ite) {
+                        out << ", ";
+                    }
+                }
+                std::cout.flags(oldflags);
+            }
             return out;
         }
         
@@ -58,10 +137,27 @@ namespace storm {
             storm::storage::BitVector::const_iterator ite = filter.end();
             
             out << std::boolalpha;
-            for (; it != ite; ++itPlusOne, ++it) {
-                out << truthValues[*it];
-                if (itPlusOne != ite) {
-                    out << ", ";
+            if (this->isResultForAllStates()) {
+                vector_type const& vector = boost::get<vector_type>(truthValues);
+                for (; it != ite; ++itPlusOne, ++it) {
+                    out << vector[*it];
+                    if (itPlusOne != ite) {
+                        out << ", ";
+                    }
+                }
+            } else {
+                map_type const& map = boost::get<map_type>(truthValues);
+                bool allResultsAvailable = true;
+                for (; it != ite; ++itPlusOne, ++it) {
+                    auto const& keyValuePair = map.find(*it);
+                    if (keyValuePair != map.end()) {
+                        out << keyValuePair->second;
+                        if (itPlusOne != ite) {
+                            out << ", ";
+                        }
+                    } else {
+                        allResultsAvailable = false;
+                    }
                 }
             }
             out << "]";
diff --git a/src/modelchecker/ExplicitQualitativeCheckResult.h b/src/modelchecker/ExplicitQualitativeCheckResult.h
index 5b3903a35..7c56fd8bb 100644
--- a/src/modelchecker/ExplicitQualitativeCheckResult.h
+++ b/src/modelchecker/ExplicitQualitativeCheckResult.h
@@ -1,31 +1,28 @@
 #ifndef STORM_MODELCHECKER_EXPLICITQUALITATIVECHECKRESULT_H_
 #define STORM_MODELCHECKER_EXPLICITQUALITATIVECHECKRESULT_H_
 
+#include <map>
+#include <functional>
+#include <boost/variant.hpp>
+
 #include "src/modelchecker/QualitativeCheckResult.h"
+#include "src/storage/sparse/StateType.h"
 #include "src/storage/BitVector.h"
+#include "src/utility/OsDetection.h"
 
 namespace storm {
     namespace modelchecker {
         class ExplicitQualitativeCheckResult : public QualitativeCheckResult {
         public:
-            /*!
-             * Constructs a check result with the provided truth values.
-             *
-             * @param truthValues The truth values of the result.
-             */
-            ExplicitQualitativeCheckResult(storm::storage::BitVector const& truthValues) : truthValues(truthValues) {
-                // Intentionally left empty.
-
-            }
+            typedef storm::storage::BitVector vector_type;
+            typedef std::map<storm::storage::sparse::state_type, bool> map_type;
             
-            /*!
-             * Constructs a check result with the provided truth values.
-             *
-             * @param truthValues The truth values of the result.
-             */
-            ExplicitQualitativeCheckResult(storm::storage::BitVector&& truthValues) : truthValues(std::move(truthValues)) {
-                // Intentionally left empty.
-            }
+            ExplicitQualitativeCheckResult();
+            ExplicitQualitativeCheckResult(map_type const& map);
+            ExplicitQualitativeCheckResult(map_type&& map);
+            ExplicitQualitativeCheckResult(storm::storage::sparse::state_type state, bool value);
+            ExplicitQualitativeCheckResult(vector_type const& truthValues);
+            ExplicitQualitativeCheckResult(vector_type&& truthValues);
             
             ExplicitQualitativeCheckResult(ExplicitQualitativeCheckResult const& other) = default;
             ExplicitQualitativeCheckResult& operator=(ExplicitQualitativeCheckResult const& other) = default;
@@ -34,7 +31,8 @@ namespace storm {
             ExplicitQualitativeCheckResult& operator=(ExplicitQualitativeCheckResult&& other) = default;
 #endif
             
-            bool operator[](uint_fast64_t index) const;
+            bool operator[](storm::storage::sparse::state_type index) const;
+            void setValue(storm::storage::sparse::state_type, bool value);
             
             virtual bool isExplicit() const override;
             virtual bool isResultForAllStates() const override;
@@ -45,14 +43,17 @@ namespace storm {
             virtual CheckResult& operator|=(CheckResult const& other) override;
             virtual void complement() override;
 
-            storm::storage::BitVector const& getTruthValues() const;
+            vector_type const& getTruthValuesVector() const;
+            map_type const& getTruthValuesVectorMap() const;
             
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             virtual std::ostream& writeToStream(std::ostream& out, storm::storage::BitVector const& filter) const override;
 
         private:
+            static void performLogicalOperation(ExplicitQualitativeCheckResult& first, CheckResult const& second, std::function<bool (bool, bool)> const& function);
+            
             // The values of the quantitative check result.
-            storm::storage::BitVector truthValues;
+            boost::variant<vector_type, map_type> truthValues;
         };
     }
 }
diff --git a/src/modelchecker/ExplicitQuantitativeCheckResult.cpp b/src/modelchecker/ExplicitQuantitativeCheckResult.cpp
index 06719223e..7c6468003 100644
--- a/src/modelchecker/ExplicitQuantitativeCheckResult.cpp
+++ b/src/modelchecker/ExplicitQuantitativeCheckResult.cpp
@@ -8,8 +8,43 @@
 namespace storm {
     namespace modelchecker {
         template<typename ValueType>
-        std::vector<ValueType> const& ExplicitQuantitativeCheckResult<ValueType>::getValues() const {
-            return values;
+        ExplicitQuantitativeCheckResult<ValueType>::ExplicitQuantitativeCheckResult() : values(map_type()) {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType>
+        ExplicitQuantitativeCheckResult<ValueType>::ExplicitQuantitativeCheckResult(map_type const& values) : values(values) {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType>
+        ExplicitQuantitativeCheckResult<ValueType>::ExplicitQuantitativeCheckResult(map_type&& values) : values(std::move(values)) {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType>
+        ExplicitQuantitativeCheckResult<ValueType>::ExplicitQuantitativeCheckResult(storm::storage::sparse::state_type const& state, ValueType const& value) : values(map_type()) {
+            boost::get<map_type>(values).emplace(state, value);
+        }
+        
+        template<typename ValueType>
+        ExplicitQuantitativeCheckResult<ValueType>::ExplicitQuantitativeCheckResult(vector_type const& values) : values(values) {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType>
+        ExplicitQuantitativeCheckResult<ValueType>::ExplicitQuantitativeCheckResult(vector_type&& values) : values(std::move(values)) {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType>
+        typename ExplicitQuantitativeCheckResult<ValueType>::vector_type const& ExplicitQuantitativeCheckResult<ValueType>::getValueVector() const {
+            return boost::get<vector_type>(values);
+        }
+        
+        template<typename ValueType>
+        typename ExplicitQuantitativeCheckResult<ValueType>::map_type const& ExplicitQuantitativeCheckResult<ValueType>::getValueMap() const {
+            return boost::get<map_type>(values);
         }
         
         template<typename ValueType>
@@ -20,12 +55,31 @@ namespace storm {
             ++itPlusOne;
             storm::storage::BitVector::const_iterator ite = filter.end();
             
-            for (; it != ite; ++itPlusOne, ++it) {
-                out << values[*it];
-                if (itPlusOne != ite) {
-                    out << ", ";
+            if (this->isResultForAllStates()) {
+                vector_type const& valuesAsVector = boost::get<vector_type>(values);
+                for (; it != ite; ++itPlusOne, ++it) {
+                    out << valuesAsVector[*it];
+                    if (itPlusOne != ite) {
+                        out << ", ";
+                    }
                 }
+            } else {
+                map_type const& valuesAsMap = boost::get<map_type>(values);
+                bool allResultsAvailable = true;
+                for (; it != ite; ++itPlusOne, ++it) {
+                    auto const& keyValuePair = valuesAsMap.find(*it);
+                    if (keyValuePair != valuesAsMap.end()) {
+                        out << keyValuePair->second;
+                        if (itPlusOne != ite) {
+                            out << ", ";
+                        }
+                    } else {
+                        allResultsAvailable = false;
+                    }
+                }
+                STORM_LOG_THROW(allResultsAvailable, storm::exceptions::InvalidOperationException, "Unable to print result for some states, because the result is not available.");
             }
+            
             out << "]";
             return out;
         }
@@ -33,9 +87,31 @@ namespace storm {
         template<typename ValueType>
         std::ostream& ExplicitQuantitativeCheckResult<ValueType>::writeToStream(std::ostream& out) const {
             out << "[";
-            if (!values.empty()) {
-                for (auto element: values) {
-                    out << element << " ";
+            if (this->isResultForAllStates()) {
+                vector_type const& valuesAsVector = boost::get<vector_type>(values);
+                typename vector_type::const_iterator it = valuesAsVector.begin();
+                typename vector_type::const_iterator itPlusOne = valuesAsVector.begin();
+                ++itPlusOne;
+                typename vector_type::const_iterator ite = valuesAsVector.end();
+                
+                for (; it != ite; ++itPlusOne, ++it) {
+                    out << *it;
+                    if (itPlusOne != ite) {
+                        out << ", ";
+                    }
+                }
+            } else {
+                map_type const& valuesAsMap = boost::get<map_type>(values);
+                typename map_type::const_iterator it = valuesAsMap.begin();
+                typename map_type::const_iterator itPlusOne = valuesAsMap.begin();
+                ++itPlusOne;
+                typename map_type::const_iterator ite = valuesAsMap.end();
+                
+                for (; it != ite; ++itPlusOne, ++it) {
+                    out << it->second;
+                    if (itPlusOne != ite) {
+                        out << ", ";
+                    }
                 }
             }
             out << "]";
@@ -44,43 +120,88 @@ namespace storm {
         
         template<typename ValueType>
         std::unique_ptr<CheckResult> ExplicitQuantitativeCheckResult<ValueType>::compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const {
-            storm::storage::BitVector result(values.size());
-            switch (comparisonType) {
-                case logic::Less:
-                    for (uint_fast64_t index = 0; index < values.size(); ++index) {
-                        if (result[index] < bound) {
-                            result.set(index);
+            if (this->isResultForAllStates()) {
+                vector_type const& valuesAsVector = boost::get<vector_type>(values);
+                storm::storage::BitVector result(valuesAsVector.size());
+                switch (comparisonType) {
+                    case logic::Less:
+                        for (uint_fast64_t index = 0; index < valuesAsVector.size(); ++index) {
+                            if (result[index] < bound) {
+                                result.set(index);
+                            }
                         }
-                    }
-                    break;
-                case logic::LessEqual:
-                    for (uint_fast64_t index = 0; index < values.size(); ++index) {
-                        if (result[index] <= bound) {
-                            result.set(index);
+                        break;
+                    case logic::LessEqual:
+                        for (uint_fast64_t index = 0; index < valuesAsVector.size(); ++index) {
+                            if (result[index] <= bound) {
+                                result.set(index);
+                            }
                         }
-                    }
-                    break;
-                case logic::Greater:
-                    for (uint_fast64_t index = 0; index < values.size(); ++index) {
-                        if (result[index] > bound) {
-                            result.set(index);
+                        break;
+                    case logic::Greater:
+                        for (uint_fast64_t index = 0; index < valuesAsVector.size(); ++index) {
+                            if (result[index] > bound) {
+                                result.set(index);
+                            }
                         }
-                    }
-                    break;
-                case logic::GreaterEqual:
-                    for (uint_fast64_t index = 0; index < values.size(); ++index) {
-                        if (result[index] >= bound) {
-                            result.set(index);
+                        break;
+                    case logic::GreaterEqual:
+                        for (uint_fast64_t index = 0; index < valuesAsVector.size(); ++index) {
+                            if (result[index] >= bound) {
+                                result.set(index);
+                            }
                         }
-                    }
-                    break;
+                        break;
+                }
+                return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(std::move(result)));
+            } else {
+                map_type const& valuesAsMap = boost::get<map_type>(values);
+                std::map<storm::storage::sparse::state_type, bool> result;
+                switch (comparisonType) {
+                    case logic::Less:
+                        for (auto const& element : valuesAsMap) {
+                            result[element.first] = element.second < bound;
+                        }
+                        break;
+                    case logic::LessEqual:
+                        for (auto const& element : valuesAsMap) {
+                            result[element.first] = element.second <= bound;
+                        }
+                        break;
+                    case logic::Greater:
+                        for (auto const& element : valuesAsMap) {
+                            result[element.first] = element.second > bound;
+                        }
+                        break;
+                    case logic::GreaterEqual:
+                        for (auto const& element : valuesAsMap) {
+                            result[element.first] = element.second >= bound;
+                        }
+                        break;
+                }
+                return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(std::move(result)));
             }
-            return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(std::move(result)));
         }
         
         template<typename ValueType>
-        ValueType ExplicitQuantitativeCheckResult<ValueType>::operator[](uint_fast64_t index) const {
-            return values[index];
+        ValueType& ExplicitQuantitativeCheckResult<ValueType>::operator[](storm::storage::sparse::state_type state) {
+            if (this->isResultForAllStates()) {
+                return boost::get<vector_type>(values)[state];
+            } else {
+                return boost::get<map_type>(values)[state];
+            }
+        }
+        
+        template<typename ValueType>
+        ValueType const& ExplicitQuantitativeCheckResult<ValueType>::operator[](storm::storage::sparse::state_type state) const {
+            if (this->isResultForAllStates()) {
+                return boost::get<vector_type>(values)[state];
+            } else {
+                map_type const& valuesAsMap = boost::get<map_type>(values);
+                auto const& keyValuePair = valuesAsMap.find(state);
+                STORM_LOG_THROW(keyValuePair != valuesAsMap.end(), storm::exceptions::InvalidOperationException, "Unknown key '" << state << "'.");
+                return keyValuePair->second;
+            }
         }
         
         template<typename ValueType>
@@ -90,7 +211,7 @@ namespace storm {
         
         template<typename ValueType>
         bool ExplicitQuantitativeCheckResult<ValueType>::isResultForAllStates() const {
-            return true;
+            return values.which() == 0;
         }
         
         template<typename ValueType>
diff --git a/src/modelchecker/ExplicitQuantitativeCheckResult.h b/src/modelchecker/ExplicitQuantitativeCheckResult.h
index ba933459e..699840c05 100644
--- a/src/modelchecker/ExplicitQuantitativeCheckResult.h
+++ b/src/modelchecker/ExplicitQuantitativeCheckResult.h
@@ -2,8 +2,11 @@
 #define STORM_MODELCHECKER_EXPLICITQUANTITATIVECHECKRESULT_H_
 
 #include <vector>
+#include <map>
+#include <boost/variant.hpp>
 
 #include "src/modelchecker/QuantitativeCheckResult.h"
+#include "src/storage/sparse/StateType.h"
 #include "src/utility/OsDetection.h"
 
 namespace storm {
@@ -11,23 +14,15 @@ namespace storm {
         template<typename ValueType>
         class ExplicitQuantitativeCheckResult : public QuantitativeCheckResult<ValueType> {
         public:
-            /*!
-             * Constructs a check result with the provided values.
-             *
-             * @param values The values of the result.
-             */
-            ExplicitQuantitativeCheckResult(std::vector<ValueType> const& values) : values(values) {
-                // Intentionally left empty.
-            }
-            
-            /*!
-             * Constructs a check result with the provided values.
-             *
-             * @param values The values of the result.
-             */
-            ExplicitQuantitativeCheckResult(std::vector<ValueType>&& values) : values(std::move(values)) {
-                // Intentionally left empty.
-            }
+            typedef std::vector<ValueType> vector_type;
+            typedef std::map<storm::storage::sparse::state_type, ValueType> map_type;
+            
+            ExplicitQuantitativeCheckResult();
+            ExplicitQuantitativeCheckResult(map_type const& values);
+            ExplicitQuantitativeCheckResult(map_type&& values);
+            ExplicitQuantitativeCheckResult(storm::storage::sparse::state_type const& state, ValueType const& value);
+            ExplicitQuantitativeCheckResult(vector_type const& values);
+            ExplicitQuantitativeCheckResult(vector_type&& values);
             
             ExplicitQuantitativeCheckResult(ExplicitQuantitativeCheckResult const& other) = default;
             ExplicitQuantitativeCheckResult& operator=(ExplicitQuantitativeCheckResult const& other) = default;
@@ -36,23 +31,25 @@ namespace storm {
             ExplicitQuantitativeCheckResult& operator=(ExplicitQuantitativeCheckResult&& other) = default;
 #endif
             
+            ValueType& operator[](storm::storage::sparse::state_type state);
+            ValueType const& operator[](storm::storage::sparse::state_type state) const;
+
             virtual std::unique_ptr<CheckResult> compareAgainstBound(storm::logic::ComparisonType comparisonType, double bound) const override;
             
-            ValueType operator[](uint_fast64_t index) const;
-            
             virtual bool isExplicit() const override;
             virtual bool isResultForAllStates() const override;
             
             virtual bool isExplicitQuantitativeCheckResult() const override;
             
-            std::vector<ValueType> const& getValues() const;
+            vector_type const& getValueVector() const;
+            map_type const& getValueMap() const;
             
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             virtual std::ostream& writeToStream(std::ostream& out, storm::storage::BitVector const& filter) const override;
             
         private:
             // The values of the quantitative check result.
-            std::vector<ValueType> values;
+            boost::variant<vector_type, map_type> values;
         };
     }
 }
diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
index 1d6a26367..508157d94 100644
--- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
+++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.cpp
@@ -187,10 +187,10 @@ namespace storm {
         std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<ValueType>::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
             STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
             STORM_LOG_THROW(pathFormula.getLeftSubformula().isTrueFormula(), storm::exceptions::NotImplementedException, "Only bounded properties of the form 'true U[t1, t2] phi' are currently supported.");
-            STORM_LOG_THROW(model.isClosed(), storm::exceptions::InvalidArgumentException, "Unable to compute time-bounded reachability probilities in non-closed Markov automaton.");
+            STORM_LOG_THROW(model.isClosed(), storm::exceptions::InvalidArgumentException, "Unable to compute time-bounded reachability probabilities in non-closed Markov automaton.");
             std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
-            ExplicitQualitativeCheckResult& rightResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*rightResultPointer);
-            std::unique_ptr<CheckResult> result = std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeBoundedUntilProbabilitiesHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, rightResult.getTruthValues(), pathFormula.getIntervalBounds())));
+            ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
+            std::unique_ptr<CheckResult> result = std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeBoundedUntilProbabilitiesHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, rightResult.getTruthValuesVector(), pathFormula.getIntervalBounds())));
             return result;
         }
         
@@ -204,22 +204,63 @@ namespace storm {
             STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
             std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula());
             std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
-            ExplicitQualitativeCheckResult& leftResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*leftResultPointer);
-            ExplicitQualitativeCheckResult& rightResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*rightResultPointer);
-            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeUntilProbabilitiesHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, leftResult.getTruthValues(), rightResult.getTruthValues(), qualitative)));
+            ExplicitQualitativeCheckResult& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
+            ExplicitQualitativeCheckResult& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
+            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeUntilProbabilitiesHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative)));
         }
         
         template<typename ValueType>
-        std::vector<ValueType> SparseMarkovAutomatonCslModelChecker<ValueType>::computeReachabilityRewardsHelper(bool minimize, storm::storage::BitVector const& targetStates, bool qualitative) const {
-            // FIXME
+        std::vector<ValueType> SparseMarkovAutomatonCslModelChecker<ValueType>::computeReachabilityRewardsHelper(bool minimize, storm::storage::BitVector const& psiStates, bool qualitative) const {
+            std::vector<ValueType> totalRewardVector;
+            if (model.hasTransitionRewards()) {
+                totalRewardVector = model.getTransitionMatrix().getPointwiseProductRowSumVector(model.getTransitionRewardMatrix());
+                if (model.hasStateRewards()) {
+                    storm::utility::vector::addVectorsInPlace(totalRewardVector, model.getStateRewardVector());
+                }
+            } else {
+                totalRewardVector = std::vector<ValueType>(model.getStateRewardVector());
+            }
+            
+            return this->computeExpectedRewards(minimize, psiStates, totalRewardVector);
         }
         
         template<typename ValueType>
         std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<ValueType>::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
             STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
+            STORM_LOG_THROW(model.isClosed(), storm::exceptions::InvalidArgumentException, "Unable to compute reachability rewards in non-closed Markov automaton.");
             std::unique_ptr<CheckResult> subResultPointer = this->check(rewardPathFormula.getSubformula());
-            ExplicitQualitativeCheckResult& subResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*subResultPointer);
-            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeReachabilityRewardsHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, subResult.getTruthValues(), qualitative)));
+            ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
+            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeReachabilityRewardsHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, subResult.getTruthValuesVector(), qualitative)));
+        }
+        
+        template<typename ValueType>
+        std::vector<ValueType> SparseMarkovAutomatonCslModelChecker<ValueType>::computeLongRunAverageHelper(bool minimize, storm::storage::BitVector const& psiStates, bool qualitative) const {
+            // FIXME
+        }
+        
+        template<typename ValueType>
+        std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<ValueType>::computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
+            STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
+            STORM_LOG_THROW(model.isClosed(), storm::exceptions::InvalidArgumentException, "Unable to compute long-run average in non-closed Markov automaton.");
+            std::unique_ptr<CheckResult> subResultPointer = this->check(stateFormula);
+            ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
+            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeLongRunAverageHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, subResult.getTruthValuesVector(), qualitative)));
+        }
+        
+        template<typename ValueType>
+        std::vector<ValueType> SparseMarkovAutomatonCslModelChecker<ValueType>::computeExpectedTimesHelper(bool minimize, storm::storage::BitVector const& psiStates, bool qualitative) const {
+            std::vector<ValueType> rewardValues(model.getNumberOfStates(), storm::utility::zero<ValueType>());
+            storm::utility::vector::setVectorValues(rewardValues, model.getMarkovianStates(), storm::utility::one<ValueType>());
+            return this->computeExpectedRewards(minimize, psiStates, rewardValues);
+        }
+        
+        template<typename ValueType>
+        std::unique_ptr<CheckResult> SparseMarkovAutomatonCslModelChecker<ValueType>::computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
+            STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
+            STORM_LOG_THROW(model.isClosed(), storm::exceptions::InvalidArgumentException, "Unable to compute expected times in non-closed Markov automaton.");
+            std::unique_ptr<CheckResult> subResultPointer = this->check(eventuallyFormula.getSubformula());
+            ExplicitQualitativeCheckResult& subResult = subResultPointer->asExplicitQualitativeCheckResult();
+            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeExpectedTimesHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, subResult.getTruthValuesVector(), qualitative)));
         }
         
         template<typename ValueType>
@@ -238,19 +279,19 @@ namespace storm {
         }
         
         template<typename ValueType>
-        std::vector<ValueType> SparseMarkovAutomatonCslModelChecker<ValueType>::checkLongRunAverage(bool min, storm::storage::BitVector const& goalStates) const {
+        std::vector<ValueType> SparseMarkovAutomatonCslModelChecker<ValueType>::computeLongRunAverage(bool minimize, storm::storage::BitVector const& psiStates) const {
             // Check whether the automaton is closed.
             if (!model.isClosed()) {
                 throw storm::exceptions::InvalidArgumentException() << "Unable to compute long-run average on non-closed Markov automaton.";
             }
             
             // If there are no goal states, we avoid the computation and directly return zero.
-            if (goalStates.empty()) {
+            if (psiStates.empty()) {
                 return std::vector<ValueType>(model.getNumberOfStates(), storm::utility::zero<ValueType>());
             }
             
             // Likewise, if all bits are set, we can avoid the computation and set.
-            if ((~goalStates).empty()) {
+            if ((~psiStates).empty()) {
                 return std::vector<ValueType>(model.getNumberOfStates(), storm::utility::one<ValueType>());
             }
             
@@ -280,7 +321,7 @@ namespace storm {
                 }
                 
                 // Compute the LRA value for the current MEC.
-                lraValuesForEndComponents.push_back(this->computeLraForMaximalEndComponent(min, transitionMatrix, nondeterministicChoiceIndices, model.getMarkovianStates(), model.getExitRates(), goalStates, mec, currentMecIndex));
+                lraValuesForEndComponents.push_back(this->computeLraForMaximalEndComponent(minimize, transitionMatrix, nondeterministicChoiceIndices, model.getMarkovianStates(), model.getExitRates(), psiStates, mec, currentMecIndex));
             }
             
             // For fast transition rewriting, we build some auxiliary data structures.
@@ -386,7 +427,7 @@ namespace storm {
             storm::storage::SparseMatrix<ValueType> sspMatrix = sspMatrixBuilder.build(currentChoice);
             
             std::vector<ValueType> x(numberOfStatesNotInMecs + mecDecomposition.size());
-            nondeterministicLinearEquationSolver->solveEquationSystem(min, sspMatrix, x, b);
+            nondeterministicLinearEquationSolver->solveEquationSystem(minimize, sspMatrix, x, b);
             
             // Prepare result vector.
             std::vector<ValueType> result(model.getNumberOfStates());
@@ -403,9 +444,9 @@ namespace storm {
         }
         
         template<typename ValueType>
-        ValueType SparseMarkovAutomatonCslModelChecker<ValueType>::computeLraForMaximalEndComponent(bool min, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::BitVector const& markovianStates, std::vector<ValueType> const& exitRates, storm::storage::BitVector const& goalStates, storm::storage::MaximalEndComponent const& mec, uint_fast64_t mecIndex) {
+        ValueType SparseMarkovAutomatonCslModelChecker<ValueType>::computeLraForMaximalEndComponent(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<uint_fast64_t> const& nondeterministicChoiceIndices, storm::storage::BitVector const& markovianStates, std::vector<ValueType> const& exitRates, storm::storage::BitVector const& psiStates, storm::storage::MaximalEndComponent const& mec, uint_fast64_t mecIndex) {
             std::shared_ptr<storm::solver::LpSolver> solver = storm::utility::solver::getLpSolver("LRA for MEC");
-            solver->setModelSense(min ? storm::solver::LpSolver::ModelSense::Maximize : storm::solver::LpSolver::ModelSense::Minimize);
+            solver->setModelSense(minimize ? storm::solver::LpSolver::ModelSense::Maximize : storm::solver::LpSolver::ModelSense::Minimize);
             
             // First, we need to create the variables for the problem.
             std::map<uint_fast64_t, storm::expressions::Variable> stateToVariableMap;
@@ -429,8 +470,8 @@ namespace storm {
                     }
                     
                     constraint = constraint + solver->getConstant(storm::utility::one<ValueType>() / exitRates[state]) * k;
-                    storm::expressions::Expression rightHandSide = goalStates.get(state) ? solver->getConstant(storm::utility::one<ValueType>() / exitRates[state]) : solver->getConstant(0);
-                    if (min) {
+                    storm::expressions::Expression rightHandSide = psiStates.get(state) ? solver->getConstant(storm::utility::one<ValueType>() / exitRates[state]) : solver->getConstant(0);
+                    if (minimize) {
                         constraint = constraint <= rightHandSide;
                     } else {
                         constraint = constraint >= rightHandSide;
@@ -447,7 +488,7 @@ namespace storm {
                         }
                         
                         storm::expressions::Expression rightHandSide = solver->getConstant(storm::utility::zero<ValueType>());
-                        if (min) {
+                        if (minimize) {
                             constraint = constraint <= rightHandSide;
                         } else {
                             constraint = constraint >= rightHandSide;
@@ -461,22 +502,8 @@ namespace storm {
             return solver->getContinuousValue(k);
         }
         
-        template<typename ValueType>
-        std::vector<ValueType> SparseMarkovAutomatonCslModelChecker<ValueType>::checkExpectedTime(bool minimize, storm::storage::BitVector const& goalStates) const {
-            // Reduce the problem of computing the expected time to computing expected rewards where the rewards
-            // for all probabilistic states are zero and the reward values of Markovian states is 1.
-            std::vector<ValueType> rewardValues(model.getNumberOfStates(), storm::utility::zero<ValueType>());
-            storm::utility::vector::setVectorValues(rewardValues, model.getMarkovianStates(), storm::utility::one<ValueType>());
-            return this->computeExpectedRewards(minimize, goalStates, rewardValues);
-        }
-        
         template<typename ValueType>
         std::vector<ValueType> SparseMarkovAutomatonCslModelChecker<ValueType>::computeExpectedRewards(bool minimize, storm::storage::BitVector const& goalStates, std::vector<ValueType> const& stateRewards) const {
-            // Check whether the automaton is closed.
-            if (!model.isClosed()) {
-                throw storm::exceptions::InvalidArgumentException() << "Unable to compute expected time on non-closed Markov automaton.";
-            }
-            
             // First, we need to check which states have infinite expected time (by definition).
             storm::storage::BitVector infinityStates;
             if (minimize) {
diff --git a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
index 51888a1ca..0b47e3cf6 100644
--- a/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
+++ b/src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h
@@ -22,19 +22,21 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
             virtual std::unique_ptr<CheckResult> computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
             virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
+            virtual std::unique_ptr<CheckResult> computeLongRunAverage(storm::logic::StateFormula const& stateFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
+            virtual std::unique_ptr<CheckResult> computeExpectedTimes(storm::logic::EventuallyFormula const& eventuallyFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>());
             virtual std::unique_ptr<CheckResult> checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) override;
             virtual std::unique_ptr<CheckResult> checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) override;
             
         private:
             // The methods that perform the actual checking.
+
             std::vector<ValueType> computeBoundedUntilProbabilitiesHelper(bool minimize, storm::storage::BitVector const& psiStates, std::pair<double, double> const& boundsPair) const;
             static void computeBoundedReachabilityProbabilities(bool minimize, storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType> const& exitRates, storm::storage::BitVector const& markovianStates, storm::storage::BitVector const& goalStates, storm::storage::BitVector const& markovianNonGoalStates, storm::storage::BitVector const& probabilisticNonGoalStates, std::vector<ValueType>& markovianNonGoalValues, std::vector<ValueType>& probabilisticNonGoalValues, ValueType delta, uint_fast64_t numberOfSteps);
             std::vector<ValueType> computeUntilProbabilitiesHelper(bool minimize, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, bool qualitative) const;
-            std::vector<ValueType> computeReachabilityRewardsHelper(bool minimize, storm::storage::BitVector const& targetStates, bool qualitative) const;
-            
-            // FIXME: Methods that are not yet accessible from the outside and need to be included in the checking framework.
-            std::vector<ValueType> checkLongRunAverage(bool minimize, storm::storage::BitVector const& goalStates) const;
-            std::vector<ValueType> checkExpectedTime(bool minimize, storm::storage::BitVector const& goalStates) const;
+            std::vector<ValueType> computeReachabilityRewardsHelper(bool minimize, storm::storage::BitVector const& psiStates, bool qualitative) const;
+            std::vector<ValueType> computeLongRunAverageHelper(bool minimize, storm::storage::BitVector const& psiStates, bool qualitative) const;
+            std::vector<ValueType> computeExpectedTimesHelper(bool minimize, storm::storage::BitVector const& psiStates, bool qualitative) const;
+            std::vector<ValueType> computeLongRunAverage(bool minimize, storm::storage::BitVector const& psiStates) const;
 
             /*!
              * Computes the long-run average value for the given maximal end component of a Markov automaton.
diff --git a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
index 3759fd1d5..f21e4fdc4 100644
--- a/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
+++ b/src/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
@@ -66,9 +66,9 @@ namespace storm {
         std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<ValueType>::computeBoundedUntilProbabilities(storm::logic::BoundedUntilFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
             std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula());
             std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
-            ExplicitQualitativeCheckResult& leftResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*leftResultPointer);
-            ExplicitQualitativeCheckResult& rightResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*rightResultPointer);
-            std::unique_ptr<CheckResult> result = std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeBoundedUntilProbabilitiesHelper(leftResult.getTruthValues(), rightResult.getTruthValues(), pathFormula.getUpperBound())));
+            ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();;
+            ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
+            std::unique_ptr<CheckResult> result = std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeBoundedUntilProbabilitiesHelper(leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound())));
             
             return result;
         }
@@ -88,8 +88,8 @@ namespace storm {
         template<typename ValueType>
         std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<ValueType>::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
             std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula());
-            ExplicitQualitativeCheckResult& subResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*subResultPointer);
-            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeNextProbabilitiesHelper(subResult.getTruthValues())));
+            ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
+            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeNextProbabilitiesHelper(subResult.getTruthValuesVector())));
         }
         
         template<typename ValueType>
@@ -153,9 +153,9 @@ namespace storm {
         std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<ValueType>::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
             std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula());
             std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
-            ExplicitQualitativeCheckResult& leftResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*leftResultPointer);
-            ExplicitQualitativeCheckResult& rightResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*rightResultPointer);
-            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeUntilProbabilitiesHelper(leftResult.getTruthValues(), rightResult.getTruthValues(), qualitative)));
+            ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();;
+            ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();;
+            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeUntilProbabilitiesHelper(leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), qualitative)));
         }
         
         template<typename ValueType>
@@ -293,8 +293,8 @@ namespace storm {
         template<typename ValueType>
         std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<ValueType>::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
             std::unique_ptr<CheckResult> subResultPointer = this->check(rewardPathFormula.getSubformula());
-            ExplicitQualitativeCheckResult& subResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*subResultPointer);
-            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeReachabilityRewardsHelper(subResult.getTruthValues(), qualitative)));
+            ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
+            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeReachabilityRewardsHelper(subResult.getTruthValuesVector(), qualitative)));
         }
         
         template<typename ValueType>
diff --git a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
index 5f73e5b9f..c1c760f99 100644
--- a/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
+++ b/src/modelchecker/prctl/SparseMdpPrctlModelChecker.cpp
@@ -72,9 +72,9 @@ namespace storm {
             STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
             std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula());
             std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
-            ExplicitQualitativeCheckResult& leftResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*leftResultPointer);
-            ExplicitQualitativeCheckResult& rightResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*rightResultPointer);
-            std::unique_ptr<CheckResult> result = std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeBoundedUntilProbabilitiesHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, leftResult.getTruthValues(), rightResult.getTruthValues(), pathFormula.getUpperBound())));
+            ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
+            ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
+            std::unique_ptr<CheckResult> result = std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeBoundedUntilProbabilitiesHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), pathFormula.getUpperBound())));
             return result;
         }
         
@@ -94,8 +94,8 @@ namespace storm {
         std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<ValueType>::computeNextProbabilities(storm::logic::NextFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
             STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
             std::unique_ptr<CheckResult> subResultPointer = this->check(pathFormula.getSubformula());
-            ExplicitQualitativeCheckResult& subResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*subResultPointer);
-            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeNextProbabilitiesHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, subResult.getTruthValues())));
+            ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
+            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeNextProbabilitiesHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, subResult.getTruthValuesVector())));
         }
         
         template<typename ValueType>
@@ -159,9 +159,9 @@ namespace storm {
             STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
             std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula());
             std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
-            ExplicitQualitativeCheckResult& leftResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*leftResultPointer);
-            ExplicitQualitativeCheckResult& rightResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*rightResultPointer);
-            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(SparseMdpPrctlModelChecker<ValueType>::computeUntilProbabilitiesHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, model.getTransitionMatrix(), model.getBackwardTransitions(), leftResult.getTruthValues(), rightResult.getTruthValues(), nondeterministicLinearEquationSolver, qualitative)));
+            ExplicitQualitativeCheckResult const& leftResult = leftResultPointer->asExplicitQualitativeCheckResult();
+            ExplicitQualitativeCheckResult const& rightResult = rightResultPointer->asExplicitQualitativeCheckResult();
+            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(SparseMdpPrctlModelChecker<ValueType>::computeUntilProbabilitiesHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, model.getTransitionMatrix(), model.getBackwardTransitions(), leftResult.getTruthValuesVector(), rightResult.getTruthValuesVector(), nondeterministicLinearEquationSolver, qualitative)));
         }
         
         template<typename ValueType>
@@ -304,8 +304,8 @@ namespace storm {
         std::unique_ptr<CheckResult> SparseMdpPrctlModelChecker<ValueType>::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
             STORM_LOG_THROW(optimalityType, storm::exceptions::InvalidArgumentException, "Formula needs to specify whether minimal or maximal values are to be computed on nondeterministic model.");
             std::unique_ptr<CheckResult> subResultPointer = this->check(rewardPathFormula.getSubformula());
-            ExplicitQualitativeCheckResult& subResult = dynamic_cast<ExplicitQualitativeCheckResult&>(*subResultPointer);
-            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeReachabilityRewardsHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, subResult.getTruthValues(), qualitative)));
+            ExplicitQualitativeCheckResult const& subResult = subResultPointer->asExplicitQualitativeCheckResult();
+            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(this->computeReachabilityRewardsHelper(optimalityType.get() == storm::logic::OptimalityType::Minimize, subResult.getTruthValuesVector(), qualitative)));
         }
         
         template<typename ValueType>
diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
new file mode 100644
index 000000000..0a531ff8d
--- /dev/null
+++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.cpp
@@ -0,0 +1,864 @@
+#include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h"
+
+#include <algorithm>
+
+#ifdef PARAMETRIC_SYSTEMS
+#include "src/storage/parameters.h"
+#endif
+
+#include "src/storage/StronglyConnectedComponentDecomposition.h"
+
+#include "src/modelchecker/ExplicitQualitativeCheckResult.h"
+#include "src/modelchecker/ExplicitQuantitativeCheckResult.h"
+
+#include "src/utility/graph.h"
+#include "src/utility/vector.h"
+#include "src/utility/macros.h"
+#include "src/utility/ConstantsComparator.h"
+
+#include "src/exceptions/InvalidPropertyException.h"
+#include "src/exceptions/InvalidStateException.h"
+
+namespace storm {
+    namespace modelchecker {
+        
+        template<typename ValueType>
+        SparseDtmcEliminationModelChecker<ValueType>::SparseDtmcEliminationModelChecker(storm::models::Dtmc<ValueType> const& model) : model(model) {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType>
+        bool SparseDtmcEliminationModelChecker<ValueType>::canHandle(storm::logic::Formula const& formula) const {
+            if (formula.isProbabilityOperatorFormula()) {
+                storm::logic::ProbabilityOperatorFormula const& probabilityOperatorFormula = formula.asProbabilityOperatorFormula();
+                // The probability operator must not have a bound.
+                if (!probabilityOperatorFormula.hasBound()) {
+                    return this->canHandle(probabilityOperatorFormula.getSubformula());
+                }
+            } else if (formula.isRewardOperatorFormula()) {
+                storm::logic::RewardOperatorFormula const& rewardOperatorFormula = formula.asRewardOperatorFormula();
+                // The reward operator must not have a bound.
+                if (!rewardOperatorFormula.hasBound()) {
+                    return this->canHandle(rewardOperatorFormula.getSubformula());
+                }
+            } else if (formula.isUntilFormula() || formula.isEventuallyFormula()) {
+                if (formula.isUntilFormula()) {
+                    storm::logic::UntilFormula const& untilFormula = formula.asUntilFormula();
+                    if (untilFormula.getLeftSubformula().isPropositionalFormula() && untilFormula.getRightSubformula().isPropositionalFormula()) {
+                        return true;
+                    }
+                } else if (formula.isEventuallyFormula()) {
+                    storm::logic::EventuallyFormula const& eventuallyFormula = formula.asEventuallyFormula();
+                    if (eventuallyFormula.getSubformula().isPropositionalFormula()) {
+                        return true;
+                    }
+                }
+            } else if (formula.isReachabilityRewardFormula()) {
+                storm::logic::ReachabilityRewardFormula reachabilityRewardFormula = formula.asReachabilityRewardFormula();
+                if (reachabilityRewardFormula.getSubformula().isPropositionalFormula()) {
+                    return true;
+                }
+            } else if (formula.isConditionalPathFormula()) {
+                storm::logic::ConditionalPathFormula conditionalPathFormula = formula.asConditionalPathFormula();
+                if (conditionalPathFormula.getLeftSubformula().isEventuallyFormula() && conditionalPathFormula.getRightSubformula().isEventuallyFormula()) {
+                    return this->canHandle(conditionalPathFormula.getLeftSubformula()) && this->canHandle(conditionalPathFormula.getRightSubformula());
+                }
+            }
+            return false;
+        }
+        
+        template<typename ValueType>
+        std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<ValueType>::computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
+            // Retrieve the appropriate bitvectors by model checking the subformulas.
+            std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula());
+            std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula());
+            storm::storage::BitVector const& phiStates = leftResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector();
+            storm::storage::BitVector const& psiStates = rightResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector();
+            
+            // Do some sanity checks to establish some required properties.
+            STORM_LOG_THROW(model.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state.");
+            
+            // Then, compute the subset of states that has a probability of 0 or 1, respectively.
+            std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(model, phiStates, psiStates);
+            storm::storage::BitVector statesWithProbability0 = statesWithProbability01.first;
+            storm::storage::BitVector statesWithProbability1 = statesWithProbability01.second;
+            storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1);
+            
+            // If the initial state is known to have either probability 0 or 1, we can directly return the result.
+            if (model.getInitialStates().isDisjointFrom(maybeStates)) {
+                STORM_LOG_DEBUG("The probability of all initial states was found in a preprocessing step.");
+                return statesWithProbability0.get(*model.getInitialStates().begin()) ? storm::utility::zero<ValueType>() : storm::utility::one<ValueType>();
+            }
+            
+            // Determine the set of states that is reachable from the initial state without jumping over a target state.
+            storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(model.getTransitionMatrix(), model.getInitialStates(), maybeStates, statesWithProbability1);
+            
+            // Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state).
+            maybeStates &= reachableStates;
+            
+            // Create a vector for the probabilities to go to a state with probability 1 in one step.
+            std::vector<ValueType> oneStepProbabilities = model.getTransitionMatrix().getConstrainedRowSumVector(maybeStates, statesWithProbability1);
+            
+            // Determine the set of initial states of the sub-model.
+            storm::storage::BitVector newInitialStates = model.getInitialStates() % maybeStates;
+            
+            // We then build the submatrix that only has the transitions of the maybe states.
+            storm::storage::SparseMatrix<ValueType> submatrix = model.getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates);
+            storm::storage::SparseMatrix<ValueType> submatrixTransposed = submatrix.transpose();
+            
+            // Before starting the model checking process, we assign priorities to states so we can use them to
+            // impose ordering constraints later.
+            std::vector<std::size_t> statePriorities = getStatePriorities(submatrix, submatrixTransposed, newInitialStates, oneStepProbabilities);
+            
+            boost::optional<std::vector<ValueType>> missingStateRewards;
+            return computeReachabilityValue(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, phiStates, psiStates, missingStateRewards, statePriorities);
+        }
+        
+        template<typename ValueType>
+        std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<ValueType>::computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
+            // Retrieve the appropriate bitvectors by model checking the subformulas.
+            std::unique_ptr<CheckResult> subResultPointer = this->check(rewardPathFormula.getSubformula());
+            storm::storage::BitVector phiStates(model.getNumberOfStates(), true);
+            storm::storage::BitVector const& psiStates = subResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector();
+            
+            // Do some sanity checks to establish some required properties.
+            STORM_LOG_THROW(!model.hasTransitionRewards(), storm::exceptions::IllegalArgumentException, "Input model does have transition-based rewards, which are currently unsupported.");
+            STORM_LOG_THROW(model.hasStateRewards(), storm::exceptions::IllegalArgumentException, "Input model does not have a state-based reward model.");
+            STORM_LOG_THROW(model.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state.");
+            
+            // Then, compute the subset of states that has a reachability reward less than infinity.
+            storm::storage::BitVector trueStates(model.getNumberOfStates(), true);
+            storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(model.getBackwardTransitions(), trueStates, psiStates);
+            infinityStates.complement();
+            storm::storage::BitVector maybeStates = ~psiStates & ~infinityStates;
+            
+            // If the initial state is known to have 0 reward or an infinite reward value, we can directly return the result.
+            STORM_LOG_THROW(model.getInitialStates().isDisjointFrom(infinityStates), storm::exceptions::IllegalArgumentException, "Initial state has infinite reward.");
+            if (!model.getInitialStates().isDisjointFrom(psiStates)) {
+                STORM_LOG_DEBUG("The reward of all initial states was found in a preprocessing step.");
+                return storm::utility::zero<ValueType>();
+            }
+            
+            // Determine the set of states that is reachable from the initial state without jumping over a target state.
+            storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(model.getTransitionMatrix(), model.getInitialStates(), maybeStates, psiStates);
+            
+            // Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state).
+            maybeStates &= reachableStates;
+            
+            // Create a vector for the probabilities to go to a state with probability 1 in one step.
+            std::vector<ValueType> oneStepProbabilities = model.getTransitionMatrix().getConstrainedRowSumVector(maybeStates, psiStates);
+            
+            // Project the state reward vector to all maybe-states.
+            boost::optional<std::vector<ValueType>> stateRewards(maybeStates.getNumberOfSetBits());
+            storm::utility::vector::selectVectorValues(stateRewards.get(), maybeStates, model.getStateRewardVector());
+            
+            // Determine the set of initial states of the sub-model.
+            storm::storage::BitVector newInitialStates = model.getInitialStates() % maybeStates;
+            
+            // We then build the submatrix that only has the transitions of the maybe states.
+            storm::storage::SparseMatrix<ValueType> submatrix = model.getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates);
+            storm::storage::SparseMatrix<ValueType> submatrixTransposed = submatrix.transpose();
+            
+            // Before starting the model checking process, we assign priorities to states so we can use them to
+            // impose ordering constraints later.
+            std::vector<std::size_t> statePriorities = getStatePriorities(submatrix, submatrixTransposed, newInitialStates, oneStepProbabilities);
+            
+            return computeReachabilityValue(submatrix, oneStepProbabilities, submatrixTransposed, newInitialStates, phiStates, psiStates, stateRewards, statePriorities);
+        }
+        
+        template<typename ValueType>
+        std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<ValueType>::computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative, boost::optional<storm::logic::OptimalityType> const& optimalityType) {
+            // Retrieve the appropriate bitvectors by model checking the subformulas.
+            STORM_LOG_THROW(pathFormula.getLeftSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Expected 'eventually' formula.");
+            STORM_LOG_THROW(pathFormula.getRightSubformula().isEventuallyFormula(), storm::exceptions::InvalidPropertyException, "Expected 'eventually' formula.");
+            
+            std::unique_ptr<CheckResult> leftResultPointer = this->check(pathFormula.getLeftSubformula().asEventuallyFormula().getSubformula());
+            std::unique_ptr<CheckResult> rightResultPointer = this->check(pathFormula.getRightSubformula().asEventuallyFormula().getSubformula());
+            storm::storage::BitVector phiStates = leftResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector();
+            storm::storage::BitVector psiStates = rightResultPointer->asExplicitQualitativeCheckResult().getTruthValuesVector();
+            storm::storage::BitVector trueStates(model.getNumberOfStates(), true);
+            
+            // Do some sanity checks to establish some required properties.
+            STORM_LOG_THROW(model.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state.");
+            STORM_LOG_THROW(storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() != storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::State, storm::exceptions::InvalidArgumentException, "Unsupported elimination method for conditional probabilities.");
+            
+            storm::storage::SparseMatrix<ValueType> backwardTransitions = model.getBackwardTransitions();
+            
+            std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(backwardTransitions, trueStates, psiStates);
+            storm::storage::BitVector statesWithProbabilityGreater0 = ~statesWithProbability01.first;
+            storm::storage::BitVector statesWithProbability1 = std::move(statesWithProbability01.second);
+            
+            STORM_LOG_THROW(model.getInitialStates().isSubsetOf(statesWithProbabilityGreater0), storm::exceptions::InvalidPropertyException, "The condition of the conditional probability has zero probability.");
+            
+            // If the initial state is known to have probability 1 of satisfying the condition, we can apply regular model checking.
+            if (model.getInitialStates().isSubsetOf(statesWithProbability1)) {
+                std::shared_ptr<storm::logic::BooleanLiteralFormula> trueFormula = std::make_shared<storm::logic::BooleanLiteralFormula>(true);
+                std::shared_ptr<storm::logic::UntilFormula> untilFormula = std::make_shared<storm::logic::UntilFormula>(trueFormula, pathFormula.getLeftSubformula().asSharedPointer());
+                return this->computeUntilProbabilities(untilFormula);
+            }
+            
+            // From now on, we know the condition does not have a trivial probability in the initial state.
+            
+            // Compute the states that can be reached on a path that has a psi state in it.
+            storm::storage::BitVector statesWithPsiPredecessor = storm::utility::graph::performProbGreater0(model.getTransitionMatrix(), trueStates, psiStates);
+            storm::storage::BitVector statesReachingPhi = storm::utility::graph::performProbGreater0(backwardTransitions, trueStates, phiStates);
+            
+            // The set of states we need to consider are those that have a non-zero probability to satisfy the condition or are on some path that has a psi state in it.
+            STORM_LOG_DEBUG("Initial state: " << model.getInitialStates());
+            STORM_LOG_DEBUG("Phi states: " << phiStates);
+            STORM_LOG_DEBUG("Psi state: " << psiStates);
+            STORM_LOG_DEBUG("States with probability greater 0 of satisfying the condition: " << statesWithProbabilityGreater0);
+            STORM_LOG_DEBUG("States with psi predecessor: " << statesWithPsiPredecessor);
+            STORM_LOG_DEBUG("States reaching phi: " << statesReachingPhi);
+            storm::storage::BitVector maybeStates = statesWithProbabilityGreater0 | (statesWithPsiPredecessor & statesReachingPhi);
+            STORM_LOG_DEBUG("Found " << maybeStates.getNumberOfSetBits() << " relevant states: " << maybeStates);
+            
+            // Determine the set of initial states of the sub-DTMC.
+            storm::storage::BitVector newInitialStates = model.getInitialStates() % maybeStates;
+            
+            // Create a dummy vector for the one-step probabilities.
+            std::vector<ValueType> oneStepProbabilities(maybeStates.getNumberOfSetBits(), storm::utility::zero<ValueType>());
+            
+            // We then build the submatrix that only has the transitions of the maybe states.
+            storm::storage::SparseMatrix<ValueType> submatrix = model.getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates);
+            storm::storage::SparseMatrix<ValueType> submatrixTransposed = submatrix.transpose();
+            
+            // The states we want to eliminate are those that are tagged with "maybe" but are not a phi or psi state.
+            phiStates = phiStates % maybeStates;
+            psiStates = psiStates % maybeStates;
+            
+            // Keep only the states that we do not eliminate in the maybe states.
+            maybeStates = phiStates | psiStates;
+            
+            STORM_LOG_DEBUG("Phi states in reduced model " << phiStates);
+            STORM_LOG_DEBUG("Psi states in reduced model " << psiStates);
+            storm::storage::BitVector statesToEliminate = ~maybeStates & ~newInitialStates;
+            STORM_LOG_DEBUG("Eliminating the states " << statesToEliminate);
+            
+            // Before starting the model checking process, we assign priorities to states so we can use them to
+            // impose ordering constraints later.
+            std::vector<std::size_t> statePriorities = getStatePriorities(submatrix, submatrixTransposed, newInitialStates, oneStepProbabilities);
+            
+            std::vector<storm::storage::sparse::state_type> states(statesToEliminate.begin(), statesToEliminate.end());
+            
+            // Sort the states according to the priorities.
+            std::sort(states.begin(), states.end(), [&statePriorities] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return statePriorities[a] < statePriorities[b]; });
+            
+            STORM_PRINT_AND_LOG("Computing conditional probilities." << std::endl);
+            STORM_PRINT_AND_LOG("Eliminating " << states.size() << " states using the state elimination technique." << std::endl);
+            boost::optional<std::vector<ValueType>> missingStateRewards;
+            FlexibleSparseMatrix flexibleMatrix = getFlexibleSparseMatrix(submatrix);
+            FlexibleSparseMatrix flexibleBackwardTransitions = getFlexibleSparseMatrix(submatrixTransposed, true);
+            for (auto const& state : states) {
+                eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions, missingStateRewards);
+            }
+            STORM_PRINT_AND_LOG("Eliminated " << states.size() << " states." << std::endl);
+            
+            eliminateState(flexibleMatrix, oneStepProbabilities, *newInitialStates.begin(), flexibleBackwardTransitions, missingStateRewards, false);
+            
+            // Now eliminate all chains of phi or psi states.
+            for (auto phiState : phiStates) {
+                // Only eliminate the state if it has a successor that is not itself.
+                auto const& currentRow = flexibleMatrix.getRow(phiState);
+                if (currentRow.size() == 1) {
+                    auto const& firstEntry = currentRow.front();
+                    if (firstEntry.getColumn() == phiState) {
+                        break;
+                    }
+                }
+                eliminateState(flexibleMatrix, oneStepProbabilities, phiState, flexibleBackwardTransitions, missingStateRewards, false, true, phiStates);
+            }
+            for (auto psiState : psiStates) {
+                // Only eliminate the state if it has a successor that is not itself.
+                auto const& currentRow = flexibleMatrix.getRow(psiState);
+                if (currentRow.size() == 1) {
+                    auto const& firstEntry = currentRow.front();
+                    if (firstEntry.getColumn() == psiState) {
+                        break;
+                    }
+                }
+                eliminateState(flexibleMatrix, oneStepProbabilities, psiState, flexibleBackwardTransitions, missingStateRewards, false, true, psiStates);
+            }
+            
+            ValueType numerator = storm::utility::zero<ValueType>();
+            ValueType denominator = storm::utility::zero<ValueType>();
+            
+            for (auto const& trans1 : flexibleMatrix.getRow(*newInitialStates.begin())) {
+                auto initialStateSuccessor = trans1.getColumn();
+                if (phiStates.get(initialStateSuccessor)) {
+                    ValueType additiveTerm = storm::utility::zero<ValueType>();
+                    for (auto const& trans2 : flexibleMatrix.getRow(initialStateSuccessor)) {
+                        STORM_LOG_ASSERT(psiStates.get(trans2.getColumn()), "Expected psi state.");
+                        additiveTerm += trans2.getValue();
+                    }
+                    additiveTerm *= trans1.getValue();
+                    numerator += additiveTerm;
+                    denominator += additiveTerm;
+                } else {
+                    STORM_LOG_ASSERT(psiStates.get(initialStateSuccessor), "Expected psi state.");
+                    denominator += trans1.getValue();
+                    ValueType additiveTerm = storm::utility::zero<ValueType>();
+                    for (auto const& trans2 : flexibleMatrix.getRow(initialStateSuccessor)) {
+                        STORM_LOG_ASSERT(phiStates.get(trans2.getColumn()), "Expected phi state.");
+                        additiveTerm += trans2.getValue();
+                    }
+                    numerator += trans1.getValue() * additiveTerm;
+                }
+            }
+            
+            return numerator / denominator;
+        }
+        
+        template<typename ValueType>
+        std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<ValueType>::checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) {
+            if (stateFormula.isTrueFormula()) {
+                return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(storm::storage::BitVector(model.getNumberOfStates(), true)));
+            } else {
+                return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(storm::storage::BitVector(model.getNumberOfStates())));
+            }
+        }
+        
+        template<typename ValueType>
+        std::unique_ptr<CheckResult> SparseDtmcEliminationModelChecker<ValueType>::checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) {
+            STORM_LOG_THROW(model.hasAtomicProposition(stateFormula.getLabel()), storm::exceptions::InvalidPropertyException, "The property refers to unknown label '" << stateFormula.getLabel() << "'.");
+            return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(model.getLabeledStates(stateFormula.getLabel())));
+        }
+        
+        template<typename ValueType>
+        ValueType SparseDtmcEliminationModelChecker<ValueType>::computeReachabilityValue(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional<std::vector<ValueType>>& stateRewards, boost::optional<std::vector<std::size_t>> const& statePriorities) {
+            std::chrono::high_resolution_clock::time_point totalTimeStart = std::chrono::high_resolution_clock::now();
+            std::chrono::high_resolution_clock::time_point conversionStart = std::chrono::high_resolution_clock::now();
+            
+            // Create a bit vector that represents the subsystem of states we still have to eliminate.
+            storm::storage::BitVector subsystem = storm::storage::BitVector(transitionMatrix.getRowCount(), true);
+            
+            // Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily.
+            FlexibleSparseMatrix flexibleMatrix = getFlexibleSparseMatrix(transitionMatrix);
+            FlexibleSparseMatrix flexibleBackwardTransitions = getFlexibleSparseMatrix(backwardTransitions, true);
+            auto conversionEnd = std::chrono::high_resolution_clock::now();
+            
+            std::chrono::high_resolution_clock::time_point modelCheckingStart = std::chrono::high_resolution_clock::now();
+            uint_fast64_t maximalDepth = 0;
+            if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::State) {
+                // If we are required to do pure state elimination, we simply create a vector of all states to
+                // eliminate and sort it according to the given priorities.
+                
+                // Remove the initial state from the states which we need to eliminate.
+                subsystem &= ~initialStates;
+                std::vector<storm::storage::sparse::state_type> states(subsystem.begin(), subsystem.end());
+                
+                if (statePriorities) {
+                    std::sort(states.begin(), states.end(), [&statePriorities] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return statePriorities.get()[a] < statePriorities.get()[b]; });
+                }
+                
+                STORM_PRINT_AND_LOG("Eliminating " << states.size() << " states using the state elimination technique." << std::endl);
+                for (auto const& state : states) {
+                    eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions, stateRewards);
+                }
+                STORM_PRINT_AND_LOG("Eliminated " << states.size() << " states." << std::endl);
+            } else if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::Hybrid) {
+                // When using the hybrid technique, we recursively treat the SCCs up to some size.
+                storm::utility::ConstantsComparator<ValueType> comparator;
+                std::vector<storm::storage::sparse::state_type> entryStateQueue;
+                STORM_PRINT_AND_LOG("Eliminating " << subsystem.size() << " states using the hybrid elimination technique." << std::endl);
+                maximalDepth = treatScc(flexibleMatrix, oneStepProbabilities, initialStates, subsystem, transitionMatrix, flexibleBackwardTransitions, false, 0, storm::settings::sparseDtmcEliminationModelCheckerSettings().getMaximalSccSize(), entryStateQueue, comparator, stateRewards, statePriorities);
+                
+                // If the entry states were to be eliminated last, we need to do so now.
+                STORM_LOG_DEBUG("Eliminating " << entryStateQueue.size() << " entry states as a last step.");
+                if (storm::settings::sparseDtmcEliminationModelCheckerSettings().isEliminateEntryStatesLastSet()) {
+                    for (auto const& state : entryStateQueue) {
+                        eliminateState(flexibleMatrix, oneStepProbabilities, state, flexibleBackwardTransitions, stateRewards);
+                    }
+                }
+                STORM_PRINT_AND_LOG("Eliminated " << subsystem.size() << " states." << std::endl);
+            }
+            
+            // Finally eliminate initial state.
+            if (!stateRewards) {
+                // If we are computing probabilities, then we can simply call the state elimination procedure. It
+                // will scale the transition row of the initial state with 1/(1-loopProbability).
+                STORM_PRINT_AND_LOG("Eliminating initial state " << *initialStates.begin() << "." << std::endl);
+                eliminateState(flexibleMatrix, oneStepProbabilities, *initialStates.begin(), flexibleBackwardTransitions, stateRewards);
+            } else {
+                // If we are computing rewards, we cannot call the state elimination procedure for technical reasons.
+                // Instead, we need to get rid of a potential loop in this state explicitly.
+                
+                // Start by finding the self-loop element. Since it can only be the only remaining outgoing transition
+                // of the initial state, this amounts to checking whether the outgoing transitions of the initial
+                // state are non-empty.
+                if (!flexibleMatrix.getRow(*initialStates.begin()).empty()) {
+                    STORM_LOG_ASSERT(flexibleMatrix.getRow(*initialStates.begin()).size() == 1, "At most one outgoing transition expected at this point, but found more.");
+                    STORM_LOG_ASSERT(flexibleMatrix.getRow(*initialStates.begin()).front().getColumn() == *initialStates.begin(), "Remaining entry should be a self-loop, but it is not.");
+                    ValueType loopProbability = flexibleMatrix.getRow(*initialStates.begin()).front().getValue();
+                    loopProbability = storm::utility::one<ValueType>() / (storm::utility::one<ValueType>() - loopProbability);
+                    loopProbability = storm::utility::pow(loopProbability, 2);
+                    STORM_PRINT_AND_LOG("Scaling the transition reward of the initial state.");
+                    stateRewards.get()[(*initialStates.begin())] *= loopProbability;
+                }
+            }
+            
+            // Make sure that we have eliminated all transitions from the initial state.
+            STORM_LOG_ASSERT(flexibleMatrix.getRow(*initialStates.begin()).empty(), "The transitions of the initial states are non-empty.");
+            
+            std::chrono::high_resolution_clock::time_point modelCheckingEnd = std::chrono::high_resolution_clock::now();
+            std::chrono::high_resolution_clock::time_point totalTimeEnd = std::chrono::high_resolution_clock::now();
+            
+            if (storm::settings::generalSettings().isShowStatisticsSet()) {
+                std::chrono::high_resolution_clock::duration conversionTime = conversionEnd - conversionStart;
+                std::chrono::milliseconds conversionTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(conversionTime);
+                std::chrono::high_resolution_clock::duration modelCheckingTime = modelCheckingEnd - modelCheckingStart;
+                std::chrono::milliseconds modelCheckingTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(modelCheckingTime);
+                std::chrono::high_resolution_clock::duration totalTime = totalTimeEnd - totalTimeStart;
+                std::chrono::milliseconds totalTimeInMilliseconds = std::chrono::duration_cast<std::chrono::milliseconds>(totalTime);
+                
+                STORM_PRINT_AND_LOG(std::endl);
+                STORM_PRINT_AND_LOG("Time breakdown:" << std::endl);
+                STORM_PRINT_AND_LOG("    * time for conversion: " << conversionTimeInMilliseconds.count() << "ms" << std::endl);
+                STORM_PRINT_AND_LOG("    * time for checking: " << modelCheckingTimeInMilliseconds.count() << "ms" << std::endl);
+                STORM_PRINT_AND_LOG("------------------------------------------" << std::endl);
+                STORM_PRINT_AND_LOG("    * total time: " << totalTimeInMilliseconds.count() << "ms" << std::endl);
+                STORM_PRINT_AND_LOG(std::endl);
+                STORM_PRINT_AND_LOG("Other:" << std::endl);
+                STORM_PRINT_AND_LOG("    * number of states eliminated: " << transitionMatrix.getRowCount() << std::endl);
+                if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationMethod() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationMethod::Hybrid) {
+                    STORM_PRINT_AND_LOG("    * maximal depth of SCC decomposition: " << maximalDepth << std::endl);
+                }
+            }
+            
+            // Now, we return the value for the only initial state.
+            if (stateRewards) {
+                return storm::utility::simplify(stateRewards.get()[*initialStates.begin()]);
+            } else {
+                return storm::utility::simplify(oneStepProbabilities[*initialStates.begin()]);
+            }
+        }
+        
+        template<typename ValueType>
+        std::vector<std::size_t> SparseDtmcEliminationModelChecker<ValueType>::getStatePriorities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector<ValueType> const& oneStepProbabilities) {
+            std::vector<std::size_t> statePriorities(transitionMatrix.getRowCount());
+            std::vector<std::size_t> states(transitionMatrix.getRowCount());
+            for (std::size_t index = 0; index < states.size(); ++index) {
+                states[index] = index;
+            }
+            if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationOrder() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Random) {
+                std::random_shuffle(states.begin(), states.end());
+            } else {
+                std::vector<std::size_t> distances;
+                if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationOrder() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Forward || storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationOrder() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::ForwardReversed) {
+                    distances = storm::utility::graph::getDistances(transitionMatrix, initialStates);
+                } else if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationOrder() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Backward || storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationOrder() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::BackwardReversed) {
+                    // Since the target states were eliminated from the matrix already, we construct a replacement by
+                    // treating all states that have some non-zero probability to go to a target state in one step.
+                    storm::utility::ConstantsComparator<ValueType> comparator;
+                    storm::storage::BitVector pseudoTargetStates(transitionMatrix.getRowCount());
+                    for (std::size_t index = 0; index < oneStepProbabilities.size(); ++index) {
+                        if (!comparator.isZero(oneStepProbabilities[index])) {
+                            pseudoTargetStates.set(index);
+                        }
+                    }
+                    
+                    distances = storm::utility::graph::getDistances(transitionMatrixTransposed, pseudoTargetStates);
+                } else {
+                    STORM_LOG_ASSERT(false, "Illegal sorting order selected.");
+                }
+                
+                // In case of the forward or backward ordering, we can sort the states according to the distances.
+                if (storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationOrder() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Forward || storm::settings::sparseDtmcEliminationModelCheckerSettings().getEliminationOrder() == storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::EliminationOrder::Backward) {
+                    std::sort(states.begin(), states.end(), [&distances] (storm::storage::sparse::state_type const& state1, storm::storage::sparse::state_type const& state2) { return distances[state1] < distances[state2]; } );
+                } else {
+                    // Otherwise, we sort them according to descending distances.
+                    std::sort(states.begin(), states.end(), [&distances] (storm::storage::sparse::state_type const& state1, storm::storage::sparse::state_type const& state2) { return distances[state1] > distances[state2]; } );
+                }
+            }
+            
+            // Now convert the ordering of the states to priorities.
+            for (std::size_t index = 0; index < states.size(); ++index) {
+                statePriorities[states[index]] = index;
+            }
+            
+            return statePriorities;
+        }
+        
+        template<typename ValueType>
+        uint_fast64_t SparseDtmcEliminationModelChecker<ValueType>::treatScc(FlexibleSparseMatrix& matrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector<storm::storage::sparse::state_type>& entryStateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator, boost::optional<std::vector<ValueType>>& stateRewards, boost::optional<std::vector<std::size_t>> const& statePriorities) {
+            uint_fast64_t maximalDepth = level;
+            
+            // If the SCCs are large enough, we try to split them further.
+            if (scc.getNumberOfSetBits() > maximalSccSize) {
+                STORM_LOG_DEBUG("SCC is large enough (" << scc.getNumberOfSetBits() << " states) to be decomposed further.");
+                
+                // Here, we further decompose the SCC into sub-SCCs.
+                storm::storage::StronglyConnectedComponentDecomposition<ValueType> decomposition(forwardTransitions, scc & ~entryStates, false, false);
+                STORM_LOG_DEBUG("Decomposed SCC into " << decomposition.size() << " sub-SCCs.");
+                
+                // Store a bit vector of remaining SCCs so we can be flexible when it comes to the order in which
+                // we eliminate the SCCs.
+                storm::storage::BitVector remainingSccs(decomposition.size(), true);
+                
+                // First, get rid of the trivial SCCs.
+                std::vector<std::pair<storm::storage::sparse::state_type, uint_fast64_t>> trivialSccs;
+                for (uint_fast64_t sccIndex = 0; sccIndex < decomposition.size(); ++sccIndex) {
+                    storm::storage::StronglyConnectedComponent const& scc = decomposition.getBlock(sccIndex);
+                    if (scc.isTrivial()) {
+                        storm::storage::sparse::state_type onlyState = *scc.begin();
+                        trivialSccs.emplace_back(onlyState, sccIndex);
+                    }
+                }
+                
+                // If we are given priorities, sort the trivial SCCs accordingly.
+                if (statePriorities) {
+                    std::sort(trivialSccs.begin(), trivialSccs.end(), [&statePriorities] (std::pair<storm::storage::sparse::state_type, uint_fast64_t> const& a, std::pair<storm::storage::sparse::state_type, uint_fast64_t> const& b) { return statePriorities.get()[a.first] < statePriorities.get()[b.first]; });
+                }
+                
+                STORM_LOG_DEBUG("Eliminating " << trivialSccs.size() << " trivial SCCs.");
+                for (auto const& stateIndexPair : trivialSccs) {
+                    eliminateState(matrix, oneStepProbabilities, stateIndexPair.first, backwardTransitions, stateRewards);
+                    remainingSccs.set(stateIndexPair.second, false);
+                }
+                STORM_LOG_DEBUG("Eliminated all trivial SCCs.");
+                
+                // And then recursively treat the remaining sub-SCCs.
+                STORM_LOG_DEBUG("Eliminating " << remainingSccs.getNumberOfSetBits() << " remaining SCCs on level " << level << ".");
+                for (auto sccIndex : remainingSccs) {
+                    storm::storage::StronglyConnectedComponent const& newScc = decomposition.getBlock(sccIndex);
+                    
+                    // Rewrite SCC into bit vector and subtract it from the remaining states.
+                    storm::storage::BitVector newSccAsBitVector(forwardTransitions.getRowCount(), newScc.begin(), newScc.end());
+                    
+                    // Determine the set of entry states of the SCC.
+                    storm::storage::BitVector entryStates(forwardTransitions.getRowCount());
+                    for (auto const& state : newScc) {
+                        for (auto const& predecessor : backwardTransitions.getRow(state)) {
+                            if (predecessor.getValue() != storm::utility::zero<ValueType>() && !newSccAsBitVector.get(predecessor.getColumn())) {
+                                entryStates.set(state);
+                            }
+                        }
+                    }
+                    
+                    // Recursively descend in SCC-hierarchy.
+                    uint_fast64_t depth = treatScc(matrix, oneStepProbabilities, entryStates, newSccAsBitVector, forwardTransitions, backwardTransitions, !storm::settings::sparseDtmcEliminationModelCheckerSettings().isEliminateEntryStatesLastSet(), level + 1, maximalSccSize, entryStateQueue, comparator, stateRewards, statePriorities);
+                    maximalDepth = std::max(maximalDepth, depth);
+                }
+                
+            } else {
+                // In this case, we perform simple state elimination in the current SCC.
+                STORM_LOG_DEBUG("SCC of size " << scc.getNumberOfSetBits() << " is small enough to be eliminated directly.");
+                storm::storage::BitVector remainingStates = scc & ~entryStates;
+                
+                std::vector<uint_fast64_t> states(remainingStates.begin(), remainingStates.end());
+                
+                // If we are given priorities, sort the trivial SCCs accordingly.
+                if (statePriorities) {
+                    std::sort(states.begin(), states.end(), [&statePriorities] (storm::storage::sparse::state_type const& a, storm::storage::sparse::state_type const& b) { return statePriorities.get()[a] < statePriorities.get()[b]; });
+                }
+                
+                // Eliminate the remaining states that do not have a self-loop (in the current, i.e. modified)
+                // transition probability matrix.
+                for (auto const& state : states) {
+                    eliminateState(matrix, oneStepProbabilities, state, backwardTransitions, stateRewards);
+                }
+                
+                STORM_LOG_DEBUG("Eliminated all states of SCC.");
+            }
+            
+            // Finally, eliminate the entry states (if we are required to do so).
+            if (eliminateEntryStates) {
+                STORM_LOG_DEBUG("Finally, eliminating/adding entry states.");
+                for (auto state : entryStates) {
+                    eliminateState(matrix, oneStepProbabilities, state, backwardTransitions, stateRewards);
+                }
+                STORM_LOG_DEBUG("Eliminated/added entry states.");
+            } else {
+                for (auto state : entryStates) {
+                    entryStateQueue.push_back(state);
+                }
+            }
+            
+            return maximalDepth;
+        }
+        
+        namespace {
+            static int chunkCounter = 0;
+            static int counter = 0;
+        }
+        
+        template<typename ValueType>
+        void SparseDtmcEliminationModelChecker<ValueType>::eliminateState(FlexibleSparseMatrix& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions, boost::optional<std::vector<ValueType>>& stateRewards, bool removeForwardTransitions, bool constrained, storm::storage::BitVector const& predecessorConstraint) {
+            auto eliminationStart = std::chrono::high_resolution_clock::now();
+            
+            ++counter;
+            STORM_LOG_DEBUG("Eliminating state " << state << ".");
+            if (counter > matrix.getNumberOfRows() / 10) {
+                ++chunkCounter;
+                STORM_PRINT_AND_LOG("Eliminated " << (chunkCounter * 10) << "% of the states." << std::endl);
+                counter = 0;
+            }
+            
+            bool hasSelfLoop = false;
+            ValueType loopProbability = storm::utility::    <ValueType>();
+            
+            // Start by finding loop probability.
+            typename FlexibleSparseMatrix::row_type& currentStateSuccessors = matrix.getRow(state);
+            for (auto const& entry : currentStateSuccessors) {
+                if (entry.getColumn() >= state) {
+                    if (entry.getColumn() == state) {
+                        loopProbability = entry.getValue();
+                        hasSelfLoop = true;
+                    }
+                    break;
+                }
+            }
+            
+            // Scale all entries in this row with (1 / (1 - loopProbability)) only in case there was a self-loop.
+            std::size_t scaledSuccessors = 0;
+            if (hasSelfLoop) {
+                loopProbability = storm::utility::one<ValueType>() / (storm::utility::one<ValueType>() - loopProbability);
+                storm::utility::simplify(loopProbability);
+                for (auto& entry : matrix.getRow(state)) {
+                    // Only scale the non-diagonal entries.
+                    if (entry.getColumn() != state) {
+                        ++scaledSuccessors;
+                        entry.setValue(storm::utility::simplify(entry.getValue() * loopProbability));
+                    }
+                }
+                if (!stateRewards) {
+                    oneStepProbabilities[state] = oneStepProbabilities[state] * loopProbability;
+                }
+            }
+            
+            STORM_LOG_DEBUG((hasSelfLoop ? "State has self-loop." : "State does not have a self-loop."));
+            
+            // Now connect the predecessors of the state being eliminated with its successors.
+            typename FlexibleSparseMatrix::row_type& currentStatePredecessors = backwardTransitions.getRow(state);
+            std::size_t numberOfPredecessors = currentStatePredecessors.size();
+            std::size_t predecessorForwardTransitionCount = 0;
+            for (auto const& predecessorEntry : currentStatePredecessors) {
+                uint_fast64_t predecessor = predecessorEntry.getColumn();
+                
+                // Skip the state itself as one of its predecessors.
+                if (predecessor == state) {
+                    assert(hasSelfLoop);
+                    continue;
+                }
+                
+                // Skip the state if the elimination is constrained, but the predecessor is not in the constraint.
+                if (constrained && !predecessorConstraint.get(predecessor)) {
+                    continue;
+                }
+                
+                // First, find the probability with which the predecessor can move to the current state, because
+                // the other probabilities need to be scaled with this factor.
+                typename FlexibleSparseMatrix::row_type& predecessorForwardTransitions = matrix.getRow(predecessor);
+                predecessorForwardTransitionCount += predecessorForwardTransitions.size();
+                typename FlexibleSparseMatrix::row_type::iterator multiplyElement = std::find_if(predecessorForwardTransitions.begin(), predecessorForwardTransitions.end(), [&](storm::storage::MatrixEntry<typename FlexibleSparseMatrix::index_type, typename FlexibleSparseMatrix::value_type> const& a) { return a.getColumn() == state; });
+                
+                // Make sure we have found the probability and set it to zero.
+                STORM_LOG_THROW(multiplyElement != predecessorForwardTransitions.end(), storm::exceptions::InvalidStateException, "No probability for successor found.");
+                ValueType multiplyFactor = multiplyElement->getValue();
+                multiplyElement->setValue(storm::utility::zero<ValueType>());
+                
+                // At this point, we need to update the (forward) transitions of the predecessor.
+                typename FlexibleSparseMatrix::row_type::iterator first1 = predecessorForwardTransitions.begin();
+                typename FlexibleSparseMatrix::row_type::iterator last1 = predecessorForwardTransitions.end();
+                typename FlexibleSparseMatrix::row_type::iterator first2 = currentStateSuccessors.begin();
+                typename FlexibleSparseMatrix::row_type::iterator last2 = currentStateSuccessors.end();
+                
+                typename FlexibleSparseMatrix::row_type newSuccessors;
+                newSuccessors.reserve((last1 - first1) + (last2 - first2));
+                std::insert_iterator<typename FlexibleSparseMatrix::row_type> result(newSuccessors, newSuccessors.end());
+                
+                // Now we merge the two successor lists. (Code taken from std::set_union and modified to suit our needs).
+                for (; first1 != last1; ++result) {
+                    // Skip the transitions to the state that is currently being eliminated.
+                    if (first1->getColumn() == state || (first2 != last2 && first2->getColumn() == state)) {
+                        if (first1->getColumn() == state) {
+                            ++first1;
+                        }
+                        if (first2 != last2 && first2->getColumn() == state) {
+                            ++first2;
+                        }
+                        continue;
+                    }
+                    
+                    if (first2 == last2) {
+                        std::copy_if(first1, last1, result, [&] (storm::storage::MatrixEntry<typename FlexibleSparseMatrix::index_type, typename FlexibleSparseMatrix::value_type> const& a) { return a.getColumn() != state; } );
+                        break;
+                    }
+                    if (first2->getColumn() < first1->getColumn()) {
+                        *result = storm::utility::simplify(std::move(*first2 * multiplyFactor));
+                        ++first2;
+                    } else if (first1->getColumn() < first2->getColumn()) {
+                        *result = *first1;
+                        ++first1;
+                    } else {
+                        *result = storm::storage::MatrixEntry<typename FlexibleSparseMatrix::index_type, typename FlexibleSparseMatrix::value_type>(first1->getColumn(), storm::utility::simplify(first1->getValue() + storm::utility::simplify(multiplyFactor * first2->getValue())));
+                        ++first1;
+                        ++first2;
+                    }
+                }
+                for (; first2 != last2; ++first2) {
+                    if (first2->getColumn() != state) {
+                        *result = storm::utility::simplify(std::move(*first2 * multiplyFactor));
+                    }
+                }
+                
+                // Now move the new transitions in place.
+                predecessorForwardTransitions = std::move(newSuccessors);
+                
+                if (!stateRewards) {
+                    // Add the probabilities to go to a target state in just one step if we have to compute probabilities.
+                    oneStepProbabilities[predecessor] += storm::utility::simplify(multiplyFactor * oneStepProbabilities[state]);
+                    STORM_LOG_DEBUG("Fixed new next-state probabilities of predecessor states.");
+                } else {
+                    // If we are computing rewards, we basically scale the state reward of the state to eliminate and
+                    // add the result to the state reward of the predecessor.
+                    if (hasSelfLoop) {
+                        stateRewards.get()[predecessor] += storm::utility::simplify(multiplyFactor * storm::utility::pow(loopProbability, 2) * stateRewards.get()[state]);
+                    } else {
+                        stateRewards.get()[predecessor] += storm::utility::simplify(multiplyFactor * stateRewards.get()[state]);
+                    }
+                }
+            }
+            
+            // Finally, we need to add the predecessor to the set of predecessors of every successor.
+            for (auto const& successorEntry : currentStateSuccessors) {
+                typename FlexibleSparseMatrix::row_type& successorBackwardTransitions = backwardTransitions.getRow(successorEntry.getColumn());
+                
+                // Delete the current state as a predecessor of the successor state.
+                typename FlexibleSparseMatrix::row_type::iterator elimIt = std::find_if(successorBackwardTransitions.begin(), successorBackwardTransitions.end(), [&](storm::storage::MatrixEntry<typename FlexibleSparseMatrix::index_type, typename FlexibleSparseMatrix::value_type> const& a) { return a.getColumn() == state; });
+                if (elimIt != successorBackwardTransitions.end()) {
+                    successorBackwardTransitions.erase(elimIt);
+                }
+                
+                typename FlexibleSparseMatrix::row_type::iterator first1 = successorBackwardTransitions.begin();
+                typename FlexibleSparseMatrix::row_type::iterator last1 = successorBackwardTransitions.end();
+                typename FlexibleSparseMatrix::row_type::iterator first2 = currentStatePredecessors.begin();
+                typename FlexibleSparseMatrix::row_type::iterator last2 = currentStatePredecessors.end();
+                
+                typename FlexibleSparseMatrix::row_type newPredecessors;
+                newPredecessors.reserve((last1 - first1) + (last2 - first2));
+                std::insert_iterator<typename FlexibleSparseMatrix::row_type> result(newPredecessors, newPredecessors.end());
+                
+                
+                for (; first1 != last1; ++result) {
+                    if (first2 == last2) {
+                        std::copy_if(first1, last1, result, [&] (storm::storage::MatrixEntry<typename FlexibleSparseMatrix::index_type, typename FlexibleSparseMatrix::value_type> const& a) { return a.getColumn() != state; });
+                        break;
+                    }
+                    if (first2->getColumn() < first1->getColumn()) {
+                        if (first2->getColumn() != state) {
+                            *result = *first2;
+                        }
+                        ++first2;
+                    } else {
+                        if (first1->getColumn() != state) {
+                            *result = *first1;
+                        }
+                        if (first1->getColumn() == first2->getColumn()) {
+                            ++first2;
+                        }
+                        ++first1;
+                    }
+                }
+                std::copy_if(first2, last2, result, [&] (storm::storage::MatrixEntry<typename FlexibleSparseMatrix::index_type, typename FlexibleSparseMatrix::value_type> const& a) { return a.getColumn() != state; });
+                
+                // Now move the new predecessors in place.
+                successorBackwardTransitions = std::move(newPredecessors);
+                
+            }
+            STORM_LOG_DEBUG("Fixed predecessor lists of successor states.");
+            
+            if (removeForwardTransitions) {
+                // Clear the eliminated row to reduce memory consumption.
+                currentStateSuccessors.clear();
+                currentStateSuccessors.shrink_to_fit();
+            }
+            if (!constrained) {
+                // FIXME: is this safe? If the elimination is constrained, we might have to repair the predecessor
+                // relation.
+                currentStatePredecessors.clear();
+                currentStatePredecessors.shrink_to_fit();
+            }
+            
+            auto eliminationEnd = std::chrono::high_resolution_clock::now();
+            auto eliminationTime = eliminationEnd - eliminationStart;
+        }
+        
+        template<typename ValueType>
+        SparseDtmcEliminationModelChecker<ValueType>::FlexibleSparseMatrix::FlexibleSparseMatrix(index_type rows) : data(rows) {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType>
+        void SparseDtmcEliminationModelChecker<ValueType>::FlexibleSparseMatrix::reserveInRow(index_type row, index_type numberOfElements) {
+            this->data[row].reserve(numberOfElements);
+        }
+        
+        template<typename ValueType>
+        typename SparseDtmcEliminationModelChecker<ValueType>::FlexibleSparseMatrix::row_type& SparseDtmcEliminationModelChecker<ValueType>::FlexibleSparseMatrix::getRow(index_type index) {
+            return this->data[index];
+        }
+        
+        template<typename ValueType>
+        typename SparseDtmcEliminationModelChecker<ValueType>::FlexibleSparseMatrix::row_type const& SparseDtmcEliminationModelChecker<ValueType>::FlexibleSparseMatrix::getRow(index_type index) const {
+            return this->data[index];
+        }
+        
+        template<typename ValueType>
+        typename SparseDtmcEliminationModelChecker<ValueType>::FlexibleSparseMatrix::index_type SparseDtmcEliminationModelChecker<ValueType>::FlexibleSparseMatrix::getNumberOfRows() const {
+            return this->data.size();
+        }
+        
+        template<typename ValueType>
+        bool SparseDtmcEliminationModelChecker<ValueType>::FlexibleSparseMatrix::hasSelfLoop(storm::storage::sparse::state_type state) {
+            for (auto const& entry : this->getRow(state)) {
+                if (entry.getColumn() < state) {
+                    continue;
+                } else if (entry.getColumn() > state) {
+                    return false;
+                } else if (entry.getColumn() == state) {
+                    return true;
+                }
+            }
+            return false;
+        }
+        
+        template<typename ValueType>
+        void SparseDtmcEliminationModelChecker<ValueType>::FlexibleSparseMatrix::print() const {
+            for (uint_fast64_t index = 0; index < this->data.size(); ++index) {
+                std::cout << index << " - ";
+                for (auto const& element : this->getRow(index)) {
+                    std::cout << "(" << element.getColumn() << ", " << element.getValue() << ") ";
+                }
+                std::cout << std::endl;
+            }
+        }
+        
+        template<typename ValueType>
+        typename SparseDtmcEliminationModelChecker<ValueType>::FlexibleSparseMatrix SparseDtmcEliminationModelChecker<ValueType>::getFlexibleSparseMatrix(storm::storage::SparseMatrix<ValueType> const& matrix, bool setAllValuesToOne) {
+            FlexibleSparseMatrix flexibleMatrix(matrix.getRowCount());
+            
+            for (typename FlexibleSparseMatrix::index_type rowIndex = 0; rowIndex < matrix.getRowCount(); ++rowIndex) {
+                typename storm::storage::SparseMatrix<ValueType>::const_rows row = matrix.getRow(rowIndex);
+                flexibleMatrix.reserveInRow(rowIndex, row.getNumberOfEntries());
+                
+                for (auto const& element : row) {
+                    if (setAllValuesToOne) {
+                        flexibleMatrix.getRow(rowIndex).emplace_back(element.getColumn(), storm::utility::one<ValueType>());
+                    } else {
+                        flexibleMatrix.getRow(rowIndex).emplace_back(element);
+                    }
+                }
+            }
+            
+            return flexibleMatrix;
+        }
+        
+        template class SparseDtmcEliminationModelChecker<double>;
+        
+#ifdef PARAMETRIC_SYSTEMS
+        template class FlexibleSparseMatrix<RationalFunction>;
+        template class SparseDtmcEliminationModelChecker<RationalFunction>;
+#endif
+    } // namespace modelchecker
+} // namespace storm
diff --git a/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h
new file mode 100644
index 000000000..d3ab0bdd0
--- /dev/null
+++ b/src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h
@@ -0,0 +1,75 @@
+#ifndef STORM_MODELCHECKER_REACHABILITY_SPARSEDTMCELIMINATIONMODELCHECKER_H_
+#define STORM_MODELCHECKER_REACHABILITY_SPARSEDTMCELIMINATIONMODELCHECKER_H_
+
+#include "src/storage/sparse/StateType.h"
+#include "src/models/Dtmc.h"
+#include "src/modelchecker/AbstractModelChecker.h"
+
+namespace storm {
+    namespace modelchecker {
+        
+        template<typename ValueType>
+        class SparseDtmcEliminationModelChecker : public AbstractModelChecker {
+        public:
+            explicit SparseDtmcEliminationModelChecker(storm::models::Dtmc<ValueType> const& model);
+            
+            // The implemented methods of the AbstractModelChecker interface.
+            virtual bool canHandle(storm::logic::Formula const& formula) const override;
+            virtual std::unique_ptr<CheckResult> computeUntilProbabilities(storm::logic::UntilFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
+            virtual std::unique_ptr<CheckResult> computeReachabilityRewards(storm::logic::ReachabilityRewardFormula const& rewardPathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
+            virtual std::unique_ptr<CheckResult> computeConditionalProbabilities(storm::logic::ConditionalPathFormula const& pathFormula, bool qualitative = false, boost::optional<storm::logic::OptimalityType> const& optimalityType = boost::optional<storm::logic::OptimalityType>()) override;
+            virtual std::unique_ptr<CheckResult> checkBooleanLiteralFormula(storm::logic::BooleanLiteralFormula const& stateFormula) override;
+            virtual std::unique_ptr<CheckResult> checkAtomicLabelFormula(storm::logic::AtomicLabelFormula const& stateFormula) override;
+            
+        private:
+            class FlexibleSparseMatrix {
+            public:
+                typedef uint_fast64_t index_type;
+                typedef ValueType value_type;
+                typedef std::vector<storm::storage::MatrixEntry<index_type, value_type>> row_type;
+                typedef typename row_type::iterator iterator;
+                typedef typename row_type::const_iterator const_iterator;
+                
+                FlexibleSparseMatrix() = default;
+                FlexibleSparseMatrix(index_type rows);
+                
+                void reserveInRow(index_type row, index_type numberOfElements);
+                
+                row_type& getRow(index_type);
+                row_type const& getRow(index_type) const;
+                
+                index_type getNumberOfRows() const;
+                
+                void print() const;
+                
+                /*!
+                 * Checks whether the given state has a self-loop with an arbitrary probability in the given probability matrix.
+                 *
+                 * @param state The state for which to check whether it possesses a self-loop.
+                 * @param matrix The matrix in which to look for the loop.
+                 * @return True iff the given state has a self-loop with an arbitrary probability in the given probability matrix.
+                 */
+                bool hasSelfLoop(storm::storage::sparse::state_type state);
+                
+            private:
+                std::vector<row_type> data;
+            };
+            
+            static ValueType computeReachabilityValue(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::SparseMatrix<ValueType> const& backwardTransitions, storm::storage::BitVector const& initialStates, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates, boost::optional<std::vector<ValueType>>& stateRewards, boost::optional<std::vector<std::size_t>> const& statePriorities = {});
+            
+            static uint_fast64_t treatScc(FlexibleSparseMatrix& matrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, FlexibleSparseMatrix& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level, uint_fast64_t maximalSccSize, std::vector<storm::storage::sparse::state_type>& entryStateQueue, storm::utility::ConstantsComparator<ValueType> const& comparator, boost::optional<std::vector<ValueType>>& stateRewards, boost::optional<std::vector<std::size_t>> const& statePriorities = {});
+            
+            static FlexibleSparseMatrix getFlexibleSparseMatrix(storm::storage::SparseMatrix<ValueType> const& matrix, bool setAllValuesToOne = false);
+            
+            static void eliminateState(FlexibleSparseMatrix& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix& backwardTransitions, boost::optional<std::vector<ValueType>>& stateRewards, bool removeForwardTransitions = true, bool constrained = false, storm::storage::BitVector const& predecessorConstraint = storm::storage::BitVector());
+            
+            static std::vector<std::size_t> getStatePriorities(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& transitionMatrixTransposed, storm::storage::BitVector const& initialStates, std::vector<ValueType> const& oneStepProbabilities);
+            
+            // The model this model checker is supposed to analyze.
+            storm::models::Dtmc<ValueType> const& model;
+        };
+        
+    } // namespace modelchecker
+} // namespace storm
+
+#endif /* STORM_MODELCHECKER_REACHABILITY_SPARSEDTMCELIMINATIONMODELCHECKER_H_ */
diff --git a/src/modelchecker/reachability/SparseSccModelChecker.cpp b/src/modelchecker/reachability/SparseSccModelChecker.cpp
deleted file mode 100644
index 6edcd08fb..000000000
--- a/src/modelchecker/reachability/SparseSccModelChecker.cpp
+++ /dev/null
@@ -1,435 +0,0 @@
-#include "src/modelchecker/reachability/SparseSccModelChecker.h"
-
-#include <algorithm>
-
-#include "src/storage/StronglyConnectedComponentDecomposition.h"
-#include "src/utility/graph.h"
-#include "src/utility/vector.h"
-#include "src/exceptions/InvalidStateException.h"
-#include "src/utility/macros.h"
-
-namespace storm {
-    namespace modelchecker {
-        namespace reachability {
-            
-            template<typename ValueType>
-            static ValueType&& simplify(ValueType&& value) {
-                // In the general case, we don't to anything here, but merely return the value. If something else is
-                // supposed to happen here, the templated function can be specialized for this particular type.
-                return std::forward<ValueType>(value);
-            }
-            
-            template<typename IndexType, typename ValueType>
-            static storm::storage::MatrixEntry<IndexType, ValueType>&& simplify(storm::storage::MatrixEntry<IndexType, ValueType>&& matrixEntry) {
-                simplify(matrixEntry.getValue());
-                return std::move(matrixEntry);
-            }
-            
-            template<typename IndexType, typename ValueType>
-            static storm::storage::MatrixEntry<IndexType, ValueType>& simplify(storm::storage::MatrixEntry<IndexType, ValueType>& matrixEntry) {
-                matrixEntry.setValue(simplify(matrixEntry.getValue()));
-                return matrixEntry;
-            }
-            
-            template<typename ValueType>
-            ValueType SparseSccModelChecker<ValueType>::computeReachabilityProbability(storm::models::Dtmc<ValueType> const& dtmc, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
-                // First, do some sanity checks to establish some required properties.
-                STORM_LOG_THROW(dtmc.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::IllegalArgumentException, "Input model is required to have exactly one initial state.");
-                typename FlexibleSparseMatrix<ValueType>::index_type initialStateIndex = *dtmc.getInitialStates().begin();
-                
-                // Then, compute the subset of states that has a probability of 0 or 1, respectively.
-                std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(dtmc, phiStates, psiStates);
-                storm::storage::BitVector statesWithProbability0 = statesWithProbability01.first;
-                storm::storage::BitVector statesWithProbability1 = statesWithProbability01.second;
-                storm::storage::BitVector maybeStates = ~(statesWithProbability0 | statesWithProbability1);
-                
-                // If the initial state is known to have either probability 0 or 1, we can directly return the result.
-                if (!maybeStates.get(initialStateIndex)) {
-                    return statesWithProbability0.get(initialStateIndex) ? 0 : 1;
-                }
-                
-                // Determine the set of states that is reachable from the initial state without jumping over a target state.
-                storm::storage::BitVector reachableStates = storm::utility::graph::getReachableStates(dtmc.getTransitionMatrix(), dtmc.getInitialStates(), maybeStates, statesWithProbability1);
-                
-                // Subtract from the maybe states the set of states that is not reachable (on a path from the initial to a target state).
-                maybeStates &= reachableStates;
-                
-                // Create a vector for the probabilities to go to a state with probability 1 in one step.
-                std::vector<ValueType> oneStepProbabilities = dtmc.getTransitionMatrix().getConstrainedRowSumVector(maybeStates, statesWithProbability1);
-                
-                // Determine the set of initial states of the sub-DTMC.
-                storm::storage::BitVector newInitialStates = dtmc.getInitialStates() % maybeStates;
-                
-                // We then build the submatrix that only has the transitions of the maybe states.
-                storm::storage::SparseMatrix<ValueType> submatrix = dtmc.getTransitionMatrix().getSubmatrix(false, maybeStates, maybeStates);
-                
-                // Create a bit vector that represents the subsystem of states we still have to eliminate.
-                storm::storage::BitVector subsystem = storm::storage::BitVector(maybeStates.getNumberOfSetBits(), true);
-                
-                // Then, we convert the reduced matrix to a more flexible format to be able to perform state elimination more easily.
-                FlexibleSparseMatrix<ValueType> flexibleMatrix = getFlexibleSparseMatrix(submatrix);
-                FlexibleSparseMatrix<ValueType> flexibleBackwardTransitions = getFlexibleSparseMatrix(submatrix.transpose(), true);
-                
-                // Then, we recursively treat all SCCs.
-                treatScc(dtmc, flexibleMatrix, oneStepProbabilities, newInitialStates, subsystem, submatrix, flexibleBackwardTransitions, false, 0);
-                
-                // Now, we return the value for the only initial state.
-                return oneStepProbabilities[initialStateIndex];
-            }
-            
-            template<typename ValueType>
-            void SparseSccModelChecker<ValueType>::treatScc(storm::models::Dtmc<ValueType> const& dtmc, FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, FlexibleSparseMatrix<ValueType>& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level) {
-                // If the SCCs are large enough, we try to split them further.
-                if (scc.getNumberOfSetBits() > SparseSccModelChecker<ValueType>::maximalSccSize) {
-                    // Here, we further decompose the SCC into sub-SCCs.
-                    storm::storage::StronglyConnectedComponentDecomposition<ValueType> decomposition(forwardTransitions, scc & ~entryStates, false, false);
-                    
-                    // To eliminate the remaining one-state SCCs, we need to keep track of them.
-                    // storm::storage::BitVector remainingStates(scc);
-                    
-                    // Store a bit vector of remaining SCCs so we can be flexible when it comes to the order in which
-                    // we eliminate the SCCs.
-                    storm::storage::BitVector remainingSccs(decomposition.size(), true);
-                    
-                    // First, get rid of the trivial SCCs.
-                    for (uint_fast64_t sccIndex = 0; sccIndex < decomposition.size(); ++sccIndex) {
-                        storm::storage::StronglyConnectedComponent const& scc = decomposition.getBlock(sccIndex);
-                        if (scc.isTrivial()) {
-                            storm::storage::sparse::state_type onlyState = *scc.begin();
-                            eliminateState(matrix, oneStepProbabilities, onlyState, backwardTransitions);
-                            remainingSccs.set(sccIndex, false);
-                        }
-                    }
-                    
-                    // And then recursively treat the remaining sub-SCCs.
-                    for (auto sccIndex : remainingSccs) {
-                        storm::storage::StronglyConnectedComponent const& newScc = decomposition.getBlock(sccIndex);
-                        // If the SCC consists of just one state, we do not explore it recursively, but rather eliminate
-                        // it directly.
-                        if (newScc.size() == 1) {
-                            continue;
-                        }
-                        
-                        // Rewrite SCC into bit vector and subtract it from the remaining states.
-                        storm::storage::BitVector newSccAsBitVector(forwardTransitions.getRowCount(), newScc.begin(), newScc.end());
-                        // remainingStates &= ~newSccAsBitVector;
-                        
-                        // Determine the set of entry states of the SCC.
-                        storm::storage::BitVector entryStates(dtmc.getNumberOfStates());
-                        for (auto const& state : newScc) {
-                            for (auto const& predecessor : backwardTransitions.getRow(state)) {
-                                if (predecessor.getValue() > storm::utility::constantZero<ValueType>() && !newSccAsBitVector.get(predecessor.getColumn())) {
-                                    entryStates.set(state);
-                                }
-                            }
-                        }
-                        
-                        // Recursively descend in SCC-hierarchy.
-                        treatScc(dtmc, matrix, oneStepProbabilities, entryStates, newSccAsBitVector, forwardTransitions, backwardTransitions, true, level + 1);
-                    }
-                    
-                    // If we are not supposed to eliminate the entry states, we need to take them out of the set of
-                    // remaining states.
-                    // if (!eliminateEntryStates) {
-                    //     remainingStates &= ~entryStates;
-                    // }
-                    //
-                    // Now that we eliminated all non-trivial sub-SCCs, we need to take care of trivial sub-SCCs.
-                    // Therefore, we need to eliminate all states.
-                    // for (auto const& state : remainingStates) {
-                    //     eliminateState(matrix, oneStepProbabilities, state, backwardTransitions);
-                    // }
-                } else {
-                    // In this case, we perform simple state elimination in the current SCC.
-                    storm::storage::BitVector remainingStates = scc;
-                    
-//                    if (eliminateEntryStates) {
-                        remainingStates &= ~entryStates;
-//                    }
-                    
-                    // Eliminate the remaining states.
-                    for (auto const& state : remainingStates) {
-                        eliminateState(matrix, oneStepProbabilities, state, backwardTransitions);
-                    }
-                    
-                    // Finally, eliminate the entry states (if we are allowed to do so).
-                    if (eliminateEntryStates) {
-                        for (auto state : entryStates) {
-                            eliminateState(matrix, oneStepProbabilities, state, backwardTransitions);
-                        }
-                    }
-                }
-            }
-            
-            template<typename ValueType>
-            void SparseSccModelChecker<ValueType>::eliminateState(FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix<ValueType>& backwardTransitions) {
-                bool hasSelfLoop = false;
-                ValueType loopProbability = storm::utility::constantZero<ValueType>();
-                
-                // Start by finding loop probability.
-                typename FlexibleSparseMatrix<ValueType>::row_type& currentStateSuccessors = matrix.getRow(state);
-                for (auto const& entry : currentStateSuccessors) {
-                    if (entry.getColumn() >= state) {
-                        if (entry.getColumn() == state) {
-                            loopProbability = entry.getValue();
-                            hasSelfLoop = true;
-                        }
-                        break;
-                    }
-                }
-                
-                // Scale all entries in this row with (1 / (1 - loopProbability)) only in case there was a self-loop.
-                if (hasSelfLoop) {
-                    loopProbability = 1 / (1 - loopProbability);
-                    simplify(loopProbability);
-                    for (auto& entry : matrix.getRow(state)) {
-                        entry.setValue(simplify(entry.getValue() * loopProbability));
-                    }
-                    oneStepProbabilities[state] = simplify(oneStepProbabilities[state] * loopProbability);
-                }
-                
-                // Now connect the predecessors of the state being eliminated with its successors.
-                typename FlexibleSparseMatrix<ValueType>::row_type& currentStatePredecessors = backwardTransitions.getRow(state);
-                for (auto const& predecessorEntry : currentStatePredecessors) {
-                    uint_fast64_t predecessor = predecessorEntry.getColumn();
-                    
-                    // Skip the state itself as one of its predecessors.
-                    if (predecessor == state) {
-                        continue;
-                    }
-                    
-                    // First, find the probability with which the predecessor can move to the current state, because
-                    // the other probabilities need to be scaled with this factor.
-                    typename FlexibleSparseMatrix<ValueType>::row_type& predecessorForwardTransitions = matrix.getRow(predecessor);
-                    typename FlexibleSparseMatrix<ValueType>::row_type::iterator multiplyElement = std::find_if(predecessorForwardTransitions.begin(), predecessorForwardTransitions.end(), [&](storm::storage::MatrixEntry<typename FlexibleSparseMatrix<ValueType>::index_type, typename FlexibleSparseMatrix<ValueType>::value_type> const& a) { return a.getColumn() == state; });
-                    
-                    // Make sure we have found the probability and set it to zero.
-                    STORM_LOG_THROW(multiplyElement != predecessorForwardTransitions.end(), storm::exceptions::InvalidStateException, "No probability for successor found.");
-                    ValueType multiplyFactor = multiplyElement->getValue();
-                    multiplyElement->setValue(0);
-                    
-                    // At this point, we need to update the (forward) transitions of the predecessor.
-                    typename FlexibleSparseMatrix<ValueType>::row_type::iterator first1 = predecessorForwardTransitions.begin();
-                    typename FlexibleSparseMatrix<ValueType>::row_type::iterator last1 = predecessorForwardTransitions.end();
-                    typename FlexibleSparseMatrix<ValueType>::row_type::iterator first2 = currentStateSuccessors.begin();
-                    typename FlexibleSparseMatrix<ValueType>::row_type::iterator last2 = currentStateSuccessors.end();
-                    
-                    typename FlexibleSparseMatrix<ValueType>::row_type newSuccessors;
-                    newSuccessors.reserve((last1 - first1) + (last2 - first2));
-                    std::insert_iterator<typename FlexibleSparseMatrix<ValueType>::row_type> result(newSuccessors, newSuccessors.end());
-                    
-                    // Now we merge the two successor lists. (Code taken from std::set_union and modified to suit our needs).
-                    for (; first1 != last1; ++result) {
-                        // Skip the transitions to the state that is currently being eliminated.
-                        if (first1->getColumn() == state || (first2 != last2 && first2->getColumn() == state)) {
-                            if (first1->getColumn() == state) {
-                                ++first1;
-                            }
-                            if (first2 != last2 && first2->getColumn() == state) {
-                                ++first2;
-                            }
-                            continue;
-                        }
-                        
-                        if (first2 == last2) {
-                            std::copy_if(first1, last1, result, [&] (storm::storage::MatrixEntry<typename FlexibleSparseMatrix<ValueType>::index_type, typename FlexibleSparseMatrix<ValueType>::value_type> const& a) { return a.getColumn() != state; } );
-                            break;
-                        }
-                        if (first2->getColumn() < first1->getColumn()) {
-                            *result = simplify(*first2 * multiplyFactor);
-                            ++first2;
-                        } else if (first1->getColumn() < first2->getColumn()) {
-                            *result = *first1;
-                            ++first1;
-                        } else {
-                            *result = storm::storage::MatrixEntry<typename FlexibleSparseMatrix<ValueType>::index_type, typename FlexibleSparseMatrix<ValueType>::value_type>(first1->getColumn(), simplify(first1->getValue() + simplify(multiplyFactor * first2->getValue())));
-                            ++first1;
-                            ++first2;
-                        }
-                    }
-                    for (; first2 != last2; ++first2) {
-                        if (first2->getColumn() != state) {
-                            *result = simplify(*first2 * multiplyFactor);
-                        }
-                    }
-                    
-                    // Now move the new transitions in place.
-                    predecessorForwardTransitions = std::move(newSuccessors);
-                    
-                    // Add the probabilities to go to a target state in just one step.
-                    oneStepProbabilities[predecessor] = simplify(oneStepProbabilities[predecessor] + simplify(multiplyFactor * oneStepProbabilities[state]));
-                }
-                
-                // Finally, we need to add the predecessor to the set of predecessors of every successor.
-                for (auto const& successorEntry : currentStateSuccessors) {
-                    typename FlexibleSparseMatrix<ValueType>::row_type& successorBackwardTransitions = backwardTransitions.getRow(successorEntry.getColumn());
-                    
-                    // Delete the current state as a predecessor of the successor state.
-                    typename FlexibleSparseMatrix<ValueType>::row_type::iterator elimIt = std::find_if(successorBackwardTransitions.begin(), successorBackwardTransitions.end(), [&](storm::storage::MatrixEntry<typename FlexibleSparseMatrix<ValueType>::index_type, typename FlexibleSparseMatrix<ValueType>::value_type> const& a) { return a.getColumn() == state; });
-                    if (elimIt != successorBackwardTransitions.end()) {
-                        successorBackwardTransitions.erase(elimIt);
-                    }
-                    
-                    typename FlexibleSparseMatrix<ValueType>::row_type::iterator first1 = successorBackwardTransitions.begin();
-                    typename FlexibleSparseMatrix<ValueType>::row_type::iterator last1 = successorBackwardTransitions.end();
-                    typename FlexibleSparseMatrix<ValueType>::row_type::iterator first2 = currentStatePredecessors.begin();
-                    typename FlexibleSparseMatrix<ValueType>::row_type::iterator last2 = currentStatePredecessors.end();
-                    
-                    typename FlexibleSparseMatrix<ValueType>::row_type newPredecessors;
-                    newPredecessors.reserve((last1 - first1) + (last2 - first2));
-                    std::insert_iterator<typename FlexibleSparseMatrix<ValueType>::row_type> result(newPredecessors, newPredecessors.end());
-                    
-                    
-                    for (; first1 != last1; ++result) {
-                        if (first2 == last2) {
-                            std::copy_if(first1, last1, result, [&] (storm::storage::MatrixEntry<typename FlexibleSparseMatrix<ValueType>::index_type, typename FlexibleSparseMatrix<ValueType>::value_type> const& a) { return a.getColumn() != state; });
-                            break;
-                        }
-                        if (first2->getColumn() < first1->getColumn()) {
-                            if (first2->getColumn() != state) {
-                                *result = *first2;
-                            }
-                            ++first2;
-                        } else {
-                            if (first1->getColumn() != state) {
-                                *result = *first1;
-                            }
-                            if (first1->getColumn() == first2->getColumn()) {
-                                ++first2;
-                            }
-                            ++first1;
-                        }
-                    }
-                    std::copy_if(first2, last2, result, [&] (storm::storage::MatrixEntry<typename FlexibleSparseMatrix<ValueType>::index_type, typename FlexibleSparseMatrix<ValueType>::value_type> const& a) { return a.getColumn() != state; });
-                    
-                    // Now move the new predecessors in place.
-                    successorBackwardTransitions = std::move(newPredecessors);
-                }
-                
-                
-                // Clear the eliminated row to reduce memory consumption.
-                currentStateSuccessors.clear();
-                currentStateSuccessors.shrink_to_fit();
-            }
-            
-            template <typename ValueType>
-            bool SparseSccModelChecker<ValueType>::eliminateStateInPlace(storm::storage::SparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, storm::storage::SparseMatrix<ValueType>& backwardTransitions) {
-                typename storm::storage::SparseMatrix<ValueType>::iterator forwardElement = matrix.getRow(state).begin();
-                typename storm::storage::SparseMatrix<ValueType>::iterator backwardElement = backwardTransitions.getRow(state).begin();
-                
-                if (forwardElement->getValue() != storm::utility::constantOne<ValueType>() || backwardElement->getValue() != storm::utility::constantOne<ValueType>()) {
-                    return false;
-                }
-                
-                std::cout << "eliminating " << state << std::endl;
-                std::cout << "fwd element: " << *forwardElement << " and bwd element: " << *backwardElement << std::endl;
-                
-                // Find the element of the predecessor that moves to the state that we want to eliminate.
-                typename storm::storage::SparseMatrix<ValueType>::rows forwardRow = matrix.getRow(backwardElement->getColumn());
-                typename storm::storage::SparseMatrix<ValueType>::iterator multiplyElement = std::find_if(forwardRow.begin(), forwardRow.end(), [&](storm::storage::MatrixEntry<typename storm::storage::SparseMatrix<ValueType>::index_type, typename storm::storage::SparseMatrix<ValueType>::value_type> const& a) { return a.getColumn() == state; });
-                
-                std::cout << "before fwd: " << std::endl;
-                for (auto element : matrix.getRow(backwardElement->getColumn())) {
-                    std::cout << element << ", " << std::endl;
-                }
-                
-                // Modify the forward probability entry of the predecessor.
-                multiplyElement->setValue(multiplyElement->getValue() * forwardElement->getValue());
-                multiplyElement->setColumn(forwardElement->getColumn());
-                
-                // Modify the one-step probability for the predecessor if necessary.
-                if (oneStepProbabilities[state] != storm::utility::constantZero<ValueType>()) {
-                    oneStepProbabilities[backwardElement->getColumn()] += multiplyElement->getValue() * oneStepProbabilities[state];
-                }
-                
-                // If the forward entry is not at the right position, we need to move it there.
-                if (multiplyElement != forwardRow.begin() && multiplyElement->getColumn() < (multiplyElement - 1)->getColumn()) {
-                    while (multiplyElement != forwardRow.begin() && multiplyElement->getColumn() < (multiplyElement - 1)->getColumn()) {
-                        std::swap(*multiplyElement, *(multiplyElement - 1));
-                        --multiplyElement;
-                    }
-                } else if ((multiplyElement + 1) != forwardRow.end() && multiplyElement->getColumn() > (multiplyElement + 1)->getColumn()) {
-                    while ((multiplyElement + 1) != forwardRow.end() && multiplyElement->getColumn() > (multiplyElement + 1)->getColumn()) {
-                        std::swap(*multiplyElement, *(multiplyElement + 1));
-                        ++multiplyElement;
-                    }
-                }
-                
-                std::cout << "after fwd: " << std::endl;
-                for (auto element : matrix.getRow(backwardElement->getColumn())) {
-                    std::cout << element << ", " << std::endl;
-                }
-                
-                // Find the backward element of the successor that moves to the state that we want to eliminate.
-                typename storm::storage::SparseMatrix<ValueType>::rows backwardRow = backwardTransitions.getRow(forwardElement->getColumn());
-                typename storm::storage::SparseMatrix<ValueType>::iterator backwardEntry = std::find_if(backwardRow.begin(), backwardRow.end(), [&](storm::storage::MatrixEntry<typename storm::storage::SparseMatrix<ValueType>::index_type, typename storm::storage::SparseMatrix<ValueType>::value_type> const& a) { return a.getColumn() == state; });
-                
-                std::cout << "before bwd" << std::endl;
-                for (auto element : backwardTransitions.getRow(forwardElement->getColumn())) {
-                    std::cout << element << ", " << std::endl;
-                }
-                
-                // Modify the predecessor list of the successor and add the predecessor of the state we eliminate.
-                backwardEntry->setColumn(backwardElement->getColumn());
-                
-                // If the backward entry is not at the right position, we need to move it there.
-                if (backwardEntry != backwardRow.begin() && backwardEntry->getColumn() < (backwardEntry - 1)->getColumn()) {
-                    while (backwardEntry != backwardRow.begin() && backwardEntry->getColumn() < (backwardEntry - 1)->getColumn()) {
-                        std::swap(*backwardEntry, *(backwardEntry - 1));
-                        --backwardEntry;
-                    }
-                } else if ((backwardEntry + 1) != backwardRow.end() && backwardEntry->getColumn() > (backwardEntry + 1)->getColumn()) {
-                    while ((backwardEntry + 1) != backwardRow.end() && backwardEntry->getColumn() > (backwardEntry + 1)->getColumn()) {
-                        std::swap(*backwardEntry, *(backwardEntry + 1));
-                        ++backwardEntry;
-                    }
-                }
-                
-                std::cout << "after bwd" << std::endl;
-                for (auto element : backwardTransitions.getRow(forwardElement->getColumn())) {
-                    std::cout << element << ", " << std::endl;
-                }
-                return true;
-            }
-            
-            template<typename ValueType>
-            FlexibleSparseMatrix<ValueType>::FlexibleSparseMatrix(index_type rows) : data(rows) {
-                // Intentionally left empty.
-            }
-            
-            template<typename ValueType>
-            void FlexibleSparseMatrix<ValueType>::reserveInRow(index_type row, index_type numberOfElements) {
-                this->data[row].reserve(numberOfElements);
-            }
-            
-            template<typename ValueType>
-            typename FlexibleSparseMatrix<ValueType>::row_type& FlexibleSparseMatrix<ValueType>::getRow(index_type index) {
-                return this->data[index];
-            }
-            
-            template<typename ValueType>
-            FlexibleSparseMatrix<ValueType> SparseSccModelChecker<ValueType>::getFlexibleSparseMatrix(storm::storage::SparseMatrix<ValueType> const& matrix, bool setAllValuesToOne) {
-                FlexibleSparseMatrix<ValueType> flexibleMatrix(matrix.getRowCount());
-                
-                for (typename FlexibleSparseMatrix<ValueType>::index_type rowIndex = 0; rowIndex < matrix.getRowCount(); ++rowIndex) {
-                    typename storm::storage::SparseMatrix<ValueType>::const_rows row = matrix.getRow(rowIndex);
-                    flexibleMatrix.reserveInRow(rowIndex, row.getNumberOfEntries());
-                    
-                    for (auto const& element : row) {
-                        if (setAllValuesToOne) {
-                            flexibleMatrix.getRow(rowIndex).emplace_back(element.getColumn(), storm::utility::constantOne<ValueType>());
-                        } else {
-                            flexibleMatrix.getRow(rowIndex).emplace_back(element);
-                        }
-                    }
-                }
-                
-                return flexibleMatrix;
-            }
-            
-            template class FlexibleSparseMatrix<double>;
-            template class SparseSccModelChecker<double>;
-            
-        } // namespace reachability
-    } // namespace modelchecker
-} // namespace storm
\ No newline at end of file
diff --git a/src/modelchecker/reachability/SparseSccModelChecker.h b/src/modelchecker/reachability/SparseSccModelChecker.h
deleted file mode 100644
index 2d9a10f15..000000000
--- a/src/modelchecker/reachability/SparseSccModelChecker.h
+++ /dev/null
@@ -1,43 +0,0 @@
-#include "src/models/Dtmc.h"
-
-namespace storm {
-    namespace modelchecker {
-        namespace reachability {
-
-            template<typename ValueType>
-            class FlexibleSparseMatrix {
-            public:
-                typedef uint_fast64_t index_type;
-                typedef ValueType value_type;
-                typedef std::vector<storm::storage::MatrixEntry<index_type, value_type>> row_type;
-                typedef typename row_type::iterator iterator;
-                typedef typename row_type::const_iterator const_iterator;
-                
-                FlexibleSparseMatrix() = default;
-                FlexibleSparseMatrix(index_type rows);
-                
-                void reserveInRow(index_type row, index_type numberOfElements);
-                
-                row_type& getRow(index_type);
-                
-            private:
-                std::vector<row_type> data;
-            };
-            
-            template<typename ValueType>
-            class SparseSccModelChecker {
-            public:
-                static ValueType computeReachabilityProbability(storm::models::Dtmc<ValueType> const& dtmc, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates);
-                
-            private:
-                static void treatScc(storm::models::Dtmc<ValueType> const& dtmc, FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, storm::storage::BitVector const& entryStates, storm::storage::BitVector const& scc, storm::storage::SparseMatrix<ValueType> const& forwardTransitions, FlexibleSparseMatrix<ValueType>& backwardTransitions, bool eliminateEntryStates, uint_fast64_t level);
-                static FlexibleSparseMatrix<ValueType> getFlexibleSparseMatrix(storm::storage::SparseMatrix<ValueType> const& matrix, bool setAllValuesToOne = false);
-                static void eliminateState(FlexibleSparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, FlexibleSparseMatrix<ValueType>& backwardTransitions);
-                static bool eliminateStateInPlace(storm::storage::SparseMatrix<ValueType>& matrix, std::vector<ValueType>& oneStepProbabilities, uint_fast64_t state, storm::storage::SparseMatrix<ValueType>& backwardTransitions);
-                
-                static const uint_fast64_t maximalSccSize = 1000;
-
-            };
-        }
-    }
-}
\ No newline at end of file
diff --git a/src/parser/FormulaParser.cpp b/src/parser/FormulaParser.cpp
index 7a34ad5c6..ba214ea2a 100644
--- a/src/parser/FormulaParser.cpp
+++ b/src/parser/FormulaParser.cpp
@@ -77,12 +77,15 @@ namespace storm {
             operatorInformation = (-optimalityOperator_[qi::_a = qi::_1] >> ((relationalOperator_[qi::_b = qi::_1] > qi::double_[qi::_c = qi::_1]) | (qi::lit("=") > qi::lit("?"))))[qi::_val = phoenix::construct<std::tuple<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>>>(qi::_a, qi::_b, qi::_c)];
             operatorInformation.name("operator information");
             
-            steadyStateOperator = (qi::lit("S") > operatorInformation > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParser::createSteadyStateOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
-            steadyStateOperator.name("steady state operator");
+            steadyStateOperator = (qi::lit("LRA") > operatorInformation > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParser::createLongRunAverageOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
+            steadyStateOperator.name("long-run average operator");
             
             rewardOperator = (qi::lit("R") > operatorInformation > qi::lit("[") > rewardPathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParser::createRewardOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
             rewardOperator.name("reward operator");
             
+            expectedTimeOperator = (qi::lit("ET") > operatorInformation > qi::lit("[") > eventuallyFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParser::createExpectedTimeOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
+            expectedTimeOperator.name("expected time operator");
+            
             probabilityOperator = (qi::lit("P") > operatorInformation > qi::lit("[") > pathFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParser::createProbabilityOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
             probabilityOperator.name("probability operator");
             
@@ -224,14 +227,18 @@ namespace storm {
             return std::shared_ptr<storm::logic::Formula>(new storm::logic::ConditionalPathFormula(leftSubformula, rightSubformula));
         }
         
-        std::shared_ptr<storm::logic::Formula> FormulaParser::createSteadyStateOperatorFormula(std::tuple<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
-            return std::shared_ptr<storm::logic::Formula>(new storm::logic::SteadyStateOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula));
+        std::shared_ptr<storm::logic::Formula> FormulaParser::createLongRunAverageOperatorFormula(std::tuple<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
+            return std::shared_ptr<storm::logic::Formula>(new storm::logic::LongRunAverageOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula));
         }
         
         std::shared_ptr<storm::logic::Formula> FormulaParser::createRewardOperatorFormula(std::tuple<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
             return std::shared_ptr<storm::logic::Formula>(new storm::logic::RewardOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula));
         }
         
+        std::shared_ptr<storm::logic::Formula> FormulaParser::createExpectedTimeOperatorFormula(std::tuple<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const {
+            return std::shared_ptr<storm::logic::Formula>(new storm::logic::ExpectedTimeOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula));
+        }
+        
         std::shared_ptr<storm::logic::Formula> FormulaParser::createProbabilityOperatorFormula(std::tuple<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) {
             return std::shared_ptr<storm::logic::Formula>(new storm::logic::ProbabilityOperatorFormula(std::get<0>(operatorInformation), std::get<1>(operatorInformation), std::get<2>(operatorInformation), subformula));
         }
diff --git a/src/parser/FormulaParser.h b/src/parser/FormulaParser.h
index 2606cf821..72f1877f4 100644
--- a/src/parser/FormulaParser.h
+++ b/src/parser/FormulaParser.h
@@ -123,6 +123,7 @@ namespace storm {
             qi::rule<Iterator, std::tuple<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>>(), qi::locals<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>>, Skipper> operatorInformation;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> probabilityOperator;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> rewardOperator;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> expectedTimeOperator;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> steadyStateOperator;
             
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula>(), Skipper> formula;
@@ -165,8 +166,9 @@ namespace storm {
             std::shared_ptr<storm::logic::Formula> createUntilFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula);
             std::shared_ptr<storm::logic::Formula> createBoundedUntilFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, unsigned stepBound, std::shared_ptr<storm::logic::Formula> const& rightSubformula) const;
             std::shared_ptr<storm::logic::Formula> createConditionalFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula) const;
-            std::shared_ptr<storm::logic::Formula> createSteadyStateOperatorFormula(std::tuple<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
+            std::shared_ptr<storm::logic::Formula> createLongRunAverageOperatorFormula(std::tuple<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
             std::shared_ptr<storm::logic::Formula> createRewardOperatorFormula(std::tuple<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
+            std::shared_ptr<storm::logic::Formula> createExpectedTimeOperatorFormula(std::tuple<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula) const;
             std::shared_ptr<storm::logic::Formula> createProbabilityOperatorFormula(std::tuple<boost::optional<storm::logic::OptimalityType>, boost::optional<storm::logic::ComparisonType>, boost::optional<double>> const& operatorInformation, std::shared_ptr<storm::logic::Formula> const& subformula);
             std::shared_ptr<storm::logic::Formula> createBinaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula> const& leftSubformula, std::shared_ptr<storm::logic::Formula> const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType);
             std::shared_ptr<storm::logic::Formula> createUnaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula> const& subformula, boost::optional<storm::logic::UnaryBooleanStateFormula::OperatorType> const& operatorType);
diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp
index 4c841acaa..9f5f02d42 100644
--- a/src/settings/SettingsManager.cpp
+++ b/src/settings/SettingsManager.cpp
@@ -27,6 +27,7 @@ namespace storm {
             this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::BisimulationSettings(*this)));
             this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::GlpkSettings(*this)));
             this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::GurobiSettings(*this)));
+            this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::SparseDtmcEliminationModelCheckerSettings(*this)));
         }
         
         SettingsManager::~SettingsManager() {
@@ -507,5 +508,9 @@ namespace storm {
         storm::settings::modules::GurobiSettings const& gurobiSettings() {
             return dynamic_cast<storm::settings::modules::GurobiSettings const&>(manager().getModule(storm::settings::modules::GurobiSettings::moduleName));
         }
+        
+        storm::settings::modules::SparseDtmcEliminationModelCheckerSettings const& sparseDtmcEliminationModelCheckerSettings() {
+            return dynamic_cast<storm::settings::modules::SparseDtmcEliminationModelCheckerSettings const&>(manager().getModule(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::moduleName));
+        }
     }
 }
\ No newline at end of file
diff --git a/src/settings/SettingsManager.h b/src/settings/SettingsManager.h
index 9d597ca2e..57fdc44b0 100644
--- a/src/settings/SettingsManager.h
+++ b/src/settings/SettingsManager.h
@@ -28,6 +28,7 @@
 #include "src/settings/modules/BisimulationSettings.h"
 #include "src/settings/modules/GlpkSettings.h"
 #include "src/settings/modules/GurobiSettings.h"
+#include "src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h"
 
 #include "src/utility/macros.h"
 #include "src/exceptions/OptionParserException.h"
@@ -309,6 +310,13 @@ namespace storm {
          */
         storm::settings::modules::GurobiSettings const& gurobiSettings();
         
+        /*!
+         * Retrieves the settings of the elimination-based DTMC model checker.
+         *
+         * @return An object that allows accessing the settings of the elimination-based DTMC model checker.
+         */
+        storm::settings::modules::SparseDtmcEliminationModelCheckerSettings const& sparseDtmcEliminationModelCheckerSettings();
+        
     } // namespace settings
 } // namespace storm
 
diff --git a/src/settings/modules/SparseDtmcEliminationModelCheckerSettings.cpp b/src/settings/modules/SparseDtmcEliminationModelCheckerSettings.cpp
new file mode 100644
index 000000000..fe4b63068
--- /dev/null
+++ b/src/settings/modules/SparseDtmcEliminationModelCheckerSettings.cpp
@@ -0,0 +1,64 @@
+#include "src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h"
+
+#include "src/settings/SettingsManager.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            
+            const std::string SparseDtmcEliminationModelCheckerSettings::moduleName = "sparseelim";
+            const std::string SparseDtmcEliminationModelCheckerSettings::eliminationMethodOptionName = "method";
+            const std::string SparseDtmcEliminationModelCheckerSettings::eliminationOrderOptionName = "order";
+            const std::string SparseDtmcEliminationModelCheckerSettings::entryStatesLastOptionName = "entrylast";
+            const std::string SparseDtmcEliminationModelCheckerSettings::maximalSccSizeOptionName = "sccsize";
+            
+            SparseDtmcEliminationModelCheckerSettings::SparseDtmcEliminationModelCheckerSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
+                std::vector<std::string> orders = {"fw", "fwrev", "bw", "bwrev", "rand"};
+                this->addOption(storm::settings::OptionBuilder(moduleName, eliminationOrderOptionName, true, "The order that is to be used for the elimination techniques. Available are {fw, fwrev, bw, bwrev, rand}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the order in which states are chosen for elimination.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(orders)).setDefaultValueString("bw").build()).build());
+                
+                std::vector<std::string> methods = {"state", "hybrid"};
+                this->addOption(storm::settings::OptionBuilder(moduleName, eliminationMethodOptionName, true, "The elimination technique to use. Available are {state, hybrid}.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the elimination technique to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(methods)).setDefaultValueString("hybrid").build()).build());
+                
+                this->addOption(storm::settings::OptionBuilder(moduleName, entryStatesLastOptionName, true, "Sets whether the entry states are eliminated last.").build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, maximalSccSizeOptionName, true, "Sets the maximal size of the SCCs for which state elimination is applied.")
+                                .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("maxsize", "The maximal size of an SCC on which state elimination is applied.").setDefaultValueUnsignedInteger(20).setIsOptional(true).build()).build());
+            }
+            
+            SparseDtmcEliminationModelCheckerSettings::EliminationMethod SparseDtmcEliminationModelCheckerSettings::getEliminationMethod() const {
+                std::string eliminationMethodAsString = this->getOption(eliminationMethodOptionName).getArgumentByName("name").getValueAsString();
+                if (eliminationMethodAsString == "state") {
+                    return EliminationMethod::State;
+                } else if (eliminationMethodAsString == "hybrid") {
+                    return EliminationMethod::Hybrid;
+                } else {
+                    STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal elimination method selected.");
+                }
+            }
+            
+            SparseDtmcEliminationModelCheckerSettings::EliminationOrder SparseDtmcEliminationModelCheckerSettings::getEliminationOrder() const {
+                std::string eliminationOrderAsString = this->getOption(eliminationOrderOptionName).getArgumentByName("name").getValueAsString();
+                if (eliminationOrderAsString == "fw") {
+                    return EliminationOrder::Forward;
+                } else if (eliminationOrderAsString == "fwrev") {
+                    return EliminationOrder::ForwardReversed;
+                } else if (eliminationOrderAsString == "bw") {
+                    return EliminationOrder::Backward;
+                } else if (eliminationOrderAsString == "bwrev") {
+                    return EliminationOrder::BackwardReversed;
+                } else if (eliminationOrderAsString == "rand") {
+                    return EliminationOrder::Random;
+                } else {
+                    STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Illegal elimination order selected.");
+                }
+            }
+            
+            bool SparseDtmcEliminationModelCheckerSettings::isEliminateEntryStatesLastSet() const {
+                return this->getOption(entryStatesLastOptionName).getHasOptionBeenSet();
+            }
+            
+            uint_fast64_t SparseDtmcEliminationModelCheckerSettings::getMaximalSccSize() const {
+                return this->getOption(maximalSccSizeOptionName).getArgumentByName("maxsize").getValueAsUnsignedInteger();
+            }
+        } // namespace modules
+    } // namespace settings
+} // namespace storm
\ No newline at end of file
diff --git a/src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h b/src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h
new file mode 100644
index 000000000..55a9b14b4
--- /dev/null
+++ b/src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h
@@ -0,0 +1,73 @@
+#ifndef STORM_SETTINGS_MODULES_SPARSEDTMCELIMINATIONMODELCHECKERSETTINGS_H_
+#define STORM_SETTINGS_MODULES_SPARSEDTMCELIMINATIONMODELCHECKERSETTINGS_H_
+
+#include "src/settings/modules/ModuleSettings.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            
+            /*!
+             * This class represents the settings for the elimination-based DTMC model checker.
+             */
+            class SparseDtmcEliminationModelCheckerSettings : public ModuleSettings {
+            public:
+                /*!
+                 * An enum that contains all available state elimination orders.
+                 */
+                enum class EliminationOrder { Forward, ForwardReversed, Backward, BackwardReversed, Random };
+				
+                /*!
+                 * An enum that contains all available techniques to solve parametric systems.
+                 */
+                enum class EliminationMethod { State, Scc, Hybrid};
+                
+                /*!
+                 * Creates a new set of parametric model checking settings that is managed by the given manager.
+                 *
+                 * @param settingsManager The responsible manager.
+                 */
+                SparseDtmcEliminationModelCheckerSettings(storm::settings::SettingsManager& settingsManager);
+                
+                /*!
+                 * Retrieves the selected elimination method.
+                 *
+                 * @return The selected elimination method.
+                 */
+                EliminationMethod getEliminationMethod() const;
+                
+                /*!
+                 * Retrieves the selected elimination order.
+                 *
+                 * @return The selected elimination order.
+                 */
+                EliminationOrder getEliminationOrder() const;
+                
+                /*!
+                 * Retrieves whether the option to eliminate entry states in the very end is set.
+                 *
+                 * @return True iff the option is set.
+                 */
+                bool isEliminateEntryStatesLastSet() const;
+                
+                /*!
+                 * Retrieves the maximal size of an SCC on which state elimination is to be directly applied.
+                 *
+                 * @return The maximal size of an SCC on which state elimination is to be directly applied.
+                 */
+                uint_fast64_t getMaximalSccSize() const;
+				
+                const static std::string moduleName;
+                
+            private:
+                const static std::string eliminationMethodOptionName;
+                const static std::string eliminationOrderOptionName;
+                const static std::string entryStatesLastOptionName;
+                const static std::string maximalSccSizeOptionName;
+            };
+            
+        } // namespace modules
+    } // namespace settings
+} // namespace storm
+
+#endif /* STORM_SETTINGS_MODULES_SPARSEDTMCELIMINATIONMODELCHECKERSETTINGS_H_ */
\ No newline at end of file
diff --git a/src/utility/ConstantsComparator.cpp b/src/utility/ConstantsComparator.cpp
index 77d76ab22..26e1d4255 100644
--- a/src/utility/ConstantsComparator.cpp
+++ b/src/utility/ConstantsComparator.cpp
@@ -1,5 +1,6 @@
 #include "src/utility/ConstantsComparator.h"
 
+#include "src/storage/SparseMatrix.h"
 #include "src/storage/sparse/StateType.h"
 
 namespace storm {
@@ -20,6 +21,11 @@ namespace storm {
             return std::numeric_limits<ValueType>::infinity();
         }
         
+        template<typename ValueType>
+        ValueType pow(ValueType const& value, uint_fast64_t exponent) {
+            return std::pow(value, exponent);
+        }
+        
         template<>
         double simplify(double value) {
             // In the general case, we don't to anything here, but merely return the value. If something else is
@@ -27,6 +33,13 @@ namespace storm {
             return value;
         }
         
+        template<>
+        int simplify(int value) {
+            // In the general case, we don't to anything here, but merely return the value. If something else is
+            // supposed to happen here, the templated function can be specialized for this particular type.
+            return value;
+        }
+        
         template<typename ValueType>
         bool ConstantsComparator<ValueType>::isOne(ValueType const& value) const {
             return value == one<ValueType>();
@@ -66,20 +79,128 @@ namespace storm {
             return true;
         }
         
+#ifdef PARAMETRIC_SYSTEMS
+        template<>
+        RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent) {
+            return carl::pow(value, exponent);
+        }
+        
+        template<>
+        RationalFunction simplify(RationalFunction value) {
+            value.simplify();
+            return value;
+        }
+        
+        template<>
+        RationalFunction& simplify(RationalFunction& value) {
+            value.simplify();
+            return value;
+        }
+        
+        template<>
+        RationalFunction&& simplify(RationalFunction&& value) {
+            value.simplify();
+            return std::move(value);
+        }
+        
+        bool ConstantsComparator<storm::RationalFunction>::isOne(storm::RationalFunction const& value) const {
+            return value.isOne();
+        }
+        
+        bool ConstantsComparator<storm::RationalFunction>::isZero(storm::RationalFunction const& value) const {
+            return value.isZero();
+        }
+        
+        bool ConstantsComparator<storm::RationalFunction>::isEqual(storm::RationalFunction const& value1, storm::RationalFunction const& value2) const {
+            return value1 == value2;
+        }
+        
+        bool ConstantsComparator<storm::RationalFunction>::isConstant(storm::RationalFunction const& value) const {
+            return value.isConstant();
+        }
+        
+        bool ConstantsComparator<storm::Polynomial>::isOne(storm::Polynomial const& value) const {
+            return value.isOne();
+        }
+        
+        bool ConstantsComparator<storm::Polynomial>::isZero(storm::Polynomial const& value) const {
+            return value.isZero();
+        }
+        
+        bool ConstantsComparator<storm::Polynomial>::isEqual(storm::Polynomial const& value1, storm::Polynomial const& value2) const {
+            return value1 == value2;
+        }
+        
+        bool ConstantsComparator<storm::Polynomial>::isConstant(storm::Polynomial const& value) const {
+            return value.isConstant();
+        }
+#endif
+        
+        template<typename IndexType, typename ValueType>
+        storm::storage::MatrixEntry<IndexType, ValueType> simplify(storm::storage::MatrixEntry<IndexType, ValueType> matrixEntry) {
+            simplify(matrixEntry.getValue());
+            return matrixEntry;
+        }
+        
         template<typename IndexType, typename ValueType>
         storm::storage::MatrixEntry<IndexType, ValueType>& simplify(storm::storage::MatrixEntry<IndexType, ValueType>& matrixEntry) {
             simplify(matrixEntry.getValue());
             return matrixEntry;
         }
         
+        template<typename IndexType, typename ValueType>
+        storm::storage::MatrixEntry<IndexType, ValueType>&& simplify(storm::storage::MatrixEntry<IndexType, ValueType>&& matrixEntry) {
+            simplify(matrixEntry.getValue());
+            return std::move(matrixEntry);
+        }
+        
         template class ConstantsComparator<double>;
         
         template double one();
         template double zero();
         template double infinity();
-
+        
+        template double pow(double const& value, uint_fast64_t exponent);
+        
         template double simplify(double value);
         
+        template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double> matrixEntry);
         template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>& matrixEntry);
+        template storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, double>&& matrixEntry);
+        
+        template class ConstantsComparator<int>;
+        
+        template int one();
+        template int zero();
+        template int infinity();
+        
+        template int pow(int const& value, uint_fast64_t exponent);
+        
+        template int simplify(int value);
+        
+        template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int> matrixEntry);
+        template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>& matrixEntry);
+        template storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, int>&& matrixEntry);
+        
+#ifdef PARAMETRIC_SYSTEMS
+        template class ConstantsComparator<RationalFunction>;
+        template class ConstantsComparator<Polynomial>;
+        
+        template RationalFunction one();
+        template RationalFunction zero();
+        
+        template RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent);
+        
+        template Polynomial one();
+        template Polynomial zero();
+        template RationalFunction simplify(RationalFunction value);
+        template RationalFunction& simplify(RationalFunction& value);
+        template RationalFunction&& simplify(RationalFunction&& value);
+        
+        template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction> simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction> matrixEntry);
+        template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>& matrixEntry);
+        template storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>&& simplify(storm::storage::MatrixEntry<storm::storage::sparse::state_type, RationalFunction>&& matrixEntry);
+#endif
+        
     }
 }
\ No newline at end of file
diff --git a/src/utility/ConstantsComparator.h b/src/utility/ConstantsComparator.h
index a25e0ac91..cfde179c8 100644
--- a/src/utility/ConstantsComparator.h
+++ b/src/utility/ConstantsComparator.h
@@ -13,9 +13,18 @@
 #include <cstdint>
 
 #include "src/settings/SettingsManager.h"
-#include "src/storage/SparseMatrix.h"
+
+#ifdef PARAMETRIC_SYSTEMS
+#include "src/storage/parameters.h"
+#endif
 
 namespace storm {
+    
+    // Forward-declare MatrixEntry class.
+    namespace storage {
+        template<typename IndexType, typename ValueType> class MatrixEntry;
+    }
+    
     namespace utility {
         
         template<typename ValueType>
@@ -27,9 +36,17 @@ namespace storm {
         template<typename ValueType>
         ValueType infinity();
         
+        template<typename ValueType>
+        ValueType pow(ValueType const& value, uint_fast64_t exponent);
+        
+#ifdef PARAMETRIC_SYSTEMS
+        template<>
+        RationalFunction pow(RationalFunction const& value, uint_fast64_t exponent);
+#endif
+        
         template<typename ValueType>
         ValueType simplify(ValueType value);
-
+        
         // A class that can be used for comparing constants.
         template<typename ValueType>
         class ConstantsComparator {
@@ -46,7 +63,7 @@ namespace storm {
         class ConstantsComparator<double> {
         public:
             ConstantsComparator();
-
+            
             ConstantsComparator(double precision);
             
             bool isOne(double const& value) const;
@@ -62,8 +79,43 @@ namespace storm {
             double precision;
         };
         
+#ifdef PARAMETRIC_SYSTEMS
+        template<>
+        RationalFunction& simplify(RationalFunction& value);
+        
+        template<>
+        RationalFunction&& simplify(RationalFunction&& value);
+        
+        template<>
+        class ConstantsComparator<storm::RationalFunction> {
+        public:
+            bool isOne(storm::RationalFunction const& value) const;
+            
+            bool isZero(storm::RationalFunction const& value) const;
+            
+            bool isEqual(storm::RationalFunction const& value1, storm::RationalFunction const& value2) const;
+            
+            bool isConstant(storm::RationalFunction const& value) const;
+        };
+        
+        template<>
+        class ConstantsComparator<storm::Polynomial> {
+        public:
+            bool isOne(storm::Polynomial const& value) const;
+            
+            bool isZero(storm::Polynomial const& value) const;
+            
+            bool isEqual(storm::Polynomial const& value1, storm::Polynomial const& value2) const;
+            
+            bool isConstant(storm::Polynomial const& value) const;
+        };
+#endif
+        
         template<typename IndexType, typename ValueType>
         storm::storage::MatrixEntry<IndexType, ValueType>& simplify(storm::storage::MatrixEntry<IndexType, ValueType>& matrixEntry);
+        
+        template<typename IndexType, typename ValueType>
+        storm::storage::MatrixEntry<IndexType, ValueType>&& simplify(storm::storage::MatrixEntry<IndexType, ValueType>&& matrixEntry);
     }
 }