diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h
index 0476d1dc22..ae9dc2b3fa 100644
--- a/src/storm-cli-utilities/model-handling.h
+++ b/src/storm-cli-utilities/model-handling.h
@@ -28,6 +28,8 @@
 
 #include "storm/exceptions/OptionParserException.h"
 
+#include "storm/modelchecker/results/CheckResult.h"
+#include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h"
 #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
 
 #include "storm/models/sparse/StandardRewardModel.h"
@@ -1141,7 +1143,21 @@ void verifyWithSparseEngine(std::shared_ptr<storm::models::ModelBase> const& mod
                     STORM_LOG_ERROR("Scheduler requested but could not be generated.");
                 }
             } else {
-                STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Scheduler export not supported for this property.");
+                if (result->isExplicitParetoCurveCheckResult()) {
+                    if (result->template asExplicitParetoCurveCheckResult<ValueType>().hasScheduler()) {
+                        auto schedulers = result->template asExplicitParetoCurveCheckResult<ValueType>().getSchedulers();
+                        for (auto const& scheduler : schedulers) {
+                            storm::api::exportScheduler(sparseModel, *scheduler.second.get(),
+                                                        (exportCount == 0 ? std::string("") : std::to_string(exportCount)) +
+                                                            ioSettings.getExportSchedulerFilename() + "-" +
+                                                            storm::utility::vector::toStringNoVerbose(scheduler.first));
+                        }
+                    } else {
+                        STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Scheduler export not supported for this property.");
+                    }
+                } else {
+                    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Scheduler export not supported for this property.");
+                }
             }
         }
         if (ioSettings.isExportCheckResultSet()) {
diff --git a/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp b/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp
index 11be8df9d5..7f92c3a994 100644
--- a/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp
+++ b/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.cpp
@@ -1,6 +1,10 @@
 #include "storm/modelchecker/multiobjective/MultiObjectivePostprocessing.h"
 
 #include "storm/adapters/RationalNumberAdapter.h"
+#include "storm/models/sparse/MarkovAutomaton.h"
+#include "storm/models/sparse/Mdp.h"
+#include "storm/storage/Scheduler.h"
+#include "storm/storage/memorystructure/SparseModelMemoryProductReverseData.h"
 
 namespace storm {
 namespace modelchecker {
@@ -66,6 +70,41 @@ std::shared_ptr<storm::storage::geometry::Polytope<GeometryValueType>> transform
     return polytope->affineTransformation(transformationMatrix, transformationVector);
 }
 
+/*
+ * This function is only responsible to reverse changes to the model made in the preprocessor
+ * (not the ones done by specific checkers)
+ */
+template<typename ValueType, typename SparseModelType>
+void transformObjectiveSchedulersToOriginal(storm::storage::SparseModelMemoryProductReverseData const& reverseData,
+                                            std::shared_ptr<SparseModelType> const& originalModel,
+                                            std::map<std::vector<ValueType>, std::shared_ptr<storm::storage::Scheduler<ValueType>>> schedulers) {
+    auto memoryStateCount = reverseData.memory.getNumberOfStates();
+    auto originalModelStates = originalModel->getNumberOfStates();
+    for (auto it = schedulers.begin(); it != schedulers.end(); ++it) {
+        std::shared_ptr<storm::storage::Scheduler<ValueType>> scheduler = it->second;
+        auto point = it->first;
+        storm::storage::Scheduler<ValueType> result(originalModelStates, reverseData.memory);
+        auto currSchedulerModelStates = scheduler->getNumberOfModelStates();
+        for (int state = 0; state < originalModelStates; state++) {
+            for (int memState = 0; memState < memoryStateCount; memState++) {
+                auto const& productState = reverseData.toResultStateMapping[state * memoryStateCount + memState];
+                if (productState != -1) {
+                    // if it's -1 it's unreachable
+                    if (productState >= currSchedulerModelStates) {
+                        // means it's been deleted as irrelevant state
+                        result.setDontCare(productState, memState, true);
+                    } else {
+                        auto choice = scheduler->getChoice(productState);
+                        result.setChoice(choice, state, memState);
+                    }
+                }
+            }
+        }
+        scheduler.reset();
+        schedulers[point] = std::move(std::make_shared<storm::storage::Scheduler<ValueType>>(result));
+    }
+}
+
 template std::vector<storm::RationalNumber> transformObjectiveValuesToOriginal(std::vector<Objective<double>> objectives,
                                                                                std::vector<storm::RationalNumber> const& point);
 template std::shared_ptr<storm::storage::geometry::Polytope<storm::RationalNumber>> transformObjectivePolytopeToOriginal(
@@ -74,6 +113,25 @@ template std::vector<storm::RationalNumber> transformObjectiveValuesToOriginal(s
                                                                                std::vector<storm::RationalNumber> const& point);
 template std::shared_ptr<storm::storage::geometry::Polytope<storm::RationalNumber>> transformObjectivePolytopeToOriginal(
     std::vector<Objective<storm::RationalNumber>> objectives, std::shared_ptr<storm::storage::geometry::Polytope<storm::RationalNumber>> const& polytope);
+
+template void transformObjectiveSchedulersToOriginal(
+    storm::storage::SparseModelMemoryProductReverseData const& reverseData,
+    std::shared_ptr<storm::models::sparse::Mdp<storm::RationalNumber>> const& originalModel,
+    std::map<std::vector<storm::RationalNumber>, std::shared_ptr<storm::storage::Scheduler<storm::RationalNumber>>> schedulers);
+
+template void transformObjectiveSchedulersToOriginal(storm::storage::SparseModelMemoryProductReverseData const& reverseData,
+                                                     std::shared_ptr<storm::models::sparse::Mdp<double>> const& originalModel,
+                                                     std::map<std::vector<double>, std::shared_ptr<storm::storage::Scheduler<double>>> schedulers);
+
+template void transformObjectiveSchedulersToOriginal(
+    storm::storage::SparseModelMemoryProductReverseData const& reverseData,
+    std::shared_ptr<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>> const& originalModel,
+    std::map<std::vector<storm::RationalNumber>, std::shared_ptr<storm::storage::Scheduler<storm::RationalNumber>>> schedulers);
+
+template void transformObjectiveSchedulersToOriginal(storm::storage::SparseModelMemoryProductReverseData const& reverseData,
+                                                     std::shared_ptr<storm::models::sparse::MarkovAutomaton<double>> const& originalModel,
+                                                     std::map<std::vector<double>, std::shared_ptr<storm::storage::Scheduler<double>>> schedulers);
+
 }  // namespace multiobjective
 }  // namespace modelchecker
 }  // namespace storm
\ No newline at end of file
diff --git a/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.h b/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.h
index 549c4c15a1..927da19b8e 100644
--- a/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.h
+++ b/src/storm/modelchecker/multiobjective/MultiObjectivePostprocessing.h
@@ -4,7 +4,9 @@
 #include <vector>
 
 #include "storm/modelchecker/multiobjective/Objective.h"
+#include "storm/storage/Scheduler.h"
 #include "storm/storage/geometry/Polytope.h"
+#include "storm/storage/memorystructure/SparseModelMemoryProductReverseData.h"
 
 namespace storm {
 namespace modelchecker {
@@ -17,6 +19,15 @@ template<typename ValueType, typename GeometryValueType>
 std::shared_ptr<storm::storage::geometry::Polytope<GeometryValueType>> transformObjectivePolytopeToOriginal(
     std::vector<Objective<ValueType>> objectives, std::shared_ptr<storm::storage::geometry::Polytope<GeometryValueType>> const& polytope);
 
+/*
+ * Uses the information from reverse data to edit the objective schedulers in 'schedulers' to ones
+ * apt for the target model.
+ */
+template<typename ValueType, typename SparseModelType>
+void transformObjectiveSchedulersToOriginal(storm::storage::SparseModelMemoryProductReverseData const& reverseData,
+                                            std::shared_ptr<SparseModelType> const& originalModel,
+                                            std::map<std::vector<ValueType>, std::shared_ptr<storm::storage::Scheduler<ValueType>>> schedulers);
+
 }  // namespace multiobjective
 }  // namespace modelchecker
 }  // namespace storm
\ No newline at end of file
diff --git a/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp b/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp
index a8065df454..e774316c25 100644
--- a/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp
+++ b/src/storm/modelchecker/multiobjective/multiObjectiveModelChecking.cpp
@@ -1,12 +1,15 @@
 #include "storm/modelchecker/multiobjective/multiObjectiveModelChecking.h"
 
 #include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h"
+#include "storm/modelchecker/multiobjective/MultiObjectivePostprocessing.h"
 #include "storm/modelchecker/multiobjective/constraintbased/SparseCbAchievabilityQuery.h"
 #include "storm/modelchecker/multiobjective/deterministicScheds/DeterministicSchedsParetoExplorer.h"
 #include "storm/modelchecker/multiobjective/pcaa/SparsePcaaAchievabilityQuery.h"
 #include "storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h"
 #include "storm/modelchecker/multiobjective/pcaa/SparsePcaaQuantitativeQuery.h"
 #include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.h"
+#include "storm/modelchecker/results/CheckResult.h"
+#include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h"
 #include "storm/models/sparse/MarkovAutomaton.h"
 #include "storm/models/sparse/Mdp.h"
 #include "storm/models/sparse/StandardRewardModel.h"
@@ -83,6 +86,13 @@ std::unique_ptr<CheckResult> performMultiObjectiveModelChecking(Environment cons
                 }
 
                 result = query->check(env);
+                if (preprocessorResult.memoryIncorporationReverseData && result->isExplicitParetoCurveCheckResult() &&
+                    result->template asExplicitParetoCurveCheckResult<typename SparseModelType::ValueType>().hasScheduler()) {
+                    // we have information to post-process schedulers
+                    auto schedulers = result->template asExplicitParetoCurveCheckResult<typename SparseModelType::ValueType>().getSchedulers();
+                    transformObjectiveSchedulersToOriginal(std::move(preprocessorResult.memoryIncorporationReverseData.value()),
+                                                           std::make_shared<SparseModelType>(model), schedulers);
+                }
 
                 if (env.modelchecker().multi().isExportPlotSet()) {
                     query->exportPlotOfCurrentApproximation(env);
diff --git a/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h
index 38d8c8f137..2bdb94560e 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h
+++ b/src/storm/modelchecker/multiobjective/pcaa/PcaaWeightVectorChecker.h
@@ -69,6 +69,14 @@ class PcaaWeightVectorChecker {
      */
     virtual storm::storage::Scheduler<ValueType> computeScheduler() const;
 
+    /*!
+     * If changes has been made to the given model this function should inverse them to return a scheduler
+     * for the given model
+     */
+    virtual storm::storage::Scheduler<ValueType> computeOriginalScheduler() const {
+        return computeScheduler();
+    }
+
    protected:
     /*!
      * Computes the weighted lower or upper bounds for the provided set of objectives.
diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp
index 24c8030628..87e770364e 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp
+++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp
@@ -7,6 +7,10 @@
 #include "storm/models/sparse/MarkovAutomaton.h"
 #include "storm/models/sparse/Mdp.h"
 #include "storm/models/sparse/StandardRewardModel.h"
+#include "storm/settings/SettingsManager.h"
+#include "storm/settings/modules/CoreSettings.h"
+#include "storm/settings/modules/IOSettings.h"
+#include "storm/storage/Scheduler.h"
 #include "storm/utility/SignalHandler.h"
 #include "storm/utility/constants.h"
 #include "storm/utility/vector.h"
@@ -51,13 +55,24 @@ std::unique_ptr<CheckResult> SparsePcaaParetoQuery<SparseModelType, GeometryValu
             storm::utility::vector::convertNumericVector<typename SparseModelType::ValueType>(transformObjectiveValuesToOriginal(this->objectives, vertex)));
     }
     return std::unique_ptr<CheckResult>(new ExplicitParetoCurveCheckResult<typename SparseModelType::ValueType>(
-        this->originalModel.getInitialStates().getNextSetIndex(0), std::move(paretoOptimalPoints),
+        this->originalModel.getInitialStates().getNextSetIndex(0), std::move(paretoOptimalPoints), std::move(schedulers),
         transformObjectivePolytopeToOriginal(this->objectives, this->underApproximation)
             ->template convertNumberRepresentation<typename SparseModelType::ValueType>(),
         transformObjectivePolytopeToOriginal(this->objectives, this->overApproximation)
             ->template convertNumberRepresentation<typename SparseModelType::ValueType>()));
 }
 
+template<class SparseModelType, typename GeometryValueType>
+void SparsePcaaParetoQuery<SparseModelType, GeometryValueType>::updateSchedulers() {
+    if (storm::settings::getModule<storm::settings::modules::IOSettings>().isExportSchedulerSet()) {
+        std::vector<typename SparseModelType::ValueType> point = this->weightVectorChecker->getUnderApproximationOfInitialStateResults();
+        if (!this->schedulers.count(point)) {
+            this->schedulers[point] =
+                std::make_shared<storm::storage::Scheduler<typename SparseModelType::ValueType>>(this->weightVectorChecker->computeOriginalScheduler());
+        }
+    }
+}
+
 template<class SparseModelType, typename GeometryValueType>
 void SparsePcaaParetoQuery<SparseModelType, GeometryValueType>::exploreSetOfAchievablePoints(Environment const& env) {
     STORM_LOG_THROW(env.modelchecker().multi().getPrecisionType() == MultiObjectiveModelCheckerEnvironment::PrecisionType::Absolute,
@@ -68,6 +83,7 @@ void SparsePcaaParetoQuery<SparseModelType, GeometryValueType>::exploreSetOfAchi
         WeightVector direction(this->objectives.size(), storm::utility::zero<GeometryValueType>());
         direction[objIndex] = storm::utility::one<GeometryValueType>();
         this->performRefinementStep(env, std::move(direction));
+        this->updateSchedulers();
         if (storm::utility::resources::isTerminate()) {
             break;
         }
@@ -95,6 +111,7 @@ void SparsePcaaParetoQuery<SparseModelType, GeometryValueType>::exploreSetOfAchi
         STORM_LOG_INFO("Current precision of the approximation of the pareto curve is ~" << storm::utility::convertNumber<double>(farestDistance));
         WeightVector direction = underApproxHalfspaces[farestHalfspaceIndex].normalVector();
         this->performRefinementStep(env, std::move(direction));
+        this->updateSchedulers();
     }
     STORM_LOG_ERROR("Could not reach the desired precision: Termination requested or maximum number of refinement steps exceeded.");
 }
diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h
index cb8c8b490b..6984aa2b5b 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h
+++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.h
@@ -31,11 +31,20 @@ class SparsePcaaParetoQuery : public SparsePcaaQuery<SparseModelType, GeometryVa
      */
     virtual std::unique_ptr<CheckResult> check(Environment const& env) override;
 
+    /*
+     * Compute the scheduler for current underaproximated point and store it
+     */
+    void updateSchedulers();
+
    private:
     /*
      * Performs refinement steps until the approximation is sufficiently precise
      */
     void exploreSetOfAchievablePoints(Environment const& env);
+    /*
+     * Schedulers corresponding to the pareto optimal points
+     */
+    std::map<std::vector<typename SparseModelType::ValueType>, std::shared_ptr<storm::storage::Scheduler<typename SparseModelType::ValueType>>> schedulers;
 };
 
 }  // namespace multiobjective
diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp
index 60c437ec0c..87729957b4 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp
+++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.cpp
@@ -64,7 +64,7 @@ void StandardPcaaWeightVectorChecker<SparseModelType>::initialize(
     auto mergerResult =
         merger.mergeTargetAndSinkStates(maybeStates, rewardAnalysis.reward0AStates, storm::storage::BitVector(maybeStates.size(), false),
                                         std::vector<std::string>(relevantRewardModels.begin(), relevantRewardModels.end()), finiteTotalRewardChoices);
-
+    goalStateMergerIndexMapping = mergerResult.oldToNewStateIndexMapping;
     // Initialize data specific for the considered model type
     initializeModelTypeSpecificData(*mergerResult.model);
 
@@ -235,6 +235,18 @@ StandardPcaaWeightVectorChecker<SparseModelType>::computeScheduler() const {
     return result;
 }
 
+template<class SparseModelType>
+storm::storage::Scheduler<typename StandardPcaaWeightVectorChecker<SparseModelType>::ValueType>
+StandardPcaaWeightVectorChecker<SparseModelType>::computeOriginalScheduler() const {
+    auto scheduler = this->computeScheduler();
+    storm::storage::Scheduler<ValueType> result(goalStateMergerIndexMapping.size());
+    auto numOfModelStates = result.getNumberOfModelStates();
+    for (int state = 0; state < numOfModelStates; state++) {
+        result.setChoice(scheduler.getChoice(goalStateMergerIndexMapping[state]), state);
+    }
+    return result;
+}
+
 template<typename ValueType>
 void computeSchedulerProb1(storm::storage::SparseMatrix<ValueType> const& transitionMatrix, storm::storage::SparseMatrix<ValueType> const& backwardTransitions,
                            storm::storage::BitVector const& consideredStates, storm::storage::BitVector const& statesToReach, std::vector<uint64_t>& choices,
diff --git a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h
index ef58c5d40b..7adcb8751b 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h
+++ b/src/storm/modelchecker/multiobjective/pcaa/StandardPcaaWeightVectorChecker.h
@@ -12,6 +12,7 @@
 #include "storm/storage/Scheduler.h"
 #include "storm/storage/SparseMatrix.h"
 #include "storm/transformer/EndComponentEliminator.h"
+#include "storm/transformer/GoalStateMerger.h"
 #include "storm/utility/vector.h"
 
 namespace storm {
@@ -67,6 +68,12 @@ class StandardPcaaWeightVectorChecker : public PcaaWeightVectorChecker<SparseMod
      */
     virtual storm::storage::Scheduler<ValueType> computeScheduler() const override;
 
+    /*!
+     * Use the "oldToNewStateIndexMapping" from the merge result to build a scheduler fit for the original scheduler
+     * from the calculated scheduler from "computerScheduler"
+     */
+    virtual storm::storage::Scheduler<ValueType> computeOriginalScheduler() const override;
+
    protected:
     void initialize(preprocessing::SparseMultiObjectivePreprocessorResult<SparseModelType> const& preprocessorResult);
     virtual void initializeModelTypeSpecificData(SparseModelType const& model) = 0;
@@ -173,6 +180,9 @@ class StandardPcaaWeightVectorChecker : public PcaaWeightVectorChecker<SparseMod
     };
     boost::optional<EcQuotient> ecQuotient;
 
+    // Merge results
+    std::vector<uint_fast64_t> goalStateMergerIndexMapping;
+
     struct LraMecDecomposition {
         storm::storage::MaximalEndComponentDecomposition<ValueType> mecs;
         std::vector<ValueType> auxMecValues;
diff --git a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp
index 0cd023781c..17ec3fd000 100644
--- a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp
+++ b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.cpp
@@ -14,6 +14,7 @@
 #include "storm/settings/modules/GeneralSettings.h"
 #include "storm/storage/MaximalEndComponentDecomposition.h"
 #include "storm/storage/expressions/ExpressionManager.h"
+#include "storm/storage/memorystructure/SparseModelMemoryProductReverseData.h"
 #include "storm/transformer/EndComponentEliminator.h"
 #include "storm/transformer/MemoryIncorporation.h"
 #include "storm/transformer/SubsystemBuilder.h"
@@ -35,12 +36,16 @@ template<typename SparseModelType>
 typename SparseMultiObjectivePreprocessor<SparseModelType>::ReturnType SparseMultiObjectivePreprocessor<SparseModelType>::preprocess(
     Environment const& env, SparseModelType const& originalModel, storm::logic::MultiObjectiveFormula const& originalFormula) {
     std::shared_ptr<SparseModelType> model;
+    boost::optional<storm::storage::SparseModelMemoryProductReverseData> memoryIncorporationReverseData;
 
     // Incorporate the necessary memory
     if (env.modelchecker().multi().isSchedulerRestrictionSet()) {
         auto const& schedRestr = env.modelchecker().multi().getSchedulerRestriction();
         if (schedRestr.getMemoryPattern() == storm::storage::SchedulerClass::MemoryPattern::GoalMemory) {
-            model = storm::transformer::MemoryIncorporation<SparseModelType>::incorporateGoalMemory(originalModel, originalFormula.getSubformulas());
+            // trying to do "auto [model, modelMemoryProduct]" causes seg fault when trying to access model
+            auto res = storm::transformer::MemoryIncorporation<SparseModelType>::incorporateGoalMemory(originalModel, originalFormula.getSubformulas());
+            model = std::get<0>(res);
+            memoryIncorporationReverseData = std::get<1>(res);
         } else if (schedRestr.getMemoryPattern() == storm::storage::SchedulerClass::MemoryPattern::Arbitrary && schedRestr.getMemoryStates() > 1) {
             model = storm::transformer::MemoryIncorporation<SparseModelType>::incorporateFullMemory(originalModel, schedRestr.getMemoryStates());
         } else if (schedRestr.getMemoryPattern() == storm::storage::SchedulerClass::MemoryPattern::Counter && schedRestr.getMemoryStates() > 1) {
@@ -51,7 +56,10 @@ typename SparseMultiObjectivePreprocessor<SparseModelType>::ReturnType SparseMul
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "The given scheduler restriction has not been implemented.");
         }
     } else {
-        model = storm::transformer::MemoryIncorporation<SparseModelType>::incorporateGoalMemory(originalModel, originalFormula.getSubformulas());
+        // trying to do "auto [model, modelMemoryProduct]" causes seg fault when trying to access model
+        auto res = storm::transformer::MemoryIncorporation<SparseModelType>::incorporateGoalMemory(originalModel, originalFormula.getSubformulas());
+        model = std::get<0>(res);
+        memoryIncorporationReverseData = std::get<1>(res);
     }
 
     // Remove states that are irrelevant for all properties (e.g. because they are only reachable via goal states
@@ -60,6 +68,7 @@ typename SparseMultiObjectivePreprocessor<SparseModelType>::ReturnType SparseMul
 
     PreprocessorData data(model);
     data.deadlockLabel = deadlockLabel;
+    data.memoryIncorporationReverseData = std::move(memoryIncorporationReverseData);
 
     // Invoke preprocessing on the individual objectives
     for (auto const& subFormula : originalFormula.getSubformulas()) {
@@ -726,6 +735,7 @@ typename SparseMultiObjectivePreprocessor<SparseModelType>::ReturnType SparseMul
     ReturnType result(originalFormula, originalModel);
     auto backwardTransitions = data.model->getBackwardTransitions();
     result.preprocessedModel = data.model;
+    result.memoryIncorporationReverseData = data.memoryIncorporationReverseData;
 
     for (auto& obj : data.objectives) {
         result.objectives.push_back(std::move(*obj));
diff --git a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.h b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.h
index da5981991e..fa6c2c740b 100644
--- a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.h
+++ b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessor.h
@@ -7,6 +7,8 @@
 #include "storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h"
 #include "storm/storage/BitVector.h"
 #include "storm/storage/memorystructure/MemoryStructure.h"
+#include "storm/storage/memorystructure/SparseModelMemoryProduct.h"
+#include "storm/storage/memorystructure/SparseModelMemoryProductReverseData.h"
 
 namespace storm {
 
@@ -49,6 +51,9 @@ class SparseMultiObjectivePreprocessor {
         // If set, some states have been merged to a deadlock state with this label.
         boost::optional<std::string> deadlockLabel;
 
+        // Mapping of incorporated memory to model+memory
+        boost::optional<storm::storage::SparseModelMemoryProductReverseData> memoryIncorporationReverseData;
+
         PreprocessorData(std::shared_ptr<SparseModelType> model);
     };
 
diff --git a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h
index 6e708790f1..6e058826e6 100644
--- a/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h
+++ b/src/storm/modelchecker/multiobjective/preprocessing/SparseMultiObjectivePreprocessorResult.h
@@ -7,6 +7,8 @@
 #include "storm/logic/Formulas.h"
 #include "storm/modelchecker/multiobjective/Objective.h"
 #include "storm/storage/BitVector.h"
+#include "storm/storage/memorystructure/SparseModelMemoryProduct.h"
+#include "storm/storage/memorystructure/SparseModelMemoryProductReverseData.h"
 
 #include "storm/exceptions/UnexpectedException.h"
 
@@ -23,6 +25,9 @@ struct SparseMultiObjectivePreprocessorResult {
     storm::logic::MultiObjectiveFormula const& originalFormula;
     SparseModelType const& originalModel;
 
+    // Mapping of incorporated memory to model+memory
+    boost::optional<storm::storage::SparseModelMemoryProductReverseData> memoryIncorporationReverseData;
+
     // The preprocessed model and objectives
     std::shared_ptr<SparseModelType> preprocessedModel;
     std::vector<Objective<typename SparseModelType::ValueType>> objectives;
diff --git a/src/storm/modelchecker/results/CheckResult.cpp b/src/storm/modelchecker/results/CheckResult.cpp
index 8549ce26d0..f29da19975 100644
--- a/src/storm/modelchecker/results/CheckResult.cpp
+++ b/src/storm/modelchecker/results/CheckResult.cpp
@@ -230,6 +230,8 @@ template ExplicitQuantitativeCheckResult<storm::RationalFunction> const& CheckRe
 
 template ExplicitParetoCurveCheckResult<storm::RationalNumber>& CheckResult::asExplicitParetoCurveCheckResult();
 template ExplicitParetoCurveCheckResult<storm::RationalNumber> const& CheckResult::asExplicitParetoCurveCheckResult() const;
+template ExplicitParetoCurveCheckResult<storm::RationalFunction>& CheckResult::asExplicitParetoCurveCheckResult();
+template ExplicitParetoCurveCheckResult<storm::RationalFunction> const& CheckResult::asExplicitParetoCurveCheckResult() const;
 
 template LexicographicCheckResult<storm::RationalNumber>& CheckResult::asLexicographicCheckResult();
 template LexicographicCheckResult<storm::RationalNumber> const& CheckResult::asLexicographicCheckResult() const;
diff --git a/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp b/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp
index 02f62702cb..e9d2ee00dc 100644
--- a/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp
+++ b/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp
@@ -33,6 +33,14 @@ ExplicitParetoCurveCheckResult<ValueType>::ExplicitParetoCurveCheckResult(storm:
     // Intentionally left empty.
 }
 
+template<typename ValueType>
+ExplicitParetoCurveCheckResult<ValueType>::ExplicitParetoCurveCheckResult(
+    storm::storage::sparse::state_type const& state, std::vector<typename ParetoCurveCheckResult<ValueType>::point_type>&& points,
+    std::map<std::vector<ValueType>, std::shared_ptr<storm::storage::Scheduler<ValueType>>>&& schedulers,
+    typename ParetoCurveCheckResult<ValueType>::polytope_type&& underApproximation,
+    typename ParetoCurveCheckResult<ValueType>::polytope_type&& overApproximation)
+    : ParetoCurveCheckResult<ValueType>(points, underApproximation, overApproximation), state(state), schedulers(schedulers) {}
+
 template<typename ValueType>
 std::unique_ptr<CheckResult> ExplicitParetoCurveCheckResult<ValueType>::clone() const {
     return std::make_unique<ExplicitParetoCurveCheckResult<ValueType>>(this->state, this->points, this->underApproximation, this->overApproximation);
@@ -65,9 +73,34 @@ storm::storage::sparse::state_type const& ExplicitParetoCurveCheckResult<ValueTy
     return state;
 }
 
+template<typename ValueType>
+bool ExplicitParetoCurveCheckResult<ValueType>::hasScheduler() const {
+    return schedulers.size() > 0;
+}
+
+template<typename ValueType>
+void ExplicitParetoCurveCheckResult<ValueType>::setSchedulers(
+    const std::map<std::vector<ValueType>, std::shared_ptr<storm::storage::Scheduler<ValueType>>> newSchedulers) {
+    schedulers = newSchedulers;
+}
+
+template<typename ValueType>
+std::map<std::vector<ValueType>, std::shared_ptr<storm::storage::Scheduler<ValueType>>> const& ExplicitParetoCurveCheckResult<ValueType>::getSchedulers()
+    const {
+    STORM_LOG_THROW(this->hasScheduler(), storm::exceptions::InvalidOperationException, "Unable to retrieve non-existing scheduler.");
+    return schedulers;
+}
+
+template<typename ValueType>
+std::map<std::vector<ValueType>, std::shared_ptr<storm::storage::Scheduler<ValueType>>>& ExplicitParetoCurveCheckResult<ValueType>::getSchedulers() {
+    STORM_LOG_THROW(this->hasScheduler(), storm::exceptions::InvalidOperationException, "Unable to retrieve non-existing scheduler.");
+    return schedulers;
+}
+
 template class ExplicitParetoCurveCheckResult<double>;
 #ifdef STORM_HAVE_CARL
 template class ExplicitParetoCurveCheckResult<storm::RationalNumber>;
+template class ExplicitParetoCurveCheckResult<storm::RationalFunction>;
 #endif
 }  // namespace modelchecker
 }  // namespace storm
diff --git a/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.h b/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.h
index f2f6472e51..90e8422957 100644
--- a/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.h
+++ b/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.h
@@ -1,9 +1,11 @@
 #ifndef STORM_MODELCHECKER_EXPLICITPARETOCURVECHECKRESULT_H_
 #define STORM_MODELCHECKER_EXPLICITPARETOCURVECHECKRESULT_H_
 
+#include <map>
 #include <vector>
 
 #include "storm/modelchecker/results/ParetoCurveCheckResult.h"
+#include "storm/storage/Scheduler.h"
 #include "storm/storage/sparse/StateType.h"
 
 namespace storm {
@@ -20,6 +22,11 @@ class ExplicitParetoCurveCheckResult : public ParetoCurveCheckResult<ValueType>
                                    std::vector<typename ParetoCurveCheckResult<ValueType>::point_type>&& points,
                                    typename ParetoCurveCheckResult<ValueType>::polytope_type&& underApproximation = nullptr,
                                    typename ParetoCurveCheckResult<ValueType>::polytope_type&& overApproximation = nullptr);
+    ExplicitParetoCurveCheckResult(storm::storage::sparse::state_type const& state,
+                                   std::vector<typename ParetoCurveCheckResult<ValueType>::point_type>&& points,
+                                   std::map<std::vector<ValueType>, std::shared_ptr<storm::storage::Scheduler<ValueType>>>&& schedulers,
+                                   typename ParetoCurveCheckResult<ValueType>::polytope_type&& underApproximation = nullptr,
+                                   typename ParetoCurveCheckResult<ValueType>::polytope_type&& overApproximation = nullptr);
 
     ExplicitParetoCurveCheckResult(ExplicitParetoCurveCheckResult const& other) = default;
     ExplicitParetoCurveCheckResult& operator=(ExplicitParetoCurveCheckResult const& other) = default;
@@ -36,9 +43,19 @@ class ExplicitParetoCurveCheckResult : public ParetoCurveCheckResult<ValueType>
 
     storm::storage::sparse::state_type const& getState() const;
 
+    virtual bool hasScheduler() const override;
+
+    void setSchedulers(std::map<std::vector<ValueType>, std::shared_ptr<storm::storage::Scheduler<ValueType>>> schedulers);
+
+    std::map<std::vector<ValueType>, std::shared_ptr<storm::storage::Scheduler<ValueType>>> const& getSchedulers() const;
+
+    std::map<std::vector<ValueType>, std::shared_ptr<storm::storage::Scheduler<ValueType>>>& getSchedulers();
+
    private:
     // The state of the checked model to which the result applies
     storm::storage::sparse::state_type state;
+    // The corresponding strategies to reach each point in the pareto curve
+    std::map<std::vector<ValueType>, std::shared_ptr<storm::storage::Scheduler<ValueType>>> schedulers;
 };
 }  // namespace modelchecker
 }  // namespace storm
diff --git a/src/storm/modelchecker/results/ParetoCurveCheckResult.cpp b/src/storm/modelchecker/results/ParetoCurveCheckResult.cpp
index 771d2e5a98..baa69b4f2f 100644
--- a/src/storm/modelchecker/results/ParetoCurveCheckResult.cpp
+++ b/src/storm/modelchecker/results/ParetoCurveCheckResult.cpp
@@ -96,6 +96,7 @@ template class ParetoCurveCheckResult<double>;
 
 #ifdef STORM_HAVE_CARL
 template class ParetoCurveCheckResult<storm::RationalNumber>;
+template class ParetoCurveCheckResult<storm::RationalFunction>;
 #endif
 }  // namespace modelchecker
 }  // namespace storm
diff --git a/src/storm/storage/Scheduler.cpp b/src/storm/storage/Scheduler.cpp
index 3cc57db960..82bc5caea6 100644
--- a/src/storm/storage/Scheduler.cpp
+++ b/src/storm/storage/Scheduler.cpp
@@ -159,6 +159,11 @@ uint_fast64_t Scheduler<ValueType>::getNumberOfMemoryStates() const {
     return memoryStructure ? memoryStructure->getNumberOfStates() : 1;
 }
 
+template<typename ValueType>
+uint_fast64_t Scheduler<ValueType>::getNumberOfModelStates() const {
+    return schedulerChoices.empty() ? 0 : schedulerChoices.front().size();
+}
+
 template<typename ValueType>
 boost::optional<storm::storage::MemoryStructure> const& Scheduler<ValueType>::getMemoryStructure() const {
     return memoryStructure;
diff --git a/src/storm/storage/Scheduler.h b/src/storm/storage/Scheduler.h
index c33dde45b0..4bf67f486a 100644
--- a/src/storm/storage/Scheduler.h
+++ b/src/storm/storage/Scheduler.h
@@ -104,6 +104,10 @@ class Scheduler {
      * Retrieves the number of memory states this scheduler considers.
      */
     uint_fast64_t getNumberOfMemoryStates() const;
+    /*!
+     * Retrieves the number of model states this scheduler considers.
+     */
+    uint_fast64_t getNumberOfModelStates() const;
 
     /*!
      * Retrieves the memory structure associated with this scheduler
diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProduct.h b/src/storm/storage/memorystructure/SparseModelMemoryProduct.h
index 017bbb30cd..9742e12db1 100644
--- a/src/storm/storage/memorystructure/SparseModelMemoryProduct.h
+++ b/src/storm/storage/memorystructure/SparseModelMemoryProduct.h
@@ -52,6 +52,10 @@ class SparseModelMemoryProduct {
     storm::models::sparse::Model<ValueType, RewardModelType> const& getOriginalModel() const;
     storm::storage::MemoryStructure const& getMemory() const;
 
+    std::vector<uint64_t> getResultStateMapping() {
+        return toResultStateMapping;
+    }
+
    private:
     // Initializes auxiliary data for building the product
     void initialize();
diff --git a/src/storm/storage/memorystructure/SparseModelMemoryProductReverseData.h b/src/storm/storage/memorystructure/SparseModelMemoryProductReverseData.h
new file mode 100644
index 0000000000..89d5e4a43e
--- /dev/null
+++ b/src/storm/storage/memorystructure/SparseModelMemoryProductReverseData.h
@@ -0,0 +1,24 @@
+#pragma once
+
+#include <boost/optional.hpp>
+#include <memory>
+#include <vector>
+#include "storm/storage/memorystructure/MemoryStructure.h"
+
+namespace storm {
+namespace storage {
+// Data to restore memory incorporation applied with SparseModelMemoryProduct
+// Only stores the least necessary to reverse data from SparseModelMemoryProduct
+struct SparseModelMemoryProductReverseData {
+    storm::storage::MemoryStructure memory;
+    // Maps (modelState * memoryStateCount) + memoryState to the state in the result that represents (memoryState,modelState)
+    std::vector<uint64_t> toResultStateMapping;
+
+    SparseModelMemoryProductReverseData(storm::storage::MemoryStructure const& memory, std::vector<uint64_t> const& toResultStateMapping)
+        : memory(memory), toResultStateMapping(toResultStateMapping) {
+        // Intentionally left empty
+    }
+};
+
+}  // namespace storage
+}  // namespace storm
diff --git a/src/storm/transformer/MemoryIncorporation.cpp b/src/storm/transformer/MemoryIncorporation.cpp
index 18a2fc38c4..79b5994bca 100644
--- a/src/storm/transformer/MemoryIncorporation.cpp
+++ b/src/storm/transformer/MemoryIncorporation.cpp
@@ -10,6 +10,7 @@
 #include "storm/storage/memorystructure/MemoryStructureBuilder.h"
 #include "storm/storage/memorystructure/NondeterministicMemoryStructureBuilder.h"
 #include "storm/storage/memorystructure/SparseModelMemoryProduct.h"
+#include "storm/storage/memorystructure/SparseModelMemoryProductReverseData.h"
 #include "storm/storage/memorystructure/SparseModelNondeterministicMemoryProduct.h"
 
 #include "storm/utility/macros.h"
@@ -56,7 +57,7 @@ storm::storage::MemoryStructure getUntilFormulaMemory(SparseModelType const& mod
 }
 
 template<class SparseModelType>
-std::shared_ptr<SparseModelType> MemoryIncorporation<SparseModelType>::incorporateGoalMemory(
+std::tuple<std::shared_ptr<SparseModelType>, storm::storage::SparseModelMemoryProductReverseData> MemoryIncorporation<SparseModelType>::incorporateGoalMemory(
     SparseModelType const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
     storm::storage::MemoryStructure memory = storm::storage::MemoryStructureBuilder<ValueType, RewardModelType>::buildTrivialMemoryStructure(model);
 
@@ -87,7 +88,8 @@ std::shared_ptr<SparseModelType> MemoryIncorporation<SparseModelType>::incorpora
     }
 
     storm::storage::SparseModelMemoryProduct<ValueType> product = memory.product(model);
-    return std::dynamic_pointer_cast<SparseModelType>(product.build());
+    auto result = std::dynamic_pointer_cast<SparseModelType>(product.build());
+    return std::make_tuple(result, storm::storage::SparseModelMemoryProductReverseData(product.getMemory(), product.getResultStateMapping()));
 }
 
 template<class SparseModelType>
diff --git a/src/storm/transformer/MemoryIncorporation.h b/src/storm/transformer/MemoryIncorporation.h
index 2bea33690a..5040b50b18 100644
--- a/src/storm/transformer/MemoryIncorporation.h
+++ b/src/storm/transformer/MemoryIncorporation.h
@@ -5,6 +5,7 @@
 #include "storm/logic/Formula.h"
 #include "storm/logic/MultiObjectiveFormula.h"
 #include "storm/storage/memorystructure/MemoryStructure.h"
+#include "storm/storage/memorystructure/SparseModelMemoryProductReverseData.h"
 
 namespace storm {
 namespace transformer {
@@ -24,8 +25,8 @@ class MemoryIncorporation {
      * Incorporates memory that stores whether a 'goal' state has already been reached. This supports operatorformulas whose subformula is
      * a (bounded-) until formula, eventually formula, or a globally formula. Total reward formulas and cumulative reward formulas will be ignored.
      */
-    static std::shared_ptr<SparseModelType> incorporateGoalMemory(SparseModelType const& model,
-                                                                  std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas);
+    static std::tuple<std::shared_ptr<SparseModelType>, storm::storage::SparseModelMemoryProductReverseData> incorporateGoalMemory(
+        SparseModelType const& model, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas);
 
     /*!
      * Incorporates a memory structure where the nondeterminism of the model decides which successor state to choose.
diff --git a/src/storm/utility/vector.h b/src/storm/utility/vector.h
index 0a5e3be2fa..5390cc802f 100644
--- a/src/storm/utility/vector.h
+++ b/src/storm/utility/vector.h
@@ -1263,6 +1263,25 @@ std::string toString(std::vector<ValueType> const& vector) {
     stream << " ]";
     return stream.str();
 }
+
+/*!
+ * Less verbose, no space vector to string representation.
+ * @param vector Vector to output.
+ * @return String containing the representation of the vector.
+ */
+template<typename ValueType>
+std::string toStringNoVerbose(std::vector<ValueType> const& vector) {
+    std::stringstream stream;
+    stream << "(";
+    if (!vector.empty()) {
+        for (uint_fast64_t i = 0; i < vector.size() - 1; ++i) {
+            stream << vector[i] << ",";
+        }
+        stream << vector.back();
+    }
+    stream << ")";
+    return stream.str();
+}
 }  // namespace vector
 }  // namespace utility
 }  // namespace storm