diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp
index 8ffaa852e..6fb83ad26 100644
--- a/src/storm-pars-cli/storm-pars.cpp
+++ b/src/storm-pars-cli/storm-pars.cpp
@@ -179,25 +179,11 @@ namespace storm {
             }
         }
         
-        template<typename ValueType>
-        std::pair<std::shared_ptr<storm::models::sparse::Model<ValueType>>, std::shared_ptr<storm::logic::Formula const>> performSimplification(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, std::shared_ptr<storm::logic::Formula const> const& formula) {
-            auto parametricSettings = storm::settings::getModule<storm::settings::modules::ParametricSettings>();
-        
-            std::pair<std::shared_ptr<storm::models::sparse::Model<ValueType>>, std::shared_ptr<storm::logic::Formula const>> result;
-            
-            if (!(parametricSettings.isSimplifySet() && storm::api::simplifyParametricModel<ValueType>(model, formula, result.first, result.second))) {
-                result = std::make_pair(model, formula);
-            }
-            
-            return result;
-        }
-        
         template <typename ValueType>
         void verifyPropertiesWithSparseEngine(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& model, SymbolicInput const& input) {
             verifyProperties<ValueType>(input.properties,
                                         [&model] (std::shared_ptr<storm::logic::Formula const> const& formula) {
-                                            auto simplificationResult = performSimplification(model, formula);
-                                            std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithSparseEngine<ValueType>(simplificationResult.first, storm::api::createTask<ValueType>(simplificationResult.second, true));
+                                            std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::verifyWithSparseEngine<ValueType>(model, storm::api::createTask<ValueType>(formula, true));
                                             result->filter(storm::modelchecker::ExplicitQualitativeCheckResult(simplificationResult.first->getInitialStates()));
                                             return result;
                                         },
@@ -235,15 +221,13 @@ namespace storm {
                 STORM_PRINT_AND_LOG(" with iterative refinement until " << (1.0 - regionSettings.getRefinementThreshold()) * 100.0 << "% is covered." << std::endl);
                 verificationCallback = [&] (std::shared_ptr<storm::logic::Formula const> const& formula) {
                                         ValueType refinementThreshold = storm::utility::convertNumber<ValueType>(regionSettings.getRefinementThreshold());
-                                        auto simplificationResult = performSimplification(model, formula);
-                                        std::unique_ptr<storm::modelchecker::RegionRefinementCheckResult<ValueType>> result = storm::api::checkAndRefineRegionWithSparseEngine<ValueType>(simplificationResult.first, storm::api::createTask<ValueType>(simplificationResult.second, true), regions.front(), refinementThreshold, engine);
+                                        std::unique_ptr<storm::modelchecker::RegionRefinementCheckResult<ValueType>> result = storm::api::checkAndRefineRegionWithSparseEngine<ValueType>(model, storm::api::createTask<ValueType>(formula, true), regions.front(), refinementThreshold, engine);
                                         return result;
                                     };
             } else {
                 STORM_PRINT_AND_LOG("." << std::endl);
                 verificationCallback = [&] (std::shared_ptr<storm::logic::Formula const> const& formula) {
-                                        auto simplificationResult = performSimplification(model, formula);
-                                        std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::checkRegionsWithSparseEngine<ValueType>(simplificationResult.first, storm::api::createTask<ValueType>(simplificationResult.second, true), regions, engine);
+                                        std::unique_ptr<storm::modelchecker::CheckResult> result = storm::api::checkRegionsWithSparseEngine<ValueType>(model, storm::api::createTask<ValueType>(formula, true), regions, engine);
                                         return result;
                                     };
             }
diff --git a/src/storm-pars/api/parametric.h b/src/storm-pars/api/parametric.h
deleted file mode 100644
index aec977003..000000000
--- a/src/storm-pars/api/parametric.h
+++ /dev/null
@@ -1,45 +0,0 @@
-#pragma once
-
-#include <memory>
-
-#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h"
-#include "storm-pars/transformer/SparseParametricMdpSimplifier.h"
-
-#include "storm/models/sparse/Model.h"
-#include "storm/logic/Formula.h"
-#include "storm/utility/macros.h"
-
-namespace storm {
-    namespace api {
-        
-        template <typename ValueType>
-        bool simplifyParametricModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> const& inputModel, std::shared_ptr<storm::logic::Formula const> const& inputFormula, std::shared_ptr<storm::models::sparse::Model<ValueType>>& outputModel, std::shared_ptr<storm::logic::Formula const>& outputFormula) {
-            
-            if (inputModel->isOfType(storm::models::ModelType::Dtmc)) {
-                auto const& dtmc = *inputModel->template as<storm::models::sparse::Dtmc<ValueType>>();
-                auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<storm::models::sparse::Dtmc<ValueType>>(dtmc);
-                if (simplifier.simplify(*inputFormula)) {
-                    outputModel = simplifier.getSimplifiedModel();
-                    outputFormula = simplifier.getSimplifiedFormula();
-                    return true;
-                }
-            } else if (inputModel->isOfType(storm::models::ModelType::Mdp)) {
-                auto const& mdp = *inputModel->template as<storm::models::sparse::Mdp<ValueType>>();
-                auto simplifier = storm::transformer::SparseParametricMdpSimplifier<storm::models::sparse::Mdp<ValueType>>(mdp);
-                if (simplifier.simplify(*inputFormula)) {
-                    outputModel = simplifier.getSimplifiedModel();
-                    outputFormula = simplifier.getSimplifiedFormula();
-                    return true;
-                }
-            } else {
-                STORM_LOG_ERROR("Unable to simplify model with the given type.");
-            }
-
-            // Reaching this point means that simplification was not successful.
-            outputModel = nullptr;
-            outputFormula = nullptr;
-            return false;
-            
-        }
-    }
-}
diff --git a/src/storm-pars/api/region.h b/src/storm-pars/api/region.h
index 2a5ff9fcd..043f461b0 100644
--- a/src/storm-pars/api/region.h
+++ b/src/storm-pars/api/region.h
@@ -6,14 +6,16 @@
 #include <memory>
 #include <boost/optional.hpp>
 
-#include "storm-pars/storage/ParameterRegion.h"
-
 #include "storm-pars/modelchecker/results/RegionCheckResult.h"
 #include "storm-pars/modelchecker/results/RegionRefinementCheckResult.h"
-#include "storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h"
 #include "storm-pars/modelchecker/region/RegionCheckEngine.h"
+#include "storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h"
 #include "storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h"
+#include "storm-pars/modelchecker/region/ValidatingSparseMdpParameterLiftingModelChecker.h"
+#include "storm-pars/modelchecker/region/ValidatingSparseDtmcParameterLiftingModelChecker.h"
 #include "storm-pars/parser/ParameterRegionParser.h"
+#include "storm-pars/storage/ParameterRegion.h"
+#include "storm-pars/utility/parameterlifting.h"
 
 #include "storm/api/transformation.h"
 #include "storm/utility/file.h"
@@ -53,51 +55,86 @@ namespace storm {
         
         template <typename ValueType>
         storm::storage::ParameterRegion<ValueType> parseRegion(std::string const& inputString, std::set<typename storm::storage::ParameterRegion<ValueType>::VariableType> const& consideredVariables) {
-            auto res = parseRegions(inputString, consideredVariables);
+            // Handle the "empty region" case
+            if (inputString == "" && consideredVariables.empty()) {
+                return storm::storage::ParameterRegion<ValueType>();
+            }
+            
+            auto res = parseRegions<ValueType>(inputString, consideredVariables);
             STORM_LOG_THROW(res.size() == 1, storm::exceptions::InvalidOperationException, "Parsed " << res.size() << " regions but exactly one was expected.");
             return res.front();
         }
         
         template <typename ValueType>
         storm::storage::ParameterRegion<ValueType> parseRegion(std::string const& inputString, storm::models::ModelBase const& model) {
-            auto res = parseRegions(inputString, model);
+            // Handle the "empty region" case
+            if (inputString == "" && !model.hasParameters()) {
+                return storm::storage::ParameterRegion<ValueType>();
+            }
+            
+            auto res = parseRegions<ValueType>(inputString, model);
             STORM_LOG_THROW(res.size() == 1, storm::exceptions::InvalidOperationException, "Parsed " << res.size() << " regions but exactly one was expected.");
             return res.front();
         }
-
         
         template <typename ParametricType, typename ConstantType>
         std::unique_ptr<storm::modelchecker::RegionModelChecker<ParametricType>> initializeParameterLiftingRegionModelChecker(std::shared_ptr<storm::models::sparse::Model<ParametricType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ParametricType> const& task) {
+            
+            STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(*model, task.getFormula()), "Could not validate whether parameter lifting is applicable. Please validate manually...");
+
+            std::shared_ptr<storm::models::sparse::Model<ParametricType>> consideredModel = model;
+            
             // Treat continuous time models
-            if (model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::MarkovAutomaton)) {
+            if (consideredModel->isOfType(storm::models::ModelType::Ctmc) || consideredModel->isOfType(storm::models::ModelType::MarkovAutomaton)) {
                     STORM_LOG_WARN("Parameter lifting not supported for continuous time models. Transforming continuous model to discrete model...");
                     std::vector<std::shared_ptr<storm::logic::Formula const>> taskFormulaAsVector { task.getFormula().asSharedPointer() };
-                    auto discreteTimeModel = storm::api::transformContinuousToDiscreteTimeSparseModel(model, taskFormulaAsVector);
-                    STORM_LOG_THROW(discreteTimeModel->isOfType(storm::models::ModelType::Dtmc) || discreteTimeModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::UnexpectedException, "Transformation to discrete time model has failed.");
-                    return initializeParameterLiftingRegionModelChecker<ParametricType, ConstantType>(discreteTimeModel, task);
+                    consideredModel = storm::api::transformContinuousToDiscreteTimeSparseModel(consideredModel, taskFormulaAsVector);
+                    STORM_LOG_THROW(consideredModel->isOfType(storm::models::ModelType::Dtmc) || consideredModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::UnexpectedException, "Transformation to discrete time model has failed.");
             }
             
             // Obtain the region model checker
             std::unique_ptr<storm::modelchecker::RegionModelChecker<ParametricType>> result;
-            if (model->isOfType(storm::models::ModelType::Dtmc)) {
-                auto const& dtmc = *model->template as<storm::models::sparse::Dtmc<ParametricType>>();
-                result = std::make_unique<storm::modelchecker::SparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<ParametricType>, ConstantType>>(dtmc);
-            } else if (model->isOfType(storm::models::ModelType::Mdp)) {
-                auto const& mdp = *model->template as<storm::models::sparse::Mdp<ParametricType>>();
-                result = std::make_unique<storm::modelchecker::SparseMdpParameterLiftingModelChecker<storm::models::sparse::Mdp<ParametricType>, ConstantType>>(mdp);
+            if (consideredModel->isOfType(storm::models::ModelType::Dtmc)) {
+                result = std::make_unique<storm::modelchecker::SparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<ParametricType>, ConstantType>>();
+            } else if (consideredModel->isOfType(storm::models::ModelType::Mdp)) {
+                result = std::make_unique<storm::modelchecker::SparseMdpParameterLiftingModelChecker<storm::models::sparse::Mdp<ParametricType>, ConstantType>>();
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform parameterLifting on the provided model type.");
             }
-                
-            result->specifyFormula(task);
-        
+            
+            result->specify(consideredModel, task);
+            
             return result;
         }
         
         template <typename ParametricType, typename ImpreciseType, typename PreciseType>
         std::unique_ptr<storm::modelchecker::RegionModelChecker<ParametricType>> initializeValidatingRegionModelChecker(std::shared_ptr<storm::models::sparse::Model<ParametricType>> const& model, storm::modelchecker::CheckTask<storm::logic::Formula, ParametricType> const& task) {
-            // todo
-            return nullptr;
+            
+            STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(*model, task.getFormula()), "Could not validate whether parameter lifting is applicable. Please validate manually...");
+
+            std::shared_ptr<storm::models::sparse::Model<ParametricType>> consideredModel = model;
+            
+            // Treat continuous time models
+            if (consideredModel->isOfType(storm::models::ModelType::Ctmc) || consideredModel->isOfType(storm::models::ModelType::MarkovAutomaton)) {
+                    STORM_LOG_WARN("Parameter lifting not supported for continuous time models. Transforming continuous model to discrete model...");
+                    std::vector<std::shared_ptr<storm::logic::Formula const>> taskFormulaAsVector { task.getFormula().asSharedPointer() };
+                    consideredModel = storm::api::transformContinuousToDiscreteTimeSparseModel(consideredModel, taskFormulaAsVector);
+                    STORM_LOG_THROW(consideredModel->isOfType(storm::models::ModelType::Dtmc) || consideredModel->isOfType(storm::models::ModelType::Mdp), storm::exceptions::UnexpectedException, "Transformation to discrete time model has failed.");
+            }
+            
+            // Obtain the region model checker
+            std::unique_ptr<storm::modelchecker::RegionModelChecker<ParametricType>> result;
+            if (consideredModel->isOfType(storm::models::ModelType::Dtmc)) {
+                result = std::make_unique<storm::modelchecker::ValidatingSparseDtmcParameterLiftingModelChecker<storm::models::sparse::Dtmc<ParametricType>, ImpreciseType, PreciseType>>();
+            } else if (consideredModel->isOfType(storm::models::ModelType::Mdp)) {
+                result = std::make_unique<storm::modelchecker::ValidatingSparseMdpParameterLiftingModelChecker<storm::models::sparse::Mdp<ParametricType>, ImpreciseType, PreciseType>>();
+            } else {
+                STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Unable to perform parameterLifting on the provided model type.");
+            }
+            
+            result->specify(consideredModel, task);
+            
+            return result;
         }
         
         template <typename ValueType>
diff --git a/src/storm-pars/api/storm-pars.h b/src/storm-pars/api/storm-pars.h
index f7b15dda0..42ac7dc79 100644
--- a/src/storm-pars/api/storm-pars.h
+++ b/src/storm-pars/api/storm-pars.h
@@ -1,4 +1,3 @@
 #pragma once
 
 #include "storm-pars/api/region.h"
-#include "storm-pars/api/parametric.h"
diff --git a/src/storm-pars/modelchecker/region/RegionModelChecker.cpp b/src/storm-pars/modelchecker/region/RegionModelChecker.cpp
index d6a457899..a2a19451d 100644
--- a/src/storm-pars/modelchecker/region/RegionModelChecker.cpp
+++ b/src/storm-pars/modelchecker/region/RegionModelChecker.cpp
@@ -40,47 +40,6 @@ namespace storm {
                 return std::make_unique<storm::modelchecker::RegionCheckResult<ParametricType>>(std::move(result));
             }
 
-            /*
-#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
-            template <typename ParametricType, typename ConstantType, typename ExactConstantType>
-            RegionResult RegionModelChecker<ParametricType, ConstantType, ExactConstantType>::analyzeRegionExactValidation(storm::storage::ParameterRegion<typename ParametricType::ValueType> const& region, RegionResult const& initialResult) {
-                RegionResult numericResult = analyzeRegion(region, initialResult, false);
-                parameterLiftingCheckerStopwatch.start();
-                if (numericResult == RegionResult::AllSat || numericResult == RegionResult::AllViolated) {
-                    applyHintsToExactChecker();
-                }
-                if (numericResult == RegionResult::AllSat) {
-                    if(!exactParameterLiftingChecker->check(region, this->currentCheckTask->getOptimizationDirection())->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
-                        // Numerical result is wrong; Check whether the region is AllViolated!
-                        STORM_LOG_INFO("Numerical result was wrong for one region... Applying exact methods to obtain the actual result...");
-                        ++numOfCorrectedRegions;
-                        if(!exactParameterLiftingChecker->check(region, storm::solver::invert(this->currentCheckTask->getOptimizationDirection()))->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
-                            parameterLiftingCheckerStopwatch.stop();
-                            return RegionResult::AllViolated;
-                        } else {
-                            parameterLiftingCheckerStopwatch.stop();
-                            return RegionResult::Unknown;
-                        }
-                    }
-                } else if (numericResult == RegionResult::AllViolated) {
-                    if(exactParameterLiftingChecker->check(region, storm::solver::invert(this->currentCheckTask->getOptimizationDirection()))->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
-                        // Numerical result is wrong; Check whether the region is AllSat!
-                        STORM_LOG_INFO("Numerical result was wrong for one region... Applying exact methods to obtain the actual result...");
-                        ++numOfCorrectedRegions;
-                        if(exactParameterLiftingChecker->check(region, this->currentCheckTask->getOptimizationDirection())->asExplicitQualitativeCheckResult()[*getConsideredParametricModel().getInitialStates().begin()]) {
-                            parameterLiftingCheckerStopwatch.stop();
-                            return RegionResult::AllSat;
-                        } else {
-                            parameterLiftingCheckerStopwatch.stop();
-                            return RegionResult::Unknown;
-                        }
-                    }
-                }
-                parameterLiftingCheckerStopwatch.stop();
-                return numericResult;
-            }
-*/
-    
             template <typename ParametricType>
             std::unique_ptr<storm::modelchecker::RegionRefinementCheckResult<ParametricType>> RegionModelChecker<ParametricType>::performRegionRefinement(storm::storage::ParameterRegion<ParametricType> const& region, ParametricType const& threshold) {
                 STORM_LOG_INFO("Applying refinement on region: " << region.toString(true) << " .");
diff --git a/src/storm-pars/modelchecker/region/RegionModelChecker.h b/src/storm-pars/modelchecker/region/RegionModelChecker.h
index 746c9b2d3..a8f1fdf01 100644
--- a/src/storm-pars/modelchecker/region/RegionModelChecker.h
+++ b/src/storm-pars/modelchecker/region/RegionModelChecker.h
@@ -7,6 +7,7 @@
 #include "storm-pars/modelchecker/region/RegionResult.h"
 #include "storm-pars/storage/ParameterRegion.h"
 
+#include "storm/models/ModelBase.h"
 #include "storm/modelchecker/CheckTask.h"
 
 namespace storm {
@@ -21,9 +22,8 @@ namespace storm {
             RegionModelChecker();
             virtual ~RegionModelChecker() = default;
             
-            virtual bool canHandle(CheckTask<storm::logic::Formula, ParametricType> const& checkTask) const = 0;
-
-            virtual void specifyFormula(CheckTask<storm::logic::Formula, ParametricType> const& checkTask) = 0;
+            virtual bool canHandle(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, ParametricType> const& checkTask) const = 0;
+            virtual void specify(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, ParametricType> const& checkTask) = 0;
             
             /*!
              * Analyzes the given region.
diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
index bdfd17f84..ff8f29577 100644
--- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
+++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.cpp
@@ -1,5 +1,6 @@
 #include "storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h"
-#include "storm-pars/utility/parameterlifting.h"
+
+#include "storm-pars/transformer/SparseParametricDtmcSimplifier.h"
 
 #include "storm/adapters/RationalFunctionAdapter.h"
 #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
@@ -15,28 +16,59 @@
 #include "storm/exceptions/InvalidArgumentException.h"
 #include "storm/exceptions/InvalidPropertyException.h"
 #include "storm/exceptions/NotSupportedException.h"
+#include "storm/exceptions/UnexpectedException.h"
 
 namespace storm {
     namespace modelchecker {
         
         template <typename SparseModelType, typename ConstantType>
-        SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseDtmcParameterLiftingModelChecker(SparseModelType const& parametricModel) : SparseParameterLiftingModelChecker<SparseModelType, ConstantType>(parametricModel), solverFactory(std::make_unique<storm::solver::GeneralMinMaxLinearEquationSolverFactory<ConstantType>>()) {
+        SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseDtmcParameterLiftingModelChecker() : SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>(std::make_unique<storm::solver::GeneralMinMaxLinearEquationSolverFactory<ConstantType>>()) {
+            // Intentionally left empty
         }
         
         template <typename SparseModelType, typename ConstantType>
-        SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseDtmcParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>>&& solverFactory) : SparseParameterLiftingModelChecker<SparseModelType, ConstantType>(parametricModel), solverFactory(std::move(solverFactory)) {
+        SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseDtmcParameterLiftingModelChecker(std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>>&& solverFactory) : solverFactory(std::move(solverFactory)) {
+            // Intentionally left empty
         }
         
         template <typename SparseModelType, typename ConstantType>
-        bool SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const {
-            bool result = checkTask.getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(true).setCumulativeRewardFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true));
-            if (result) {
-                storm::utility::parameterlifting::validateParameterLiftingSound(this->parametricModel, checkTask.getFormula());
-                STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(this->parametricModel, checkTask.getFormula()), "Could not validate whether parameter lifting is applicable. Please validate manually...");
-            }
+        bool SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::canHandle(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const {
+            bool result = parametricModel->isOfType(storm::models::ModelType::Dtmc);
+            result &= parametricModel->isSparseModel();
+            result &= parametricModel->supportsParameters();
+            auto dtmc = parametricModel->template as<SparseModelType>();
+            result &= static_cast<bool>(dtmc);
+            result &= checkTask.getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(true).setCumulativeRewardFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true));
             return result;
         }
         
+        template <typename SparseModelType, typename ConstantType>
+        void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
+            auto dtmc = parametricModel->template as<SparseModelType>();
+            specify(dtmc, checkTask, false);
+        }
+        
+        template <typename SparseModelType, typename ConstantType>
+        void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool skipModelSimplification) {
+
+            STORM_LOG_ASSERT(this->canHandle(parametricModel, checkTask), "specified model and formula can not be handled by this.");
+         
+            reset();
+            
+            if (skipModelSimplification) {
+                this->parametricModel = parametricModel;
+                this->specifyFormula(checkTask);
+            } else {
+                auto simplifier = storm::transformer::SparseParametricDtmcSimplifier<SparseModelType>(*parametricModel);
+                if (!simplifier.simplify(checkTask.getFormula())) {
+                    STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Simplifying the model was not successfull.");
+                }
+                this->parametricModel = simplifier.getSimplifiedModel();
+                this->specifyFormula(checkTask.substituteFormula(*simplifier.getSimplifiedFormula()));
+            }
+        }
+        
+        
         template <typename SparseModelType, typename ConstantType>
         void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyBoundedUntilFormula(CheckTask<storm::logic::BoundedUntilFormula, ConstantType> const& checkTask) {
             
@@ -53,25 +85,25 @@ namespace storm {
             STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Can not apply parameter lifting on step bounded formula: The step bound has to be positive.");
 
             // get the results for the subformulas
-            storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(this->parametricModel);
+            storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(*this->parametricModel);
             STORM_LOG_THROW(propositionalChecker.canHandle(checkTask.getFormula().getLeftSubformula()) && propositionalChecker.canHandle(checkTask.getFormula().getRightSubformula()), storm::exceptions::NotSupportedException, "Parameter lifting with non-propositional subformulas is not supported");
             storm::storage::BitVector phiStates = std::move(propositionalChecker.check(checkTask.getFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
             storm::storage::BitVector psiStates = std::move(propositionalChecker.check(checkTask.getFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
             
             // get the maybeStates
-            maybeStates = storm::utility::graph::performProbGreater0(this->parametricModel.getBackwardTransitions(), phiStates, psiStates, true, *stepBound);
+            maybeStates = storm::utility::graph::performProbGreater0(this->parametricModel->getBackwardTransitions(), phiStates, psiStates, true, *stepBound);
             maybeStates &= ~psiStates;
             
             // set the result for all non-maybe states
-            resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel.getNumberOfStates(), storm::utility::zero<ConstantType>());
+            resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel->getNumberOfStates(), storm::utility::zero<ConstantType>());
             storm::utility::vector::setVectorValues(resultsForNonMaybeStates, psiStates, storm::utility::one<ConstantType>());
             
             // if there are maybestates, create the parameterLifter
             if (!maybeStates.empty()) {
                 // 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);
+                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);
             }
             
             // We know some bounds for the results so set them
@@ -83,25 +115,25 @@ namespace storm {
         void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyUntilFormula(CheckTask<storm::logic::UntilFormula, ConstantType> const& checkTask) {
             
             // get the results for the subformulas
-            storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(this->parametricModel);
+            storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(*this->parametricModel);
             STORM_LOG_THROW(propositionalChecker.canHandle(checkTask.getFormula().getLeftSubformula()) && propositionalChecker.canHandle(checkTask.getFormula().getRightSubformula()), storm::exceptions::NotSupportedException, "Parameter lifting with non-propositional subformulas is not supported");
             storm::storage::BitVector phiStates = std::move(propositionalChecker.check(checkTask.getFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
             storm::storage::BitVector psiStates = std::move(propositionalChecker.check(checkTask.getFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
             
             // get the maybeStates
-            std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(this->parametricModel.getBackwardTransitions(), phiStates, psiStates);
+            std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::utility::graph::performProb01(this->parametricModel->getBackwardTransitions(), phiStates, psiStates);
             maybeStates = ~(statesWithProbability01.first | statesWithProbability01.second);
             
             // set the result for all non-maybe states
-            resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel.getNumberOfStates(), storm::utility::zero<ConstantType>());
+            resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel->getNumberOfStates(), storm::utility::zero<ConstantType>());
             storm::utility::vector::setVectorValues(resultsForNonMaybeStates, statesWithProbability01.second, storm::utility::one<ConstantType>());
             
             // if there are maybestates, create the parameterLifter
             if (!maybeStates.empty()) {
                 // 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);
+                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);
             }
             
             // We know some bounds for the results so set them
@@ -113,29 +145,29 @@ namespace storm {
         void SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyReachabilityRewardFormula(CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask) {
             
             // get the results for the subformula
-            storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(this->parametricModel);
+            storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(*this->parametricModel);
             STORM_LOG_THROW(propositionalChecker.canHandle(checkTask.getFormula().getSubformula()), storm::exceptions::NotSupportedException, "Parameter lifting with non-propositional subformulas is not supported");
             storm::storage::BitVector targetStates = std::move(propositionalChecker.check(checkTask.getFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
             
             // get the maybeStates
-            storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(this->parametricModel.getBackwardTransitions(), storm::storage::BitVector(this->parametricModel.getNumberOfStates(), true), targetStates);
+            storm::storage::BitVector infinityStates = storm::utility::graph::performProb1(this->parametricModel->getBackwardTransitions(), storm::storage::BitVector(this->parametricModel->getNumberOfStates(), true), targetStates);
             infinityStates.complement();
             maybeStates = ~(targetStates | infinityStates);
             
             // set the result for all the non-maybe states
-            resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel.getNumberOfStates(), storm::utility::zero<ConstantType>());
+            resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel->getNumberOfStates(), storm::utility::zero<ConstantType>());
             storm::utility::vector::setVectorValues(resultsForNonMaybeStates, infinityStates, storm::utility::infinity<ConstantType>());
             
             // if there are maybestates, create the parameterLifter
             if (!maybeStates.empty()) {
                 // Create the reward vector
-                STORM_LOG_THROW((checkTask.isRewardModelSet() && this->parametricModel.hasRewardModel(checkTask.getRewardModel())) || (!checkTask.isRewardModelSet() && this->parametricModel.hasUniqueRewardModel()), storm::exceptions::InvalidPropertyException, "The reward model specified by the CheckTask is not available in the given model.");
+                STORM_LOG_THROW((checkTask.isRewardModelSet() && this->parametricModel->hasRewardModel(checkTask.getRewardModel())) || (!checkTask.isRewardModelSet() && this->parametricModel->hasUniqueRewardModel()), storm::exceptions::InvalidPropertyException, "The reward model specified by the CheckTask is not available in the given model.");
 
-                typename SparseModelType::RewardModelType const& rewardModel = checkTask.isRewardModelSet() ? this->parametricModel.getRewardModel(checkTask.getRewardModel()) : this->parametricModel.getUniqueRewardModel();
+                typename SparseModelType::RewardModelType const& rewardModel = checkTask.isRewardModelSet() ? this->parametricModel->getRewardModel(checkTask.getRewardModel()) : this->parametricModel->getUniqueRewardModel();
 
-                std::vector<typename SparseModelType::ValueType> b = rewardModel.getTotalRewardVector(this->parametricModel.getTransitionMatrix());
+                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);
             }
             
             // We only know a lower bound for the result
@@ -155,15 +187,15 @@ namespace storm {
             STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Can not apply parameter lifting on step bounded formula: The step bound has to be positive.");
             
             //Every state is a maybeState
-            maybeStates = storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getColumnCount(), true);
-            resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel.getNumberOfStates());
+            maybeStates = storm::storage::BitVector(this->parametricModel->getTransitionMatrix().getColumnCount(), true);
+            resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel->getNumberOfStates());
             
             // Create the reward vector
-            STORM_LOG_THROW((checkTask.isRewardModelSet() && this->parametricModel.hasRewardModel(checkTask.getRewardModel())) || (!checkTask.isRewardModelSet() && this->parametricModel.hasUniqueRewardModel()), storm::exceptions::InvalidPropertyException, "The reward model specified by the CheckTask is not available in the given model.");
-            typename SparseModelType::RewardModelType const& rewardModel = checkTask.isRewardModelSet() ? this->parametricModel.getRewardModel(checkTask.getRewardModel()) : this->parametricModel.getUniqueRewardModel();
-            std::vector<typename SparseModelType::ValueType> b = rewardModel.getTotalRewardVector(this->parametricModel.getTransitionMatrix());
+            STORM_LOG_THROW((checkTask.isRewardModelSet() && this->parametricModel->hasRewardModel(checkTask.getRewardModel())) || (!checkTask.isRewardModelSet() && this->parametricModel->hasUniqueRewardModel()), storm::exceptions::InvalidPropertyException, "The reward model specified by the CheckTask is not available in the given model.");
+            typename SparseModelType::RewardModelType const& rewardModel = checkTask.isRewardModelSet() ? this->parametricModel->getRewardModel(checkTask.getRewardModel()) : this->parametricModel->getUniqueRewardModel();
+            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);
             
             
             // We only know a lower bound for the result
@@ -173,7 +205,7 @@ namespace storm {
         template <typename SparseModelType, typename ConstantType>
         storm::modelchecker::SparseInstantiationModelChecker<SparseModelType, ConstantType>& SparseDtmcParameterLiftingModelChecker<SparseModelType, ConstantType>::getInstantiationChecker() {
             if (!instantiationChecker) {
-                instantiationChecker = std::make_unique<storm::modelchecker::SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>>(this->parametricModel);
+                instantiationChecker = std::make_unique<storm::modelchecker::SparseDtmcInstantiationModelChecker<SparseModelType, ConstantType>>(*this->parametricModel);
                 instantiationChecker->specifyFormula(this->currentCheckTask->template convertValueType<typename SparseModelType::ValueType>());
             }
             return *instantiationChecker;
@@ -205,7 +237,7 @@ namespace storm {
             if (this->currentCheckTask->isBoundSet() && solver->hasSchedulerHint()) {
                 // If we reach this point, we know that after applying the hint, the x-values can only become larger (if we maximize) or smaller (if we minimize).
                 std::unique_ptr<storm::solver::TerminationCondition<ConstantType>> termCond;
-                storm::storage::BitVector relevantStatesInSubsystem = this->currentCheckTask->isOnlyInitialStatesRelevantSet() ? this->parametricModel.getInitialStates() % maybeStates : storm::storage::BitVector(maybeStates.getNumberOfSetBits(), true);
+                storm::storage::BitVector relevantStatesInSubsystem = this->currentCheckTask->isOnlyInitialStatesRelevantSet() ? this->parametricModel->getInitialStates() % maybeStates : storm::storage::BitVector(maybeStates.getNumberOfSetBits(), true);
                 if (storm::solver::minimize(dirForParameters)) {
                     // Terminate if the value for ALL relevant states is already below the threshold
                     termCond = std::make_unique<storm::solver::TerminateIfFilteredExtremumBelowThreshold<ConstantType>> (relevantStatesInSubsystem, this->currentCheckTask->getBoundThreshold(), true, false);
diff --git a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h
index 8831bbe6b..d6f51032b 100644
--- a/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h
+++ b/src/storm-pars/modelchecker/region/SparseDtmcParameterLiftingModelChecker.h
@@ -19,11 +19,14 @@ namespace storm {
         template <typename SparseModelType, typename ConstantType>
         class SparseDtmcParameterLiftingModelChecker : public SparseParameterLiftingModelChecker<SparseModelType, ConstantType> {
         public:
-            SparseDtmcParameterLiftingModelChecker(SparseModelType const& parametricModel);
-            SparseDtmcParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>>&& solverFactory);
-                
-            virtual bool canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const override;
-                
+            SparseDtmcParameterLiftingModelChecker();
+            SparseDtmcParameterLiftingModelChecker(std::unique_ptr<storm::solver::MinMaxLinearEquationSolverFactory<ConstantType>>&& solverFactory);
+            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(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) override;
+            void specify(std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool skipModelSimplification);
+            
             boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMinScheduler();
             boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMaxScheduler();
 
diff --git a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp
index f2c6bb21b..32f8ca809 100644
--- a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp
+++ b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.cpp
@@ -1,5 +1,6 @@
 #include "storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h"
 #include "storm-pars/utility/parameterlifting.h"
+#include "storm-pars/transformer/SparseParametricMdpSimplifier.h"
 
 #include "storm/adapters/RationalFunctionAdapter.h"
 #include "storm/modelchecker/propositional/SparsePropositionalModelChecker.h"
@@ -16,25 +17,57 @@
 #include "storm/exceptions/InvalidArgumentException.h"
 #include "storm/exceptions/InvalidPropertyException.h"
 #include "storm/exceptions/NotSupportedException.h"
+#include "storm/exceptions/UnexpectedException.h"
 
 namespace storm {
     namespace modelchecker {
+        
+        
         template <typename SparseModelType, typename ConstantType>
-        SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel) : SparseParameterLiftingModelChecker<SparseModelType, ConstantType>(parametricModel), solverFactory(std::make_unique<storm::solver::GameSolverFactory<ConstantType>>()) {
+        SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseMdpParameterLiftingModelChecker() : SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>(std::make_unique<storm::solver::GameSolverFactory<ConstantType>>()) {
+            // Intentionally left empty
         }
         
         template <typename SparseModelType, typename ConstantType>
-        SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr<storm::solver::GameSolverFactory<ConstantType>>&& solverFactory) : SparseParameterLiftingModelChecker<SparseModelType, ConstantType>(parametricModel), solverFactory(std::move(solverFactory)) {
+        SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseMdpParameterLiftingModelChecker(std::unique_ptr<storm::solver::GameSolverFactory<ConstantType>>&& solverFactory) : solverFactory(std::move(solverFactory)) {
+            // Intentionally left empty
         }
-
+        
         template <typename SparseModelType, typename ConstantType>
-        bool SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const {
-            bool result = checkTask.getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setCumulativeRewardFormulasAllowed(true));
-            if (result) {
-                STORM_LOG_WARN_COND(storm::utility::parameterlifting::validateParameterLiftingSound(this->parametricModel, checkTask.getFormula()), "Could not validate whether parameter lifting is applicable. Please validate manually...");
-            }
+        bool SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::canHandle(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const {
+            bool result = parametricModel->isOfType(storm::models::ModelType::Mdp);
+            result &= parametricModel->isSparseModel();
+            result &= parametricModel->supportsParameters();
+            auto mdp = parametricModel->template as<SparseModelType>();
+            result &= static_cast<bool>(mdp);
+            result &= checkTask.getFormula().isInFragment(storm::logic::reachability().setRewardOperatorsAllowed(true).setReachabilityRewardFormulasAllowed(true).setBoundedUntilFormulasAllowed(true).setCumulativeRewardFormulasAllowed(true).setStepBoundedUntilFormulasAllowed(true).setTimeBoundedUntilFormulasAllowed(true));
             return result;
+        }
+        
+        template <typename SparseModelType, typename ConstantType>
+        void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
+            auto mdp = parametricModel->template as<SparseModelType>();
+            specify(mdp, checkTask, false);
+        }
+        
+        template <typename SparseModelType, typename ConstantType>
+        void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specify(std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool skipModelSimplification) {
 
+            STORM_LOG_ASSERT(this->canHandle(parametricModel, checkTask), "specified model and formula can not be handled by this.");
+         
+            reset();
+            
+            if (skipModelSimplification) {
+                this->parametricModel = parametricModel;
+                this->specifyFormula(checkTask);
+            } else {
+                auto simplifier = storm::transformer::SparseParametricMdpSimplifier<SparseModelType>(*parametricModel);
+                if (!simplifier.simplify(checkTask.getFormula())) {
+                    STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Simplifying the model was not successfull.");
+                }
+                this->parametricModel = simplifier.getSimplifiedModel();
+                this->specifyFormula(checkTask.substituteFormula(*simplifier.getSimplifiedFormula()));
+            }
         }
         
         template <typename SparseModelType, typename ConstantType>
@@ -53,27 +86,27 @@ namespace storm {
             STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Can not apply parameter lifting on step bounded formula: The step bound has to be positive.");
 
             // get the results for the subformulas
-            storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(this->parametricModel);
+            storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(*this->parametricModel);
             STORM_LOG_THROW(propositionalChecker.canHandle(checkTask.getFormula().getLeftSubformula()) && propositionalChecker.canHandle(checkTask.getFormula().getRightSubformula()), storm::exceptions::NotSupportedException, "Parameter lifting with non-propositional subformulas is not supported");
             storm::storage::BitVector phiStates = std::move(propositionalChecker.check(checkTask.getFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
             storm::storage::BitVector psiStates = std::move(propositionalChecker.check(checkTask.getFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
             
             // get the maybeStates
             maybeStates = storm::solver::minimize(checkTask.getOptimizationDirection()) ?
-                          storm::utility::graph::performProbGreater0A(this->parametricModel.getTransitionMatrix(), this->parametricModel.getTransitionMatrix().getRowGroupIndices(), this->parametricModel.getBackwardTransitions(), phiStates, psiStates, true, *stepBound) :
-                          storm::utility::graph::performProbGreater0E(this->parametricModel.getBackwardTransitions(), phiStates, psiStates, true, *stepBound);
+                          storm::utility::graph::performProbGreater0A(this->parametricModel->getTransitionMatrix(), this->parametricModel->getTransitionMatrix().getRowGroupIndices(), this->parametricModel->getBackwardTransitions(), phiStates, psiStates, true, *stepBound) :
+                          storm::utility::graph::performProbGreater0E(this->parametricModel->getBackwardTransitions(), phiStates, psiStates, true, *stepBound);
             maybeStates &= ~psiStates;
             
             // set the result for all non-maybe states
-            resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel.getNumberOfStates(), storm::utility::zero<ConstantType>());
+            resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel->getNumberOfStates(), storm::utility::zero<ConstantType>());
             storm::utility::vector::setVectorValues(resultsForNonMaybeStates, psiStates, storm::utility::one<ConstantType>());
             
             // if there are maybestates, create the parameterLifter
             if (!maybeStates.empty()) {
                 // 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);
+                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, this->parametricModel.getTransitionMatrix().getRowFilter(maybeStates), maybeStates);
+                parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel->getTransitionMatrix(), b, this->parametricModel->getTransitionMatrix().getRowFilter(maybeStates), maybeStates);
                 computePlayer1Matrix();
                 
                 applyPreviousResultAsHint = false;
@@ -88,32 +121,32 @@ namespace storm {
         void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyUntilFormula(CheckTask<storm::logic::UntilFormula, ConstantType> const& checkTask) {
             
             // get the results for the subformulas
-            storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(this->parametricModel);
+            storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(*this->parametricModel);
             STORM_LOG_THROW(propositionalChecker.canHandle(checkTask.getFormula().getLeftSubformula()) && propositionalChecker.canHandle(checkTask.getFormula().getRightSubformula()), storm::exceptions::NotSupportedException, "Parameter lifting with non-propositional subformulas is not supported");
             storm::storage::BitVector phiStates = std::move(propositionalChecker.check(checkTask.getFormula().getLeftSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
             storm::storage::BitVector psiStates = std::move(propositionalChecker.check(checkTask.getFormula().getRightSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
             
             // get the maybeStates
             std::pair<storm::storage::BitVector, storm::storage::BitVector> statesWithProbability01 = storm::solver::minimize(checkTask.getOptimizationDirection()) ?
-                                                                                                      storm::utility::graph::performProb01Min(this->parametricModel.getTransitionMatrix(), this->parametricModel.getTransitionMatrix().getRowGroupIndices(), this->parametricModel.getBackwardTransitions(), phiStates, psiStates) :
-                                                                                                      storm::utility::graph::performProb01Max(this->parametricModel.getTransitionMatrix(), this->parametricModel.getTransitionMatrix().getRowGroupIndices(), this->parametricModel.getBackwardTransitions(), phiStates, psiStates);
+                                                                                                      storm::utility::graph::performProb01Min(this->parametricModel->getTransitionMatrix(), this->parametricModel->getTransitionMatrix().getRowGroupIndices(), this->parametricModel->getBackwardTransitions(), phiStates, psiStates) :
+                                                                                                      storm::utility::graph::performProb01Max(this->parametricModel->getTransitionMatrix(), this->parametricModel->getTransitionMatrix().getRowGroupIndices(), this->parametricModel->getBackwardTransitions(), phiStates, psiStates);
             maybeStates = ~(statesWithProbability01.first | statesWithProbability01.second);
             
             // set the result for all non-maybe states
-            resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel.getNumberOfStates(), storm::utility::zero<ConstantType>());
+            resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel->getNumberOfStates(), storm::utility::zero<ConstantType>());
             storm::utility::vector::setVectorValues(resultsForNonMaybeStates, statesWithProbability01.second, storm::utility::one<ConstantType>());
             
             // if there are maybestates, create the parameterLifter
             if (!maybeStates.empty()) {
                 // 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), statesWithProbability01.second);
+                std::vector<typename SparseModelType::ValueType> b = this->parametricModel->getTransitionMatrix().getConstrainedRowSumVector(storm::storage::BitVector(this->parametricModel->getTransitionMatrix().getRowCount(), true), statesWithProbability01.second);
                 
-                parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel.getTransitionMatrix(), b, this->parametricModel.getTransitionMatrix().getRowFilter(maybeStates), maybeStates);
+                parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel->getTransitionMatrix(), b, this->parametricModel->getTransitionMatrix().getRowFilter(maybeStates), maybeStates);
                 computePlayer1Matrix();
                 
                 // Check whether there is an EC consisting of maybestates
                 applyPreviousResultAsHint = storm::solver::minimize(checkTask.getOptimizationDirection()) || // when minimizing, there can not be an EC within the maybestates
-                                            storm::utility::graph::performProb1A(this->parametricModel.getTransitionMatrix(), this->parametricModel.getTransitionMatrix().getRowGroupIndices(), this->parametricModel.getBackwardTransitions(), maybeStates, ~maybeStates).full();
+                                            storm::utility::graph::performProb1A(this->parametricModel->getTransitionMatrix(), this->parametricModel->getTransitionMatrix().getRowGroupIndices(), this->parametricModel->getBackwardTransitions(), maybeStates, ~maybeStates).full();
             }
             
             // We know some bounds for the results
@@ -125,40 +158,40 @@ namespace storm {
         void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyReachabilityRewardFormula(CheckTask<storm::logic::EventuallyFormula, ConstantType> const& checkTask) {
             
             // get the results for the subformula
-            storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(this->parametricModel);
+            storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> propositionalChecker(*this->parametricModel);
             STORM_LOG_THROW(propositionalChecker.canHandle(checkTask.getFormula().getSubformula()), storm::exceptions::NotSupportedException, "Parameter lifting with non-propositional subformulas is not supported");
             storm::storage::BitVector targetStates = std::move(propositionalChecker.check(checkTask.getFormula().getSubformula())->asExplicitQualitativeCheckResult().getTruthValuesVector());
             
             // get the maybeStates
             storm::storage::BitVector infinityStates = storm::solver::minimize(checkTask.getOptimizationDirection()) ?
-                                                       storm::utility::graph::performProb1E(this->parametricModel.getTransitionMatrix(), this->parametricModel.getTransitionMatrix().getRowGroupIndices(), this->parametricModel.getBackwardTransitions(), storm::storage::BitVector(this->parametricModel.getNumberOfStates(), true), targetStates) :
-                                                       storm::utility::graph::performProb1A(this->parametricModel.getTransitionMatrix(), this->parametricModel.getTransitionMatrix().getRowGroupIndices(), this->parametricModel.getBackwardTransitions(), storm::storage::BitVector(this->parametricModel.getNumberOfStates(), true), targetStates);
+                                                       storm::utility::graph::performProb1E(this->parametricModel->getTransitionMatrix(), this->parametricModel->getTransitionMatrix().getRowGroupIndices(), this->parametricModel->getBackwardTransitions(), storm::storage::BitVector(this->parametricModel->getNumberOfStates(), true), targetStates) :
+                                                       storm::utility::graph::performProb1A(this->parametricModel->getTransitionMatrix(), this->parametricModel->getTransitionMatrix().getRowGroupIndices(), this->parametricModel->getBackwardTransitions(), storm::storage::BitVector(this->parametricModel->getNumberOfStates(), true), targetStates);
             infinityStates.complement();
             maybeStates = ~(targetStates | infinityStates);
             
             // set the result for all the non-maybe states
-            resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel.getNumberOfStates(), storm::utility::zero<ConstantType>());
+            resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel->getNumberOfStates(), storm::utility::zero<ConstantType>());
             storm::utility::vector::setVectorValues(resultsForNonMaybeStates, infinityStates, storm::utility::infinity<ConstantType>());
             
             // if there are maybestates, create the parameterLifter
             if (!maybeStates.empty()) {
                 // Create the reward vector
-                STORM_LOG_THROW((checkTask.isRewardModelSet() && this->parametricModel.hasRewardModel(checkTask.getRewardModel())) || (!checkTask.isRewardModelSet() && this->parametricModel.hasUniqueRewardModel()), storm::exceptions::InvalidPropertyException, "The reward model specified by the CheckTask is not available in the given model.");
+                STORM_LOG_THROW((checkTask.isRewardModelSet() && this->parametricModel->hasRewardModel(checkTask.getRewardModel())) || (!checkTask.isRewardModelSet() && this->parametricModel->hasUniqueRewardModel()), storm::exceptions::InvalidPropertyException, "The reward model specified by the CheckTask is not available in the given model.");
 
-                typename SparseModelType::RewardModelType const& rewardModel = checkTask.isRewardModelSet() ? this->parametricModel.getRewardModel(checkTask.getRewardModel()) : this->parametricModel.getUniqueRewardModel();
+                typename SparseModelType::RewardModelType const& rewardModel = checkTask.isRewardModelSet() ? this->parametricModel->getRewardModel(checkTask.getRewardModel()) : this->parametricModel->getUniqueRewardModel();
 
-                std::vector<typename SparseModelType::ValueType> b = rewardModel.getTotalRewardVector(this->parametricModel.getTransitionMatrix());
+                std::vector<typename SparseModelType::ValueType> b = rewardModel.getTotalRewardVector(this->parametricModel->getTransitionMatrix());
                 
                 // We need to handle choices that lead to an infinity state.
                 // As a maybeState does not have reward infinity, a choice leading to an infinity state will never be picked. Hence, we can unselect the corresponding rows
-                storm::storage::BitVector selectedRows = this->parametricModel.getTransitionMatrix().getRowFilter(maybeStates, ~infinityStates);
+                storm::storage::BitVector selectedRows = this->parametricModel->getTransitionMatrix().getRowFilter(maybeStates, ~infinityStates);
                 
-                parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel.getTransitionMatrix(), b, selectedRows, maybeStates);
+                parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel->getTransitionMatrix(), b, selectedRows, maybeStates);
                 computePlayer1Matrix();
                 
                 // Check whether there is an EC consisting of maybestates
                 applyPreviousResultAsHint = !storm::solver::minimize(checkTask.getOptimizationDirection()) || // when maximizing, there can not be an EC within the maybestates
-                                            storm::utility::graph::performProb1A(this->parametricModel.getTransitionMatrix(), this->parametricModel.getTransitionMatrix().getRowGroupIndices(), this->parametricModel.getBackwardTransitions(), maybeStates, ~maybeStates).full();
+                                            storm::utility::graph::performProb1A(this->parametricModel->getTransitionMatrix(), this->parametricModel->getTransitionMatrix().getRowGroupIndices(), this->parametricModel->getBackwardTransitions(), maybeStates, ~maybeStates).full();
             }
             
             // We only know a lower bound for the result
@@ -178,15 +211,15 @@ namespace storm {
             STORM_LOG_THROW(*stepBound > 0, storm::exceptions::NotSupportedException, "Can not apply parameter lifting on step bounded formula: The step bound has to be positive.");
             
             //Every state is a maybeState
-            maybeStates = storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getColumnCount(), true);
-            resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel.getNumberOfStates());
+            maybeStates = storm::storage::BitVector(this->parametricModel->getTransitionMatrix().getColumnCount(), true);
+            resultsForNonMaybeStates = std::vector<ConstantType>(this->parametricModel->getNumberOfStates());
 
             // Create the reward vector
-            STORM_LOG_THROW((checkTask.isRewardModelSet() && this->parametricModel.hasRewardModel(checkTask.getRewardModel())) || (!checkTask.isRewardModelSet() && this->parametricModel.hasUniqueRewardModel()), storm::exceptions::InvalidPropertyException, "The reward model specified by the CheckTask is not available in the given model.");
-            typename SparseModelType::RewardModelType const& rewardModel = checkTask.isRewardModelSet() ? this->parametricModel.getRewardModel(checkTask.getRewardModel()) : this->parametricModel.getUniqueRewardModel();
-            std::vector<typename SparseModelType::ValueType> b = rewardModel.getTotalRewardVector(this->parametricModel.getTransitionMatrix());
+            STORM_LOG_THROW((checkTask.isRewardModelSet() && this->parametricModel->hasRewardModel(checkTask.getRewardModel())) || (!checkTask.isRewardModelSet() && this->parametricModel->hasUniqueRewardModel()), storm::exceptions::InvalidPropertyException, "The reward model specified by the CheckTask is not available in the given model.");
+            typename SparseModelType::RewardModelType const& rewardModel = checkTask.isRewardModelSet() ? this->parametricModel->getRewardModel(checkTask.getRewardModel()) : this->parametricModel->getUniqueRewardModel();
+            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, storm::storage::BitVector(this->parametricModel.getTransitionMatrix().getRowCount(), true), maybeStates);
+            parameterLifter = std::make_unique<storm::transformer::ParameterLifter<typename SparseModelType::ValueType, ConstantType>>(this->parametricModel->getTransitionMatrix(), b, storm::storage::BitVector(this->parametricModel->getTransitionMatrix().getRowCount(), true), maybeStates);
             computePlayer1Matrix();
 
             applyPreviousResultAsHint = false;
@@ -198,7 +231,7 @@ namespace storm {
         template <typename SparseModelType, typename ConstantType>
         storm::modelchecker::SparseInstantiationModelChecker<SparseModelType, ConstantType>& SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::getInstantiationChecker() {
             if (!instantiationChecker) {
-                instantiationChecker = std::make_unique<storm::modelchecker::SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>>(this->parametricModel);
+                instantiationChecker = std::make_unique<storm::modelchecker::SparseMdpInstantiationModelChecker<SparseModelType, ConstantType>>(*this->parametricModel);
                 instantiationChecker->specifyFormula(this->currentCheckTask->template convertValueType<typename SparseModelType::ValueType>());
             }
             return *instantiationChecker;
@@ -235,7 +268,7 @@ namespace storm {
             if (this->currentCheckTask->isBoundSet() && this->currentCheckTask->getOptimizationDirection() == dirForParameters && solver->hasSchedulerHints()) {
                 // If we reach this point, we know that after applying the hints, the x-values can only become larger (if we maximize) or smaller (if we minimize).
                 std::unique_ptr<storm::solver::TerminationCondition<ConstantType>> termCond;
-                storm::storage::BitVector relevantStatesInSubsystem = this->currentCheckTask->isOnlyInitialStatesRelevantSet() ? this->parametricModel.getInitialStates() % maybeStates : storm::storage::BitVector(maybeStates.getNumberOfSetBits(), true);
+                storm::storage::BitVector relevantStatesInSubsystem = this->currentCheckTask->isOnlyInitialStatesRelevantSet() ? this->parametricModel->getInitialStates() % maybeStates : storm::storage::BitVector(maybeStates.getNumberOfSetBits(), true);
                 if (storm::solver::minimize(dirForParameters)) {
                     // Terminate if the value for ALL relevant states is already below the threshold
                     termCond = std::make_unique<storm::solver::TerminateIfFilteredExtremumBelowThreshold<ConstantType>> (relevantStatesInSubsystem, this->currentCheckTask->getBoundThreshold(), true, false);
@@ -276,14 +309,14 @@ namespace storm {
         void SparseMdpParameterLiftingModelChecker<SparseModelType, ConstantType>::computePlayer1Matrix() {
             uint_fast64_t n = 0;
             for(auto const& maybeState : maybeStates) {
-                n += this->parametricModel.getTransitionMatrix().getRowGroupSize(maybeState);
+                n += this->parametricModel->getTransitionMatrix().getRowGroupSize(maybeState);
             }
             // The player 1 matrix is the identity matrix of size n with the row groups as given by the original matrix
             storm::storage::SparseMatrixBuilder<storm::storage::sparse::state_type> matrixBuilder(n, n, n, true, true, maybeStates.getNumberOfSetBits());
             uint_fast64_t p1MatrixRow = 0;
             for (auto maybeState : maybeStates){
                 matrixBuilder.newRowGroup(p1MatrixRow);
-                for (uint_fast64_t row = this->parametricModel.getTransitionMatrix().getRowGroupIndices()[maybeState]; row < this->parametricModel.getTransitionMatrix().getRowGroupIndices()[maybeState + 1]; ++row){
+                for (uint_fast64_t row = this->parametricModel->getTransitionMatrix().getRowGroupIndices()[maybeState]; row < this->parametricModel->getTransitionMatrix().getRowGroupIndices()[maybeState + 1]; ++row){
                     matrixBuilder.addNextValue(p1MatrixRow, p1MatrixRow, storm::utility::one<storm::storage::sparse::state_type>());
                     ++p1MatrixRow;
                 }
diff --git a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h
index 55504bd9e..b08d71da2 100644
--- a/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h
+++ b/src/storm-pars/modelchecker/region/SparseMdpParameterLiftingModelChecker.h
@@ -20,11 +20,14 @@ namespace storm {
         template <typename SparseModelType, typename ConstantType>
         class SparseMdpParameterLiftingModelChecker : public SparseParameterLiftingModelChecker<SparseModelType, ConstantType> {
         public:
-            SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel);
-            SparseMdpParameterLiftingModelChecker(SparseModelType const& parametricModel, std::unique_ptr<storm::solver::GameSolverFactory<ConstantType>>&& solverFactory);
-                
-            virtual bool canHandle(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) const override;
-                
+            SparseMdpParameterLiftingModelChecker();
+            SparseMdpParameterLiftingModelChecker(std::unique_ptr<storm::solver::GameSolverFactory<ConstantType>>&& solverFactory);
+            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(std::shared_ptr<storm::models::ModelBase> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) override;
+            void specify(std::shared_ptr<SparseModelType> parametricModel, CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask, bool skipModelSimplification);
+
             boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMinScheduler();
             boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentMaxScheduler();
             boost::optional<storm::storage::Scheduler<ConstantType>> getCurrentPlayer1Scheduler();
diff --git a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp
index 544dd734d..95886ffbd 100644
--- a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp
+++ b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.cpp
@@ -1,4 +1,4 @@
-#include "SparseParameterLiftingModelChecker.h"
+#include "storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h"
 
 #include "storm/adapters/RationalFunctionAdapter.h"
 #include "storm/logic/FragmentSpecification.h"
@@ -15,14 +15,13 @@ namespace storm {
     namespace modelchecker {
         
         template <typename SparseModelType, typename ConstantType>
-        SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseParameterLiftingModelChecker(SparseModelType const& parametricModel) : parametricModel(parametricModel) {
+        SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::SparseParameterLiftingModelChecker() {
             //Intentionally left empty
         }
         
         template <typename SparseModelType, typename ConstantType>
         void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyFormula(storm::modelchecker::CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) {
-            STORM_LOG_ASSERT(this->canHandle(checkTask), "specified formula can not be handled by this.");
-            reset();
+
             currentFormula = checkTask.getFormula().asSharedPointer();
             currentCheckTask = std::make_unique<storm::modelchecker::CheckTask<storm::logic::Formula, ConstantType>>(checkTask.substituteFormula(*currentFormula).template convertValueType<ConstantType>());
             
@@ -52,49 +51,74 @@ namespace storm {
         
             STORM_LOG_THROW(this->currentCheckTask->isOnlyInitialStatesRelevantSet(), storm::exceptions::NotSupportedException, "Analyzing regions with parameter lifting requires a property where only the value in the initial states is relevant.");
             STORM_LOG_THROW(this->currentCheckTask->isBoundSet(), storm::exceptions::NotSupportedException, "Analyzing regions with parameter lifting requires a bounded property.");
-            STORM_LOG_THROW(this->parametricModel.getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "Analyzing regions with parameter lifting requires a model with a single initial state.");
+            STORM_LOG_THROW(this->parametricModel->getInitialStates().getNumberOfSetBits() == 1, storm::exceptions::NotSupportedException, "Analyzing regions with parameter lifting requires a model with a single initial state.");
             
             RegionResult result = initialResult;
 
             // Check if we need to check the formula on one point to decide whether to show AllSat or AllViolated
             if (result == RegionResult::Unknown) {
-                 result = getInstantiationChecker().check(region.getCenterPoint())->asExplicitQualitativeCheckResult()[*this->parametricModel.getInitialStates().begin()] ? RegionResult::CenterSat : RegionResult::CenterViolated;
+                 result = getInstantiationChecker().check(region.getCenterPoint())->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()] ? RegionResult::CenterSat : RegionResult::CenterViolated;
             }
             
             // try to prove AllSat or AllViolated, depending on the obtained result
             if (result == RegionResult::ExistsSat || result == RegionResult::CenterSat) {
                 // show AllSat:
                 storm::solver::OptimizationDirection parameterOptimizationDirection = isLowerBound(this->currentCheckTask->getBound().comparisonType) ? storm::solver::OptimizationDirection::Minimize : storm::solver::OptimizationDirection::Maximize;
-                if (this->check(region, parameterOptimizationDirection)->asExplicitQualitativeCheckResult()[*this->parametricModel.getInitialStates().begin()]) {
+                if (this->check(region, parameterOptimizationDirection)->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()]) {
                     result = RegionResult::AllSat;
                 } else if (sampleVerticesOfRegion) {
-                    // Check if there is a point in the region for which the property is violated
-                    auto vertices = region.getVerticesOfRegion(region.getVariables());
-                    for (auto const& v : vertices) {
-                        if (!getInstantiationChecker().check(v)->asExplicitQualitativeCheckResult()[*this->parametricModel.getInitialStates().begin()]) {
-                            result = RegionResult::ExistsBoth;
-                        }
-                    }
+                    result = sampleVertices(region, result);
                 }
             } else if (result == RegionResult::ExistsViolated || result == RegionResult::CenterViolated) {
                 // show AllViolated:
                 storm::solver::OptimizationDirection parameterOptimizationDirection = isLowerBound(this->currentCheckTask->getBound().comparisonType) ? storm::solver::OptimizationDirection::Maximize : storm::solver::OptimizationDirection::Minimize;
-                if (!this->check(region, parameterOptimizationDirection)->asExplicitQualitativeCheckResult()[*this->parametricModel.getInitialStates().begin()]) {
+                if (!this->check(region, parameterOptimizationDirection)->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()]) {
                     result = RegionResult::AllViolated;
                 } else if (sampleVerticesOfRegion) {
-                    // Check if there is a point in the region for which the property is satisfied
-                    auto vertices = region.getVerticesOfRegion(region.getVariables());
-                    for (auto const& v : vertices) {
-                        if (getInstantiationChecker().check(v)->asExplicitQualitativeCheckResult()[*this->parametricModel.getInitialStates().begin()]) {
-                            result = RegionResult::ExistsBoth;
-                        }
-                    }
+                    result = sampleVertices(region, result);
                 }
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "When analyzing a region, an invalid initial result was given: " << initialResult);
             }
             return result;
         }
+        
+        template <typename SparseModelType, typename ConstantType>
+        RegionResult SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::sampleVertices(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResult const& initialResult) {
+            RegionResult result = initialResult;
+            
+            if (result == RegionResult::AllSat || result == RegionResult::AllViolated) {
+                return result;
+            }
+            
+            bool hasSatPoint = result == RegionResult::ExistsViolated || result == RegionResult::CenterViolated;
+            bool hasViolatedPoint = result == RegionResult::ExistsSat || result == RegionResult::CenterSat;
+            
+            // Check if there is a point in the region for which the property is satisfied
+            auto vertices = region.getVerticesOfRegion(region.getVariables());
+            auto vertexIt = vertices.begin();
+            while (vertexIt != vertices.end() && !(hasSatPoint && hasViolatedPoint)) {
+                if (getInstantiationChecker().check(*vertexIt)->asExplicitQualitativeCheckResult()[*this->parametricModel->getInitialStates().begin()]) {
+                    hasSatPoint = true;
+                } else {
+                    hasViolatedPoint = true;
+                }
+                ++vertexIt;
+            }
+            
+            if (hasSatPoint) {
+                if (hasViolatedPoint) {
+                    result = RegionResult::ExistsBoth;
+                } else if (result != RegionResult::CenterSat) {
+                    result = RegionResult::ExistsSat;
+                }
+            } else if (hasViolatedPoint && result != RegionResult::CenterViolated) {
+                result = RegionResult::ExistsViolated;
+            }
+            
+            return result;
+        }
+
 
         template <typename SparseModelType, typename ConstantType>
         std::unique_ptr<CheckResult> SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::check(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) {
@@ -105,6 +129,16 @@ namespace storm {
                 return quantitativeResult->template asExplicitQuantitativeCheckResult<ConstantType>().compareAgainstBound(this->currentCheckTask->getFormula().asOperatorFormula().getComparisonType(), this->currentCheckTask->getFormula().asOperatorFormula().template getThresholdAs<ConstantType>());
             }
         }
+        
+        template <typename SparseModelType, typename ConstantType>
+        SparseModelType const& SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::getConsideredParametricModel() const {
+            return *parametricModel;
+        }
+        
+        template <typename SparseModelType, typename ConstantType>
+        CheckTask<storm::logic::Formula, ConstantType> const& SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::getCurrentCheckTask() const {
+            return *currentCheckTask;
+        }
 
         template <typename SparseModelType, typename ConstantType>
         void SparseParameterLiftingModelChecker<SparseModelType, ConstantType>::specifyBoundedUntilFormula(CheckTask<logic::BoundedUntilFormula, ConstantType> const& checkTask) {
diff --git a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h
index ea53dd803..b8abd518c 100644
--- a/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h
+++ b/src/storm-pars/modelchecker/region/SparseParameterLiftingModelChecker.h
@@ -22,10 +22,9 @@ namespace storm {
         template <typename SparseModelType, typename ConstantType>
         class SparseParameterLiftingModelChecker : public RegionModelChecker<typename SparseModelType::ValueType> {
         public:
-            SparseParameterLiftingModelChecker(SparseModelType const& parametricModel);
+            SparseParameterLiftingModelChecker();
             virtual ~SparseParameterLiftingModelChecker() = default;
             
-            virtual void specifyFormula(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask) override;
 
             /*!
              * Analyzes the given region by means of parameter lifting.
@@ -36,6 +35,11 @@ namespace storm {
              */
             virtual RegionResult analyzeRegion(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResult const& initialResult = RegionResult::Unknown, bool sampleVerticesOfRegion = false) override;
 
+            /*!
+             * Analyzes the 2^#parameters corner points of the given region.
+             */
+            RegionResult sampleVertices(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, RegionResult const& initialResult = RegionResult::Unknown);
+            
             /*!
              * Checks the specified formula on the given region by applying parameter lifting (Parameter choices are lifted to nondeterministic choices)
              * This yields a (sound) approximative model checking result.
@@ -45,7 +49,12 @@ namespace storm {
              */
             std::unique_ptr<CheckResult> check(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters);
             
+            
+            SparseModelType const& getConsideredParametricModel() const;
+            CheckTask<storm::logic::Formula, ConstantType> const& getCurrentCheckTask() const;
+            
         protected:
+            void specifyFormula(CheckTask<storm::logic::Formula, typename SparseModelType::ValueType> const& checkTask);
             
             // Resets all data that correspond to the currently defined property.
             virtual void reset() = 0;
@@ -62,7 +71,7 @@ namespace storm {
             virtual std::unique_ptr<CheckResult> computeQuantitativeValues(storm::storage::ParameterRegion<typename SparseModelType::ValueType> const& region, storm::solver::OptimizationDirection const& dirForParameters) = 0;
             
             
-            SparseModelType const& parametricModel;
+            std::shared_ptr<SparseModelType> parametricModel;
             std::unique_ptr<CheckTask<storm::logic::Formula, ConstantType>> currentCheckTask;
 
         private:
diff --git a/src/storm-pars/settings/modules/ParametricSettings.cpp b/src/storm-pars/settings/modules/ParametricSettings.cpp
index 5b7024af8..a50ef941e 100644
--- a/src/storm-pars/settings/modules/ParametricSettings.cpp
+++ b/src/storm-pars/settings/modules/ParametricSettings.cpp
@@ -14,7 +14,6 @@ namespace storm {
             
             const std::string ParametricSettings::moduleName = "parametric";
             const std::string ParametricSettings::exportResultOptionName = "resultfile";
-            const std::string ParametricSettings::simplifyOptionName = "simplify";
             const std::string ParametricSettings::derivativesOptionName = "derivatives";
             const std::string ParametricSettings::transformContinuousOptionName = "transformcontinuous";
             const std::string ParametricSettings::transformContinuousShortOptionName = "tc";
@@ -22,7 +21,6 @@ namespace storm {
             ParametricSettings::ParametricSettings() : ModuleSettings(moduleName) {
                 this->addOption(storm::settings::OptionBuilder(moduleName, exportResultOptionName, false, "A path to a file where the parametric result should be saved.")
                                 .addArgument(storm::settings::ArgumentBuilder::createStringArgument("path", "the location.").addValidatorString(ArgumentValidatorFactory::createWritableFileValidator()).build()).build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, simplifyOptionName, false, "Sets whether to perform simplification steps before model analysis.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, derivativesOptionName, false, "Sets whether to generate the derivatives of the resulting rational function.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, transformContinuousOptionName, false, "Sets whether to transform a continuous time input model to a discrete time model.").setShortName(transformContinuousShortOptionName).build());
             }
@@ -35,10 +33,6 @@ namespace storm {
                 return this->getOption(exportResultOptionName).getArgumentByName("path").getValueAsString();
             }
             
-            bool ParametricSettings::isSimplifySet() const {
-                return this->getOption(simplifyOptionName).getHasOptionBeenSet();
-            }
-            
             bool ParametricSettings::isDerivativesSet() const {
                 return this->getOption(derivativesOptionName).getHasOptionBeenSet();
             }
diff --git a/src/storm-pars/settings/modules/ParametricSettings.h b/src/storm-pars/settings/modules/ParametricSettings.h
index 9bcfa9ea1..436faa92d 100644
--- a/src/storm-pars/settings/modules/ParametricSettings.h
+++ b/src/storm-pars/settings/modules/ParametricSettings.h
@@ -30,11 +30,6 @@ namespace storm {
                  */
 				std::string exportResultPath() const;
 				
-                /*!
-                 * Retrieves whether or not the input model should be simplified before its analysis.
-                 */
-                bool isSimplifySet() const;
-                
                /*!
                  * Retrieves whether or not derivatives of the resulting rational function are to be generated.
                  *
@@ -51,7 +46,6 @@ namespace storm {
                 
             private:
 				const static std::string exportResultOptionName;
-                const static std::string simplifyOptionName;
                 const static std::string derivativesOptionName;
                 const static std::string transformContinuousOptionName;
                 const static std::string transformContinuousShortOptionName;