diff --git a/resources/3rdparty/CMakeLists.txt b/resources/3rdparty/CMakeLists.txt
index 3cfefe1cc..979c5cbe8 100644
--- a/resources/3rdparty/CMakeLists.txt
+++ b/resources/3rdparty/CMakeLists.txt
@@ -208,7 +208,7 @@ include(${STORM_3RDPARTY_SOURCE_DIR}/include_cudd.cmake)
 #############################################################
 
 set(STORM_HAVE_CARL OFF)
-set(CARL_MINVERSION "17.10")
+set(CARL_MINVERSION "17.12")
 if (NOT STORM_FORCE_SHIPPED_CARL)
     if (NOT "${STORM_CARL_DIR_HINT}" STREQUAL "")
 		find_package(carl QUIET PATHS ${STORM_CARL_DIR_HINT} NO_DEFAULT_PATH)
@@ -226,7 +226,7 @@ if(carl_FOUND AND NOT STORM_FORCE_SHIPPED_CARL)
     else()
         message(SEND_ERROR "File ${carlLOCATION} does not exist, did you build carl?")
     endif()
-    if("${carl_VERSION}" VERSION_LESS "${CARL_MINVERSION}")
+    if("${carl_VERSION_MAJOR}.${carl_VERSION_MINOR}" VERSION_LESS "${CARL_MINVERSION}")
     	message(SEND_ERROR "Carl outdated, require ${CARL_MINVERSION}, have ${carl_VERSION}")
     endif()
 
diff --git a/src/storm-pars/modelchecker/region/RegionModelChecker.cpp b/src/storm-pars/modelchecker/region/RegionModelChecker.cpp
index b3669e9b8..2b2e8a350 100644
--- a/src/storm-pars/modelchecker/region/RegionModelChecker.cpp
+++ b/src/storm-pars/modelchecker/region/RegionModelChecker.cpp
@@ -11,13 +11,12 @@
 #include "storm/models/sparse/Dtmc.h"
 #include "storm/models/sparse/Mdp.h"
 
-#include "storm/exceptions/NotSupportedException.h"
-#include "storm/exceptions/InvalidStateException.h"
-#include "storm/exceptions/InvalidArgumentException.h"
-
 #include "storm/settings/SettingsManager.h"
 #include "storm/settings/modules/CoreSettings.h"
 #include "storm/exceptions/NotImplementedException.h"
+#include "storm/exceptions/NotSupportedException.h"
+#include "storm/exceptions/InvalidStateException.h"
+#include "storm/exceptions/InvalidArgumentException.h"
 
 
 namespace storm {
@@ -152,6 +151,18 @@ namespace storm {
                 auto regionCopyForResult = region;
                 return std::make_unique<storm::modelchecker::RegionRefinementCheckResult<ParametricType>>(std::move(result), std::move(regionCopyForResult));
             }
+
+        template <typename ParametricType>
+        bool RegionModelChecker<ParametricType>::isRegionSplitEstimateSupported() const {
+            return false;
+        }
+        
+        template <typename ParametricType>
+        std::map<typename RegionModelChecker<ParametricType>::VariableType, double> RegionModelChecker<ParametricType>::getRegionSplitEstimate() const {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Region split estimation is not supported by this region model checker.");
+            return std::map<typename RegionModelChecker<ParametricType>::VariableType, double>();
+        }
+
     
 #ifdef STORM_HAVE_CARL
             template class RegionModelChecker<storm::RationalFunction>;
diff --git a/src/storm-pars/modelchecker/region/RegionModelChecker.h b/src/storm-pars/modelchecker/region/RegionModelChecker.h
index fc9997c3c..72f56bf73 100644
--- a/src/storm-pars/modelchecker/region/RegionModelChecker.h
+++ b/src/storm-pars/modelchecker/region/RegionModelChecker.h
@@ -22,12 +22,13 @@ namespace storm {
         public:
             
             typedef typename storm::storage::ParameterRegion<ParametricType>::CoefficientType CoefficientType;
+            typedef typename storm::storage::ParameterRegion<ParametricType>::VariableType VariableType;
 
             RegionModelChecker();
             virtual ~RegionModelChecker() = default;
             
             virtual bool canHandle(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, ParametricType> const& checkTask) const = 0;
-            virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, ParametricType> const& checkTask) = 0;
+            virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, ParametricType> const& checkTask, bool generateRegionSplitEstimates = false) = 0;
             
             /*!
              * Analyzes the given region.
@@ -57,6 +58,17 @@ namespace storm {
              */
             std::unique_ptr<storm::modelchecker::RegionRefinementCheckResult<ParametricType>> performRegionRefinement(Environment const& env, storm::storage::ParameterRegion<ParametricType> const& region, boost::optional<ParametricType> const& coverageThreshold, boost::optional<uint64_t> depthThreshold = boost::none, RegionResultHypothesis const& hypothesis = RegionResultHypothesis::Unknown);
             
+            /*!
+             * Returns true if region split estimation (a) was enabled when model and check task have been specified and (b) is supported by this region model checker.
+             */
+            virtual bool isRegionSplitEstimateSupported() const;
+            
+            /*!
+             * Returns an estimate of the benefit of splitting the last checked region with respect to each parameter. This method should only be called if region split estimation is supported and enabled.
+             * If a parameter is assigned a high value, we should prefer splitting with respect to this parameter.
+             */
+            virtual std::map<VariableType, double> getRegionSplitEstimate() const;
+            
         };
 
     } //namespace modelchecker
diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
index 7bce00c6a..9c009ccee 100644
--- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
+++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
@@ -19,6 +19,7 @@
 #include "storm/exceptions/InvalidPropertyException.h"
 #include "storm/exceptions/NotSupportedException.h"
 #include "storm/exceptions/UnexpectedException.h"
+#include "storm/exceptions/InvalidOperationException.h"
 #include "storm/exceptions/UncheckedRequirementException.h"
 
 
@@ -31,7 +32,7 @@ namespace storm {
         }
         
         template <typename SparseModelType, typename ConstantType>
-        SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseDtmcParameterLiftingModelChecker(std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>>&& solverFactory) : solverFactory(std::move(solverFactory)), solvingRequiresUpperRewardBounds(false) {
+        SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseDtmcParameterLiftingModelChecker(std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>>&& solverFactory) : solverFactory(std::move(solverFactory)), solvingRequiresUpperRewardBounds(false), regionSplitEstimationsEnabled(false) {
             // Intentionally left empty
         }
         
@@ -47,18 +48,20 @@ namespace storm {
         }
         
         template <typename SparseModelType, typename ConstantType>
-        void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
+        void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates) {
             auto dtmc = parametricModel->template as<SparseModelType>();
-            specify(env, dtmc, checkTask, false);
+            specify(env, dtmc, checkTask, generateRegionSplitEstimates, false);
         }
         
         template <typename SparseModelType, typename ConstantType>
-        void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(Environment const& env, std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool skipModelSimplification) {
-
+        void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(Environment const& env, std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates, bool skipModelSimplification) {
+            
             STORM_LOG_ASSERT(this->canHandle(parametricModel, checkTask), "specified model and formula can not be handled by this.");
-         
+            
             reset();
             
+            regionSplitEstimationsEnabled = generateRegionSplitEstimates;
+            
             if (skipModelSimplification) {
                 this->parametricModel = parametricModel;
                 this->specifyFormula(env, checkTask);
@@ -139,7 +142,7 @@ namespace storm {
                 // Create the vector of one-step probabilities to go to target states.
                 std::vector<typename SparseModelType::ValueType> b = this->parametricModel->getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel->getTransitionMatrix().getRowCount(), true), psiStates);
                 
-                parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel->getTransitionMatrix(), b, maybeStates, maybeStates);
+                parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel->getTransitionMatrix(), b, maybeStates, maybeStates, regionSplitEstimationsEnabled);
             }
             
             // We know some bounds for the results so set them
@@ -179,7 +182,7 @@ namespace storm {
 
                 std::vector<typename SparseModelType::ValueType> b = rewardModel.getTotalRewardVector(this->parametricModel->getTransitionMatrix());
                 
-                parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel->getTransitionMatrix(), b, maybeStates, maybeStates);
+                parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel->getTransitionMatrix(), b, maybeStates, maybeStates, regionSplitEstimationsEnabled);
             }
             
             // We only know a lower bound for the result
@@ -297,6 +300,9 @@ namespace storm {
                 } else {
                     maxSchedChoices = solver->getSchedulerChoices();
                 }
+                if (isRegionSplitEstimateSupported()) {
+                    computeRegionSplitEstimates(x, solver->getSchedulerChoices(), region, dirForParameters);
+                }
             }
             
             // Get the result for the complete model (including maybestates)
@@ -309,6 +315,68 @@ namespace storm {
             return std::make_unique<storm::modelchecker::ExplicitQuantitativeCheckResult<ConstantType>>(std::move(result));
         }
         
+        template <typename SparseModelType, typename ConstantType>
+        void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::computeRegionSplitEstimates(std::vector<ConstantType> const& quantitativeResult, std::vector<uint_fast64_t> const& schedulerChoices, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
+            std::map<typename RegionModelChecker<typename SparseModelType::ValueType>::VariableType, double> deltaLower, deltaUpper;
+            for (auto const& p : region.getVariables()) {
+                deltaLower.insert(std::make_pair(p, 0.0));
+                deltaUpper.insert(std::make_pair(p, 0.0));
+            }
+            auto const& choiceValuations = parameterLifter->getRowLabels();
+            auto const& matrix = parameterLifter->getMatrix();
+            auto const& vector = parameterLifter->getVector();
+            
+            std::vector<ConstantType> stateResults;
+            for (uint64_t state = 0; state < schedulerChoices.size(); ++state) {
+                uint64_t rowOffset = matrix.getRowGroupIndices()[state];
+                uint64_t optimalChoice = schedulerChoices[state];
+                auto const& optimalChoiceVal = choiceValuations[rowOffset + optimalChoice];
+                assert(optimalChoiceVal.getUnspecifiedParameters().empty());
+                stateResults.clear();
+                for (uint64_t row = rowOffset; row < matrix.getRowGroupIndices()[state + 1]; ++row) {
+                    stateResults.push_back(matrix.multiplyRowWithVector(row, quantitativeResult) + vector[row]);
+                }
+                bool checkUpperParameters = false;
+                do {
+                    auto const& consideredParameters = checkUpperParameters ? optimalChoiceVal.getUpperParameters() : optimalChoiceVal.getLowerParameters();
+                    for (auto const& p : consideredParameters) {
+                        // Find the 'best' choice that assigns the parameter to the other bound
+                        ConstantType bestValue;
+                        bool foundBestValue = false;
+                        for (uint64_t choice = 0; choice < stateResults.size(); ++choice) {
+                            if (choice != optimalChoice) {
+                                auto const& otherBoundParsOfChoice = checkUpperParameters ? choiceValuations[rowOffset + choice].getLowerParameters() : choiceValuations[rowOffset + choice].getUpperParameters();
+                                if (otherBoundParsOfChoice.find(p) != otherBoundParsOfChoice.end()) {
+                                    ConstantType const& choiceValue = stateResults[choice];
+                                    if (!foundBestValue || (storm::solver::minimize(dirForParameters) ? choiceValue < bestValue : choiceValue > bestValue)) {
+                                        foundBestValue = true;
+                                        bestValue = choiceValue;
+                                    }
+                                }
+                            }
+                        }
+                        if (checkUpperParameters) {
+                            deltaLower[p] += storm::utility::convertNumber<double>(bestValue);
+                        } else {
+                            deltaUpper[p] += storm::utility::convertNumber<double>(bestValue);
+                        }
+
+                    }
+                    checkUpperParameters = !checkUpperParameters;
+                } while (checkUpperParameters);
+            }
+            
+            regionSplitEstimates.clear();
+            for (auto const& p : region.getVariables()) {
+                if (deltaLower[p] > deltaUpper[p]) {
+                    regionSplitEstimates.insert(std::make_pair(p, deltaUpper[p]));
+                } else {
+                    regionSplitEstimates.insert(std::make_pair(p, deltaLower[p]));
+                }
+            }
+            
+        }
+        
         template <typename SparseModelType, typename ConstantType>
         void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::reset() {
             maybeStates.resize(0);
@@ -321,6 +389,7 @@ namespace storm {
             x.clear();
             lowerResultBound = boost::none;
             upperResultBound = boost::none;
+            regionSplitEstimationsEnabled = false;
         }
         
         template <typename SparseModelType, typename ConstantType>
@@ -355,6 +424,18 @@ namespace storm {
             return result;
         }
         
+        template <typename SparseModelType, typename ConstantType>
+        bool SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::isRegionSplitEstimateSupported() const {
+            return regionSplitEstimationsEnabled && !stepBound;
+        }
+        
+        template <typename SparseModelType, typename ConstantType>
+        std::map<typename RegionModelChecker<typename SparseModelType::ValueType>::VariableType, double> SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::getRegionSplitEstimate() const {
+            STORM_LOG_THROW(isRegionSplitEstimateSupported(), storm::exceptions::InvalidOperationException, "Region split estimation requested but are not enabled (or supported).");
+            return regionSplitEstimates;
+        }
+
+        
         template class SparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, double>;
         template class SparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>, storm::RationalNumber>;
 
diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h
index 18bb302b9..88231e76c 100644
--- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h
+++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h
@@ -23,12 +23,15 @@ namespace storm {
             virtual ~SparseDtmcParameterLiftingModelChecker() = default;
             
             virtual bool canHandle(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const override;
-            virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) override;
-            void specify(Environment const& env, std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool skipModelSimplification);
+            virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates = false) override;
+            void specify(Environment const& env, std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates, bool skipModelSimplification);
             
             boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMinScheduler();
             boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMaxScheduler();
 
+            virtual bool isRegionSplitEstimateSupported() const override;
+            virtual std::map<typename RegionModelChecker<typename SparseModelType::ValueType>::VariableType, double> getRegionSplitEstimate() const override;
+            
         protected:
                 
             virtual void specifyBoundedUntilFormula(Environment const& env, CheckTask<storm::logic::BoundedUntilFormula, ConstantType> const& checkTask) override;
@@ -39,7 +42,9 @@ namespace storm {
             virtual storm::modelchecker::SparseInstantiationModelChecker<SparseModelType, ConstantType>& getInstantiationChecker() override;
                 
             virtual std::unique_ptr<CheckResult> computeQuantitativeValues(Environment const& env, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) override;
-                
+            
+            void computeRegionSplitEstimates(std::vector<ConstantType> const& quantitativeResult, std::vector<uint_fast64_t> const& schedulerChoices, storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters);
+            
             virtual void reset() override;
                 
         private:
@@ -59,6 +64,9 @@ namespace storm {
             boost::optional<std::vector<uint_fast64_t>> minSchedChoices, maxSchedChoices;
             std::vector<ConstantType> x;
             boost::optional<ConstantType> lowerResultBound, upperResultBound;
+            
+            bool regionSplitEstimationsEnabled;
+            std::map<typename RegionModelChecker<typename SparseModelType::ValueType>::VariableType, double> regionSplitEstimates;
         };
     }
 }
diff --git a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp
index 04a5c41e1..55a1b65a7 100644
--- a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp
+++ b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp
@@ -45,13 +45,13 @@ namespace storm {
         }
         
         template <typename SparseModelType, typename ConstantType>
-        void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
+        void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates) {
             auto mdp = parametricModel->template as<SparseModelType>();
-            specify(env, mdp, checkTask, false);
+            specify(env, mdp, checkTask, generateRegionSplitEstimates, false);
         }
         
         template <typename SparseModelType, typename ConstantType>
-        void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(Environment const& env, std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool skipModelSimplification) {
+        void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(Environment const& env, std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates, bool skipModelSimplification) {
 
             STORM_LOG_ASSERT(this->canHandle(parametricModel, checkTask), "specified model and formula can not be handled by this.");
          
diff --git a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h
index 09a3e44cb..cffab74ed 100644
--- a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h
+++ b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h
@@ -25,8 +25,8 @@ namespace storm {
             virtual ~SparseMdpParameterLiftingModelChecker() = default;
             
             virtual bool canHandle(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const override;
-            virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) override;
-            void specify(Environment const& env, std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool skipModelSimplification);
+            virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates = false) override;
+            void specify(Environment const& env, std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates, bool skipModelSimplification);
 
             boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMinScheduler();
             boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMaxScheduler();
diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.cpp
index e95cf2d61..e84f6c9d0 100644
--- a/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.cpp
+++ b/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.cpp
@@ -15,7 +15,7 @@ namespace storm {
         }
         
         template <typename SparseModelType, typename ImpreciseType, typename PreciseType>
-        void ValidatingSparseDtmcParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
+        void ValidatingSparseDtmcParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates) {
             STORM_LOG_ASSERT(this->canHandle(parametricModel, checkTask), "specified model and formula can not be handled by this.");
         
             auto dtmc = parametricModel->template as<SparseModelType>();
@@ -27,8 +27,8 @@ namespace storm {
             
             auto simplifiedTask = checkTask.substituteFormula(*simplifier.getSimplifiedFormula());
             
-            impreciseChecker.specify(env, simplifier.getSimplifiedModel(), simplifiedTask, true);
-            preciseChecker.specify(env, simplifier.getSimplifiedModel(), simplifiedTask, true);
+            impreciseChecker.specify(env, simplifier.getSimplifiedModel(), simplifiedTask, false, true);
+            preciseChecker.specify(env, simplifier.getSimplifiedModel(), simplifiedTask, false, true);
         }
         
         template <typename SparseModelType, typename ImpreciseType, typename PreciseType>
diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.h
index f441353fb..5aed6b5d3 100644
--- a/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.h
+++ b/src/storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.h
@@ -12,7 +12,7 @@ namespace storm {
             ValidatingSparseDtmcParameterLiftingModelChecker();
             virtual ~ValidatingSparseDtmcParameterLiftingModelChecker() = default;
             
-            virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) override;
+            virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates = false) override;
 
         protected:
             virtual SparseParameterLiftingModelChecker<SparseModelType, ImpreciseType>& getImpreciseChecker() override;
diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.cpp
index 7cdb1c7b0..a3c01b4bd 100644
--- a/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.cpp
+++ b/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.cpp
@@ -16,7 +16,7 @@ namespace storm {
         
         
         template <typename SparseModelType, typename ImpreciseType, typename PreciseType>
-        void ValidatingSparseMdpParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
+        void ValidatingSparseMdpParameterLiftingModelChecker<SparseModelType, ImpreciseType, PreciseType>::specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates) {
             STORM_LOG_ASSERT(this->canHandle(parametricModel, checkTask), "specified model and formula can not be handled by this.");
         
             auto mdp = parametricModel->template as<SparseModelType>();
@@ -28,8 +28,8 @@ namespace storm {
             
             auto simplifiedTask = checkTask.substituteFormula(*simplifier.getSimplifiedFormula());
             
-            impreciseChecker.specify(env, simplifier.getSimplifiedModel(), simplifiedTask, true);
-            preciseChecker.specify(env, simplifier.getSimplifiedModel(), simplifiedTask, true);
+            impreciseChecker.specify(env, simplifier.getSimplifiedModel(), simplifiedTask, false, true);
+            preciseChecker.specify(env, simplifier.getSimplifiedModel(), simplifiedTask, false, true);
         }
         
         template <typename SparseModelType, typename ImpreciseType, typename PreciseType>
diff --git a/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.h
index fdb304747..d6ef0ba74 100644
--- a/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.h
+++ b/src/storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.h
@@ -12,7 +12,7 @@ namespace storm {
             ValidatingSparseMdpParameterLiftingModelChecker();
             virtual ~ValidatingSparseMdpParameterLiftingModelChecker() = default;
             
-            virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) override;
+            virtual void specify(Environment const& env, std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool generateRegionSplitEstimates = false) override;
 
         protected:
             virtual SparseParameterLiftingModelChecker<SparseModelType, ImpreciseType>& getImpreciseChecker() override;
diff --git a/src/storm-pars/transformer/ParameterLifter.cpp b/src/storm-pars/transformer/ParameterLifter.cpp
index 551529c4c..9eba6e8f2 100644
--- a/src/storm-pars/transformer/ParameterLifter.cpp
+++ b/src/storm-pars/transformer/ParameterLifter.cpp
@@ -12,8 +12,9 @@ namespace storm {
     namespace transformer {
 
         template<typename ParametricType, typename ConstantType>
-        ParameterLifter<ParametricType, ConstantType>::ParameterLifter(storm::storage::SparseMatrix<ParametricType> const& pMatrix, std::vector<ParametricType> const& pVector, storm::storage::BitVector const& selectedRows, storm::storage::BitVector const& selectedColumns) {
+        ParameterLifter<ParametricType, ConstantType>::ParameterLifter(storm::storage::SparseMatrix<ParametricType> const& pMatrix, std::vector<ParametricType> const& pVector, storm::storage::BitVector const& selectedRows, storm::storage::BitVector const& selectedColumns, bool generateRowLabels) {
         
+            
             // get a mapping from old column indices to new ones
             std::vector<uint_fast64_t> oldToNewColumnIndexMapping(selectedColumns.size(), selectedColumns.size());
             uint_fast64_t newIndex = 0;
@@ -45,10 +46,16 @@ namespace storm {
                         ++pMatrixEntryCount;
                     }
                 }
+                
                 ParametricType const& pVectorEntry = pVector[rowIndex];
                 std::set<VariableType> vectorEntryVariables;
                 if (!storm::utility::isConstant(pVectorEntry)) {
                     storm::utility::parametric::gatherOccurringVariables(pVectorEntry, vectorEntryVariables);
+                    if (generateRowLabels) {
+                        // If row labels are to be generated, we do not allow unspecified valuations.
+                        // Therefore, we also 'lift' parameters that only occurr on a vector.
+                        occurringVariables.insert(vectorEntryVariables.begin(), vectorEntryVariables.end());
+                    }
                     nonConstVectorEntries.set(pVectorEntryCount, true);
                 }
                 ++pVectorEntryCount;
@@ -57,6 +64,10 @@ namespace storm {
                 auto rowValuations = getVerticesOfAbstractRegion(occurringVariables);
                 
                 for (auto const& val : rowValuations) {
+                    if (generateRowLabels) {
+                        rowLabels.push_back(val);
+                    }
+                    
                     // Insert matrix entries for each valuation. For non-constant entries, a dummy value is inserted and the function and the valuation are collected.
                     // The placeholder for the collected function/valuation are stored in the matrixAssignment. The matrixAssignment is completed after the matrix is finished
                     for (auto const& entry: pMatrix.getRow(rowIndex)) {
@@ -78,7 +89,8 @@ namespace storm {
                         vector.push_back(storm::utility::one<ConstantType>());
                         AbstractValuation vectorVal(val);
                         for(auto const& vectorVar : vectorEntryVariables) {
-                            if(occurringVariables.find(vectorVar) == occurringVariables.end()) {
+                            if (occurringVariables.find(vectorVar) == occurringVariables.end()) {
+                                assert(!generateRowLabels);
                                 vectorVal.addParameterUnspecified(vectorVar);
                             }
                         }
@@ -148,6 +160,11 @@ namespace storm {
         std::vector<ConstantType> const& ParameterLifter<ParametricType, ConstantType>::getVector() const {
             return vector;
         }
+        
+        template<typename ParametricType, typename ConstantType>
+        std::vector<typename ParameterLifter<ParametricType, ConstantType>::AbstractValuation> const& ParameterLifter<ParametricType, ConstantType>::getRowLabels() const {
+            return rowLabels;
+        }
     
         template<typename ParametricType, typename ConstantType>
         std::vector<typename ParameterLifter<ParametricType, ConstantType>::AbstractValuation> ParameterLifter<ParametricType, ConstantType>::getVerticesOfAbstractRegion(std::set<VariableType> const& variables) const {
@@ -223,6 +240,21 @@ namespace storm {
             return result;
         }
             
+        template<typename ParametricType, typename ConstantType>
+        std::set<typename ParameterLifter<ParametricType, ConstantType>::VariableType> const& ParameterLifter<ParametricType, ConstantType>::AbstractValuation::getLowerParameters() const {
+            return lowerPars;
+        }
+        
+        template<typename ParametricType, typename ConstantType>
+        std::set<typename ParameterLifter<ParametricType, ConstantType>::VariableType> const& ParameterLifter<ParametricType, ConstantType>::AbstractValuation::getUpperParameters() const {
+            return upperPars;
+        }
+        
+        template<typename ParametricType, typename ConstantType>
+        std::set<typename ParameterLifter<ParametricType, ConstantType>::VariableType> const& ParameterLifter<ParametricType, ConstantType>::AbstractValuation::getUnspecifiedParameters() const {
+            return unspecifiedPars;
+        }
+        
         template<typename ParametricType, typename ConstantType>
         std::vector<storm::utility::parametric::Valuation<ParametricType>> ParameterLifter<ParametricType, ConstantType>::AbstractValuation::getConcreteValuations(storm::storage::ParameterRegion<ParametricType> const& region) const {
             auto result = region.getVerticesOfRegion(unspecifiedPars);
diff --git a/src/storm-pars/transformer/ParameterLifter.h b/src/storm-pars/transformer/ParameterLifter.h
index ab16e5a88..c7837fa5c 100644
--- a/src/storm-pars/transformer/ParameterLifter.h
+++ b/src/storm-pars/transformer/ParameterLifter.h
@@ -39,7 +39,7 @@ namespace storm {
              * @param selectedRows a Bitvector that specifies which rows of the matrix and the vector are considered.
              * @param selectedColumns a Bitvector that specifies which columns of the matrix are considered.
              */
-            ParameterLifter(storm::storage::SparseMatrix<ParametricType> const& pMatrix, std::vector<ParametricType> const& pVector, storm::storage::BitVector const& selectedRows, storm::storage::BitVector const& selectedColumns);
+            ParameterLifter(storm::storage::SparseMatrix<ParametricType> const& pMatrix, std::vector<ParametricType> const& pVector, storm::storage::BitVector const& selectedRows, storm::storage::BitVector const& selectedColumns,  bool generateRowLabels = false);
             
             void specifyRegion(storm::storage::ParameterRegion<ParametricType> const& region, storm::solver::OptimizationDirection const& dirForParameters);
             
@@ -49,13 +49,6 @@ namespace storm {
             // Returns the resulting vector. Should only be called AFTER specifying a region
             std::vector<ConstantType> const& getVector() const;
             
-            
-        private:
-            /*
-             * We minimize the number of function evaluations by only calling evaluate() once for each unique pair of function and valuation.
-             * The result of each evaluation is then written to all positions in the matrix (and the vector) where the corresponding (function,valuation) occurred.
-             */
-            
             /*
              * During initialization, the actual regions are not known. Hence, we consider abstract valuations,
              * where it is only known whether a parameter will be set to either the lower/upper bound of the region or whether this is unspecified
@@ -72,6 +65,9 @@ namespace storm {
                 
                 std::size_t getHashValue() const;
                 AbstractValuation getSubValuation(std::set<VariableType> const& pars) const;
+                std::set<VariableType> const& getLowerParameters() const;
+                std::set<VariableType> const& getUpperParameters() const;
+                std::set<VariableType> const& getUnspecifiedParameters() const;
                 
                 /*!
                  * Returns the concrete valuation(s) (w.r.t. the provided region) represented by this abstract valuation.
@@ -83,6 +79,17 @@ namespace storm {
                 std::set<VariableType> lowerPars, upperPars, unspecifiedPars;
             };
             
+            // Returns for each row the abstract valuation for this row
+            // Note: the returned vector might be empty if row label generaion was disabled initially
+            std::vector<AbstractValuation> const& getRowLabels() const;
+
+            
+        private:
+            /*
+             * We minimize the number of function evaluations by only calling evaluate() once for each unique pair of function and valuation.
+             * The result of each evaluation is then written to all positions in the matrix (and the vector) where the corresponding (function,valuation) occurred.
+             */
+            
             /*!
              * Collects all occurring pairs of functions and (abstract) valuations.
              * We also store a placeholder for the result of each pair. The result is computed and written into the placeholder whenever a region and optimization direction is specified.
@@ -121,7 +128,8 @@ namespace storm {
             // Returns the 2^(variables.size()) vertices of the region
             std::vector<AbstractValuation> getVerticesOfAbstractRegion(std::set<VariableType> const& variables) const;
             
-            
+            std::vector<AbstractValuation> rowLabels;
+
             storm::storage::SparseMatrix<ConstantType> matrix; //The resulting matrix;
             std::vector<std::pair<typename storm::storage::SparseMatrix<ConstantType>::iterator, ConstantType&>> matrixAssignment; // Connection of matrix entries with placeholders
             
diff --git a/src/storm/builder/ExplicitModelBuilder.cpp b/src/storm/builder/ExplicitModelBuilder.cpp
index ac4b554d5..6467793c6 100644
--- a/src/storm/builder/ExplicitModelBuilder.cpp
+++ b/src/storm/builder/ExplicitModelBuilder.cpp
@@ -309,8 +309,8 @@ namespace storm {
             buildMatrices(transitionMatrixBuilder, rewardModelBuilders, choiceInformationBuilder, markovianStates);
             
             // Initialize the model components with the obtained information.
-            storm::storage::sparse::ModelComponents<ValueType, RewardModelType> modelComponents(transitionMatrixBuilder.build(), buildStateLabeling(), std::unordered_map<std::string, RewardModelType>(), !generator->isDiscreteTimeModel(), std::move(markovianStates));
-            
+            storm::storage::sparse::ModelComponents<ValueType, RewardModelType> modelComponents(transitionMatrixBuilder.build(0, transitionMatrixBuilder.getCurrentRowGroupCount()), buildStateLabeling(), std::unordered_map<std::string, RewardModelType>(), !generator->isDiscreteTimeModel(), std::move(markovianStates));
+                        
             // Now finalize all reward models.
             for (auto& rewardModelBuilder : rewardModelBuilders) {
                 modelComponents.rewardModels.emplace(rewardModelBuilder.getName(), rewardModelBuilder.build(modelComponents.transitionMatrix.getRowCount(), modelComponents.transitionMatrix.getColumnCount(), modelComponents.transitionMatrix.getRowGroupCount()));
diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp
index 8ce496426..bd93a44ef 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp
+++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp
@@ -8,6 +8,8 @@
 #include "storm/models/sparse/MarkovAutomaton.h"
 #include "storm/models/sparse/StandardRewardModel.h"
 #include "storm/modelchecker/prctl/helper/SparseDtmcPrctlHelper.h"
+#include "storm/modelchecker/prctl/helper/DsMpiUpperRewardBoundsComputer.h"
+#include "storm/modelchecker/prctl/helper/BaierUpperRewardBoundsComputer.h"
 #include "storm/solver/MinMaxLinearEquationSolver.h"
 #include "storm/utility/graph.h"
 #include "storm/utility/macros.h"
@@ -42,12 +44,13 @@ namespace storm {
                 // Build a subsystem of the preprocessor result model that discards states that yield infinite reward for all schedulers.
                 // We can also merge the states that will have reward zero anyway.
                 storm::storage::BitVector maybeStates = preprocessorResult.rewardLessInfinityEStates.get() & ~preprocessorResult.reward0AStates;
+                storm::storage::BitVector finiteRewardChoices = preprocessorResult.preprocessedModel->getTransitionMatrix().getRowFilter(preprocessorResult.rewardLessInfinityEStates.get(), preprocessorResult.rewardLessInfinityEStates.get());
                 std::set<std::string> relevantRewardModels;
                 for (auto const& obj : this->objectives) {
                     obj.formula->gatherReferencedRewardModels(relevantRewardModels);
                 }
                 storm::transformer::GoalStateMerger<SparseModelType> merger(*preprocessorResult.preprocessedModel);
-                auto mergerResult = merger.mergeTargetAndSinkStates(maybeStates, preprocessorResult.reward0AStates, storm::storage::BitVector(maybeStates.size(), false), std::vector<std::string>(relevantRewardModels.begin(), relevantRewardModels.end()));
+                auto mergerResult = merger.mergeTargetAndSinkStates(maybeStates, preprocessorResult.reward0AStates, storm::storage::BitVector(maybeStates.size(), false), std::vector<std::string>(relevantRewardModels.begin(), relevantRewardModels.end()), finiteRewardChoices);
                 
                 // Initialize data specific for the considered model type
                 initializeModelTypeSpecificData(*mergerResult.model);
@@ -175,20 +178,17 @@ namespace storm {
                 std::unique_ptr<storm::solver::MinMaxLinearEquationSolver<ValueType>> solver = solverFactory.create(env, ecQuotient->matrix);
                 solver->setTrackScheduler(true);
                 solver->setHasUniqueSolution(true);
+                solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize);
                 auto req = solver->getRequirements(env, storm::solver::OptimizationDirection::Maximize, true);
-                boost::optional<ValueType> lowerBound = this->computeWeightedResultBound(true, weightVector, objectivesWithNoUpperTimeBound);
-                if (lowerBound) {
-                    solver->setLowerBound(lowerBound.get());
+                setBoundsToSolver(*solver, req.requiresLowerBounds(), req.requiresUpperBounds(), weightVector, objectivesWithNoUpperTimeBound, ecQuotient->matrix, ecQuotient->rowsWithSumLessOne, ecQuotient->auxChoiceValues);
+                if (solver->hasLowerBound()) {
                     req.clearLowerBounds();
                 }
-                boost::optional<ValueType> upperBound = this->computeWeightedResultBound(false, weightVector, objectivesWithNoUpperTimeBound);
-                if (upperBound) {
-                    solver->setUpperBound(upperBound.get());
+                if (solver->hasUpperBound()) {
                     req.clearUpperBounds();
                 }
                 STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement was not checked.");
                 solver->setRequirementsChecked(true);
-                solver->setOptimizationDirection(storm::solver::OptimizationDirection::Maximize);
                 
                 // Use the (0...0) vector as initial guess for the solution.
                 std::fill(ecQuotient->auxStateValues.begin(), ecQuotient->auxStateValues.end(), storm::utility::zero<ValueType>());
@@ -208,11 +208,11 @@ namespace storm {
                    if (storm::solver::minimize(this->objectives[objIndex].formula->getOptimalityType())) {
                        storm::utility::vector::scaleVectorInPlace(objectiveResults[objIndex], -storm::utility::one<ValueType>());
                    }
-                    for (uint_fast64_t objIndex2 = 0; objIndex2 < this->objectives.size(); ++objIndex2) {
-			            if (objIndex != objIndex2) {
-                            objectiveResults[objIndex2] = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
-                        }
-                    }
+                   for (uint_fast64_t objIndex2 = 0; objIndex2 < this->objectives.size(); ++objIndex2) {
+                       if (objIndex != objIndex2) {
+                           objectiveResults[objIndex2] = std::vector<ValueType>(transitionMatrix.getRowGroupCount(), storm::utility::zero<ValueType>());
+                       }
+                   }
                 } else {
                    storm::storage::SparseMatrix<ValueType> deterministicMatrix = transitionMatrix.selectRowsFromRowGroups(this->optimalChoices, true);
                    storm::storage::SparseMatrix<ValueType> deterministicBackwardTransitions = deterministicMatrix.transpose();
@@ -262,17 +262,19 @@ namespace storm {
                                std::vector<ValueType> b = storm::utility::vector::filterVector(deterministicStateRewards, maybeStates);
 
                                // Now solve the resulting equation system.
-                               std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(env, std::move(submatrix));
+                               std::unique_ptr<storm::solver::LinearEquationSolver<ValueType>> solver = linearEquationSolverFactory.create(env, submatrix);
                                auto req = solver->getRequirements(env);
                                solver->clearBounds();
-                               if (obj.lowerResultBound) {
+                               storm::storage::BitVector submatrixRowsWithSumLessOne = deterministicMatrix.getRowFilter(maybeStates, maybeStates) % maybeStates;
+                               submatrixRowsWithSumLessOne.complement();
+                               this->setBoundsToSolver(*solver, req.requiresLowerBounds(), req.requiresUpperBounds(), objIndex, submatrix, submatrixRowsWithSumLessOne, b);
+                               if (solver->hasLowerBound()) {
                                    req.clearLowerBounds();
-                                   solver->setLowerBound(*obj.lowerResultBound);
                                }
-                               if (obj.upperResultBound) {
-                                   solver->setUpperBound(*obj.upperResultBound);
+                               if (solver->hasUpperBound()) {
                                    req.clearUpperBounds();
                                }
+
                                STORM_LOG_THROW(req.empty(), storm::exceptions::UncheckedRequirementException, "At least one requirement of the LinearEquationSolver was not met.");
                                solver->solveEquations(env, x, b);
 
@@ -311,11 +313,26 @@ namespace storm {
                     // Remove neutral end components, i.e., ECs in which no reward is earned.
                     auto ecElimResult = storm::transformer::EndComponentEliminator<ValueType>::transform(transitionMatrix, subsystemStates, ecChoicesHint & newReward0Choices, reward0EStates);
                     
+                    storm::storage::BitVector rowsWithSumLessOne(ecElimResult.matrix.getRowCount(), false);
+                    for (uint64_t row = 0; row < rowsWithSumLessOne.size(); ++row) {
+                        if (ecElimResult.matrix.getRow(row).getNumberOfEntries() == 0) {
+                            rowsWithSumLessOne.set(row, true);
+                        } else {
+                            for (auto const& entry : transitionMatrix.getRow(ecElimResult.newToOldRowMapping[row])) {
+                                if (!subsystemStates.get(entry.getColumn())) {
+                                    rowsWithSumLessOne.set(row, true);
+                                    break;
+                                }
+                            }
+                        }
+                    }
+                    
                     ecQuotient = EcQuotient();
                     ecQuotient->matrix = std::move(ecElimResult.matrix);
                     ecQuotient->ecqToOriginalChoiceMapping = std::move(ecElimResult.newToOldRowMapping);
                     ecQuotient->originalToEcqStateMapping = std::move(ecElimResult.oldToNewStateMapping);
                     ecQuotient->origReward0Choices = std::move(newReward0Choices);
+                    ecQuotient->rowsWithSumLessOne = std::move(rowsWithSumLessOne);
                     ecQuotient->auxStateValues.reserve(transitionMatrix.getRowGroupCount());
                     ecQuotient->auxStateValues.resize(ecQuotient->matrix.getRowGroupCount());
                     ecQuotient->auxChoiceValues.reserve(transitionMatrix.getRowCount());
@@ -323,6 +340,91 @@ namespace storm {
                 }
             }
 
+            template <class SparseModelType>
+            void StandardPcaaWeightVectorChecker<SparseModelType>::setBoundsToSolver(storm::solver::AbstractEquationSolver<ValueType>& solver, bool requiresLower, bool requiresUpper, uint64_t objIndex, storm::storage::SparseMatrix<ValueType> const& transitions, storm::storage::BitVector const& rowsWithSumLessOne, std::vector<ValueType> const& rewards) const {
+                
+                // Check whether bounds are already available
+                if (this->objectives[objIndex].lowerResultBound) {
+                    solver.setLowerBound(this->objectives[objIndex].lowerResultBound.get());
+                }
+                if (this->objectives[objIndex].upperResultBound) {
+                    solver.setUpperBound(this->objectives[objIndex].upperResultBound.get());
+                }
+                
+                if ((requiresLower && !solver.hasLowerBound()) || (requiresUpper && !solver.hasUpperBound())) {
+                    computeAndSetBoundsToSolver(solver, requiresLower, requiresUpper, transitions, rowsWithSumLessOne, rewards);
+                }
+            }
+            
+            template <class SparseModelType>
+            void StandardPcaaWeightVectorChecker<SparseModelType>::setBoundsToSolver(storm::solver::AbstractEquationSolver<ValueType>& solver, bool requiresLower, bool requiresUpper, std::vector<ValueType> const& weightVector, storm::storage::BitVector const& objectiveFilter, storm::storage::SparseMatrix<ValueType> const& transitions, storm::storage::BitVector const& rowsWithSumLessOne, std::vector<ValueType> const& rewards) const {
+                
+                // Check whether bounds are already available
+                boost::optional<ValueType> lowerBound = this->computeWeightedResultBound(true, weightVector, objectiveFilter);
+                if (lowerBound) {
+                    solver.setLowerBound(lowerBound.get());
+                }
+                boost::optional<ValueType> upperBound = this->computeWeightedResultBound(false, weightVector, objectiveFilter);
+                if (upperBound) {
+                    solver.setUpperBound(upperBound.get());
+                }
+                
+                if ((requiresLower && !solver.hasLowerBound()) || (requiresUpper && !solver.hasUpperBound())) {
+                    computeAndSetBoundsToSolver(solver, requiresLower, requiresUpper, transitions, rowsWithSumLessOne, rewards);
+                }
+            }
+            
+            template <class SparseModelType>
+            void StandardPcaaWeightVectorChecker<SparseModelType>::computeAndSetBoundsToSolver(storm::solver::AbstractEquationSolver<ValueType>& solver, bool requiresLower, bool requiresUpper, storm::storage::SparseMatrix<ValueType> const& transitions, storm::storage::BitVector const& rowsWithSumLessOne, std::vector<ValueType> const& rewards) const {
+
+                // Compute the one step target probs
+                std::vector<ValueType> oneStepTargetProbs(transitions.getRowCount(), storm::utility::zero<ValueType>());
+                for (auto const& row : rowsWithSumLessOne) {
+                    oneStepTargetProbs[row] = storm::utility::one<ValueType>() - transitions.getRowSum(row);
+                }
+                
+                if (requiresLower && !solver.hasLowerBound()) {
+                    // Compute lower bounds
+                    std::vector<ValueType> negativeRewards;
+                    negativeRewards.reserve(transitions.getRowCount());
+                    uint64_t row = 0;
+                    for (auto const& rew : rewards) {
+                        if (rew < storm::utility::zero<ValueType>()) {
+                            negativeRewards.resize(row, storm::utility::zero<ValueType>());
+                            negativeRewards.push_back(-rew);
+                        }
+                        ++row;
+                    }
+                    if (!negativeRewards.empty()) {
+                        negativeRewards.resize(row, storm::utility::zero<ValueType>());
+                        std::vector<ValueType> lowerBounds = storm::modelchecker::helper::DsMpiMdpUpperRewardBoundsComputer<ValueType>(transitions, negativeRewards, oneStepTargetProbs).computeUpperBounds();
+                        storm::utility::vector::scaleVectorInPlace(lowerBounds, -storm::utility::one<ValueType>());
+                        solver.setLowerBounds(std::move(lowerBounds));
+                    } else {
+                        solver.setLowerBound(storm::utility::zero<ValueType>());
+                    }
+                }
+                
+                // Compute upper bounds
+                if (requiresUpper && !solver.hasUpperBound()) {
+                    std::vector<ValueType> positiveRewards;
+                    positiveRewards.reserve(transitions.getRowCount());
+                    uint64_t row = 0;
+                    for (auto const& rew : rewards) {
+                        if (rew > storm::utility::zero<ValueType>()) {
+                            positiveRewards.resize(row, storm::utility::zero<ValueType>());
+                            positiveRewards.push_back(rew);
+                        }
+                        ++row;
+                    }
+                    if (!positiveRewards.empty()) {
+                        positiveRewards.resize(row, storm::utility::zero<ValueType>());
+                        solver.setUpperBound(storm::modelchecker::helper::BaierUpperRewardBoundsComputer<ValueType>(transitions, positiveRewards, oneStepTargetProbs).computeUpperBound());
+                    } else {
+                        solver.setUpperBound(storm::utility::zero<ValueType>());
+                    }
+                }
+            }
             
             template <class SparseModelType>
             void StandardPcaaWeightVectorChecker<SparseModelType>::transformReducedSolutionToOriginalModel(storm::storage::SparseMatrix<ValueType> const& reducedMatrix,
diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h
index 86cd79c7f..2f0a27f33 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h
+++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h
@@ -1,5 +1,6 @@
 #pragma once
 
+#include "storm/solver/AbstractEquationSolver.h"
 #include "storm/storage/BitVector.h"
 #include "storm/storage/SparseMatrix.h"
 #include "storm/storage/Scheduler.h"
@@ -93,6 +94,11 @@ namespace storm {
                 
                 void updateEcQuotient(std::vector<ValueType> const& weightedRewardVector);
                 
+                
+                void setBoundsToSolver(storm::solver::AbstractEquationSolver<ValueType>& solver, bool requiresLower, bool requiresUpper, uint64_t objIndex, storm::storage::SparseMatrix<ValueType> const& transitions, storm::storage::BitVector const& rowsWithSumLessOne, std::vector<ValueType> const& rewards) const;
+                void setBoundsToSolver(storm::solver::AbstractEquationSolver<ValueType>& solver, bool requiresLower, bool requiresUpper, std::vector<ValueType> const& weightVector, storm::storage::BitVector const& objectiveFilter, storm::storage::SparseMatrix<ValueType> const& transitions, storm::storage::BitVector const& rowsWithSumLessOne, std::vector<ValueType> const& rewards) const;
+                void computeAndSetBoundsToSolver(storm::solver::AbstractEquationSolver<ValueType>& solver, bool requiresLower, bool requiresUpper, storm::storage::SparseMatrix<ValueType> const& transitions, storm::storage::BitVector const& rowsWithSumLessOne, std::vector<ValueType> const& rewards) const;
+
                 /*!
                  * Transforms the results of a min-max-solver that considers a reduced model (without end components) to a result for the original (unreduced) model
                  */
@@ -141,6 +147,7 @@ namespace storm {
                     std::vector<uint_fast64_t> ecqToOriginalChoiceMapping;
                     std::vector<uint_fast64_t> originalToEcqStateMapping;
                     storm::storage::BitVector origReward0Choices;
+                    storm::storage::BitVector rowsWithSumLessOne;
                     
                     std::vector<ValueType> auxStateValues;
                     std::vector<ValueType> auxChoiceValues;
diff --git a/src/storm/storage/SparseMatrix.cpp b/src/storm/storage/SparseMatrix.cpp
index 83ff4f3af..36dd5724e 100644
--- a/src/storm/storage/SparseMatrix.cpp
+++ b/src/storm/storage/SparseMatrix.cpp
@@ -87,7 +87,7 @@ namespace storm {
         }
         
         template<typename ValueType>
-        SparseMatrixBuilder<ValueType>::SparseMatrixBuilder(index_type rows, index_type columns, index_type entries, bool forceDimensions, bool hasCustomRowGrouping, index_type rowGroups) : initialRowCountSet(rows != 0), initialRowCount(rows), initialColumnCountSet(columns != 0), initialColumnCount(columns), initialEntryCountSet(entries != 0), initialEntryCount(entries), forceInitialDimensions(forceDimensions), hasCustomRowGrouping(hasCustomRowGrouping), initialRowGroupCountSet(rowGroups != 0), initialRowGroupCount(rowGroups), rowGroupIndices(), columnsAndValues(), rowIndications(), currentEntryCount(0), lastRow(0), lastColumn(0), highestColumn(0), currentRowGroup(0) {
+        SparseMatrixBuilder<ValueType>::SparseMatrixBuilder(index_type rows, index_type columns, index_type entries, bool forceDimensions, bool hasCustomRowGrouping, index_type rowGroups) : initialRowCountSet(rows != 0), initialRowCount(rows), initialColumnCountSet(columns != 0), initialColumnCount(columns), initialEntryCountSet(entries != 0), initialEntryCount(entries), forceInitialDimensions(forceDimensions), hasCustomRowGrouping(hasCustomRowGrouping), initialRowGroupCountSet(rowGroups != 0), initialRowGroupCount(rowGroups), rowGroupIndices(), columnsAndValues(), rowIndications(), currentEntryCount(0), lastRow(0), lastColumn(0), highestColumn(0), currentRowGroupCount(0) {
             // Prepare the internal storage.
             if (initialRowCountSet) {
                 rowIndications.reserve(initialRowCount + 1);
@@ -105,7 +105,7 @@ namespace storm {
         }
         
         template<typename ValueType>
-        SparseMatrixBuilder<ValueType>::SparseMatrixBuilder(SparseMatrix<ValueType>&& matrix) :  initialRowCountSet(false), initialRowCount(0), initialColumnCountSet(false), initialColumnCount(0), initialEntryCountSet(false), initialEntryCount(0), forceInitialDimensions(false), hasCustomRowGrouping(!matrix.trivialRowGrouping), initialRowGroupCountSet(false), initialRowGroupCount(0), rowGroupIndices(), columnsAndValues(std::move(matrix.columnsAndValues)), rowIndications(std::move(matrix.rowIndications)), currentEntryCount(matrix.entryCount), currentRowGroup() {
+        SparseMatrixBuilder<ValueType>::SparseMatrixBuilder(SparseMatrix<ValueType>&& matrix) :  initialRowCountSet(false), initialRowCount(0), initialColumnCountSet(false), initialColumnCount(0), initialEntryCountSet(false), initialEntryCount(0), forceInitialDimensions(false), hasCustomRowGrouping(!matrix.trivialRowGrouping), initialRowGroupCountSet(false), initialRowGroupCount(0), rowGroupIndices(), columnsAndValues(std::move(matrix.columnsAndValues)), rowIndications(std::move(matrix.rowIndications)), currentEntryCount(matrix.entryCount), currentRowGroupCount() {
             
             lastRow = matrix.rowCount == 0 ? 0 : matrix.rowCount - 1;
             lastColumn = columnsAndValues.empty() ? 0 : columnsAndValues.back().getColumn();
@@ -117,7 +117,7 @@ namespace storm {
                 if (!rowGroupIndices->empty()) {
                     rowGroupIndices.get().pop_back();
                 }
-                currentRowGroup = rowGroupIndices->empty() ? 0 : rowGroupIndices.get().size() - 1;
+                currentRowGroupCount = rowGroupIndices->empty() ? 0 : rowGroupIndices.get().size() - 1;
             }
             
             // Likewise, we need to 'open' the row indications again.
@@ -191,7 +191,7 @@ namespace storm {
             STORM_LOG_THROW(hasCustomRowGrouping, storm::exceptions::InvalidStateException, "Matrix was not created to have a custom row grouping.");
             STORM_LOG_THROW(startingRow >= lastRow, storm::exceptions::InvalidStateException, "Illegal row group with negative size.");
             rowGroupIndices.get().push_back(startingRow);
-            ++currentRowGroup;
+            ++currentRowGroupCount;
             
             // Close all rows from the most recent one to the starting row.
             for (index_type i = lastRow + 1; i < startingRow; ++i) {
@@ -252,14 +252,14 @@ namespace storm {
             
             // Check whether row groups are missing some entries.
             if (hasCustomRowGrouping) {
-                uint_fast64_t rowGroupCount = currentRowGroup;
+                uint_fast64_t rowGroupCount = currentRowGroupCount;
                 if (initialRowGroupCountSet && forceInitialDimensions) {
                     STORM_LOG_THROW(rowGroupCount <= initialRowGroupCount, storm::exceptions::InvalidStateException, "Expected not more than " << initialRowGroupCount << " row groups, but got " << rowGroupCount << ".");
                     rowGroupCount = std::max(rowGroupCount, initialRowGroupCount);
                 }
                 rowGroupCount = std::max(rowGroupCount, overriddenRowGroupCount);
                 
-                for (index_type i = currentRowGroup; i <= rowGroupCount; ++i) {
+                for (index_type i = currentRowGroupCount; i <= rowGroupCount; ++i) {
                     rowGroupIndices.get().push_back(rowCount);
                 }
             }
@@ -271,7 +271,16 @@ namespace storm {
         typename SparseMatrixBuilder<ValueType>::index_type SparseMatrixBuilder<ValueType>::getLastRow() const {
             return lastRow;
         }
-        
+
+        template<typename ValueType>
+        typename SparseMatrixBuilder<ValueType>::index_type SparseMatrixBuilder<ValueType>::getCurrentRowGroupCount() const {
+            if (this->hasCustomRowGrouping) {
+                return currentRowGroupCount;
+            } else {
+                return getLastRow() + 1;
+            }
+        }
+
         template<typename ValueType>
         typename SparseMatrixBuilder<ValueType>::index_type SparseMatrixBuilder<ValueType>::getLastColumn() const {
             return lastColumn;
diff --git a/src/storm/storage/SparseMatrix.h b/src/storm/storage/SparseMatrix.h
index 08a23ab2e..e07389e5a 100644
--- a/src/storm/storage/SparseMatrix.h
+++ b/src/storm/storage/SparseMatrix.h
@@ -219,6 +219,13 @@ namespace storm {
              */
             index_type getLastRow() const;
 
+            /*!
+             * Retrieves the current row group count.
+             *
+             * @return The current row group count.
+             */
+            index_type getCurrentRowGroupCount() const;
+
             /*!
              * Retrieves the most recently used row.
              *
@@ -296,7 +303,7 @@ namespace storm {
             
             // Stores the currently active row group. This is used for correctly constructing the row grouping of the
             // matrix.
-            index_type currentRowGroup;
+            index_type currentRowGroupCount;
         };
         
         /*!
diff --git a/src/storm/transformer/GoalStateMerger.cpp b/src/storm/transformer/GoalStateMerger.cpp
index 49497237e..7707bd3f1 100644
--- a/src/storm/transformer/GoalStateMerger.cpp
+++ b/src/storm/transformer/GoalStateMerger.cpp
@@ -24,10 +24,10 @@ namespace storm {
         }
             
         template <typename SparseModelType>
-        typename GoalStateMerger<SparseModelType>::ReturnType GoalStateMerger<SparseModelType>::mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, std::vector<std::string> const& selectedRewardModels) const {
+        typename GoalStateMerger<SparseModelType>::ReturnType GoalStateMerger<SparseModelType>::mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, std::vector<std::string> const& selectedRewardModels, boost::optional<storm::storage::BitVector> const& choiceFilter) const {
             STORM_LOG_THROW(maybeStates.isDisjointFrom(targetStates) && targetStates.isDisjointFrom(sinkStates) && sinkStates.isDisjointFrom(maybeStates), storm::exceptions::InvalidArgumentException, "maybestates, targetstates, and sinkstates are assumed to be disjoint when creating the submodel. However, this is not the case.");
   
-            auto result = initialize(maybeStates, targetStates, sinkStates);
+            auto result = initialize(maybeStates, targetStates, sinkStates, choiceFilter);
             
             auto transitionMatrix = buildTransitionMatrix(maybeStates, result.first, result.second);
             auto labeling = buildStateLabeling(maybeStates, targetStates, sinkStates, result.first);
@@ -39,7 +39,7 @@ namespace storm {
         }
         
         template <typename SparseModelType>
-        std::pair<typename GoalStateMerger<SparseModelType>::ReturnType, uint_fast64_t> GoalStateMerger<SparseModelType>::initialize(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates) const {
+        std::pair<typename GoalStateMerger<SparseModelType>::ReturnType, uint_fast64_t> GoalStateMerger<SparseModelType>::initialize(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, boost::optional<storm::storage::BitVector> const& choiceFilter) const {
             
             storm::storage::SparseMatrix<typename SparseModelType::ValueType> const& origMatrix = originalModel.getTransitionMatrix();
             
@@ -58,33 +58,35 @@ namespace storm {
                 for (uint_fast64_t row = origMatrix.getRowGroupIndices()[state]; row < endOfRowGroup; ++row) {
                     uint_fast64_t transitionsToMaybeStates = 0;
                     bool keepThisRow(true), hasTransitionToTarget(false), hasTransitionToSink(false);
-                    for (auto const& entry : origMatrix.getRow(row)) {
-                        if (maybeStates.get(entry.getColumn())) {
-                            ++transitionsToMaybeStates;
-                        } else if (targetStates.get(entry.getColumn())) {
-                            hasTransitionToTarget = true;
-                        } else if (sinkStates.get(entry.getColumn())) {
-                            hasTransitionToSink = true;
-                        } else {
-                            keepThisRow = false;
-                            break;
-                        }
-                    }
-                    if (keepThisRow) {
-                        stateIsDeadlock = false;
-                        result.keptChoices.set(row, true);
-                        transitionCount += transitionsToMaybeStates;
-                        if (hasTransitionToTarget) {
-                            ++transitionCount;
-                            targetStateRequired = true;
+                    if (!choiceFilter || choiceFilter.get().get(row)) {
+                        for (auto const& entry : origMatrix.getRow(row)) {
+                            if (maybeStates.get(entry.getColumn())) {
+                                ++transitionsToMaybeStates;
+                            } else if (targetStates.get(entry.getColumn())) {
+                                hasTransitionToTarget = true;
+                            } else if (sinkStates.get(entry.getColumn())) {
+                                hasTransitionToSink = true;
+                            } else {
+                                keepThisRow = false;
+                                break;
+                            }
                         }
-                        if (hasTransitionToSink) {
-                            ++transitionCount;
-                            sinkStateRequired = true;
+                        if (keepThisRow) {
+                            stateIsDeadlock = false;
+                            result.keptChoices.set(row, true);
+                            transitionCount += transitionsToMaybeStates;
+                            if (hasTransitionToTarget) {
+                                ++transitionCount;
+                                targetStateRequired = true;
+                            }
+                            if (hasTransitionToSink) {
+                                ++transitionCount;
+                                sinkStateRequired = true;
+                            }
                         }
                     }
-                    STORM_LOG_THROW(!stateIsDeadlock, storm::exceptions::InvalidArgumentException, "Merging goal states leads to deadlocks!");
                 }
+                STORM_LOG_THROW(!stateIsDeadlock, storm::exceptions::InvalidArgumentException, "Merging goal states leads to deadlocks!");
                 ++stateCount;
             }
             
diff --git a/src/storm/transformer/GoalStateMerger.h b/src/storm/transformer/GoalStateMerger.h
index bc9dadcda..f79a127a6 100644
--- a/src/storm/transformer/GoalStateMerger.h
+++ b/src/storm/transformer/GoalStateMerger.h
@@ -35,6 +35,8 @@ namespace storm {
              *  * one target state to which all transitions to a state selected by targetStates are redirected and
              *  * one sink state to which all transitions to a state selected by sinkStates are redirected.
              *
+             * If a choiceFilter is given, choices on maybestates that are not selected by the filter will be removed.
+             *
              *  Notes:
              *  * the target (or sink) state is not created, if it is not reachable
              *  * the target (or sink) state will get a label iff it is reachable and at least one of the given targetStates (sinkStates) have that label.
@@ -43,7 +45,7 @@ namespace storm {
              *  * It is assumed that maybeStates, targetStates, and sinkStates are pairwise disjoint. Otherwise an exception is thrown.
              *  * The order of the maybeStates will not be affected (i.e. s_1 < s_2 in the input model implies s'_1 < s'_2 in the output model).
              */
-             ReturnType mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, std::vector<std::string> const& selectedRewardModels = std::vector<std::string>()) const;
+             ReturnType mergeTargetAndSinkStates(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, std::vector<std::string> const& selectedRewardModels = std::vector<std::string>(), boost::optional<storm::storage::BitVector> const& choiceFilter = boost::none) const;
             
         private:
             SparseModelType const& originalModel;
@@ -53,7 +55,7 @@ namespace storm {
              *
              * @return The initialized result and the number of transitions of the result model
              */
-            std::pair<ReturnType, uint_fast64_t> initialize(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates) const;
+            std::pair<ReturnType, uint_fast64_t> initialize(storm::storage::BitVector const& maybeStates, storm::storage::BitVector const& targetStates, storm::storage::BitVector const& sinkStates, boost::optional<storm::storage::BitVector> const& choiceFilter = boost::none) const;
             
             /*!
              * Builds the transition matrix of the resulting model