diff --git a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp
index 639589592..93337995d 100644
--- a/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp
+++ b/src/storm/modelchecker/multiobjective/pcaa/SparsePcaaParetoQuery.cpp
@@ -4,7 +4,7 @@
 #include "storm/models/sparse/Mdp.h"
 #include "storm/models/sparse/MarkovAutomaton.h"
 #include "storm/models/sparse/StandardRewardModel.h"
-#include "storm/modelchecker/results/ParetoCurveCheckResult.h"
+#include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h"
 #include "storm/utility/constants.h"
 #include "storm/utility/vector.h"
 #include "storm/settings/SettingsManager.h"
@@ -43,7 +43,7 @@ namespace storm {
                 for(auto const& vertex : vertices) {
                     paretoOptimalPoints.push_back(storm::utility::vector::convertNumericVector<typename SparseModelType::ValueType>(this->transformPointToOriginalModel(vertex)));
                 }
-                return std::unique_ptr<CheckResult>(new ParetoCurveCheckResult<typename SparseModelType::ValueType>(this->originalModel.getInitialStates().getNextSetIndex(0),
+                return std::unique_ptr<CheckResult>(new ExplicitParetoCurveCheckResult<typename SparseModelType::ValueType>(this->originalModel.getInitialStates().getNextSetIndex(0),
                                                                         std::move(paretoOptimalPoints),
                                                                         this->transformPolytopeToOriginalModel(this->underApproximation)->template convertNumberRepresentation<typename SparseModelType::ValueType>(),
                                                                         this->transformPolytopeToOriginalModel(this->overApproximation)->template convertNumberRepresentation<typename SparseModelType::ValueType>()));
diff --git a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp
index d42d81251..d42de45dd 100644
--- a/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp
+++ b/src/storm/modelchecker/prctl/HybridMdpPrctlModelChecker.cpp
@@ -5,8 +5,14 @@
 #include "storm/models/symbolic/Mdp.h"
 #include "storm/models/symbolic/StandardRewardModel.h"
 
+#include "storm/storage/dd/DdManager.h"
+
 #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
 #include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h"
+#include "storm/modelchecker/results/SymbolicParetoCurveCheckResult.h"
+#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
+#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+#include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h"
 
 #include "storm/logic/FragmentSpecification.h"
 
@@ -21,6 +27,7 @@
 
 #include "storm/exceptions/InvalidStateException.h"
 #include "storm/exceptions/InvalidPropertyException.h"
+#include "storm/exceptions/UnexpectedException.h"
 
 namespace storm {
     namespace modelchecker {
@@ -41,7 +48,8 @@ namespace storm {
                 return true;
             } else {
                 // Check whether we consider a multi-objective formula
-                // For multi-objective model checking, each state requires an individual scheduler (in contrast to single-objective model checking). Let's exclude that all states are considered.
+                // For multi-objective model checking, each state requires an individual scheduler (in contrast to single-objective model checking). Let's exclude that multiple states are relevant
+                if(this->getModel().getInitialStates().getNonZeroCount() > 1) return false;
                 if(!checkTask.isOnlyInitialStatesRelevantSet()) return false;
                 return formula.isInFragment(storm::logic::multiObjective().setCumulativeRewardFormulasAllowed(true));
             }
@@ -118,7 +126,25 @@ namespace storm {
         template<typename ModelType>
         std::unique_ptr<CheckResult> HybridMdpPrctlModelChecker<ModelType>::checkMultiObjectiveFormula(CheckTask<storm::logic::MultiObjectiveFormula, ValueType> const& checkTask) {
             auto sparseModel = storm::transformer::SymbolicMdpToSparseMdpTransformer<DdType, ValueType>::translate(this->getModel());
-			return multiobjective::performPcaa(*sparseModel, checkTask.getFormula());
+            std::unique_ptr<CheckResult> explicitResult = multiobjective::performPcaa(*sparseModel, checkTask.getFormula());
+
+            // Convert the explicit result
+            if(explicitResult->isExplicitQualitativeCheckResult()) {
+                if(explicitResult->asExplicitQualitativeCheckResult()[*sparseModel->getInitialStates().begin()]) {
+                    return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(this->getModel().getReachableStates(), this->getModel().getInitialStates(), this->getModel().getManager().getBddOne()));
+                } else {
+                    return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQualitativeCheckResult<DdType>(this->getModel().getReachableStates(), this->getModel().getInitialStates(), this->getModel().getManager().getBddZero()));
+                }
+            } else if(explicitResult->isExplicitQuantitativeCheckResult()) {
+                ValueType const& res = explicitResult->template asExplicitQuantitativeCheckResult<ValueType>()[*sparseModel->getInitialStates().begin()];
+                return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicQuantitativeCheckResult<DdType, ValueType>(this->getModel().getReachableStates(), this->getModel().getInitialStates(), this->getModel().getManager().template getConstant<ValueType>(res)));
+            } else if(explicitResult->isExplicitParetoCurveCheckResult()) {
+                ExplicitParetoCurveCheckResult<ValueType> const& paretoResult = explicitResult->template asExplicitParetoCurveCheckResult<ValueType>();
+                return std::unique_ptr<CheckResult>(new storm::modelchecker::SymbolicParetoCurveCheckResult<DdType, ValueType>(this->getModel().getInitialStates(), paretoResult.getPoints(), paretoResult.getUnderApproximation(), paretoResult.getOverApproximation()));
+            } else {
+                STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "The obtained checkresult has an unexpected type.");
+                return nullptr;
+            }
         }
 
         template class HybridMdpPrctlModelChecker<storm::models::symbolic::Mdp<storm::dd::DdType::CUDD, double>>;
diff --git a/src/storm/modelchecker/results/CheckResult.cpp b/src/storm/modelchecker/results/CheckResult.cpp
index 210ca3b59..44cedb816 100644
--- a/src/storm/modelchecker/results/CheckResult.cpp
+++ b/src/storm/modelchecker/results/CheckResult.cpp
@@ -5,10 +5,11 @@
 
 #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
 #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+#include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h"
 #include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
 #include "storm/modelchecker/results/SymbolicQuantitativeCheckResult.h"
+#include "storm/modelchecker/results/SymbolicParetoCurveCheckResult.h"
 #include "storm/modelchecker/results/HybridQuantitativeCheckResult.h"
-#include "storm/modelchecker/results/ParetoCurveCheckResult.h"
 
 #include "storm/utility/macros.h"
 #include "storm/exceptions/InvalidOperationException.h"
@@ -34,7 +35,11 @@ namespace storm {
         bool CheckResult::isQualitative() const {
             return false;
         }
-        
+
+        bool CheckResult::isParetoCurveCheckResult() const {
+            return false;
+        }
+
         bool CheckResult::isResultForAllStates() const {
             return false;
         }
@@ -51,7 +56,11 @@ namespace storm {
         bool CheckResult::isExplicitQuantitativeCheckResult() const {
             return false;
         }
-        
+
+        bool CheckResult::isExplicitParetoCurveCheckResult() const {
+            return false;
+        }
+
         bool CheckResult::isSymbolicQualitativeCheckResult() const {
             return false;
         }
@@ -59,12 +68,12 @@ namespace storm {
         bool CheckResult::isSymbolicQuantitativeCheckResult() const {
             return false;
         }
-        
-        bool CheckResult::isHybridQuantitativeCheckResult() const {
+
+        bool CheckResult::isSymbolicParetoCurveCheckResult() const {
             return false;
         }
-        
-        bool CheckResult::isParetoCurveCheckResult() const {
+
+        bool CheckResult::isHybridQuantitativeCheckResult() const {
             return false;
         }
         
@@ -85,6 +94,16 @@ namespace storm {
         ExplicitQuantitativeCheckResult<ValueType> const& CheckResult::asExplicitQuantitativeCheckResult() const {
             return dynamic_cast<ExplicitQuantitativeCheckResult<ValueType> const&>(*this);
         }
+
+        template<typename ValueType>
+        ExplicitParetoCurveCheckResult<ValueType>& CheckResult::asExplicitParetoCurveCheckResult() {
+            return dynamic_cast<ExplicitParetoCurveCheckResult<ValueType>&>(*this);
+        }
+
+        template<typename ValueType>
+        ExplicitParetoCurveCheckResult<ValueType> const& CheckResult::asExplicitParetoCurveCheckResult() const {
+            return dynamic_cast<ExplicitParetoCurveCheckResult<ValueType> const&>(*this);
+        }
         
         QualitativeCheckResult& CheckResult::asQualitativeCheckResult() {
             return dynamic_cast<QualitativeCheckResult&>(*this);
@@ -124,25 +143,29 @@ namespace storm {
         HybridQuantitativeCheckResult<Type, ValueType> const& CheckResult::asHybridQuantitativeCheckResult() const {
             return dynamic_cast<HybridQuantitativeCheckResult<Type, ValueType> const&>(*this);
         }
-        
-        template<typename ValueType>
-        ParetoCurveCheckResult<ValueType>& CheckResult::asParetoCurveCheckResult() {
-            return dynamic_cast<ParetoCurveCheckResult<ValueType>&>(*this);
+
+        template <storm::dd::DdType Type, typename ValueType>
+        SymbolicParetoCurveCheckResult<Type, ValueType>& CheckResult::asSymbolicParetoCurveCheckResult() {
+            return dynamic_cast<SymbolicParetoCurveCheckResult<Type, ValueType>&>(*this);
         }
-        
-        template<typename ValueType>
-        ParetoCurveCheckResult<ValueType> const& CheckResult::asParetoCurveCheckResult() const {
-            return dynamic_cast<ParetoCurveCheckResult<ValueType> const&>(*this);
+
+        template <storm::dd::DdType Type, typename ValueType>
+        SymbolicParetoCurveCheckResult<Type, ValueType> const& CheckResult::asSymbolicParetoCurveCheckResult() const {
+            return dynamic_cast<SymbolicParetoCurveCheckResult<Type, ValueType> const&>(*this);
         }
         
         // Explicitly instantiate the template functions.
         template ExplicitQuantitativeCheckResult<double>& CheckResult::asExplicitQuantitativeCheckResult();
         template ExplicitQuantitativeCheckResult<double> const& CheckResult::asExplicitQuantitativeCheckResult() const;
+        template ExplicitParetoCurveCheckResult<double>& CheckResult::asExplicitParetoCurveCheckResult();
+        template ExplicitParetoCurveCheckResult<double> const& CheckResult::asExplicitParetoCurveCheckResult() const;
 
         template SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD>& CheckResult::asSymbolicQualitativeCheckResult();
         template SymbolicQualitativeCheckResult<storm::dd::DdType::CUDD> const& CheckResult::asSymbolicQualitativeCheckResult() const;
         template SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double>& CheckResult::asSymbolicQuantitativeCheckResult();
         template SymbolicQuantitativeCheckResult<storm::dd::DdType::CUDD, double> const& CheckResult::asSymbolicQuantitativeCheckResult() const;
+        template SymbolicParetoCurveCheckResult<storm::dd::DdType::CUDD, double>& CheckResult::asSymbolicParetoCurveCheckResult();
+        template SymbolicParetoCurveCheckResult<storm::dd::DdType::CUDD, double> const& CheckResult::asSymbolicParetoCurveCheckResult() const;
         template HybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double>& CheckResult::asHybridQuantitativeCheckResult();
         template HybridQuantitativeCheckResult<storm::dd::DdType::CUDD, double> const& CheckResult::asHybridQuantitativeCheckResult() const;
 
@@ -150,11 +173,11 @@ namespace storm {
         template SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan> const& CheckResult::asSymbolicQualitativeCheckResult() const;
         template SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double>& CheckResult::asSymbolicQuantitativeCheckResult();
         template SymbolicQuantitativeCheckResult<storm::dd::DdType::Sylvan, double> const& CheckResult::asSymbolicQuantitativeCheckResult() const;
+        template SymbolicParetoCurveCheckResult<storm::dd::DdType::Sylvan, double>& CheckResult::asSymbolicParetoCurveCheckResult();
+        template SymbolicParetoCurveCheckResult<storm::dd::DdType::Sylvan, double> const& CheckResult::asSymbolicParetoCurveCheckResult() 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::RationalNumber>& CheckResult::asExplicitQuantitativeCheckResult();
@@ -163,8 +186,8 @@ namespace storm {
         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;
+        template ExplicitParetoCurveCheckResult<storm::RationalNumber>& CheckResult::asExplicitParetoCurveCheckResult();
+        template ExplicitParetoCurveCheckResult<storm::RationalNumber> const& CheckResult::asExplicitParetoCurveCheckResult() const;
 #endif
     }
 }
diff --git a/src/storm/modelchecker/results/CheckResult.h b/src/storm/modelchecker/results/CheckResult.h
index 6cf39669d..2cff249c9 100644
--- a/src/storm/modelchecker/results/CheckResult.h
+++ b/src/storm/modelchecker/results/CheckResult.h
@@ -18,18 +18,21 @@ namespace storm {
         template <typename ValueType>
         class ExplicitQuantitativeCheckResult;
         
+        template <typename ValueType>
+        class ExplicitParetoCurveCheckResult;
+
         template <storm::dd::DdType Type>
         class SymbolicQualitativeCheckResult;
-        
+
         template <storm::dd::DdType Type, typename ValueType>
         class SymbolicQuantitativeCheckResult;
-        
+
         template <storm::dd::DdType Type, typename ValueType>
         class HybridQuantitativeCheckResult;
-        
-        template <typename ValueType>
-        class ParetoCurveCheckResult;
-        
+
+        template <storm::dd::DdType Type, typename ValueType>
+        class SymbolicParetoCurveCheckResult;
+
         // The base class of all check results.
         class CheckResult {
         public:
@@ -49,12 +52,14 @@ namespace storm {
             virtual bool isHybrid() const;
             virtual bool isQuantitative() const;
             virtual bool isQualitative() const;
+            virtual bool isParetoCurveCheckResult() const;
             virtual bool isExplicitQualitativeCheckResult() const;
             virtual bool isExplicitQuantitativeCheckResult() const;
+            virtual bool isExplicitParetoCurveCheckResult() const;
             virtual bool isSymbolicQualitativeCheckResult() const;
             virtual bool isSymbolicQuantitativeCheckResult() const;
+            virtual bool isSymbolicParetoCurveCheckResult() const;
             virtual bool isHybridQuantitativeCheckResult() const;
-            virtual bool isParetoCurveCheckResult() const;
             virtual bool isResultForAllStates() const;
             
             QualitativeCheckResult& asQualitativeCheckResult();
@@ -78,6 +83,12 @@ namespace storm {
 
             template<typename ValueType>
             ExplicitQuantitativeCheckResult<ValueType> const& asExplicitQuantitativeCheckResult() const;
+
+            template <typename ValueType>
+            ExplicitParetoCurveCheckResult<ValueType>& asExplicitParetoCurveCheckResult();
+
+            template <typename ValueType>
+            ExplicitParetoCurveCheckResult<ValueType> const& asExplicitParetoCurveCheckResult() const;
             
             template <storm::dd::DdType Type>
             SymbolicQualitativeCheckResult<Type>& asSymbolicQualitativeCheckResult();
@@ -97,11 +108,11 @@ 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;
+            template <storm::dd::DdType Type, typename ValueType>
+            SymbolicParetoCurveCheckResult<Type, ValueType>& asSymbolicParetoCurveCheckResult();
+
+            template <storm::dd::DdType Type, typename ValueType>
+            SymbolicParetoCurveCheckResult<Type, ValueType> const& asSymbolicParetoCurveCheckResult() const;
             
             virtual std::ostream& writeToStream(std::ostream& out) const = 0;
         };
diff --git a/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp b/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp
new file mode 100644
index 000000000..9294cd627
--- /dev/null
+++ b/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.cpp
@@ -0,0 +1,58 @@
+
+#include "storm/modelchecker/results/ExplicitParetoCurveCheckResult.h"
+
+#include "storm/adapters/CarlAdapter.h"
+#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
+#include "storm/utility/macros.h"
+#include "storm/utility/vector.h"
+
+#include "storm/exceptions/InvalidOperationException.h"
+
+namespace storm {
+    namespace modelchecker {
+        template<typename ValueType>
+        ExplicitParetoCurveCheckResult<ValueType>::ExplicitParetoCurveCheckResult() {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType>
+        ExplicitParetoCurveCheckResult<ValueType>::ExplicitParetoCurveCheckResult(storm::storage::sparse::state_type const& state, std::vector<typename ParetoCurveCheckResult<ValueType>::point_type> const& points, typename ParetoCurveCheckResult<ValueType>::polytope_type const& underApproximation, typename ParetoCurveCheckResult<ValueType>::polytope_type const& overApproximation) : ParetoCurveCheckResult<ValueType>(points, underApproximation, overApproximation), state(state) {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType>
+        ExplicitParetoCurveCheckResult<ValueType>::ExplicitParetoCurveCheckResult(storm::storage::sparse::state_type const& state, std::vector<typename ParetoCurveCheckResult<ValueType>::point_type>&& points, typename ParetoCurveCheckResult<ValueType>::polytope_type&& underApproximation, typename ParetoCurveCheckResult<ValueType>::polytope_type&& overApproximation) : ParetoCurveCheckResult<ValueType>(points, underApproximation, overApproximation), state(state) {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType>
+        bool ExplicitParetoCurveCheckResult<ValueType>::isExplicitParetoCurveCheckResult() const {
+            return true;
+        }
+
+        template<typename ValueType>
+        bool ExplicitParetoCurveCheckResult<ValueType>::isExplicit() const {
+            return true;
+        }
+        
+        template<typename ValueType>
+        void ExplicitParetoCurveCheckResult<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& ExplicitParetoCurveCheckResult<ValueType>:: getState() const {
+            return state;
+        }
+
+        template class ExplicitParetoCurveCheckResult<double>;
+#ifdef STORM_HAVE_CARL
+        template class ExplicitParetoCurveCheckResult<storm::RationalNumber>;
+#endif
+    }
+}
diff --git a/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.h b/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.h
new file mode 100644
index 000000000..251102f01
--- /dev/null
+++ b/src/storm/modelchecker/results/ExplicitParetoCurveCheckResult.h
@@ -0,0 +1,39 @@
+#ifndef STORM_MODELCHECKER_EXPLICITPARETOCURVECHECKRESULT_H_
+#define STORM_MODELCHECKER_EXPLICITPARETOCURVECHECKRESULT_H_
+
+#include <vector>
+
+#include "storm/modelchecker/results/ParetoCurveCheckResult.h"
+#include "storm/storage/sparse/StateType.h"
+
+namespace storm {
+    namespace modelchecker {
+        template<typename ValueType>
+        class ExplicitParetoCurveCheckResult : public ParetoCurveCheckResult<ValueType> {
+        public:
+
+            ExplicitParetoCurveCheckResult();
+            ExplicitParetoCurveCheckResult(storm::storage::sparse::state_type const& state, std::vector<typename ParetoCurveCheckResult<ValueType>::point_type> const& points, typename ParetoCurveCheckResult<ValueType>::polytope_type const& underApproximation, typename ParetoCurveCheckResult<ValueType>::polytope_type const& overApproximation);
+            ExplicitParetoCurveCheckResult(storm::storage::sparse::state_type const& state, std::vector<typename ParetoCurveCheckResult<ValueType>::point_type>&& points, typename ParetoCurveCheckResult<ValueType>::polytope_type&& underApproximation, typename ParetoCurveCheckResult<ValueType>::polytope_type&& overApproximation);
+            
+            ExplicitParetoCurveCheckResult(ExplicitParetoCurveCheckResult const& other) = default;
+            ExplicitParetoCurveCheckResult& operator=(ExplicitParetoCurveCheckResult const& other) = default;
+            ExplicitParetoCurveCheckResult(ExplicitParetoCurveCheckResult&& other) = default;
+            ExplicitParetoCurveCheckResult& operator=(ExplicitParetoCurveCheckResult&& other) = default;
+            virtual ~ExplicitParetoCurveCheckResult() = default;
+            
+            virtual bool isExplicitParetoCurveCheckResult() const override;
+            virtual bool isExplicit() const override;
+
+            virtual void filter(QualitativeCheckResult const& filter) override;
+            
+            storm::storage::sparse::state_type const& getState() const;
+
+        private:
+            // The state of the checked model to which the result applies
+            storm::storage::sparse::state_type state;
+        };
+    }
+}
+
+#endif /* STORM_MODELCHECKER_EXPLICITPARETOCURVECHECKRESULT_H_ */
diff --git a/src/storm/modelchecker/results/ParetoCurveCheckResult.cpp b/src/storm/modelchecker/results/ParetoCurveCheckResult.cpp
index d4aa5ca64..a76857576 100644
--- a/src/storm/modelchecker/results/ParetoCurveCheckResult.cpp
+++ b/src/storm/modelchecker/results/ParetoCurveCheckResult.cpp
@@ -1,49 +1,31 @@
 #include "storm/modelchecker/results/ParetoCurveCheckResult.h"
 
 #include "storm/adapters/CarlAdapter.h"
-#include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
-#include "storm/utility/macros.h"
 #include "storm/utility/vector.h"
 
-#include "storm/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) {
+        ParetoCurveCheckResult<ValueType>::ParetoCurveCheckResult(std::vector<point_type> const& points, polytope_type const& underApproximation, polytope_type const& overApproximation) : 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) {
+        ParetoCurveCheckResult<ValueType>::ParetoCurveCheckResult(std::vector<point_type>&& points, polytope_type&& underApproximation, polytope_type&& overApproximation) : 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;
diff --git a/src/storm/modelchecker/results/ParetoCurveCheckResult.h b/src/storm/modelchecker/results/ParetoCurveCheckResult.h
index 3a2618b3d..5f0979f44 100644
--- a/src/storm/modelchecker/results/ParetoCurveCheckResult.h
+++ b/src/storm/modelchecker/results/ParetoCurveCheckResult.h
@@ -4,8 +4,6 @@
 #include <vector>
 
 #include "storm/modelchecker/results/CheckResult.h"
-#include "storm/utility/OsDetection.h"
-#include "storm/storage/sparse/StateType.h"
 #include "storm/storage/geometry/Polytope.h"
 
 namespace storm {
@@ -15,32 +13,22 @@ namespace storm {
         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;
-            
+        protected:
+            ParetoCurveCheckResult(std::vector<point_type> const& points, polytope_type const& underApproximation, polytope_type const& overApproximation);
+            ParetoCurveCheckResult(std::vector<point_type>&& points, polytope_type&& underApproximation, polytope_type&& overApproximation);
+
+
             // The pareto optimal points that have been found.
             std::vector<point_type> points;
             
diff --git a/src/storm/modelchecker/results/SymbolicParetoCurveCheckResult.cpp b/src/storm/modelchecker/results/SymbolicParetoCurveCheckResult.cpp
new file mode 100644
index 000000000..868116adf
--- /dev/null
+++ b/src/storm/modelchecker/results/SymbolicParetoCurveCheckResult.cpp
@@ -0,0 +1,57 @@
+
+#include "storm/modelchecker/results/SymbolicParetoCurveCheckResult.h"
+
+#include "storm/adapters/CarlAdapter.h"
+#include "storm/modelchecker/results/SymbolicQualitativeCheckResult.h"
+#include "storm/utility/macros.h"
+#include "storm/storage/dd/DdManager.h"
+
+#include "storm/exceptions/InvalidOperationException.h"
+
+namespace storm {
+    namespace modelchecker {
+        template<storm::dd::DdType Type, typename ValueType>
+        SymbolicParetoCurveCheckResult<Type, ValueType>::SymbolicParetoCurveCheckResult() {
+            // Intentionally left empty.
+        }
+
+        template<storm::dd::DdType Type, typename ValueType>
+        SymbolicParetoCurveCheckResult<Type, ValueType>::SymbolicParetoCurveCheckResult(storm::dd::Bdd<Type> const& state, std::vector<typename ParetoCurveCheckResult<ValueType>::point_type> const& points, typename ParetoCurveCheckResult<ValueType>::polytope_type const& underApproximation, typename ParetoCurveCheckResult<ValueType>::polytope_type const& overApproximation) : ParetoCurveCheckResult<ValueType>(points, underApproximation, overApproximation), state(state) {
+            STORM_LOG_THROW(this->state.getNonZeroCount() == 1, storm::exceptions::InvalidOperationException, "ParetoCheckResults are only relevant for a single state.");
+        }
+
+        template<storm::dd::DdType Type, typename ValueType>
+        SymbolicParetoCurveCheckResult<Type, ValueType>::SymbolicParetoCurveCheckResult(storm::dd::Bdd<Type> const& state, std::vector<typename ParetoCurveCheckResult<ValueType>::point_type>&& points, typename ParetoCurveCheckResult<ValueType>::polytope_type&& underApproximation, typename ParetoCurveCheckResult<ValueType>::polytope_type&& overApproximation) : ParetoCurveCheckResult<ValueType>(points, underApproximation, overApproximation), state(state) {
+            STORM_LOG_THROW(this->state.getNonZeroCount() == 1, storm::exceptions::InvalidOperationException, "ParetoCheckResults are only relevant for a single state.");
+        }
+
+        template<storm::dd::DdType Type, typename ValueType>
+        bool SymbolicParetoCurveCheckResult<Type, ValueType>::isSymbolicParetoCurveCheckResult() const {
+            return true;
+        }
+
+        template<storm::dd::DdType Type, typename ValueType>
+        bool SymbolicParetoCurveCheckResult<Type, ValueType>::isSymbolic() const {
+            return true;
+        }
+
+        template<storm::dd::DdType Type, typename ValueType>
+        void SymbolicParetoCurveCheckResult<Type, ValueType>::filter(QualitativeCheckResult const& filter) {
+            STORM_LOG_THROW(filter.isSymbolicQualitativeCheckResult(), storm::exceptions::InvalidOperationException, "Cannot filter Symbolic check result with non-Symbolic filter.");
+            STORM_LOG_THROW(filter.isResultForAllStates(), storm::exceptions::InvalidOperationException, "Cannot filter check result with non-complete filter.");
+            SymbolicQualitativeCheckResult<Type> const& symbolicFilter = filter.template asSymbolicQualitativeCheckResult<Type>();
+
+            storm::dd::Bdd<Type> const& filterTruthValues = symbolicFilter.getTruthValuesVector();
+
+            STORM_LOG_THROW(filterTruthValues.getNonZeroCount() == 1 && !(filterTruthValues && state).isZero(), storm::exceptions::InvalidOperationException, "The check result fails to contain some results referred to by the filter.");
+        }
+
+        template<storm::dd::DdType Type, typename ValueType>
+        storm::dd::Bdd<Type> const& SymbolicParetoCurveCheckResult<Type, ValueType>::getState() const {
+            return state;
+        }
+
+        template class SymbolicParetoCurveCheckResult<storm::dd::DdType::CUDD, double>;
+        template class SymbolicParetoCurveCheckResult<storm::dd::DdType::Sylvan, double>;
+    }
+}
diff --git a/src/storm/modelchecker/results/SymbolicParetoCurveCheckResult.h b/src/storm/modelchecker/results/SymbolicParetoCurveCheckResult.h
new file mode 100644
index 000000000..edda08abf
--- /dev/null
+++ b/src/storm/modelchecker/results/SymbolicParetoCurveCheckResult.h
@@ -0,0 +1,41 @@
+#ifndef STORM_MODELCHECKER_SYMBOLICPARETOCURVECHECKRESULT_H_
+#define STORM_MODELCHECKER_SYMBOLICPARETOCURVECHECKRESULT_H_
+
+#include <vector>
+
+#include "storm/modelchecker/results/ParetoCurveCheckResult.h"
+#include "storm/storage/dd/DdType.h"
+#include "storm/storage/dd/Bdd.h"
+
+
+namespace storm {
+    namespace modelchecker {
+        template<storm::dd::DdType Type, typename ValueType = double>
+        class SymbolicParetoCurveCheckResult : public ParetoCurveCheckResult<ValueType> {
+        public:
+
+            SymbolicParetoCurveCheckResult();
+            SymbolicParetoCurveCheckResult(storm::dd::Bdd<Type> const& state, std::vector<typename ParetoCurveCheckResult<ValueType>::point_type> const& points, typename ParetoCurveCheckResult<ValueType>::polytope_type const& underApproximation, typename ParetoCurveCheckResult<ValueType>::polytope_type const& overApproximation);
+            SymbolicParetoCurveCheckResult(storm::dd::Bdd<Type> const& state, std::vector<typename ParetoCurveCheckResult<ValueType>::point_type>&& points, typename ParetoCurveCheckResult<ValueType>::polytope_type&& underApproximation, typename ParetoCurveCheckResult<ValueType>::polytope_type&& overApproximation);
+
+            SymbolicParetoCurveCheckResult(SymbolicParetoCurveCheckResult const& other) = default;
+            SymbolicParetoCurveCheckResult& operator=(SymbolicParetoCurveCheckResult const& other) = default;
+            SymbolicParetoCurveCheckResult(SymbolicParetoCurveCheckResult&& other) = default;
+            SymbolicParetoCurveCheckResult& operator=(SymbolicParetoCurveCheckResult&& other) = default;
+            virtual ~SymbolicParetoCurveCheckResult() = default;
+
+            virtual bool isSymbolicParetoCurveCheckResult() const override;
+            virtual bool isSymbolic() const override;
+
+            virtual void filter(QualitativeCheckResult const& filter) override;
+
+            storm::dd::Bdd<Type> const& getState() const;
+
+        private:
+            // The state of the checked model to which the result applies
+            storm::dd::Bdd<Type> state;
+        };
+    }
+}
+
+#endif /* STORM_MODELCHECKER_SYMBOLICPARETOCURVECHECKRESULT_H_ */
diff --git a/src/storm/solver/SolverSelectionOptions.cpp b/src/storm/solver/SolverSelectionOptions.cpp
index 125ed2461..fe42f299a 100644
--- a/src/storm/solver/SolverSelectionOptions.cpp
+++ b/src/storm/solver/SolverSelectionOptions.cpp
@@ -21,6 +21,8 @@ namespace storm {
                     return "Gurobi";
                 case LpSolverType::Glpk:
                     return "Glpk";
+                case LpSolverType::Z3:
+                    return "Z3";
             }
             return "invalid";
         }