diff --git a/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp b/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp
index 230cc9f53..1b3f71146 100644
--- a/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp
+++ b/src/modelchecker/multiobjective/SparseMdpMultiObjectiveModelChecker.cpp
@@ -37,16 +37,13 @@ namespace storm {
         template<typename SparseMdpModelType>
         std::unique_ptr<CheckResult> SparseMdpMultiObjectiveModelChecker<SparseMdpModelType>::checkMultiObjectiveFormula(CheckTask<storm::logic::MultiObjectiveFormula> const& checkTask) {
             STORM_LOG_ASSERT(this->getModel().getInitialStates().getNumberOfSetBits() == 1, "Multi Objective Model checking on model with multiple initial states is not supported.");
-            storm::utility::Stopwatch swModelChecking;
             std::unique_ptr<CheckResult> result;
             
 #ifdef STORM_HAVE_CARL
             storm::utility::Stopwatch swPreprocessing;
             auto preprocessorData = helper::SparseMultiObjectivePreprocessor<SparseMdpModelType>::preprocess(checkTask.getFormula(), this->getModel());
             swPreprocessing.pause();
-            std::cout << std::endl;
-            preprocessorData.printToStream(std::cout);
-            STORM_LOG_DEBUG("Preprocessing done.");
+            STORM_LOG_DEBUG("Preprocessing done. Data: " << preprocessorData);
             
             storm::utility::Stopwatch swHelper;
             auto resultData = helper::SparseMultiObjectiveHelper<SparseMdpModelType, storm::RationalNumber>::check(preprocessorData);
@@ -54,26 +51,11 @@ namespace storm {
             STORM_LOG_DEBUG("Modelchecking done.");
             
             storm::utility::Stopwatch swPostprocessing;
-            result = helper::SparseMultiObjectivePostprocessor<SparseMdpModelType, storm::RationalNumber>::postprocess(preprocessorData, resultData);
-            swPostprocessing.pause();
+            result = helper::SparseMultiObjectivePostprocessor<SparseMdpModelType, storm::RationalNumber>::postprocess(preprocessorData, resultData, swPreprocessing, swHelper, swPostprocessing);
             STORM_LOG_DEBUG("Postprocessing done.");
 #else
             STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Multi objective model checking requires carl.");
 #endif
-            std::cout << std::endl;
-            std::cout << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;
-            std::cout << "                                                 Multi-objective Model Checking Statistics:                                            " << std::endl;
-            std::cout << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;
-            std::cout << std::endl;
-            std::cout << "Runtimes (in seconds):" << std::endl;
-            std::cout << "\t Preprocessing:    " << std::setw(8) << swPreprocessing << std::endl;
-            std::cout << "\t Value Iterations: " << std::setw(8) << swHelper << std::endl;
-            std::cout << "\t Postprocessing:   " << std::setw(8) << swPostprocessing << std::endl;
-            std::cout << "\t Combined:         " << std::setw(8) << swModelChecking << std::endl;
-            std::cout << std::endl;
-            std::cout << "Performed Refinement Steps: " << resultData.refinementSteps().size() << std::endl;
-            std::cout << std::endl;
-            std::cout << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;
             return result;
         }
         
diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp
index 5f2bdf8f7..22089a63d 100644
--- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp
+++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.cpp
@@ -7,7 +7,13 @@
 #include "src/models/sparse/StandardRewardModel.h"
 #include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
 #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+#include "src/modelchecker/results/ParetoCurveCheckResult.h"
 #include "src/storage/geometry/Polytope.h"
+#include "src/storage/geometry/Hyperrectangle.h"
+#include "src/settings//SettingsManager.h"
+#include "src/settings/modules/MultiObjectiveSettings.h"
+#include "src/settings/modules/GeneralSettings.h"
+#include "src/utility/export.h"
 #include "src/utility/macros.h"
 #include "src/utility/vector.h"
 
@@ -18,18 +24,26 @@ namespace storm {
         namespace helper {
             
             template<typename SparseModelType, typename RationalNumberType>
-            typename std::unique_ptr<CheckResult> SparseMultiObjectivePostprocessor<SparseModelType, RationalNumberType>::postprocess(PreprocessorData const& preprocessorData, ResultData const& resultData) {
+            typename std::unique_ptr<CheckResult> SparseMultiObjectivePostprocessor<SparseModelType, RationalNumberType>::postprocess(PreprocessorData const& preprocessorData, ResultData const& resultData, boost::optional<storm::utility::Stopwatch> const& preprocessorStopwatch, boost::optional<storm::utility::Stopwatch> const& helperStopwatch, boost::optional<storm::utility::Stopwatch> const& postprocessorStopwatch) {
                 STORM_LOG_WARN_COND(!resultData.getMaxStepsPerformed(), "Multi-objective model checking has been aborted since the maximum number of refinement steps has been performed. The results are most likely incorrect.");
+                
+                std::unique_ptr<CheckResult> result(new ExplicitQualitativeCheckResult());;
+                
                 if(preprocessorData.originalFormula.hasQualitativeResult()) {
-                    return postprocessAchievabilityQuery(preprocessorData, resultData);
+                    result = postprocessAchievabilityQuery(preprocessorData, resultData);
                 } else if(preprocessorData.originalFormula.hasNumericalResult()){
-                    return postprocessNumericalQuery(preprocessorData, resultData);
+                    result = postprocessNumericalQuery(preprocessorData, resultData);
                 } else if (preprocessorData.originalFormula.hasParetoCurveResult()) {
-                    return postprocessParetoQuery(preprocessorData, resultData);
+                    result = postprocessParetoQuery(preprocessorData, resultData);
                 } else {
                     STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unknown Query Type");
                 }
-                  return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult());;
+                
+                STORM_LOG_INFO(getInfo(result, preprocessorData, resultData, preprocessorStopwatch, helperStopwatch, postprocessorStopwatch));
+                
+                exportPlot(result, preprocessorData, resultData, preprocessorStopwatch, helperStopwatch, postprocessorStopwatch);
+                
+                return result;
             }
             
             template<typename SparseModelType, typename RationalNumberType>
@@ -125,11 +139,184 @@ namespace storm {
             
             template<typename SparseModelType, typename RationalNumberType>
             typename std::unique_ptr<CheckResult> SparseMultiObjectivePostprocessor<SparseModelType, RationalNumberType>::postprocessParetoQuery(PreprocessorData const& preprocessorData, ResultData const& resultData) {
-                STORM_LOG_ERROR("Postprocessing pareto queries not yet implemented");
                 uint_fast64_t initState = preprocessorData.originalModel.getInitialStates().getNextSetIndex(0);
-                return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(initState, false));
+                
+                //Issue a warning for objectives that have been solved in preprocessing
+                for(uint_fast64_t subformulaIndex = 0; subformulaIndex < preprocessorData.originalFormula.getNumberOfSubformulas(); ++subformulaIndex) {
+                    switch(preprocessorData.solutionsFromPreprocessing[subformulaIndex]) {
+                        case PreprocessorData::PreprocessorObjectiveSolution::None:
+                            // Nothing to be done
+                            break;
+                        case PreprocessorData::PreprocessorObjectiveSolution::False:
+                            return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(initState, false));
+                        case PreprocessorData::PreprocessorObjectiveSolution::True:
+                            // Nothing to be done
+                            break;
+                        case PreprocessorData::PreprocessorObjectiveSolution::Zero:
+                            STORM_LOG_WARN("The result of the objective " << preprocessorData.originalFormula.getSubformula(subformulaIndex) << " was obtained in preprocessing and will not be incorporated in the check result. Objective Result is zero.");
+                            break;
+                        case PreprocessorData::PreprocessorObjectiveSolution::Unbounded:
+                            STORM_LOG_WARN("The result of the objective " << preprocessorData.originalFormula.getSubformula(subformulaIndex) << " was obtained in preprocessing and will not be incorporated in the check result. Objective Result is infinity.");
+                            break;
+                        case PreprocessorData::PreprocessorObjectiveSolution::Undefined:
+                            STORM_LOG_ERROR("The result for the objective " << preprocessorData.originalFormula.getSubformula(subformulaIndex) << " is not defined.");
+                            return std::unique_ptr<CheckResult>(new ExplicitQualitativeCheckResult(initState, false));
+                        default:
+                            STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unexpected solution obtained in preprocessing.");
+                    }
+                }
+                
+                std::vector<std::vector<ValueType>> paretoOptimalPoints;
+                paretoOptimalPoints.reserve(resultData.refinementSteps().size());
+                for(auto const& step : resultData.refinementSteps()) {
+                    paretoOptimalPoints.push_back(storm::utility::vector::convertNumericVector<ValueType>(transformToOriginalValues(step.getPoint(), preprocessorData)));
+                }
+                return std::unique_ptr<CheckResult>(new ParetoCurveCheckResult<ValueType>(
+                          initState,
+                          std::move(paretoOptimalPoints),
+                          transformToOriginalValues(resultData.underApproximation(), preprocessorData)->template convertNumberRepresentation<ValueType>(),
+                          transformToOriginalValues(resultData.overApproximation(), preprocessorData)->template convertNumberRepresentation<ValueType>()));
+            }
+            
+            template<typename SparseModelType, typename RationalNumberType>
+            std::vector<RationalNumberType> SparseMultiObjectivePostprocessor<SparseModelType, RationalNumberType>::transformToOriginalValues(std::vector<RationalNumberType> const& vector, PreprocessorData const& preprocessorData) {
+                std::vector<RationalNumberType> result;
+                result.reserve(vector.size());
+                for(uint_fast64_t objIndex = 0; objIndex < preprocessorData.objectives.size(); ++objIndex) {
+                    result.push_back(vector[objIndex] * storm::utility::convertNumber<RationalNumberType>(preprocessorData.objectives[objIndex].toOriginalValueTransformationFactor) + storm::utility::convertNumber<RationalNumberType>(preprocessorData.objectives[objIndex].toOriginalValueTransformationOffset));
+                }
+                return result;
             }
             
+            template<typename SparseModelType, typename RationalNumberType>
+            std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> SparseMultiObjectivePostprocessor<SparseModelType, RationalNumberType>::transformToOriginalValues(std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> const& polytope, PreprocessorData const& preprocessorData) {
+                
+                uint_fast64_t numObjectives = preprocessorData.objectives.size();
+                std::vector<std::vector<RationalNumberType>> transformationMatrix(numObjectives, std::vector<RationalNumberType>(numObjectives, storm::utility::zero<RationalNumberType>()));
+                std::vector<RationalNumberType> transformationVector;
+                transformationVector.reserve(numObjectives);
+                for(uint_fast64_t objIndex = 0; objIndex < numObjectives; ++objIndex) {
+                    transformationMatrix[objIndex][objIndex] = storm::utility::convertNumber<RationalNumberType>(preprocessorData.objectives[objIndex].toOriginalValueTransformationFactor);
+                    transformationVector.push_back(storm::utility::convertNumber<RationalNumberType>(preprocessorData.objectives[objIndex].toOriginalValueTransformationOffset));
+                }
+                return polytope->linearTransformation(transformationMatrix, transformationVector);
+            }
+            
+            
+            template<typename SparseModelType, typename RationalNumberType>
+            void SparseMultiObjectivePostprocessor<SparseModelType, RationalNumberType>::exportPlot(std::unique_ptr<CheckResult> const& checkResult, PreprocessorData const& preprocessorData, ResultData const& resultData, boost::optional<storm::utility::Stopwatch> const& preprocessorStopwatch, boost::optional<storm::utility::Stopwatch> const& helperStopwatch, boost::optional<storm::utility::Stopwatch> const& postprocessorStopwatch) {
+                
+                if(!settings::getModule<storm::settings::modules::MultiObjectiveSettings>().isExportPlotSet()) {
+                    return;
+                }
+                STORM_LOG_ERROR_COND(preprocessorData.objectives.size()==2, "Exporting plot requested but this is only implemented for the two-dimensional case.");
+                
+                auto transformedUnderApprox = transformToOriginalValues(resultData.underApproximation(), preprocessorData);
+                auto transformedOverApprox = transformToOriginalValues(resultData.overApproximation(), preprocessorData);
+                
+                // Get pareto points as well as a hyperrectangle that is used to guarantee that the resulting polytopes are bounded.
+                storm::storage::geometry::Hyperrectangle<RationalNumberType> boundaries(std::vector<RationalNumber>(preprocessorData.objectives.size(), storm::utility::zero<RationalNumberType>()), std::vector<RationalNumber>(preprocessorData.objectives.size(), storm::utility::zero<RationalNumberType>()));
+                std::vector<std::vector<RationalNumberType>> paretoPoints;
+                paretoPoints.reserve(resultData.refinementSteps().size());
+                for(auto const& step : resultData.refinementSteps()) {
+                    paretoPoints.push_back(transformToOriginalValues(step.getPoint(), preprocessorData));
+                    boundaries.enlarge(paretoPoints.back());
+                }
+                auto underApproxVertices = transformedUnderApprox->getVertices();
+                for(auto const& v : underApproxVertices) {
+                    boundaries.enlarge(v);
+                }
+                auto overApproxVertices = transformedOverApprox->getVertices();
+                for(auto const& v : overApproxVertices) {
+                    boundaries.enlarge(v);
+                }
+                
+                //Further enlarge the boundaries a little
+                storm::utility::vector::scaleVectorInPlace(boundaries.lowerBounds(), RationalNumberType(11) / RationalNumberType(10));
+                storm::utility::vector::scaleVectorInPlace(boundaries.upperBounds(), RationalNumberType(11) / RationalNumberType(10));
+                
+                auto boundariesAsPolytope = boundaries.asPolytope();
+                std::vector<std::string> columnHeaders = {"x", "y"};
+                
+                std::vector<std::vector<double>> pointsForPlotting;
+                underApproxVertices = transformedUnderApprox->intersection(boundariesAsPolytope)->getVerticesInClockwiseOrder();
+                pointsForPlotting.reserve(underApproxVertices.size());
+                for(auto const& v : underApproxVertices) {
+                    pointsForPlotting.push_back(storm::utility::vector::convertNumericVector<double>(v));
+                }
+                storm::utility::exportDataToCSVFile(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getExportPlotUnderApproximationFileName(), pointsForPlotting, columnHeaders);
+                                                    
+                pointsForPlotting.clear();
+                overApproxVertices = transformedOverApprox->intersection(boundariesAsPolytope)->getVerticesInClockwiseOrder();
+                pointsForPlotting.reserve(overApproxVertices.size());
+                for(auto const& v : overApproxVertices) {
+                    pointsForPlotting.push_back(storm::utility::vector::convertNumericVector<double>(v));
+                }
+                storm::utility::exportDataToCSVFile(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getExportPlotOverApproximationFileName(), pointsForPlotting, columnHeaders);
+                                                    
+                pointsForPlotting.clear();
+                pointsForPlotting.reserve(paretoPoints.size());
+                for(auto const& v : paretoPoints) {
+                    pointsForPlotting.push_back(storm::utility::vector::convertNumericVector<double>(v));
+                }
+                storm::utility::exportDataToCSVFile(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getExportPlotParetoPointsFileName(), pointsForPlotting, columnHeaders);
+                                                    
+                pointsForPlotting.clear();
+                auto boundVertices = boundariesAsPolytope->getVerticesInClockwiseOrder();
+                pointsForPlotting.reserve(4);
+                for(auto const& v : boundVertices) {
+                    pointsForPlotting.push_back(storm::utility::vector::convertNumericVector<double>(v));
+                }
+                storm::utility::exportDataToCSVFile(storm::settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getExportPlotBoundariesFileName(), pointsForPlotting, columnHeaders);
+                                                    
+            }
+            
+            
+            template<typename SparseModelType, typename RationalNumberType>
+            std::string SparseMultiObjectivePostprocessor<SparseModelType, RationalNumberType>::getInfo(std::unique_ptr<CheckResult> const& checkResult, PreprocessorData const& preprocessorData, ResultData const& resultData, boost::optional<storm::utility::Stopwatch> const& preprocessorStopwatch, boost::optional<storm::utility::Stopwatch> const& helperStopwatch, boost::optional<storm::utility::Stopwatch> const& postprocessorStopwatch) {
+                
+                std::stringstream statistics;
+                statistics << preprocessorData;
+                statistics << std::endl;
+                statistics << std::endl;
+                statistics << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;
+                statistics << "                                                 Multi-objective Model Checking Result                                            " << std::endl;
+                statistics << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;
+                statistics << std::endl;
+                statistics << *checkResult;
+                statistics << std::endl;
+                statistics << std::endl;
+                statistics << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;
+                statistics << "                                                 Multi-objective Model Checking Statistics                                            " << std::endl;
+                statistics << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;
+                statistics << std::endl;
+                statistics << "Recorded Runtimes (in seconds):" << std::endl;
+                storm::utility::Stopwatch combinedTime;
+                combinedTime.pause();
+                if(preprocessorStopwatch) {
+                    statistics << "\t Preprocessing:    " << std::setw(8) << *preprocessorStopwatch << std::endl;
+                    combinedTime.addToAccumulatedSeconds(preprocessorStopwatch->getAccumulatedSeconds());
+                }
+                if(helperStopwatch) {
+                    statistics << "\t Value Iterations: " << std::setw(8) << *helperStopwatch << std::endl;
+                    combinedTime.addToAccumulatedSeconds(helperStopwatch->getAccumulatedSeconds());
+                }
+                if(postprocessorStopwatch) {
+                    statistics << "\t Postprocessing:   " << std::setw(8) << *postprocessorStopwatch << std::endl;
+                    combinedTime.addToAccumulatedSeconds(postprocessorStopwatch->getAccumulatedSeconds());
+                }
+                statistics << "\t Combined:         " << std::setw(8) << combinedTime << std::endl;
+                statistics << std::endl;
+                statistics << "Performed Refinement Steps: " << resultData.refinementSteps().size() << std::endl;
+                statistics << "Precision (Approximation): " << settings::getModule<storm::settings::modules::MultiObjectiveSettings>().getPrecision() << std::endl;
+                statistics << "Precision (Value Iteration): " << settings::getModule<storm::settings::modules::GeneralSettings>().getPrecision() << std::endl;
+                statistics << std::endl;
+                statistics << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;
+                
+                return statistics.str();
+            }
+            
+            
 #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
index 75a40fbfb..8ca4274f0 100644
--- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.h
+++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePostprocessor.h
@@ -3,10 +3,12 @@
 
 
 #include <memory>
+#include <boost/optional.hpp>
 
 #include "src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h"
 #include "src/modelchecker/multiobjective/helper/SparseMultiObjectiveResultData.h"
 #include "src/modelchecker/results/CheckResult.h"
+#include "src/utility/Stopwatch.h"
 
 namespace storm {
     namespace modelchecker {
@@ -31,14 +33,19 @@ namespace storm {
                  * @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);
+                static std::unique_ptr<CheckResult> postprocess(PreprocessorData const& preprocessorData, ResultData const& resultData, boost::optional<storm::utility::Stopwatch> const& preprocessorStopwatch = boost::none, boost::optional<storm::utility::Stopwatch> const& helperStopwatch = boost::none, boost::optional<storm::utility::Stopwatch> const& postprocessorStopwatch = boost::none);
                 
             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);
                 
+                static std::vector<RationalNumberType> transformToOriginalValues(std::vector<RationalNumberType> const& vector, PreprocessorData const& preprocessorData);
+                static std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> transformToOriginalValues(std::shared_ptr<storm::storage::geometry::Polytope<RationalNumberType>> const& polytope, PreprocessorData const& preprocessorData);
                 
+                static void exportPlot(std::unique_ptr<CheckResult> const& checkResult, PreprocessorData const& preprocessorData, ResultData const& resultData, boost::optional<storm::utility::Stopwatch> const& preprocessorStopwatch, boost::optional<storm::utility::Stopwatch> const& helperStopwatch, boost::optional<storm::utility::Stopwatch> const& postprocessorStopwatch);
+                
+                static std::string getInfo(std::unique_ptr<CheckResult> const& checkResult, PreprocessorData const& preprocessorData, ResultData const& resultData, boost::optional<storm::utility::Stopwatch> const& preprocessorStopwatch, boost::optional<storm::utility::Stopwatch> const& helperStopwatch, boost::optional<storm::utility::Stopwatch> const& postprocessorStopwatch);
             };
             
         }
diff --git a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h
index 89255cd33..373a086fc 100644
--- a/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h
+++ b/src/modelchecker/multiobjective/helper/SparseMultiObjectivePreprocessorData.h
@@ -47,7 +47,8 @@ namespace storm {
                     this->preprocessedModel.getStateLabeling().addLabel(this->prob1StatesLabel, storm::storage::BitVector(this->preprocessedModel.getNumberOfStates(), true));
                 }
                 
-                void printToStream(std::ostream& out) {
+                void printToStream(std::ostream& out) const {
+                    out << std::endl;
                     out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;
                     out << "                                                       Multi-objective Preprocessor Data                                               " << std::endl;
                     out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;
@@ -102,6 +103,12 @@ namespace storm {
                     out << "---------------------------------------------------------------------------------------------------------------------------------------" << std::endl;
                 }
            
+                
+                friend std::ostream& operator<<(std::ostream& out, SparseMultiObjectivePreprocessorData<SparseModelType> const& data) {
+                    data.printToStream(out);
+                    return out;
+                }
+                
             };
         }
     }
diff --git a/src/modelchecker/results/CheckResult.cpp b/src/modelchecker/results/CheckResult.cpp
index 40ca4badb..737064883 100644
--- a/src/modelchecker/results/CheckResult.cpp
+++ b/src/modelchecker/results/CheckResult.cpp
@@ -8,6 +8,7 @@
 #include "src/modelchecker/results/SymbolicQualitativeCheckResult.h"
 #include "src/modelchecker/results/SymbolicQuantitativeCheckResult.h"
 #include "src/modelchecker/results/HybridQuantitativeCheckResult.h"
+#include "src/modelchecker/results/ParetoCurveCheckResult.h"
 
 #include "src/utility/macros.h"
 #include "src/exceptions/InvalidOperationException.h"
@@ -63,6 +64,10 @@ namespace storm {
             return false;
         }
         
+        bool CheckResult::isParetoCurveCheckResult() const {
+            return false;
+        }
+        
         ExplicitQualitativeCheckResult& CheckResult::asExplicitQualitativeCheckResult() {
             return dynamic_cast<ExplicitQualitativeCheckResult&>(*this);
         }
@@ -127,6 +132,16 @@ namespace storm {
             return dynamic_cast<HybridQuantitativeCheckResult<Type, ValueType> const&>(*this);
         }
         
+        template<typename ValueType>
+        ParetoCurveCheckResult<ValueType>& CheckResult::asParetoCurveCheckResult() {
+            return dynamic_cast<ParetoCurveCheckResult<ValueType>&>(*this);
+        }
+        
+        template<typename ValueType>
+        ParetoCurveCheckResult<ValueType> const& CheckResult::asParetoCurveCheckResult() const {
+            return dynamic_cast<ParetoCurveCheckResult<ValueType> const&>(*this);
+        }
+        
         // Explicitly instantiate the template functions.
         template ExplicitQuantitativeCheckResult<double>& CheckResult::asExplicitQuantitativeCheckResult();
         template ExplicitQuantitativeCheckResult<double> const& CheckResult::asExplicitQuantitativeCheckResult() const;
@@ -144,10 +159,16 @@ namespace storm {
         template SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double> const& CheckResult::asSymbolicQuantitativeCheckResult() const;
         template HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>& CheckResult::asHybridQuantitativeCheckResult();
         template HybridQuantitativeCheckResult<storm::dd::DdType::Sylvan, double> const& CheckResult::asHybridQuantitativeCheckResult() const;
+        
+        template ParetoCurveCheckResult<double>& CheckResult::asParetoCurveCheckResult();
+        template ParetoCurveCheckResult<double> const& CheckResult::asParetoCurveCheckResult() const;
 
 #ifdef STORM_HAVE_CARL
         template ExplicitQuantitativeCheckResult<storm::RationalFunction>& CheckResult::asExplicitQuantitativeCheckResult();
         template ExplicitQuantitativeCheckResult<storm::RationalFunction> const& CheckResult::asExplicitQuantitativeCheckResult() const;
+        
+        template ParetoCurveCheckResult<storm::RationalNumber>& CheckResult::asParetoCurveCheckResult();
+        template ParetoCurveCheckResult<storm::RationalNumber> const& CheckResult::asParetoCurveCheckResult() const;
 #endif
     }
-}
\ No newline at end of file
+}
diff --git a/src/modelchecker/results/CheckResult.h b/src/modelchecker/results/CheckResult.h
index 152fc9e3b..a3d6c8eec 100644
--- a/src/modelchecker/results/CheckResult.h
+++ b/src/modelchecker/results/CheckResult.h
@@ -26,6 +26,9 @@ namespace storm {
         template <storm::dd::DdType Type, typename ValueType>
         class HybridQuantitativeCheckResult;
         
+        template <typename ValueType>
+        class ParetoCurveCheckResult;
+        
         // The base class of all check results.
         class CheckResult {
         public:
@@ -50,6 +53,7 @@ namespace storm {
             virtual bool isSymbolicQualitativeCheckResult() const;
             virtual bool isSymbolicQuantitativeCheckResult() const;
             virtual bool isHybridQuantitativeCheckResult() const;
+            virtual bool isParetoCurveCheckResult() const;
             virtual bool isResultForAllStates() const;
             
             QualitativeCheckResult& asQualitativeCheckResult();
@@ -84,6 +88,12 @@ namespace storm {
             
             template <storm::dd::DdType Type, typename ValueType>
             HybridQuantitativeCheckResult<Type, ValueType> const& asHybridQuantitativeCheckResult() const;
+
+            template <typename ValueType>
+            ParetoCurveCheckResult<ValueType>& asParetoCurveCheckResult();
+            
+            template <typename ValueType>
+            ParetoCurveCheckResult<ValueType> const& asParetoCurveCheckResult() const;
             
             virtual std::ostream& writeToStream(std::ostream& out) const = 0;
         };
@@ -92,4 +102,4 @@ namespace storm {
     }
 }
 
-#endif /* STORM_MODELCHECKER_CHECKRESULT_H_ */
\ No newline at end of file
+#endif /* STORM_MODELCHECKER_CHECKRESULT_H_ */
diff --git a/src/modelchecker/results/ParetoCurveCheckResult.cpp b/src/modelchecker/results/ParetoCurveCheckResult.cpp
new file mode 100644
index 000000000..00297f1f2
--- /dev/null
+++ b/src/modelchecker/results/ParetoCurveCheckResult.cpp
@@ -0,0 +1,88 @@
+#include "src/modelchecker/results/ParetoCurveCheckResult.h"
+
+#include "src/adapters/CarlAdapter.h"
+#include "src/modelchecker/results/ExplicitQualitativeCheckResult.h"
+#include "src/utility/macros.h"
+#include "src/utility/vector.h"
+
+#include "src/exceptions/InvalidOperationException.h"
+
+namespace storm {
+    namespace modelchecker {
+        template<typename ValueType>
+        ParetoCurveCheckResult<ValueType>::ParetoCurveCheckResult() {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType>
+        ParetoCurveCheckResult<ValueType>::ParetoCurveCheckResult(storm::storage::sparse::state_type const& state, std::vector<point_type> const& points, polytope_type const& underApproximation, polytope_type const& overApproximation) : state(state), points(points), underApproximation(underApproximation), overApproximation(overApproximation) {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType>
+        ParetoCurveCheckResult<ValueType>::ParetoCurveCheckResult(storm::storage::sparse::state_type const& state, std::vector<point_type>&& points, polytope_type&& underApproximation, polytope_type&& overApproximation) : state(state), points(points), underApproximation(underApproximation), overApproximation(overApproximation) {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType>
+        bool ParetoCurveCheckResult<ValueType>::isParetoCurveCheckResult() const {
+            return true;
+        }
+        
+        template<typename ValueType>
+        void ParetoCurveCheckResult<ValueType>::filter(QualitativeCheckResult const& filter) {
+            STORM_LOG_THROW(filter.isExplicitQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot filter explicit check result with non-explicit filter.");
+            STORM_LOG_THROW(filter.isResultForAllStates(), storm::exceptions::InvalidOperationException, "Cannot filter check result with non-complete filter.");
+            ExplicitQualitativeCheckResult const& explicitFilter = filter.asExplicitQualitativeCheckResult();
+            ExplicitQualitativeCheckResult::vector_type const& filterTruthValues = explicitFilter.getTruthValuesVector();
+            
+            STORM_LOG_THROW(filterTruthValues.getNumberOfSetBits() == 1 && filterTruthValues.get(state), storm::exceptions::InvalidOperationException, "The check result fails to contain some results referred to by the filter.");
+        }
+        
+        template<typename ValueType>
+        storm::storage::sparse::state_type const& ParetoCurveCheckResult<ValueType>:: getState() const {
+            return state;
+        }
+        
+        template<typename ValueType>
+        std::vector<typename ParetoCurveCheckResult<ValueType>::point_type> const& ParetoCurveCheckResult<ValueType>::getPoints() const {
+            return points;
+        }
+        
+        template<typename ValueType>
+        typename ParetoCurveCheckResult<ValueType>::polytope_type const& ParetoCurveCheckResult<ValueType>::getUnderApproximation() const {
+            return underApproximation;
+        }
+        
+        template<typename ValueType>
+        typename ParetoCurveCheckResult<ValueType>::polytope_type const& ParetoCurveCheckResult<ValueType>::getOverApproximation() const {
+            return overApproximation;
+        }
+        
+        
+        template<typename ValueType>
+        std::ostream& ParetoCurveCheckResult<ValueType>::writeToStream(std::ostream& out) const {
+            out << std::endl;
+            out << "Underapproximation of achievable values: " << underApproximation->toString() << std::endl;
+            out << "Overapproximation of achievable values: " << overApproximation->toString() << std::endl;
+            out << points.size() << " pareto optimal points found:" << std::endl;
+            for(auto const& p : points) {
+                out << "   (";
+                for(auto it = p.begin(); it != p.end(); ++it){
+                    if(it != p.begin()){
+                        out << ", ";
+                    }
+                    out << std::setw(10) << *it;
+                }
+                out << " )" << std::endl;
+            }
+            return out;
+        }
+        
+        template class ParetoCurveCheckResult<double>;
+        
+#ifdef STORM_HAVE_CARL
+        template class ParetoCurveCheckResult<storm::RationalNumber>;
+#endif
+    }
+}
diff --git a/src/modelchecker/results/ParetoCurveCheckResult.h b/src/modelchecker/results/ParetoCurveCheckResult.h
new file mode 100644
index 000000000..6781e9454
--- /dev/null
+++ b/src/modelchecker/results/ParetoCurveCheckResult.h
@@ -0,0 +1,56 @@
+#ifndef STORM_MODELCHECKER_PARETOCURVECHECKRESULT_H_
+#define STORM_MODELCHECKER_PARETOCURVECHECKRESULT_H_
+
+#include <vector>
+
+#include "src/modelchecker/results/CheckResult.h"
+#include "src/utility/OsDetection.h"
+#include "src/storage/sparse/StateType.h"
+#include "src/storage/geometry/Polytope.h"
+
+namespace storm {
+    namespace modelchecker {
+        template<typename ValueType>
+        class ParetoCurveCheckResult : public CheckResult {
+        public:
+            typedef std::vector<ValueType> point_type;
+            typedef std::shared_ptr<storm::storage::geometry::Polytope<ValueType>> polytope_type;
+            
+            ParetoCurveCheckResult();
+            ParetoCurveCheckResult(storm::storage::sparse::state_type const& state, std::vector<point_type> const& points, polytope_type const& underApproximation, polytope_type const& overApproximation);
+            ParetoCurveCheckResult(storm::storage::sparse::state_type const& state, std::vector<point_type>&& points, polytope_type&& underApproximation, polytope_type&& overApproximation);
+            
+            ParetoCurveCheckResult(ParetoCurveCheckResult const& other) = default;
+            ParetoCurveCheckResult& operator=(ParetoCurveCheckResult const& other) = default;
+            ParetoCurveCheckResult(ParetoCurveCheckResult&& other) = default;
+            ParetoCurveCheckResult& operator=(ParetoCurveCheckResult&& other) = default;
+            virtual ~ParetoCurveCheckResult() = default;
+            
+            virtual bool isParetoCurveCheckResult() const override;
+            
+            virtual void filter(QualitativeCheckResult const& filter) override;
+            
+            storm::storage::sparse::state_type const& getState() const;
+            std::vector<point_type> const& getPoints() const;
+            polytope_type const& getUnderApproximation() const;
+            polytope_type const& getOverApproximation() const;
+            
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
+
+        private:
+            // The state of the checked model to which the result applies
+            storm::storage::sparse::state_type state;
+            
+            // The pareto optimal points that have been found.
+            std::vector<point_type> points;
+            
+            // An underapproximation of the set of achievable values
+            polytope_type underApproximation;
+            
+            // An overapproximation of the set of achievable values
+            polytope_type overApproximation;
+        };
+    }
+}
+
+#endif /* STORM_MODELCHECKER_PARETOCURVECHECKRESULT_H_ */
diff --git a/src/settings/ArgumentValidators.h b/src/settings/ArgumentValidators.h
index 60a36b55b..b89aefd2c 100644
--- a/src/settings/ArgumentValidators.h
+++ b/src/settings/ArgumentValidators.h
@@ -10,6 +10,7 @@
 #include <vector>
 #include <memory>
 #include <string>
+#include <stdio.h>
 
 #include "src/settings/Argument.h"
 #include "src/utility/macros.h"
@@ -171,6 +172,25 @@ namespace storm {
 				};
 			}
 
+            /*!
+             * Creates a validation function that checks whether a given string corresponds to a path to a file in which we can write
+             *
+             * @return The resulting validation function.
+             */
+			static std::function<bool (std::string const&)> writableFileValidator() {
+				return [] (std::string const fileName) -> bool {
+                    struct stat info;
+                    STORM_LOG_THROW(stat (fileName.c_str(), &info) != 0, storm::exceptions::IllegalArgumentValueException , "Could not open file '" << fileName << "' for writing because file or directory already exists.");
+                    
+                    std::ofstream filestream(fileName);
+                    STORM_LOG_THROW(filestream.is_open(), storm::exceptions::IllegalArgumentValueException , "Could not open file '" << fileName << "' for writing.");
+                    filestream.close();
+                    std::remove(fileName.c_str());
+                    
+                    return true;
+				};
+			}
+
             /*!
              * Creates a validation function that checks whether a given string is in a provided list of strings.
              *
@@ -252,4 +272,4 @@ namespace storm {
 	}
 }
 
-#endif // STORM_SETTINGS_ARGUMENTVALIDATORS_H_
\ No newline at end of file
+#endif // STORM_SETTINGS_ARGUMENTVALIDATORS_H_
diff --git a/src/settings/modules/MultiObjectiveSettings.cpp b/src/settings/modules/MultiObjectiveSettings.cpp
index 02e04e762..1cd1f51b1 100644
--- a/src/settings/modules/MultiObjectiveSettings.cpp
+++ b/src/settings/modules/MultiObjectiveSettings.cpp
@@ -4,6 +4,7 @@
 #include "src/settings/OptionBuilder.h"
 #include "src/settings/ArgumentBuilder.h"
 #include "src/settings/Argument.h"
+#include "src/settings/ArgumentValidators.h"
 
 
 namespace storm {
@@ -11,25 +12,42 @@ namespace storm {
         namespace modules {
             
             const std::string MultiObjectiveSettings::moduleName = "multiobjective";
-            const std::string MultiObjectiveSettings::exportResultFileOptionName = "resultfile";
+            const std::string MultiObjectiveSettings::exportPlotOptionName = "exportplot";
             const std::string MultiObjectiveSettings::precisionOptionName = "precision";
             const std::string MultiObjectiveSettings::maxStepsOptionName = "maxsteps";
             
             MultiObjectiveSettings::MultiObjectiveSettings() : ModuleSettings(moduleName) {
-                this->addOption(storm::settings::OptionBuilder(moduleName, exportResultFileOptionName, true, "Saves the result as LaTeX document.")
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("filename", "A path to a file where the result should be saved.").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, exportPlotOptionName, true, "Saves data for plotting of pareto curves and achievable values. The latter will be intersected with some boundaries to obtain a bounded polytope.")
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("directory", "A path to a directory in which the results will be saved.").build())
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("underapproximation", "The name of the file in which vertices of the under approximation of achievable values will be stored. (default: underapproximation.csv)").setDefaultValueString("underapproximation.csv").build())
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("overapproximation", "The name of the file in which vertices of the over approximation of achievable values will be stored. (default: overapproximation.csv)").setDefaultValueString("overapproximation.csv").build())
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("paretopoints", "The name of the file in which the computed pareto optimal points will be stored. (default: paretopoints.csv)").setDefaultValueString("paretopoints.csv").build())
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("boundaries", "The name of the file in which the corner points of the bounding rectangle will be stored. (default: boundaries.csv)").setDefaultValueString("boundaries.csv").build())
+                                .build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, true, "The precision used for the approximation of numerical- and pareto queries.")
                                 .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision. Default is 1e-04.").setDefaultValueDouble(1e-04).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, maxStepsOptionName, true, "Aborts the computation after the given number of refinement steps (= computed pareto optimal points).")
                                 .addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("value", "the threshold for the number of refinement steps to be performed.").build()).build());
             }
             
-            bool MultiObjectiveSettings::exportResultToFile() const {
-                return this->getOption(exportResultFileOptionName).getHasOptionBeenSet();
+            bool MultiObjectiveSettings::isExportPlotSet() const {
+                return this->getOption(exportPlotOptionName).getHasOptionBeenSet();
             }
             
-            std::string MultiObjectiveSettings::exportResultPath() const {
-                return this->getOption(exportResultFileOptionName).getArgumentByName("filename").getValueAsString();
+            std::string MultiObjectiveSettings::getExportPlotUnderApproximationFileName() const {
+                return this->getOption(exportPlotOptionName).getArgumentByName("directory").getValueAsString() + this->getOption(exportPlotOptionName).getArgumentByName("underapproximation").getValueAsString();
+            }
+            
+            std::string MultiObjectiveSettings::getExportPlotOverApproximationFileName() const {
+                return this->getOption(exportPlotOptionName).getArgumentByName("directory").getValueAsString() + this->getOption(exportPlotOptionName).getArgumentByName("overapproximation").getValueAsString();
+            }
+            
+            std::string MultiObjectiveSettings::getExportPlotParetoPointsFileName() const {
+                return this->getOption(exportPlotOptionName).getArgumentByName("directory").getValueAsString() + this->getOption(exportPlotOptionName).getArgumentByName("paretopoints").getValueAsString();
+            }
+            
+            std::string MultiObjectiveSettings::getExportPlotBoundariesFileName() const {
+                return this->getOption(exportPlotOptionName).getArgumentByName("directory").getValueAsString() + this->getOption(exportPlotOptionName).getArgumentByName("boundaries").getValueAsString();
             }
             
             double MultiObjectiveSettings::getPrecision() const {
@@ -43,6 +61,13 @@ namespace storm {
             uint_fast64_t MultiObjectiveSettings::getMaxSteps() const {
                 return this->getOption(maxStepsOptionName).getArgumentByName("value").getValueAsUnsignedInteger();
             }
+            
+            bool MultiObjectiveSettings::check() const {
+                return ArgumentValidators::writableFileValidator()(getExportPlotUnderApproximationFileName())
+                    && ArgumentValidators::writableFileValidator()(getExportPlotOverApproximationFileName())
+                    && ArgumentValidators::writableFileValidator()(getExportPlotParetoPointsFileName())
+                && ArgumentValidators::writableFileValidator()(getExportPlotBoundariesFileName());
+            }
 
         } // namespace modules
     } // namespace settings
diff --git a/src/settings/modules/MultiObjectiveSettings.h b/src/settings/modules/MultiObjectiveSettings.h
index 42c7d92bd..387e5b771 100644
--- a/src/settings/modules/MultiObjectiveSettings.h
+++ b/src/settings/modules/MultiObjectiveSettings.h
@@ -18,17 +18,35 @@ namespace storm {
                  */
                 MultiObjectiveSettings();
 				
-				/**
-				 * Retrieves whether the model checking result should be exported to a file.
-                 * @return  True iff the result should be exported to a file.
+				/*!
+				 * Retrieves whether the data for plotting should be exported.
+                 * @return  True iff the data for plotting should be exported.
                  */
-				bool exportResultToFile() const;
+				bool isExportPlotSet() const;
 				
-				/**
-				 * The path to a file location which should contain the model checking result.
-                 * @return A path to a file location.
+				/*!
+				 * The path to a file in which vertices of the underapproximation of achievable values should be stored.
+                 * @return A path to a file.
+                 */
+				std::string getExportPlotUnderApproximationFileName() const;
+				
+				/*!
+				 * The path to a file in which vertices of the overapproximation of achievable values should be stored.
+                 * @return A path to a file.
                  */
-				std::string exportResultPath() const;
+				std::string getExportPlotOverApproximationFileName() const;
+				
+				/*!
+				 * The path to a file in which the computed pareto optimal points should be stored.
+                 * @return A path to a file.
+                 */
+				std::string getExportPlotParetoPointsFileName() const;
+				
+				/*!
+				 * The path to a file in which the computed pareto optimal points should be stored.
+                 * @return A path to a file.
+                 */
+				std::string getExportPlotBoundariesFileName() const;
 				
 				/**
 				 * Retrieves the desired precision for numerical- and pareto queries.
@@ -52,10 +70,18 @@ namespace storm {
                 uint_fast64_t getMaxSteps() const;
                 
                 
+                /*!
+                 * Checks whether the settings are consistent. If they are inconsistent, an exception is thrown.
+                 *
+                 * @return True if the settings are consistent.
+                 */
+                virtual bool check() const override;
+                
+                
                 const static std::string moduleName;
                 
             private:
-				const static std::string exportResultFileOptionName;
+				const static std::string exportPlotOptionName;
 				const static std::string precisionOptionName;
 				const static std::string maxStepsOptionName;
             };
diff --git a/src/storage/geometry/Hyperrectangle.h b/src/storage/geometry/Hyperrectangle.h
index 2afdf242e..58c666a90 100644
--- a/src/storage/geometry/Hyperrectangle.h
+++ b/src/storage/geometry/Hyperrectangle.h
@@ -7,7 +7,7 @@
 #include "src/utility/macros.h"
 #include "src/storage/geometry/Polytope.h"
 #include "src/storage/geometry/Halfspace.h"
-#include "src/exceptions/InvalidArgumentException"
+#include "src/exceptions/InvalidArgumentException.h"
 
 namespace storm {
     namespace storage {
@@ -34,7 +34,7 @@ namespace storm {
                     return mLowerBounds;
                 }
                 
-                std::vector<ValueType>& lowerBounds(){
+                std::vector<ValueType>& lowerBounds() {
                     return mLowerBounds;
                 }
                 
@@ -42,21 +42,32 @@ namespace storm {
                     return mUpperBounds;
                 }
                 
-                std::vector<ValueType>& upperBounds(){
+                std::vector<ValueType>& upperBounds() {
                     return mUpperBounds;
                 }
                 
+                /*
+                 * Enlarges this hyperrectangle such that it contains the given point
+                 */
+                void enlarge(std::vector<ValueType> const& point) {
+                    STORM_LOG_THROW(point.size() == lowerBounds().size() && point.size() == upperBounds().size(), storm::exceptions::InvalidArgumentException, "Tried to enlarge a hyperrectangle but the dimension of the given point does not match.");
+                    for(uint_fast64_t i = 0; i<lowerBounds().size(); ++i) {
+                        lowerBounds()[i] = std::min(lowerBounds()[i], point[i]);
+                        upperBounds()[i] = std::max(upperBounds()[i], point[i]);
+                    }
+                }
+                
                 std::shared_ptr<Polytope<ValueType>> asPolytope() const {
-                    STORM_LOG_THROW(lowerBounds.size() == upperBounds.size(), storm::exceptions::InvalidArgumentException, "Tried to construct a polytope form a hyperrectangle but the numbers of given lower and upper bounds do not match.");
+                    STORM_LOG_THROW(lowerBounds().size() == upperBounds().size(), storm::exceptions::InvalidArgumentException, "Tried to construct a polytope form a hyperrectangle but the numbers of given lower and upper bounds do not match.");
                     std::vector<Halfspace<ValueType>> halfspaces;
-                    halfspaces.reserve(2*lowerBounds.size());
-                    for(uint_fast64_t i = 0; i<lowerBounds.size(); ++i) {
-                        std::vector<ValueType> direction(lowerBounds.size(), storm::utility::zero<ValueType>());
+                    halfspaces.reserve(2*lowerBounds().size());
+                    for(uint_fast64_t i = 0; i<lowerBounds().size(); ++i) {
+                        std::vector<ValueType> direction(lowerBounds().size(), storm::utility::zero<ValueType>());
                         direction[i] = -storm::utility::one<ValueType>();
                         ValueType offset = -lowerBounds()[i];
                         halfspaces.emplace_back(std::move(direction), std::move(offset));
                         
-                        direction = std::vector<ValueType>(lowerBounds.size(), storm::utility::zero<ValueType>());
+                        direction = std::vector<ValueType>(lowerBounds().size(), storm::utility::zero<ValueType>());
                         direction[i] = storm::utility::one<ValueType>();
                         offset = upperBounds()[i];
                         halfspaces.emplace_back(std::move(direction), std::move(offset));
diff --git a/src/storage/geometry/HyproPolytope.cpp b/src/storage/geometry/HyproPolytope.cpp
index 0670edd37..a33118e0b 100644
--- a/src/storage/geometry/HyproPolytope.cpp
+++ b/src/storage/geometry/HyproPolytope.cpp
@@ -174,10 +174,10 @@ namespace storm {
                 return true;
             }
             
+            template class HyproPolytope<double>;
 #ifdef STORM_HAVE_CARL
             template class HyproPolytope<storm::RationalNumber>;
 #endif
-            // Note that hypro's polytopes only support exact arithmetic
         }
     }
 }
diff --git a/src/storage/geometry/Polytope.cpp b/src/storage/geometry/Polytope.cpp
index 92f7b08c8..dd65de8e0 100644
--- a/src/storage/geometry/Polytope.cpp
+++ b/src/storage/geometry/Polytope.cpp
@@ -6,7 +6,9 @@
 #include "src/adapters/HyproAdapter.h"
 #include "src/storage/geometry/HyproPolytope.h"
 #include "src/utility/macros.h"
+
 #include "src/exceptions/NotImplementedException.h"
+#include "src/exceptions/IllegalFunctionCallException.h"
 
 namespace storm {
     namespace storage {
@@ -32,22 +34,12 @@ namespace storm {
                 return create(boost::none, std::vector<Point>());
             }
             
-#ifdef STORM_HAVE_CARL
-            template <>
-            std::shared_ptr<Polytope<storm::RationalNumber>> Polytope<storm::RationalNumber>::create(boost::optional<std::vector<Halfspace<storm::RationalNumber>>> const& halfspaces,
-                                                                             boost::optional<std::vector<Point>> const& points) {
-#ifdef STORM_HAVE_HYPRO
-                return HyproPolytope<storm::RationalNumber>::create(halfspaces, points);
-#endif
-                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "No polytope implementation specified.");
-                return nullptr;
-            }
-#endif
-            
             template <typename ValueType>
             std::shared_ptr<Polytope<ValueType>> Polytope<ValueType>::create(boost::optional<std::vector<Halfspace<ValueType>>> const& halfspaces,
                                                                              boost::optional<std::vector<Point>> const& points) {
-                //Note: hypro polytopes (currently) do not work with non-exact arithmetic (e.g., double)
+#ifdef STORM_HAVE_HYPRO
+                return HyproPolytope<ValueType>::create(halfspaces, points);
+#endif
                 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "No polytope implementation specified.");
                 return nullptr;
             }
@@ -105,6 +97,70 @@ namespace storm {
                 return std::vector<Point>();
             }
             
+#ifdef STORM_HAVE_CARL
+            template <>
+            std::vector<typename Polytope<storm::RationalNumber>::Point> Polytope<storm::RationalNumber>::getVerticesInClockwiseOrder() const{
+                std::vector<Point> vertices = getVertices();
+                if(vertices.size()<=2) {
+                    // In this case, every ordering is clockwise
+                    return vertices;
+                }
+                STORM_LOG_THROW(vertices.front().size()==2, storm::exceptions::IllegalFunctionCallException, "Getting Vertices in clockwise order is only possible for a 2D-polytope.");
+                
+                std::vector<storm::storage::BitVector> neighborsOfVertices(vertices.size(), storm::storage::BitVector(vertices.size(), false));
+                std::vector<Halfspace<storm::RationalNumber>> halfspaces = getHalfspaces();
+                for(auto const& h : halfspaces) {
+                    storm::storage::BitVector verticesOnHalfspace(vertices.size(), false);
+                    for(uint_fast64_t v = 0; v<vertices.size(); ++v) {
+                        if(storm::utility::isZero(h.distance(vertices[v]))) {
+                            verticesOnHalfspace.set(v);
+                        }
+                    }
+                    for(auto const& v : verticesOnHalfspace) {
+                        neighborsOfVertices[v] |= verticesOnHalfspace;
+                        neighborsOfVertices[v].set(v, false);
+                    }
+                }
+                
+                std::vector<Point> result;
+                result.reserve(vertices.size());
+                storm::storage::BitVector unprocessedVertices(vertices.size(), true);
+                
+                uint_fast64_t currentVertex = 0;
+                for(uint_fast64_t v = 1; v<vertices.size(); ++v) {
+                    if(vertices[v].front() < vertices[currentVertex].front()) {
+                        currentVertex = v;
+                    }
+                }
+                STORM_LOG_ASSERT(neighborsOfVertices[currentVertex].getNumberOfSetBits()==2, "For 2D Polytopes with at least 3 vertices, each vertex should have exactly 2 neighbors");
+                uint_fast64_t firstNeighbor = neighborsOfVertices[currentVertex].getNextSetIndex(0);
+                uint_fast64_t secondNeighbor = neighborsOfVertices[currentVertex].getNextSetIndex(firstNeighbor+1);
+                uint_fast64_t previousVertex = vertices[firstNeighbor].back() <= vertices[secondNeighbor].back() ? firstNeighbor : secondNeighbor;
+                do {
+                    unprocessedVertices.set(currentVertex, false);
+                    result.push_back(std::move(vertices[currentVertex]));
+                    
+                    STORM_LOG_ASSERT(neighborsOfVertices[currentVertex].getNumberOfSetBits()==2, "For 2D Polytopes with at least 3 vertices, each vertex should have exactly 2 neighbors");
+                    firstNeighbor = neighborsOfVertices[currentVertex].getNextSetIndex(0);
+                    secondNeighbor = neighborsOfVertices[currentVertex].getNextSetIndex(firstNeighbor+1);
+                    uint_fast64_t nextVertex = firstNeighbor != previousVertex ? firstNeighbor : secondNeighbor;
+                    previousVertex = currentVertex;
+                    currentVertex = nextVertex;
+                } while(!unprocessedVertices.empty());
+                
+                return result;
+            }
+#endif
+            
+
+            template <typename ValueType>
+            std::vector<typename Polytope<ValueType>::Point> Polytope<ValueType>::getVerticesInClockwiseOrder() const{
+                STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented.");
+                // Note that the implementation for RationalNumber above only works for exact ValueType since
+                // checking whether the distance between halfspace and point is zero is problematic otherwise.
+                return std::vector<Point>();
+            }
+            
             template <typename ValueType>
             std::vector<Halfspace<ValueType>> Polytope<ValueType>::getHalfspaces() const {
                 STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Functionality not implemented.");
@@ -176,13 +232,29 @@ namespace storm {
                 return std::make_pair(Point(), false);
             }
             
+            template <typename ValueType>
+            template <typename TargetType>
+            std::shared_ptr<Polytope<TargetType>> Polytope<ValueType>::convertNumberRepresentation() const {
+                if(isEmpty()) {
+                    return Polytope<TargetType>::createEmptyPolytope();
+                }
+                auto halfspaces = getHalfspaces();
+                std::vector<Halfspace<TargetType>> halfspacesPrime;
+                halfspacesPrime.reserve(halfspaces.size());
+                for(auto const& h : halfspaces) {
+                    halfspacesPrime.emplace_back(storm::utility::vector::convertNumericVector<TargetType>(h.normalVector()), storm::utility::convertNumber<TargetType>(h.offset()));
+                }
+                
+                return Polytope<TargetType>::create(halfspacesPrime);
+            }
+            
             template <typename ValueType>
             std::string Polytope<ValueType>::toString(bool numbersAsDouble) const {
                 auto halfspaces = this->getHalfspaces();
                 std::stringstream stream;
                 stream << "Polytope with " << halfspaces.size() << " Halfspaces" << (halfspaces.empty() ? "" : ":") << std::endl;
                 for (auto const& h : halfspaces) {
-                    stream << "|   " << h.toString(numbersAsDouble) << std::endl;
+                    stream << "   " << h.toString(numbersAsDouble) << std::endl;
                 }
                 return stream.str();
             }
@@ -192,11 +264,13 @@ namespace storm {
                 return false;
             }
             
+            template class Polytope<double>;
+            
 #ifdef STORM_HAVE_CARL
             template class Polytope<storm::RationalNumber>;
+            template std::shared_ptr<Polytope<double>> Polytope<storm::RationalNumber>::convertNumberRepresentation() const;
+            template std::shared_ptr<Polytope<storm::RationalNumber>> Polytope<double>::convertNumberRepresentation() const;
 #endif
-            template class Polytope<double>;
-            // Note that HyproPolytopes only support exact arithmetic
         }
     }
 }
diff --git a/src/storage/geometry/Polytope.h b/src/storage/geometry/Polytope.h
index 2950d2c94..0767ce346 100644
--- a/src/storage/geometry/Polytope.h
+++ b/src/storage/geometry/Polytope.h
@@ -52,6 +52,12 @@ namespace storm {
                  */
                 virtual std::vector<Point> getVertices() const;
                 
+                /*!
+                 * Returns the vertices of this 2D-polytope in clockwise order.
+                 * An Exception is thrown if the dimension of this polytope is not two.
+                 */
+                virtual std::vector<Point> getVerticesInClockwiseOrder() const;
+                
                 /*!
                  * Returns the halfspaces of this polytope.
                  */
@@ -116,8 +122,14 @@ namespace storm {
                  */
                 virtual std::pair<Point, bool> optimize(Point const& direction) const;
                 
+                /*!
+                 * converts the intern number representation of the polytope to the given target type
+                 */
+                template <typename TargetType>
+                std::shared_ptr<Polytope<TargetType>> convertNumberRepresentation() const;
+                
                 /*
-                 * Returns a string representation of this polytope.
+                 * Returns a string repre/Users/tim/storm/src/storage/geometry/Polytope.h:129:17: 'virtual' cannot be specified on member function templatessentation of this polytope.
                  * If the given flag is true, the occurring numbers are converted to double before printing to increase readability
                  */
                 virtual std::string toString(bool numbersAsDouble = false) const;
diff --git a/src/utility/Stopwatch.h b/src/utility/Stopwatch.h
index 0af496c54..0ee408808 100644
--- a/src/utility/Stopwatch.h
+++ b/src/utility/Stopwatch.h
@@ -25,6 +25,10 @@ namespace storm {
                 }
             }
             
+            void addToAccumulatedSeconds(double value) {
+                accumulatedSeconds += value;
+            }
+            
             void pause() {
                 if(paused) {
                     STORM_LOG_WARN("Tried to pause a stopwatch that was already paused.");
diff --git a/src/utility/export.h b/src/utility/export.h
index 4d172bcdc..1af871efc 100644
--- a/src/utility/export.h
+++ b/src/utility/export.h
@@ -9,43 +9,74 @@
 #define STORM_UTILITY_EXPORT_H_
 
 #include <iostream>
+#include <boost/optional.hpp>
 
-#include "src/storage/parameters.h"
-#include "src/settings/modules/ParametricSettings.h"
-#include "src/modelchecker/reachability/CollectConstraints.h"
+#include "src/utility/macros.h"
+#include "src/exceptions/FileIoException.h"
 
-namespace storm {
-namespace utility {
-
-template<typename ValueType>	
-void exportParametricMcResult(const ValueType& mcresult, storm::modelchecker::reachability::CollectConstraints<storm::RationalFunction> const& constraintCollector) {
-	std::string path = storm::settings::getModule<storm::settings::modules::ParametricSettings>().exportResultPath();
-	std::ofstream filestream;
-	filestream.open(path);
-	// todo add checks.
-	filestream << "!Parameters: ";
-	std::set<storm::Variable> vars = mcresult.gatherVariables();
-	std::copy(vars.begin(), vars.end(), std::ostream_iterator<storm::Variable>(filestream, ", "));
-	filestream << std::endl;
-	filestream << "!Result: " << mcresult << std::endl;
-	filestream << "!Well-formed Constraints: " << std::endl;
-	std::copy(constraintCollector.wellformedConstraints().begin(), constraintCollector.wellformedConstraints().end(), std::ostream_iterator<carl::Constraint<ValueType>>(filestream, "\n"));
-	filestream << "!Graph-preserving Constraints: " << std::endl;
-	std::copy(constraintCollector.graphPreservingConstraints().begin(), constraintCollector.graphPreservingConstraints().end(), std::ostream_iterator<carl::Constraint<ValueType>>(filestream, "\n"));
-	filestream.close();
-}
+//#include "src/storage/parameters.h"
+//#include "src/settings/modules/ParametricSettings.h"
+//#include "src/modelchecker/reachability/CollectConstraints.h"
 
-void exportStringStreamToFile(std::string const& str, std::string filepath) {
-	// todo add checks.
-	std::ofstream filestream;
-	filestream.open(filepath);
-	filestream << str;
-	filestream.close();
-}
+namespace storm {
+    namespace utility {
 
-}
+            /* TODO Fix me
+        template<typename ValueType>	
+        void exportParametricMcResult(const ValueType& mcresult, storm::modelchecker::reachability::CollectConstraints<storm::RationalFunction> const& constraintCollector) {
+            std::string path = storm::settings::getModule<storm::settings::modules::ParametricSettings>().exportResultPath();
+            std::ofstream filestream;
+            filestream.open(path);
+            // todo add checks.
+            filestream << "!Parameters: ";
+            std::set<storm::Variable> vars = mcresult.gatherVariables();
+            std::copy(vars.begin(), vars.end(), std::ostream_iterator<storm::Variable>(filestream, ", "));
+            filestream << std::endl;
+            filestream << "!Result: " << mcresult << std::endl;
+            filestream << "!Well-formed Constraints: " << std::endl;
+            std::copy(constraintCollector.wellformedConstraints().begin(), constraintCollector.wellformedConstraints().end(), std::ostream_iterator<carl::Constraint<ValueType>>(filestream, "\n"));
+            filestream << "!Graph-preserving Constraints: " << std::endl;
+            std::copy(constraintCollector.graphPreservingConstraints().begin(), constraintCollector.graphPreservingConstraints().end(), std::ostream_iterator<carl::Constraint<ValueType>>(filestream, "\n"));
+            filestream.close();
+        }
+        */
+            
+        void exportStringToFile(std::string const& str, std::string filepath) {
+            std::ofstream filestream;
+            filestream.open(filepath);
+            STORM_LOG_THROW(filestream.is_open(), storm::exceptions::FileIoException , "Could not open file " << filepath << ".");
+            filestream << str;
+        }
+        
+        template <typename ValueType>
+        void exportDataToCSVFile(std::string filepath, std::vector<std::vector<ValueType>> const& data, boost::optional<std::vector<std::string>> const& columnHeaders) {
+            std::ofstream filestream;
+            filestream.open(filepath);
+            STORM_LOG_THROW(filestream.is_open(), storm::exceptions::FileIoException , "Could not open file " << filepath << ".");
+            
+            if(columnHeaders) {
+                for(auto columnIt = columnHeaders->begin(); columnIt != columnHeaders->end(); ++columnIt) {
+                    if(columnIt != columnHeaders->begin()) {
+                        filestream << ",";
+                    }
+                    filestream << *columnIt;
+                }
+                filestream << std::endl;
+            }
+            
+            for (auto const& row : data) {
+                for(auto columnIt = row.begin(); columnIt != row.end(); ++columnIt) {
+                    if(columnIt != row.begin()) {
+                        filestream << ",";
+                    }
+                    filestream << *columnIt;
+                }
+                filestream << std::endl;
+            }
+        }
+    }
 }
 
 
 
-#endif
\ No newline at end of file
+#endif