diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h
index 41faf8732..e4ae114bf 100644
--- a/src/storm-cli-utilities/model-handling.h
+++ b/src/storm-cli-utilities/model-handling.h
@@ -359,18 +359,12 @@ namespace storm {
                 result->second = true;
                 
                 std::shared_ptr<storm::models::symbolic::Model<DdType, ExportValueType>> symbolicModel = result->first->template as<storm::models::symbolic::Model<DdType, ExportValueType>>();
-                if (symbolicModel->isOfType(storm::models::ModelType::Dtmc)) {
-                    storm::transformer::SymbolicDtmcToSparseDtmcTransformer<DdType, ExportValueType> transformer;
-                    result->first = transformer.translate(*symbolicModel->template as<storm::models::symbolic::Dtmc<DdType, ExportValueType>>());
-                } else if (symbolicModel->isOfType(storm::models::ModelType::Ctmc)) {
-                    storm::transformer::SymbolicCtmcToSparseCtmcTransformer<DdType, ExportValueType> transformer;
-                    result->first = transformer.translate(*symbolicModel->template as<storm::models::symbolic::Ctmc<DdType, ExportValueType>>());
-                } else if (symbolicModel->isOfType(storm::models::ModelType::Mdp)) {
-                    storm::transformer::SymbolicMdpToSparseMdpTransformer<DdType, ExportValueType> transformer;
-                    result->first = transformer.translate(*symbolicModel->template as<storm::models::symbolic::Mdp<DdType, ExportValueType>>());
-                } else {
-                    STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "The translation to a sparse model is not supported for the given model type.");
+                std::vector<std::shared_ptr<storm::logic::Formula const>> formulas;
+                for (auto const& property : input.properties) {
+                    formulas.emplace_back(property.getRawFormula());
                 }
+                result->first = storm::api::transformSymbolicToSparseModel(symbolicModel, formulas);
+                STORM_LOG_THROW(result, storm::exceptions::NotSupportedException, "The translation to a sparse model is not supported for the given model type.");
             }
             
             return *result;
diff --git a/src/storm/api/transformation.h b/src/storm/api/transformation.h
index 204e283db..d26f32ea1 100644
--- a/src/storm/api/transformation.h
+++ b/src/storm/api/transformation.h
@@ -62,14 +62,14 @@ namespace storm {
          * Transforms the given symbolic model to a sparse model.
          */
         template<storm::dd::DdType Type, typename ValueType>
-        std::shared_ptr<storm::models::sparse::Model<ValueType>> transformSymbolicToSparseModel(std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> const& symbolicModel) {
+        std::shared_ptr<storm::models::sparse::Model<ValueType>> transformSymbolicToSparseModel(std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> const& symbolicModel, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas = std::vector<std::shared_ptr<storm::logic::Formula const>>()) {
             switch (symbolicModel->getType()) {
                 case storm::models::ModelType::Dtmc:
-                    return storm::transformer::SymbolicDtmcToSparseDtmcTransformer<Type, ValueType>().translate(*symbolicModel->template as<storm::models::symbolic::Dtmc<Type, ValueType>>());
+                    return storm::transformer::SymbolicDtmcToSparseDtmcTransformer<Type, ValueType>().translate(*symbolicModel->template as<storm::models::symbolic::Dtmc<Type, ValueType>>(), formulas);
                 case storm::models::ModelType::Mdp:
-                    return storm::transformer::SymbolicMdpToSparseMdpTransformer<Type, ValueType>::translate(*symbolicModel->template as<storm::models::symbolic::Mdp<Type, ValueType>>());
+                    return storm::transformer::SymbolicMdpToSparseMdpTransformer<Type, ValueType>::translate(*symbolicModel->template as<storm::models::symbolic::Mdp<Type, ValueType>>(), formulas);
                 case storm::models::ModelType::Ctmc:
-                    return storm::transformer::SymbolicCtmcToSparseCtmcTransformer<Type, ValueType>::translate(*symbolicModel->template as<storm::models::symbolic::Ctmc<Type, ValueType>>());
+                    return storm::transformer::SymbolicCtmcToSparseCtmcTransformer<Type, ValueType>::translate(*symbolicModel->template as<storm::models::symbolic::Ctmc<Type, ValueType>>(), formulas);
                 default:
                     STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Transformation of symbolic " << symbolicModel->getType() << " to sparse model is not supported.");
             }
diff --git a/src/storm/transformer/SymbolicToSparseTransformer.cpp b/src/storm/transformer/SymbolicToSparseTransformer.cpp
index 8ebac17de..66d3dd1b3 100644
--- a/src/storm/transformer/SymbolicToSparseTransformer.cpp
+++ b/src/storm/transformer/SymbolicToSparseTransformer.cpp
@@ -7,12 +7,35 @@
 #include "storm/models/sparse/StandardRewardModel.h"
 #include "storm/utility/macros.h"
 #include "storm/exceptions/NotImplementedException.h"
+#include "storm/logic/AtomicExpressionFormula.h"
+#include "storm/logic/AtomicLabelFormula.h"
 
 namespace storm {
     namespace transformer {
 
+        struct LabelInformation {
+            LabelInformation(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
+                for (auto const& formula : formulas) {
+                    std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> atomicLabelFormulas = formula->getAtomicLabelFormulas();
+                    for (auto const& labelFormula : atomicLabelFormulas) {
+                        atomicLabels.insert(labelFormula->getLabel());
+                    }
+                    
+                    std::vector<std::shared_ptr<storm::logic::AtomicExpressionFormula const>> atomicExpressionFormulas = formula->getAtomicExpressionFormulas();
+                    for (auto const& expressionFormula : atomicExpressionFormulas) {
+                        std::stringstream ss;
+                        ss << expressionFormula->getExpression();
+                        expressionLabels[ss.str()] = expressionFormula->getExpression();
+                    }
+                }
+            }
+            
+            std::set<std::string> atomicLabels;
+            std::map<std::string, storm::expressions::Expression> expressionLabels;
+        };
+        
         template<storm::dd::DdType Type, typename ValueType>
-        std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> SymbolicDtmcToSparseDtmcTransformer<Type, ValueType>::translate(storm::models::symbolic::Dtmc<Type, ValueType> const& symbolicDtmc) {
+        std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> SymbolicDtmcToSparseDtmcTransformer<Type, ValueType>::translate(storm::models::symbolic::Dtmc<Type, ValueType> const& symbolicDtmc, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
             
             this->odd = symbolicDtmc.getReachableStates().createOdd();
             storm::storage::SparseMatrix<ValueType> transitionMatrix = symbolicDtmc.getTransitionMatrix().toMatrix(this->odd, this->odd);
@@ -36,8 +59,18 @@ namespace storm {
             
             labelling.addLabel("init", symbolicDtmc.getInitialStates().toVector(this->odd));
             labelling.addLabel("deadlock", symbolicDtmc.getDeadlockStates().toVector(this->odd));
-            for(auto const& label : symbolicDtmc.getLabels()) {
-                labelling.addLabel(label, symbolicDtmc.getStates(label).toVector(this->odd));
+            if (formulas.empty()) {
+                for (auto const& label : symbolicDtmc.getLabels()) {
+                    labelling.addLabel(label, symbolicDtmc.getStates(label).toVector(this->odd));
+                }
+            } else {
+                LabelInformation labelInfo(formulas);
+                for (auto const& label : labelInfo.atomicLabels) {
+                    labelling.addLabel(label, symbolicDtmc.getStates(label).toVector(this->odd));
+                }
+                for (auto const& expressionLabel : labelInfo.expressionLabels) {
+                    labelling.addLabel(expressionLabel.first, symbolicDtmc.getStates(expressionLabel.second).toVector(this->odd));
+                }
             }
             return std::make_shared<storm::models::sparse::Dtmc<ValueType>>(transitionMatrix, labelling, rewardModels);
         }
@@ -48,7 +81,7 @@ namespace storm {
         }
         
         template<storm::dd::DdType Type, typename ValueType>
-        std::shared_ptr<storm::models::sparse::Mdp<ValueType>> SymbolicMdpToSparseMdpTransformer<Type, ValueType>::translate(storm::models::symbolic::Mdp<Type, ValueType> const& symbolicMdp) {
+        std::shared_ptr<storm::models::sparse::Mdp<ValueType>> SymbolicMdpToSparseMdpTransformer<Type, ValueType>::translate(storm::models::symbolic::Mdp<Type, ValueType> const& symbolicMdp, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
             storm::dd::Odd odd = symbolicMdp.getReachableStates().createOdd();
             storm::storage::SparseMatrix<ValueType> transitionMatrix = symbolicMdp.getTransitionMatrix().toMatrix(symbolicMdp.getNondeterminismVariables(), odd, odd);
             std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> rewardModels;
@@ -69,15 +102,25 @@ namespace storm {
 
             labelling.addLabel("init", symbolicMdp.getInitialStates().toVector(odd));
             labelling.addLabel("deadlock", symbolicMdp.getDeadlockStates().toVector(odd));
-            for(auto const& label : symbolicMdp.getLabels()) {
-                labelling.addLabel(label, symbolicMdp.getStates(label).toVector(odd));
+            if (formulas.empty()) {
+                for (auto const& label : symbolicMdp.getLabels()) {
+                    labelling.addLabel(label, symbolicMdp.getStates(label).toVector(odd));
+                }
+            } else {
+                LabelInformation labelInfo(formulas);
+                for (auto const& label : labelInfo.atomicLabels) {
+                    labelling.addLabel(label, symbolicMdp.getStates(label).toVector(odd));
+                }
+                for (auto const& expressionLabel : labelInfo.expressionLabels) {
+                    labelling.addLabel(expressionLabel.first, symbolicMdp.getStates(expressionLabel.second).toVector(odd));
+                }
             }
+            
             return std::make_shared<storm::models::sparse::Mdp<ValueType>>(transitionMatrix, labelling, rewardModels);
         }
 
         template<storm::dd::DdType Type, typename ValueType>
-        std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> SymbolicCtmcToSparseCtmcTransformer<Type, ValueType>::translate(
-                storm::models::symbolic::Ctmc<Type, ValueType> const& symbolicCtmc) {
+        std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> SymbolicCtmcToSparseCtmcTransformer<Type, ValueType>::translate(storm::models::symbolic::Ctmc<Type, ValueType> const& symbolicCtmc, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) {
             storm::dd::Odd odd = symbolicCtmc.getReachableStates().createOdd();
             storm::storage::SparseMatrix<ValueType> transitionMatrix = symbolicCtmc.getTransitionMatrix().toMatrix(odd, odd);
             std::unordered_map<std::string, storm::models::sparse::StandardRewardModel<ValueType>> rewardModels;
@@ -100,9 +143,20 @@ namespace storm {
 
             labelling.addLabel("init", symbolicCtmc.getInitialStates().toVector(odd));
             labelling.addLabel("deadlock", symbolicCtmc.getDeadlockStates().toVector(odd));
-            for(auto const& label : symbolicCtmc.getLabels()) {
-                labelling.addLabel(label, symbolicCtmc.getStates(label).toVector(odd));
+            if (formulas.empty()) {
+                for (auto const& label : symbolicCtmc.getLabels()) {
+                    labelling.addLabel(label, symbolicCtmc.getStates(label).toVector(odd));
+                }
+            } else {
+                LabelInformation labelInfo(formulas);
+                for (auto const& label : labelInfo.atomicLabels) {
+                    labelling.addLabel(label, symbolicCtmc.getStates(label).toVector(odd));
+                }
+                for (auto const& expressionLabel : labelInfo.expressionLabels) {
+                    labelling.addLabel(expressionLabel.first, symbolicCtmc.getStates(expressionLabel.second).toVector(odd));
+                }
             }
+            
             return std::make_shared<storm::models::sparse::Ctmc<ValueType>>(transitionMatrix, labelling, rewardModels);
         }
 
diff --git a/src/storm/transformer/SymbolicToSparseTransformer.h b/src/storm/transformer/SymbolicToSparseTransformer.h
index 5f4bed6c4..e2c191b49 100644
--- a/src/storm/transformer/SymbolicToSparseTransformer.h
+++ b/src/storm/transformer/SymbolicToSparseTransformer.h
@@ -1,5 +1,6 @@
 #pragma once
 
+#include "storm/logic/Formula.h"
 #include "storm/models/sparse/Dtmc.h"
 #include "storm/models/symbolic/Dtmc.h"
 #include "storm/models/sparse/Mdp.h"
@@ -15,7 +16,7 @@ namespace storm {
         template<storm::dd::DdType Type, typename ValueType>
         class SymbolicDtmcToSparseDtmcTransformer {
         public:
-            std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> translate(storm::models::symbolic::Dtmc<Type, ValueType> const& symbolicDtmc);
+            std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> translate(storm::models::symbolic::Dtmc<Type, ValueType> const& symbolicDtmc, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas = std::vector<std::shared_ptr<storm::logic::Formula const>>());
             storm::dd::Odd const& getOdd() const;
             
         private:
@@ -25,13 +26,13 @@ namespace storm {
         template<storm::dd::DdType Type, typename ValueType>
         class SymbolicMdpToSparseMdpTransformer {
         public:
-            static std::shared_ptr<storm::models::sparse::Mdp<ValueType>> translate(storm::models::symbolic::Mdp<Type, ValueType> const& symbolicMdp);
+            static std::shared_ptr<storm::models::sparse::Mdp<ValueType>> translate(storm::models::symbolic::Mdp<Type, ValueType> const& symbolicMdp, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas = std::vector<std::shared_ptr<storm::logic::Formula const>>());
         };
         
         template<storm::dd::DdType Type, typename ValueType>
         class SymbolicCtmcToSparseCtmcTransformer {
         public:
-            static std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> translate(storm::models::symbolic::Ctmc<Type, ValueType> const& symbolicCtmc);
+            static std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> translate(storm::models::symbolic::Ctmc<Type, ValueType> const& symbolicCtmc, std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas = std::vector<std::shared_ptr<storm::logic::Formula const>>());
         };
     }
 }