diff --git a/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp b/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp
index 919328b9a..75a2c0008 100644
--- a/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp
+++ b/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp
@@ -11,6 +11,7 @@
 
 #include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h"
 #include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.h"
+#include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.h"
 
 #include "src/exceptions/NotImplementedException.h"
 
@@ -33,19 +34,21 @@ namespace storm {
         
         template<typename SparseMdpModelType>
         std::unique_ptr<CheckResult> SparseMdpMultiObjectiveModelChecker<SparseMdpModelType>::checkMultiObjectiveFormula(CheckTask<storm::logic::MultiObjectiveFormula> const& checkTask) {
+            std::unique_ptr<CheckResult> result;
             
-            auto preprocessedData = helper::SparseMultiObjectivePreprocessor<SparseMdpModelType>::preprocess(checkTask.getFormula(), this->getModel());
+#ifdef STORM_HAVE_CARL
+            auto preprocessorData = helper::SparseMultiObjectivePreprocessor<SparseMdpModelType>::preprocess(checkTask.getFormula(), this->getModel());
             std::cout << std::endl;
             std::cout << "Preprocessing done." << std::endl;
-            preprocessedData.printToStream(std::cout);
-            
-#ifdef STORM_HAVE_CARL
-            helper::SparseMultiObjectiveHelper<SparseMdpModelType, storm::RationalNumber>::check(preprocessedData);
+            preprocessorData.printToStream(std::cout);
+            auto resultData = helper::SparseMultiObjectiveHelper<SparseMdpModelType, storm::RationalNumber>::check(preprocessorData);
+            std::cout << "Modelchecking done." << std::endl;
+            result = helper::SparseMultiObjectivePostprocessor<SparseMdpModelType, storm::RationalNumber>::postprocess(preprocessorData, resultData);
+            std::cout << "Postprocessing done." << std::endl;
 #else
             STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Multi objective model checking requires carl.");
 #endif
-            
-            return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult());
+            return result;
         }
         
         
diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp
index 65b2c3123..62f48ce42 100644
--- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp
+++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.cpp
@@ -3,6 +3,7 @@
 #include "src/adapters/CarlAdapter.h"
 #include "src/models/sparse/Mdp.h"
 #include "src/models/sparse/StandardRewardModel.h"
+#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveObjectiveInformation.h"
 #include "src/utility/constants.h"
 #include "src/utility/vector.h"
 #include "src/settings//SettingsManager.h"
@@ -16,94 +17,92 @@ namespace storm {
             
             
             template <class SparseModelType, typename RationalNumberType>
-            typename SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::ReturnType SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::check(PreprocessorData const& data) {
-                ReturnType result;
-                result.overApproximation() = storm::storage::geometry::Polytope<RationalNumberType>::createUniversalPolytope();
-                result.underApproximation() = storm::storage::geometry::Polytope<RationalNumberType>::createEmptyPolytope();
+            typename SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::ResultData SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::check(PreprocessorData const& preprocessorData) {
+                ResultData resultData;
+                resultData.overApproximation() = storm::storage::geometry::Polytope<RationalNumberType>::createUniversalPolytope();
+                resultData.underApproximation() = storm::storage::geometry::Polytope<RationalNumberType>::createEmptyPolytope();
                 
-                uint_fast64_t numOfObjectivesWithoutThreshold = 0;
-                for(auto const& obj : data.objectives) {
-                    if(!obj.threshold) {
-                        ++numOfObjectivesWithoutThreshold;
-                    }
-                }
-                if(numOfObjectivesWithoutThreshold == 0) {
-                    achievabilityQuery(data, result);
-                } else if (numOfObjectivesWithoutThreshold == 1) {
-                    numericalQuery(data, result);
-                } else if (numOfObjectivesWithoutThreshold == data.objectives.size()) {
-                    paretoQuery(data, result);
-                } else {
-                    STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "The number of objecties without threshold is not valid. It should be either 0 (achievabilityQuery), 1 (numericalQuery), or " << data.objectives.size() << " (paretoQuery). Got " << numOfObjectivesWithoutThreshold << " instead.");
+                switch(preprocessorData.queryType) {
+                    case PreprocessorData::QueryType::Achievability:
+                        achievabilityQuery(preprocessorData, resultData);
+                        break;
+                    case PreprocessorData::QueryType::Numerical:
+                        numericalQuery(preprocessorData, resultData);
+                        break;
+                    case PreprocessorData::QueryType::Pareto:
+                        paretoQuery(preprocessorData, resultData);
+                        break;
+                    default:
+                        STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unknown Query Type");
                 }
-                return result;
+                return resultData;
             }
             
             template <class SparseModelType, typename RationalNumberType>
-            void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::achievabilityQuery(PreprocessorData const& data, ReturnType& result) {
+            void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::achievabilityQuery(PreprocessorData const& preprocessorData, ResultData& resultData) {
                 Point thresholds;
-                thresholds.reserve(data.objectives.size());
-                storm::storage::BitVector strictThresholds(data.objectives.size());
-                for(uint_fast64_t objIndex = 0; objIndex < data.objectives.size(); ++objIndex) {
-                    thresholds.push_back(storm::utility::convertNumber<RationalNumberType>(*data.objectives[objIndex].threshold));
-                    strictThresholds.set(objIndex, data.objectives[objIndex].thresholdIsStrict);
+                thresholds.reserve(preprocessorData.objectives.size());
+                storm::storage::BitVector strictThresholds(preprocessorData.objectives.size());
+                for(uint_fast64_t objIndex = 0; objIndex < preprocessorData.objectives.size(); ++objIndex) {
+                    thresholds.push_back(storm::utility::convertNumber<RationalNumberType>(*preprocessorData.objectives[objIndex].threshold));
+                    strictThresholds.set(objIndex, preprocessorData.objectives[objIndex].thresholdIsStrict);
                 }
                 
-                storm::storage::BitVector individualObjectivesToBeChecked(data.objectives.size(), true);
-                SparseMultiObjectiveWeightVectorChecker<SparseModelType> weightVectorChecker(data);
+                storm::storage::BitVector individualObjectivesToBeChecked(preprocessorData.objectives.size(), true);
+                SparseMultiObjectiveWeightVectorChecker<SparseModelType> weightVectorChecker(preprocessorData);
                 do {
-                    WeightVector separatingVector = findSeparatingVector(thresholds, result.underApproximation(), individualObjectivesToBeChecked);
-                    performRefinementStep(separatingVector, data.produceSchedulers, weightVectorChecker, result);
-                    if(!checkIfThresholdsAreSatisfied(result.overApproximation(), thresholds, strictThresholds)){
-                        result.setThresholdsAreAchievable(false);
+                    WeightVector separatingVector = findSeparatingVector(thresholds, resultData.underApproximation(), individualObjectivesToBeChecked);
+                    performRefinementStep(separatingVector, preprocessorData.produceSchedulers, weightVectorChecker, resultData);
+                    if(!checkIfThresholdsAreSatisfied(resultData.overApproximation(), thresholds, strictThresholds)){
+                        resultData.setThresholdsAreAchievable(false);
                     }
-                    if(checkIfThresholdsAreSatisfied(result.underApproximation(), thresholds, strictThresholds)){
-                        result.setThresholdsAreAchievable(true);
+                    if(checkIfThresholdsAreSatisfied(resultData.underApproximation(), thresholds, strictThresholds)){
+                        resultData.setThresholdsAreAchievable(true);
                     }
-                } while(!result.isThresholdsAreAchievableSet() && !maxStepsPerformed(result));
+                } while(!resultData.isThresholdsAreAchievableSet() && !maxStepsPerformed(resultData));
             }
             
             template <class SparseModelType, typename RationalNumberType>
-            void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::numericalQuery(PreprocessorData const& data, ReturnType& result) {
+            void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::numericalQuery(PreprocessorData const& preprocessorData, ResultData& resultData) {
+                STORM_LOG_ASSERT(preprocessorData.indexOfOptimizingObjective, "Detected numerical query but index of optimizing objective is not set.");
+                uint_fast64_t optimizingObjIndex = *preprocessorData.indexOfOptimizingObjective;
                 Point thresholds;
-                thresholds.reserve(data.objectives.size());
-                storm::storage::BitVector strictThresholds(data.objectives.size());
+                thresholds.reserve(preprocessorData.objectives.size());
+                storm::storage::BitVector strictThresholds(preprocessorData.objectives.size());
                 std::vector<storm::storage::geometry::Halfspace<RationalNumberType>> thresholdConstraints;
-                thresholdConstraints.reserve(data.objectives.size()-1);
-                uint_fast64_t optimizingObjIndex = data.objectives.size(); // init with invalid value...
-                for(uint_fast64_t objIndex = 0; objIndex < data.objectives.size(); ++objIndex) {
-                    if(data.objectives[objIndex].threshold) {
-                        thresholds.push_back(storm::utility::convertNumber<RationalNumberType>(*data.objectives[objIndex].threshold));
-                        WeightVector normalVector(data.objectives.size(), storm::utility::zero<RationalNumberType>());
+                thresholdConstraints.reserve(preprocessorData.objectives.size()-1);
+                for(uint_fast64_t objIndex = 0; objIndex < preprocessorData.objectives.size(); ++objIndex) {
+                    if(preprocessorData.objectives[objIndex].threshold) {
+                        thresholds.push_back(storm::utility::convertNumber<RationalNumberType>(*preprocessorData.objectives[objIndex].threshold));
+                        WeightVector normalVector(preprocessorData.objectives.size(), storm::utility::zero<RationalNumberType>());
                         normalVector[objIndex] = -storm::utility::one<RationalNumberType>();
                         thresholdConstraints.emplace_back(std::move(normalVector), -thresholds.back());
-                        strictThresholds.set(objIndex, data.objectives[objIndex].thresholdIsStrict);
+                        strictThresholds.set(objIndex, preprocessorData.objectives[objIndex].thresholdIsStrict);
                     } else {
-                        optimizingObjIndex = objIndex;
                         thresholds.push_back(storm::utility::zero<RationalNumberType>());
                     }
                 }
                 auto thresholdsAsPolytope = storm::storage::geometry::Polytope<RationalNumberType>::create(thresholdConstraints);
-                WeightVector directionOfOptimizingObjective(data.objectives.size(), storm::utility::zero<RationalNumberType>());
+                WeightVector directionOfOptimizingObjective(preprocessorData.objectives.size(), storm::utility::zero<RationalNumberType>());
                 directionOfOptimizingObjective[optimizingObjIndex] = storm::utility::one<RationalNumberType>();
                 
                 // Try to find one valid solution
-                storm::storage::BitVector individualObjectivesToBeChecked(data.objectives.size(), true);
+                storm::storage::BitVector individualObjectivesToBeChecked(preprocessorData.objectives.size(), true);
                 individualObjectivesToBeChecked.set(optimizingObjIndex, false);
-                SparseMultiObjectiveWeightVectorChecker<SparseModelType> weightVectorChecker(data);
+                SparseMultiObjectiveWeightVectorChecker<SparseModelType> weightVectorChecker(preprocessorData);
                 do {
-                    WeightVector separatingVector = findSeparatingVector(thresholds, result.underApproximation(), individualObjectivesToBeChecked);
-                    performRefinementStep(separatingVector, data.produceSchedulers, weightVectorChecker, result);
+                    WeightVector separatingVector = findSeparatingVector(thresholds, resultData.underApproximation(), individualObjectivesToBeChecked);
+                    performRefinementStep(separatingVector, preprocessorData.produceSchedulers, weightVectorChecker, resultData);
                     //Pick the threshold for the optimizing objective low enough so valid solutions are not excluded
-                    thresholds[optimizingObjIndex] = std::min(thresholds[optimizingObjIndex], result.refinementSteps().back().getPoint()[optimizingObjIndex]);
-                    if(!checkIfThresholdsAreSatisfied(result.overApproximation(), thresholds, strictThresholds)){
-                        result.setThresholdsAreAchievable(false);
+                    thresholds[optimizingObjIndex] = std::min(thresholds[optimizingObjIndex], resultData.refinementSteps().back().getPoint()[optimizingObjIndex]);
+                    if(!checkIfThresholdsAreSatisfied(resultData.overApproximation(), thresholds, strictThresholds)){
+                        resultData.setThresholdsAreAchievable(false);
                     }
-                    if(checkIfThresholdsAreSatisfied(result.underApproximation(), thresholds, strictThresholds)){
-                        result.setThresholdsAreAchievable(true);
+                    if(checkIfThresholdsAreSatisfied(resultData.underApproximation(), thresholds, strictThresholds)){
+                        resultData.setThresholdsAreAchievable(true);
                     }
-                } while(!result.isThresholdsAreAchievableSet() && !maxStepsPerformed(result));
-                if(result.getThresholdsAreAchievable()) {
+                } while(!resultData.isThresholdsAreAchievableSet() && !maxStepsPerformed(resultData));
+                if(resultData.getThresholdsAreAchievable()) {
                     STORM_LOG_DEBUG("Found a solution that satisfies the objective thresholds.");
                     individualObjectivesToBeChecked.clear();
                     // Improve the found solution.
@@ -111,41 +110,41 @@ namespace storm {
                     // the supremum over all strategies. Hence, one could combine a scheduler inducing the optimum value (but possibly violating strict
                     // thresholds) and (with very low probability) a scheduler that satisfies all (possibly strict) thresholds.
                     while(true) {
-                        std::pair<Point, bool> optimizationRes = result.underApproximation()->intersection(thresholdsAsPolytope)->optimize(directionOfOptimizingObjective);
+                        std::pair<Point, bool> optimizationRes = resultData.underApproximation()->intersection(thresholdsAsPolytope)->optimize(directionOfOptimizingObjective);
                         STORM_LOG_THROW(optimizationRes.second, storm::exceptions::UnexpectedException, "The underapproximation is either unbounded or empty.");
                         thresholds[optimizingObjIndex] = optimizationRes.first[optimizingObjIndex];
-                        result.setNumericalResult(thresholds[optimizingObjIndex]);
-                        STORM_LOG_DEBUG("Best solution found so far is " << result.template getNumericalResult<double>() << ".");
+                        resultData.setNumericalResult(thresholds[optimizingObjIndex]);
+                        STORM_LOG_DEBUG("Best solution found so far is " << resultData.template getNumericalResult<double>() << ".");
                         //Compute an upper bound for the optimum and check for convergence
-                        optimizationRes = result.overApproximation()->intersection(thresholdsAsPolytope)->optimize(directionOfOptimizingObjective);
+                        optimizationRes = resultData.overApproximation()->intersection(thresholdsAsPolytope)->optimize(directionOfOptimizingObjective);
                         if(optimizationRes.second) {
-                            result.setPrecisionOfResult(optimizationRes.first[optimizingObjIndex] - thresholds[optimizingObjIndex]);
-                            STORM_LOG_DEBUG("Solution can be improved by at most " << result.template getPrecisionOfResult<double>());
+                            resultData.setPrecisionOfResult(optimizationRes.first[optimizingObjIndex] - thresholds[optimizingObjIndex]);
+                            STORM_LOG_DEBUG("Solution can be improved by at most " << resultData.template getPrecisionOfResult<double>());
                         }
-                        if(targetPrecisionReached(result) || maxStepsPerformed(result)) {
-                            result.setOptimumIsAchievable(checkIfThresholdsAreSatisfied(result.underApproximation(), thresholds, strictThresholds));
+                        if(targetPrecisionReached(resultData) || maxStepsPerformed(resultData)) {
+                            resultData.setOptimumIsAchievable(checkIfThresholdsAreSatisfied(resultData.underApproximation(), thresholds, strictThresholds));
                             break;
                         }
-                        WeightVector separatingVector = findSeparatingVector(thresholds, result.underApproximation(), individualObjectivesToBeChecked);
-                        performRefinementStep(separatingVector, data.produceSchedulers, weightVectorChecker, result);
+                        WeightVector separatingVector = findSeparatingVector(thresholds, resultData.underApproximation(), individualObjectivesToBeChecked);
+                        performRefinementStep(separatingVector, preprocessorData.produceSchedulers, weightVectorChecker, resultData);
                     }
                 }
             }
             
             template <class SparseModelType, typename RationalNumberType>
-            void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::paretoQuery(PreprocessorData const& data, ReturnType& result) {
-                SparseMultiObjectiveWeightVectorChecker<SparseModelType> weightVectorChecker(data);
+            void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::paretoQuery(PreprocessorData const& preprocessorData, ResultData& resultData) {
+                SparseMultiObjectiveWeightVectorChecker<SparseModelType> weightVectorChecker(preprocessorData);
                 //First consider the objectives individually
-                for(uint_fast64_t objIndex = 0; objIndex<data.objectives.size() && !maxStepsPerformed(result); ++objIndex) {
-                    WeightVector direction(data.objectives.size(), storm::utility::zero<RationalNumberType>());
+                for(uint_fast64_t objIndex = 0; objIndex<preprocessorData.objectives.size() && !maxStepsPerformed(resultData); ++objIndex) {
+                    WeightVector direction(preprocessorData.objectives.size(), storm::utility::zero<RationalNumberType>());
                     direction[objIndex] = storm::utility::one<RationalNumberType>();
-                    performRefinementStep(direction, data.produceSchedulers, weightVectorChecker, result);
+                    performRefinementStep(direction, preprocessorData.produceSchedulers, weightVectorChecker, resultData);
                 }
                 
                 while(true) {
                     // Get the halfspace of the underApproximation with maximal distance to a vertex of the overApproximation
-                    std::vector<storm::storage::geometry::Halfspace<RationalNumberType>> underApproxHalfspaces = result.underApproximation()->getHalfspaces();
-                    std::vector<Point> overApproxVertices = result.overApproximation()->getVertices();
+                    std::vector<storm::storage::geometry::Halfspace<RationalNumberType>> underApproxHalfspaces = resultData.underApproximation()->getHalfspaces();
+                    std::vector<Point> overApproxVertices = resultData.overApproximation()->getVertices();
                     uint_fast64_t farestHalfspaceIndex = underApproxHalfspaces.size();
                     RationalNumberType farestDistance = storm::utility::zero<RationalNumberType>();
                     for(uint_fast64_t halfspaceIndex = 0; halfspaceIndex < underApproxHalfspaces.size(); ++halfspaceIndex) {
@@ -157,13 +156,13 @@ namespace storm {
                             }
                         }
                     }
-                    result.setPrecisionOfResult(farestDistance);
-                    STORM_LOG_DEBUG("Current precision of the approximation of the pareto curve is " << result.template getPrecisionOfResult<double>());
-                    if(targetPrecisionReached(result) || maxStepsPerformed(result)) {
+                    resultData.setPrecisionOfResult(farestDistance);
+                    STORM_LOG_DEBUG("Current precision of the approximation of the pareto curve is " << resultData.template getPrecisionOfResult<double>());
+                    if(targetPrecisionReached(resultData) || maxStepsPerformed(resultData)) {
                         break;
                     }
                     WeightVector direction = underApproxHalfspaces[farestHalfspaceIndex].normalVector();
-                    performRefinementStep(direction, data.produceSchedulers, weightVectorChecker, result);
+                    performRefinementStep(direction, preprocessorData.produceSchedulers, weightVectorChecker, resultData);
                 }
             }
             
@@ -211,7 +210,7 @@ namespace storm {
             }
             
             template <class SparseModelType, typename RationalNumberType>
-            void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::performRefinementStep(WeightVector const& direction, bool saveScheduler, SparseMultiObjectiveWeightVectorChecker<SparseModelType>& weightVectorChecker, ReturnType& result) {
+            void SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::performRefinementStep(WeightVector const& direction, bool saveScheduler, SparseMultiObjectiveWeightVectorChecker<SparseModelType>& weightVectorChecker, ResultData& result) {
                 weightVectorChecker.check(storm::utility::vector::convertNumericVector<typename SparseModelType::ValueType>(direction));
                 STORM_LOG_DEBUG("weighted objectives checker result is " << weightVectorChecker.getInitialStateResultOfObjectives());
                 if(saveScheduler) {
@@ -306,17 +305,17 @@ namespace storm {
             }
             
             template <class SparseModelType, typename RationalNumberType>
-            bool SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::targetPrecisionReached(ReturnType& result) {
-                result.setTargetPrecisionReached(result.isPrecisionOfResultSet() &&
-                                                 result.getPrecisionOfResult() < storm::utility::convertNumber<RationalNumberType>(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getPrecision()));
-                return result.getTargetPrecisionReached();
+            bool SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::targetPrecisionReached(ResultData& resultData) {
+                resultData.setTargetPrecisionReached(resultData.isPrecisionOfResultSet() &&
+                                                 resultData.getPrecisionOfResult() < storm::utility::convertNumber<RationalNumberType>(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getPrecision()));
+                return resultData.getTargetPrecisionReached();
             }
             
             template <class SparseModelType, typename RationalNumberType>
-            bool SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::maxStepsPerformed(ReturnType& result) {
-                result.setMaxStepsPerformed(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().isMaxStepsSet() &&
-                                            result.refinementSteps().size() >= storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getMaxSteps());
-                return result.getMaxStepsPerformed();
+            bool SparseMultiObjectiveHelper<SparseModelType, RationalNumberType>::maxStepsPerformed(ResultData& resultData) {
+                resultData.setMaxStepsPerformed(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().isMaxStepsSet() &&
+                                            resultData.refinementSteps().size() >= storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getMaxSteps());
+                return resultData.getMaxStepsPerformed();
             }
             
 #ifdef STORM_HAVE_CARL
diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.h
index 0d13bdb00..4ada316e5 100644
--- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.h
+++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelper.h
@@ -1,9 +1,9 @@
 #ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEHELPER_H_
 #define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEHELPER_H_
 
-#include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorReturnType.h"
-#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelperReturnType.h"
-#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelperRefinementStep.h"
+#include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h"
+#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveResultData.h"
+#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveRefinementStep.h"
 #include "src/modelchecker/multiObjective/helper/SparseMultiObjectiveWeightVectorChecker.h"
 #include "src/storage/geometry/Polytope.h"
 #include "src/storage/TotalScheduler.h"
@@ -16,20 +16,20 @@ namespace storm {
             template <class SparseModelType, typename RationalNumberType>
             class SparseMultiObjectiveHelper {
             public:
-                typedef SparseMultiObjectivePreprocessorReturnType<SparseModelType> PreprocessorData;
-                typedef SparseMultiObjectiveHelperReturnType<RationalNumberType> ReturnType;
-                typedef SparseMultiObjectiveHelperRefinementStep<RationalNumberType> RefinementStep;
+                typedef SparseMultiObjectivePreprocessorData<SparseModelType> PreprocessorData;
+                typedef SparseMultiObjectiveResultData<RationalNumberType> ResultData;
+                typedef SparseMultiObjectiveRefinementStep<RationalNumberType> RefinementStep;
                 
                 typedef std::vector<RationalNumberType> Point;
                 typedef std::vector<RationalNumberType> WeightVector;
                 
-                static ReturnType check(PreprocessorData const& data);
+                static ResultData check(PreprocessorData const& preprocessorData);
                 
             private:
                 
-                static void achievabilityQuery(PreprocessorData const& data, ReturnType& result);
-                static void numericalQuery(PreprocessorData const& data, ReturnType& result);
-                static void paretoQuery(PreprocessorData const& data, ReturnType& result);
+                static void achievabilityQuery(PreprocessorData const& preprocessorData, ResultData& resultData);
+                static void numericalQuery(PreprocessorData const& preprocessorData, ResultData& resultData);
+                static void paretoQuery(PreprocessorData const& preprocessorData, ResultData& resultData);
                 
                 /*
                  * Returns a weight vector w that separates the under approximation from the given point p, i.e.,
@@ -44,7 +44,7 @@ namespace storm {
                 /*
                  * Refines the current result w.r.t. the given direction vector
                  */
-                static void performRefinementStep(WeightVector const& direction, bool saveScheduler, SparseMultiObjectiveWeightVectorChecker<SparseModelType>& weightVectorChecker, ReturnType& result);
+                static void performRefinementStep(WeightVector const& direction, bool saveScheduler, SparseMultiObjectiveWeightVectorChecker<SparseModelType>& weightVectorChecker, ResultData& resultData);
                 
                 /*
                  * Updates the overapproximation after a refinement step has been performed
@@ -70,16 +70,16 @@ namespace storm {
                 
                 /*
                  * Returns whether the desired precision (as given in the settings) is reached by the current result.
-                 * If the given result does not specify a precisionOfResult, false is returned.
-                 * Also sets the result.targetPrecisionReached flag accordingly.
+                 * If the given resultData does not specify a precisionOfResult, false is returned.
+                 * Also sets the resultData.targetPrecisionReached flag accordingly.
                  */
-                static bool targetPrecisionReached(ReturnType& result);
+                static bool targetPrecisionReached(ResultData& resultData);
                 
                 /*
                  * Returns whether a maximum number of refinement steps is given in the settings and this threshold has been reached.
-                 * Also sets the result.maxStepsPerformed flag accordingly.
+                 * Also sets the resultData.maxStepsPerformed flag accordingly.
                  */
-                static bool maxStepsPerformed(ReturnType& result);
+                static bool maxStepsPerformed(ResultData& resultData);
             };
             
         }
diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveObjectiveInformation.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveObjectiveInformation.h
new file mode 100644
index 000000000..50660d133
--- /dev/null
+++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveObjectiveInformation.h
@@ -0,0 +1,63 @@
+#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEOBJECTIVEINFORMATION_H_
+#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEOBJECTIVEINFORMATION_H_
+
+#include <iomanip>
+#include <boost/optional.hpp>
+
+#include "src/logic/Formulas.h"
+
+namespace storm {
+    namespace modelchecker {
+        namespace helper {
+            template <typename ValueType>
+            struct SparseMultiObjectiveObjectiveInformation {
+                // the original input formula
+                std::shared_ptr<storm::logic::Formula const> originalFormula;
+                
+                // the name of the considered reward model in the preprocessedModel
+                std::string rewardModelName;
+                
+                // true if all rewards for this objective are positive, false if all rewards are negative.
+                bool rewardsArePositive;
+                
+                // transformation from the values of the preprocessed model to the ones for the actual input model, i.e.,
+                // x is achievable in the preprocessed model iff factor*x + offset is achievable in the original model
+                ValueType toOriginalValueTransformationFactor;
+                ValueType toOriginalValueTransformationOffset;
+                
+                // The probability/reward threshold for the preprocessed model (if originalFormula specifies one).
+                // This is always a lower bound.
+                boost::optional<ValueType> threshold;
+                // True iff the specified threshold is strict, i.e., >
+                bool thresholdIsStrict = false;
+                
+                // The (discrete) stepBound for the formula (if given by the originalFormula)
+                boost::optional<uint_fast64_t> stepBound;
+                
+                void printToStream(std::ostream& out) const {
+                    out << std::setw(30) << originalFormula->toString();
+                    out << " \t(toOrigVal:" << std::setw(3) << toOriginalValueTransformationFactor << "*x +" << std::setw(3) << toOriginalValueTransformationOffset << ", \t";
+                    out << "intern threshold:";
+                    if(threshold){
+                        out << (thresholdIsStrict ? " >" : ">=");
+                        out << std::setw(5) << (*threshold) << ",";
+                    } else {
+                        out << "   none,";
+                    }
+                    out << " \t";
+                    out << "intern reward model: " << std::setw(10) << rewardModelName;
+                    out << (rewardsArePositive ? " (positive)" : " (negative)") << ", \t";
+                    out << "step bound:";
+                    if(stepBound) {
+                        out << std::setw(5) << (*stepBound);
+                    } else {
+                        out << " none";
+                    }
+                    out << ")" << std::endl;
+                 }
+            };
+        }
+    }
+}
+
+#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEOBJECTIVEINFORMATION_H_ */
diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp
new file mode 100644
index 000000000..b1af9b9ab
--- /dev/null
+++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp
@@ -0,0 +1,57 @@
+ #include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.h"
+
+#include "src/adapters/CarlAdapter.h"
+#include "src/models/sparse/Mdp.h"
+#include "src/models/sparse/StandardRewardModel.h"
+#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
+#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+#include "src/storage/geometry/Polytope.h"
+#include "src/utility/macros.h"
+#include "src/utility/vector.h"
+
+#include "src/exceptions/UnexpectedException.h"
+
+namespace storm {
+    namespace modelchecker {
+        namespace helper {
+            
+            template<typename SparseModelType, typename RationalNumberType>
+            typename std::unique_ptr<CheckResult> SparseMultiObjectivePostprocessor<SparseModelType, RationalNumberType>::postprocess(PreprocessorData const& preprocessorData, ResultData const& resultData) {
+                STORM_LOG_ASSERT(preprocessor.
+                switch(preprocessorData.queryType) {
+                    case PreprocessorData::QueryType::Achievability:
+                        return postprocessAchievabilityQuery(preprocessorData, resultData);
+                    case PreprocessorData::QueryType::Numerical:
+                        return postprocessNumericalQuery(preprocessorData, resultData);
+                    case PreprocessorData::QueryType::Pareto:
+                        return postprocessParetoQuery(preprocessorData, resultData);
+                    default:
+                        STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unknown Query Type");
+                }
+                
+                  return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult());;
+            }
+            
+            template<typename SparseModelType, typename RationalNumberType>
+            typename std::unique_ptr<CheckResult> SparseMultiObjectivePostprocessor<SparseModelType, RationalNumberType>::postprocessAchievabilityQuery(PreprocessorData const& preprocessorData, ResultData const& resultData) {
+            
+            }
+            
+            template<typename SparseModelType, typename RationalNumberType>
+            typename std::unique_ptr<CheckResult> SparseMultiObjectivePostprocessor<SparseModelType, RationalNumberType>::postprocessNumericalQuery(PreprocessorData const& preprocessorData, ResultData const& resultData) {
+            
+            }
+            
+            template<typename SparseModelType, typename RationalNumberType>
+            typename std::unique_ptr<CheckResult> SparseMultiObjectivePostprocessor<SparseModelType, RationalNumberType>::postprocessParetoQuery(PreprocessorData const& preprocessorData, ResultData const& resultData) {
+            
+                std::cout << "Postprocessing pareto queries not yet implemented";
+            }
+            
+#ifdef STORM_HAVE_CARL
+            template class SparseMultiObjectivePostprocessor<storm::models::sparse::Mdp<double>, storm::RationalNumber>;
+#endif
+            
+        }
+    }
+}
diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.h
new file mode 100644
index 000000000..75a40fbfb
--- /dev/null
+++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.h
@@ -0,0 +1,48 @@
+#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPOSTPROCESSOR_H_
+#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPOSTPROCESSOR_H_
+
+
+#include <memory>
+
+#include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h"
+#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveResultData.h"
+#include "src/modelchecker/results/CheckResult.h"
+
+namespace storm {
+    namespace modelchecker {
+        namespace helper {
+            
+            /*
+             * Helper Class to invoke the necessary preprocessing for multi objective model checking
+             */
+            template <class SparseModelType, typename RationalNumberType>
+            class SparseMultiObjectivePostprocessor {
+            public:
+                typedef typename SparseModelType::ValueType ValueType;
+                typedef typename SparseModelType::RewardModelType RewardModelType;
+                
+                typedef SparseMultiObjectiveObjectiveInformation<ValueType> ObjectiveInformation;
+                typedef SparseMultiObjectivePreprocessorData<SparseModelType> PreprocessorData;
+                typedef SparseMultiObjectiveResultData<RationalNumberType> ResultData;
+                
+                /*!
+                 * Postprocesses the multi objective model checking result.
+                 *
+                 * @param preprocessorData the data of the preprocessing
+                 * @param resultData the data of the model checking
+                 */
+                static std::unique_ptr<CheckResult> postprocess(PreprocessorData const& preprocessorData, ResultData const& resultData);
+                
+            private:
+                static std::unique_ptr<CheckResult> postprocessAchievabilityQuery(PreprocessorData const& preprocessorData, ResultData const& resultData);
+                static std::unique_ptr<CheckResult> postprocessNumericalQuery(PreprocessorData const& preprocessorData, ResultData const& resultData);
+                static std::unique_ptr<CheckResult> postprocessParetoQuery(PreprocessorData const& preprocessorData, ResultData const& resultData);
+                
+                
+            };
+            
+        }
+    }
+}
+
+#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPOSTPROCESSOR_H_ */
diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp
index 29f1b3edb..a3da9b1d4 100644
--- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp
+++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.cpp
@@ -11,15 +11,15 @@
 #include "src/utility/graph.h"
 
 #include "src/exceptions/InvalidPropertyException.h"
-#include "src/exceptions/NotImplementedException.h"
+#include "src/exceptions/UnexpectedException.h"
 
 namespace storm {
     namespace modelchecker {
         namespace helper {
             
             template<typename SparseModelType>
-            typename SparseMultiObjectivePreprocessor<SparseModelType>::ReturnType SparseMultiObjectivePreprocessor<SparseModelType>::preprocess(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel) {
-                ReturnType data(std::move(originalModel));
+            typename SparseMultiObjectivePreprocessor<SparseModelType>::PreprocessorData SparseMultiObjectivePreprocessor<SparseModelType>::preprocess(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel) {
+                PreprocessorData data(std::move(originalModel));
                 //Initialize the state mapping.
                 data.newToOldStateIndexMapping = storm::utility::vector::buildVectorForRange(0, data.preprocessedModel.getNumberOfStates());
                 //Invoke preprocessing on the individual objectives
@@ -40,11 +40,28 @@ namespace storm {
                 for (auto const& rewModel : origRewardModels){
                     data.preprocessedModel.removeRewardModel(rewModel);
                 }
+                
+                //Set the query type. In case of a numerical query, also set the index of the objective to be optimized.
+                storm::storage::BitVector objectivesWithoutThreshold(data.objectives.size());
+                for(uint_fast64_t objIndex = 0; objIndex < data.objectives.size(); ++objIndex) {
+                    objectivesWithoutThreshold.set(objIndex, !data.objectives[objIndex].threshold);
+                }
+                uint_fast64_t numOfObjectivesWithoutThreshold = objectivesWithoutThreshold.getNumberOfSetBits();
+                if(numOfObjectivesWithoutThreshold == 0) {
+                    data.queryType = PreprocessorData::QueryType::Achievability;
+                } else if (numOfObjectivesWithoutThreshold == 1) {
+                    data.queryType = PreprocessorData::QueryType::Numerical;
+                    data.indexOfOptimizingObjective = objectivesWithoutThreshold.getNextSetIndex(0);
+                } else if (numOfObjectivesWithoutThreshold == data.objectives.size()) {
+                    data.queryType = PreprocessorData::QueryType::Pareto;
+                } else {
+                    STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "The number of objecties without threshold is not valid. It should be either 0 (achievabilityQuery), 1 (numericalQuery), or " << data.objectives.size() << " (paretoQuery). Got " << numOfObjectivesWithoutThreshold << " instead.");
+                }
                 return data;
             }
             
             template<typename SparseModelType>
-            void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::OperatorFormula const& formula, ReturnType& data, ObjectiveInformation& currentObjective) {
+            void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::OperatorFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective) {
                 
                 // Get a unique name for the new reward model.
                 currentObjective.rewardModelName = "objective" + std::to_string(data.objectives.size());
@@ -88,7 +105,7 @@ namespace storm {
             }
             
             template<typename SparseModelType>
-            void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::ProbabilityOperatorFormula const& formula, ReturnType& data, ObjectiveInformation& currentObjective) {
+            void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::ProbabilityOperatorFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective) {
                 if(formula.getSubformula().isUntilFormula()){
                     preprocessFormula(formula.getSubformula().asUntilFormula(), data, currentObjective);
                 } else if(formula.getSubformula().isBoundedUntilFormula()){
@@ -103,7 +120,7 @@ namespace storm {
             }
 
             template<typename SparseModelType>
-            void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::RewardOperatorFormula const& formula, ReturnType& data, ObjectiveInformation& currentObjective) {
+            void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::RewardOperatorFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective) {
                 // Check if the reward model is uniquely specified
                 STORM_LOG_THROW((formula.hasRewardModelName() && data.preprocessedModel.hasRewardModel(formula.getRewardModelName()))
                                 || data.preprocessedModel.hasUniqueRewardModel(), storm::exceptions::InvalidPropertyException, "The reward model is not unique and the formula " << formula << " does not specify a reward model.");
@@ -117,7 +134,7 @@ namespace storm {
             }
             
             template<typename SparseModelType>
-            void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::UntilFormula const& formula, ReturnType& data, ObjectiveInformation& currentObjective) {
+            void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::UntilFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective) {
                 CheckTask<storm::logic::Formula> phiTask(formula.getLeftSubformula());
                 CheckTask<storm::logic::Formula> psiTask(formula.getRightSubformula());
                 storm::modelchecker::SparsePropositionalModelChecker<SparseModelType> mc(data.preprocessedModel);
@@ -153,14 +170,14 @@ namespace storm {
             }
             
             template<typename SparseModelType>
-            void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::BoundedUntilFormula const& formula, ReturnType& data, ObjectiveInformation& currentObjective) {
+            void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::BoundedUntilFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective) {
                 STORM_LOG_THROW(formula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Expected a boundedUntilFormula with a discrete time bound but got " << formula << ".");
                 currentObjective.stepBound = formula.getDiscreteTimeBound();
                     preprocessFormula(storm::logic::UntilFormula(formula.getLeftSubformula().asSharedPointer(), formula.getRightSubformula().asSharedPointer()), data, currentObjective);
             }
             
             template<typename SparseModelType>
-            void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::GloballyFormula const& formula, ReturnType& data, ObjectiveInformation& currentObjective) {
+            void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::GloballyFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective) {
                 // The formula will be transformed to an until formula for the complementary event.
                 // If the original formula minimizes, the complementary one will maximize and vice versa.
                 // Hence, the decision whether to consider positive or negative rewards flips.
@@ -177,7 +194,7 @@ namespace storm {
             }
             
             template<typename SparseModelType>
-            void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::EventuallyFormula const& formula, ReturnType& data, ObjectiveInformation& currentObjective, boost::optional<std::string> const& optionalRewardModelName) {
+            void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::EventuallyFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, boost::optional<std::string> const& optionalRewardModelName) {
                 if(formula.isReachabilityProbabilityFormula()){
                     preprocessFormula(storm::logic::UntilFormula(storm::logic::Formula::getTrueFormula(), formula.getSubformula().asSharedPointer()), data, currentObjective);
                     return;
@@ -212,7 +229,7 @@ namespace storm {
             }
             
             template<typename SparseModelType>
-            void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::CumulativeRewardFormula const& formula, ReturnType& data, ObjectiveInformation& currentObjective, boost::optional<std::string> const& optionalRewardModelName) {
+            void SparseMultiObjectivePreprocessor<SparseModelType>::preprocessFormula(storm::logic::CumulativeRewardFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, boost::optional<std::string> const& optionalRewardModelName) {
                 STORM_LOG_THROW(formula.hasDiscreteTimeBound(), storm::exceptions::InvalidPropertyException, "Expected a cumulativeRewardFormula with a discrete time bound but got " << formula << ".");
                 currentObjective.stepBound = formula.getDiscreteTimeBound();
                 
diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h
index 8226d0dc0..580fbeef0 100644
--- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h
+++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessor.h
@@ -2,7 +2,7 @@
 #define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPREPROCESSOR_H_
 
 #include "src/logic/Formulas.h"
-#include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorReturnType.h"
+#include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h"
 
 namespace storm {
     namespace modelchecker {
@@ -18,15 +18,15 @@ namespace storm {
             public:
                 typedef typename SparseModelType::ValueType ValueType;
                 typedef typename SparseModelType::RewardModelType RewardModelType;
-                typedef SparseMultiObjectivePreprocessorReturnType<SparseModelType> ReturnType;
-                typedef typename SparseMultiObjectivePreprocessorReturnType<SparseModelType>::ObjectiveInformation ObjectiveInformation;
+                typedef SparseMultiObjectivePreprocessorData<SparseModelType> PreprocessorData;
+                typedef SparseMultiObjectiveObjectiveInformation<ValueType> ObjectiveInformation;
                 
                 /*!
                  * Preprocesses the given model w.r.t. the given formulas.
                  * @param originalModel The considered model
                  * @param originalFormula the considered formula. The subformulas should only contain one OperatorFormula at top level, i.e., the formula is simple.
                  */
-                static ReturnType preprocess(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel);
+                static PreprocessorData preprocess(storm::logic::MultiObjectiveFormula const& originalFormula, SparseModelType const& originalModel);
                 
             private:
                 
@@ -37,14 +37,14 @@ namespace storm {
                  * @param currentObjective the currently considered objective. The given formula should be a a (sub)formula of this objective
                  * @param optionalRewardModelName the reward model name that is considered for the formula (if available)
                  */
-                static void preprocessFormula(storm::logic::OperatorFormula const& formula, ReturnType& info, ObjectiveInformation& currentObjective);
-                static void preprocessFormula(storm::logic::ProbabilityOperatorFormula const& formula, ReturnType& info, ObjectiveInformation& currentObjective);
-                static void preprocessFormula(storm::logic::RewardOperatorFormula const& formula, ReturnType& info, ObjectiveInformation& currentObjective);
-                static void preprocessFormula(storm::logic::UntilFormula const& formula, ReturnType& info, ObjectiveInformation& currentObjective);
-                static void preprocessFormula(storm::logic::BoundedUntilFormula const& formula, ReturnType& info, ObjectiveInformation& currentObjective);
-                static void preprocessFormula(storm::logic::GloballyFormula const& formula, ReturnType& info, ObjectiveInformation& currentObjective);
-                static void preprocessFormula(storm::logic::EventuallyFormula const& formula, ReturnType& info, ObjectiveInformation& currentObjective, boost::optional<std::string> const& optionalRewardModelName = boost::none);
-                static void preprocessFormula(storm::logic::CumulativeRewardFormula const& formula, ReturnType& info, ObjectiveInformation& currentObjective, boost::optional<std::string> const& optionalRewardModelName = boost::none);
+                static void preprocessFormula(storm::logic::OperatorFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective);
+                static void preprocessFormula(storm::logic::ProbabilityOperatorFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective);
+                static void preprocessFormula(storm::logic::RewardOperatorFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective);
+                static void preprocessFormula(storm::logic::UntilFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective);
+                static void preprocessFormula(storm::logic::BoundedUntilFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective);
+                static void preprocessFormula(storm::logic::GloballyFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective);
+                static void preprocessFormula(storm::logic::EventuallyFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, boost::optional<std::string> const& optionalRewardModelName = boost::none);
+                static void preprocessFormula(storm::logic::CumulativeRewardFormula const& formula, PreprocessorData& data, ObjectiveInformation& currentObjective, boost::optional<std::string> const& optionalRewardModelName = boost::none);
                 
             };
             
diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h
new file mode 100644
index 000000000..28f196b39
--- /dev/null
+++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h
@@ -0,0 +1,62 @@
+#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPREPROCESSORDATA_H_
+#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPREPROCESSORDATA_H_
+
+#include <vector>
+#include <memory>
+#include <iomanip>
+#include <boost/optional.hpp>
+
+#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveObjectiveInformation.h"
+
+namespace storm {
+    namespace modelchecker {
+        
+
+        namespace helper {
+            
+            template <class SparseModelType>
+            struct SparseMultiObjectivePreprocessorData {
+                
+                enum class QueryType { Achievability, Numerical, Pareto };
+                
+                SparseModelType preprocessedModel;
+                SparseModelType const& originalModel;
+                std::vector<uint_fast64_t> newToOldStateIndexMapping;
+                
+                QueryType queryType;
+                std::vector<SparseMultiObjectiveObjectiveInformation<typename SparseModelType::ValueType>> objectives;
+                boost::optional<uint_fast64_t> indexOfOptimizingObjective;
+                
+                bool produceSchedulers;
+                
+                SparseMultiObjectivePreprocessorData(SparseModelType const& model) : preprocessedModel(model),  originalModel(model), produceSchedulers(false) {
+                    //Intentionally left empty
+                }
+                
+                void printToStream(std::ostream& out) {
+                    out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;
+                    out << "                                                       Multi-objective Preprocessor Data                                               " << std::endl;
+                    out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;
+                    out << std::endl;
+                    out << "Objectives:" << std::endl;
+                    out << "--------------------------------------------------------------" << std::endl;
+                    for (auto const& obj : objectives) {
+                        obj.printToStream(out);
+                    }
+                    out << "--------------------------------------------------------------" << std::endl;
+                    out << std::endl;
+                    out << "Original Model Information:" << std::endl;
+                    originalModel.printModelInformationToStream(out);
+                    out << std::endl;
+                    out << "Preprocessed Model Information:" << std::endl;
+                    preprocessedModel.printModelInformationToStream(out);
+                    out << std::endl;
+                    out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;
+                }
+           
+            };
+        }
+    }
+}
+
+#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPREPROCESSORDATA_H_ */
diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorReturnType.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorReturnType.h
deleted file mode 100644
index 3678bf416..000000000
--- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorReturnType.h
+++ /dev/null
@@ -1,105 +0,0 @@
-#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPREPROCESSORRETURNTYPE_H_
-#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPREPROCESSORRETURNTYPE_H_
-
-#include <vector>
-#include <memory>
-#include <iomanip>
-#include <boost/optional.hpp>
-
-#include "src/logic/Formulas.h"
-
-namespace storm {
-    namespace modelchecker {
-        
-
-        namespace helper {
-            
-            template <class SparseModelType>
-            struct SparseMultiObjectivePreprocessorReturnType {
-                
-                typedef typename SparseModelType::ValueType ValueType;
-                typedef typename SparseModelType::RewardModelType RewardModelType;
-                
-                struct ObjectiveInformation {
-                    // the original input formula
-                    std::shared_ptr<storm::logic::Formula const> originalFormula;
-                    
-                    // the name of the considered reward model in the preprocessedModel
-                    std::string rewardModelName;
-                    
-                    // true if all rewards for this objective are positive, false if all rewards are negative.
-                    bool rewardsArePositive;
-                    
-                    // transformation from the values of the preprocessed model to the ones for the actual input model, i.e.,
-                    // x is achievable in the preprocessed model iff factor*x + offset is achievable in the original model
-                    ValueType toOriginalValueTransformationFactor;
-                    ValueType toOriginalValueTransformationOffset;
-                    
-                    // The probability/reward threshold for the preprocessed model (if originalFormula specifies one).
-                    // This is always a lower bound.
-                    boost::optional<ValueType> threshold;
-                    // True iff the specified threshold is strict, i.e., >
-                    bool thresholdIsStrict = false;
-                    
-                    // The (discrete) stepBound for the formula (if given by the originalFormula)
-                    boost::optional<uint_fast64_t> stepBound;
-                    
-                    void printToStream(std::ostream& out) const {
-                        out << std::setw(30) << originalFormula->toString();
-                        out << " \t(toOrigVal:" << std::setw(3) << toOriginalValueTransformationFactor << "*x +" << std::setw(3) << toOriginalValueTransformationOffset << ", \t";
-                        out << "intern threshold:";
-                        if(threshold){
-                            out << (thresholdIsStrict ? " >" : ">=");
-                            out << std::setw(5) << (*threshold) << ",";
-                        } else {
-                            out << "   none,";
-                        }
-                        out << " \t";
-                        out << "intern reward model: " << std::setw(10) << rewardModelName;
-                        out << (rewardsArePositive ? " (positive)" : " (negative)") << ", \t";
-                        out << "step bound:";
-                        if(stepBound) {
-                            out << std::setw(5) << (*stepBound);
-                        } else {
-                            out << " none";
-                        }
-                        out << ")" << std::endl;
-                     }
-                };
-                
-                SparseMultiObjectivePreprocessorReturnType(SparseModelType const& model) : preprocessedModel(model),  originalModel(model) , produceSchedulers(false) {
-                    //Intentionally left empty
-                }
-                
-                void printToStream(std::ostream& out) {
-                    out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;
-                    out << "                                                      Multi-objective Preprocessor Result                                              " << std::endl;
-                    out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;
-                    out << std::endl;
-                    out << "Objectives:" << std::endl;
-                    out << "--------------------------------------------------------------" << std::endl;
-                    for (auto const& obj : objectives) {
-                        obj.printToStream(out);
-                    }
-                    out << "--------------------------------------------------------------" << std::endl;
-                    out << std::endl;
-                    out << "Original Model Information:" << std::endl;
-                    originalModel.printModelInformationToStream(out);
-                    out << std::endl;
-                    out << "Preprocessed Model Information:" << std::endl;
-                    preprocessedModel.printModelInformationToStream(out);
-                    out << std::endl;
-                    out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;
-                }
-                
-                SparseModelType preprocessedModel;
-                SparseModelType const& originalModel;
-                std::vector<uint_fast64_t> newToOldStateIndexMapping;
-                std::vector<ObjectiveInformation> objectives;
-                bool produceSchedulers;
-            };
-        }
-    }
-}
-
-#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEPREPROCESSORRETURNTYPE_H_ */
diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelperRefinementStep.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveRefinementStep.h
similarity index 60%
rename from src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelperRefinementStep.h
rename to src/modelchecker/multiobjective/helper/SparseMultiObjectiveRefinementStep.h
index 3c42c0060..577e2984c 100644
--- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelperRefinementStep.h
+++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveRefinementStep.h
@@ -1,5 +1,5 @@
-#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEHELPERREFINEMENTSTEP_H_
-#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEHELPERREFINEMENTSTEP_H_
+#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEREFINEMENTSTEP_H_
+#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEREFINEMENTSTEP_H_
 
 #include <vector>
 #include <boost/optional.hpp>
@@ -11,22 +11,22 @@ namespace storm {
         namespace helper {
             
             template <typename RationalNumberType>
-            class SparseMultiObjectiveHelperRefinementStep {
+            class SparseMultiObjectiveRefinementStep {
                 
             public:
-                SparseMultiObjectiveHelperRefinementStep(std::vector<RationalNumberType> const& weightVector, std::vector<RationalNumberType> const& point, storm::storage::TotalScheduler const& scheduler) : weightVector(weightVector), point(point), scheduler(scheduler) {
+                SparseMultiObjectiveRefinementStep(std::vector<RationalNumberType> const& weightVector, std::vector<RationalNumberType> const& point, storm::storage::TotalScheduler const& scheduler) : weightVector(weightVector), point(point), scheduler(scheduler) {
                     //Intentionally left empty
                 }
                 
-                SparseMultiObjectiveHelperRefinementStep(std::vector<RationalNumberType>&& weightVector, std::vector<RationalNumberType>&& point, storm::storage::TotalScheduler&& scheduler) : weightVector(weightVector), point(point), scheduler(scheduler) {
+                SparseMultiObjectiveRefinementStep(std::vector<RationalNumberType>&& weightVector, std::vector<RationalNumberType>&& point, storm::storage::TotalScheduler&& scheduler) : weightVector(weightVector), point(point), scheduler(scheduler) {
                     //Intentionally left empty
                 }
                 
-                SparseMultiObjectiveHelperRefinementStep(std::vector<RationalNumberType> const& weightVector, std::vector<RationalNumberType> const& point) : weightVector(weightVector), point(point) {
+                SparseMultiObjectiveRefinementStep(std::vector<RationalNumberType> const& weightVector, std::vector<RationalNumberType> const& point) : weightVector(weightVector), point(point) {
                     //Intentionally left empty
                 }
                 
-                SparseMultiObjectiveHelperRefinementStep(std::vector<RationalNumberType>&& weightVector, std::vector<RationalNumberType>&& point) : weightVector(weightVector), point(point) {
+                SparseMultiObjectiveRefinementStep(std::vector<RationalNumberType>&& weightVector, std::vector<RationalNumberType>&& point) : weightVector(weightVector), point(point) {
                     //Intentionally left empty
                 }
                 
@@ -55,4 +55,4 @@ namespace storm {
     }
 }
 
-#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEHELPERREFINEMENTSTEP_H_ */
+#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEREFINEMENTSTEP_H_ */
diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelperReturnType.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveResultData.h
similarity index 92%
rename from src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelperReturnType.h
rename to src/modelchecker/multiobjective/helper/SparseMultiObjectiveResultData.h
index 3a2bd80f2..5ba05020e 100644
--- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelperReturnType.h
+++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveResultData.h
@@ -1,11 +1,11 @@
-#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEHELPERRETURNTYPE_H_
-#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEHELPERRETURNTYPE_H_
+#ifndef STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVERESULTDATA_H_
+#define STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVERESULTDATA_H_
 
 #include <vector>
 #include <memory>
 #include <boost/optional.hpp>
 
-#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveHelperRefinementStep.h"
+#include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveRefinementStep.h"
 #include "src/storage/geometry/Polytope.h"
 #include "src/utility/macros.h"
 
@@ -16,13 +16,13 @@ namespace storm {
         namespace helper {
 
             template <typename RationalNumberType>
-            class SparseMultiObjectiveHelperReturnType {
+            class SparseMultiObjectiveResultData {
                 
             public:
-                std::vector<SparseMultiObjectiveHelperRefinementStep<RationalNumberType>>& refinementSteps() {
+                std::vector<SparseMultiObjectiveRefinementStep<RationalNumberType>>& refinementSteps() {
                     return steps;
                 }
-                std::vector<SparseMultiObjectiveHelperRefinementStep<RationalNumberType>> const& refinementSteps() const {
+                std::vector<SparseMultiObjectiveRefinementStep<RationalNumberType>> const& refinementSteps() const {
                     return steps;
                 }
                 
@@ -103,7 +103,7 @@ namespace storm {
                 enum class Tribool { FF, TT, INDETERMINATE };
                 
                 //Stores the results for the individual iterations
-                std::vector<SparseMultiObjectiveHelperRefinementStep<RationalNumberType>> steps;
+                std::vector<SparseMultiObjectiveRefinementStep<RationalNumberType>> steps;
                 //Stores an overapproximation of the set of achievable values
                 std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> overApprox;
                 //Stores an underapproximation of the set of achievable values
@@ -131,4 +131,4 @@ namespace storm {
     }
 }
 
-#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVEHELPERRETURNTYPE_H_ */
+#endif /* STORM_MODELCHECKER_MULTIOBJECTIVE_HELPER_SPARSEMULTIOBJECTIVERESULTDATA_H_ */
diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h
index 2488a8e42..ba660684b 100644
--- a/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h
+++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectiveWeightVectorChecker.h
@@ -3,7 +3,7 @@
 
 #include <vector>
 
-#include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorReturnType.h"
+#include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h"
 #include "src/storage/TotalScheduler.h"
 
 namespace storm {
@@ -21,7 +21,7 @@ namespace storm {
             public:
                 typedef typename SparseModelType::ValueType ValueType;
                 typedef typename SparseModelType::RewardModelType RewardModelType;
-                typedef SparseMultiObjectivePreprocessorReturnType<SparseModelType> PreprocessorData;
+                typedef SparseMultiObjectivePreprocessorData<SparseModelType> PreprocessorData;
             
                 SparseMultiObjectiveWeightVectorChecker(PreprocessorData const& data);