diff --git a/src/storm/builder/BuilderType.cpp b/src/storm/builder/BuilderType.cpp
index 6bc7e766a..35512a220 100644
--- a/src/storm/builder/BuilderType.cpp
+++ b/src/storm/builder/BuilderType.cpp
@@ -32,7 +32,7 @@ namespace storm {
         }
         
         template <typename ValueType>
-        bool canHandle(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription) {
+        bool canHandle(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription, boost::optional<std::vector<storm::jani::Property>> const& properties) {
             storm::dd::DdType const ddType = storm::dd::DdType::Sylvan;
             if (!modelDescription.hasModel()) {
                 // If there is no model to be build, we assume that the task of obtaining a model is either not required or can be accomplished somehow.
@@ -50,7 +50,7 @@ namespace storm {
                     if (modelDescription.isPrismProgram()) {
                         return storm::builder::DdPrismModelBuilder<ddType, ValueType>::canHandle(modelDescription.asPrismProgram());
                     } else {
-                        return storm::builder::DdJaniModelBuilder<ddType, ValueType>::canHandle(modelDescription.asJaniModel());
+                        return storm::builder::DdJaniModelBuilder<ddType, ValueType>::canHandle(modelDescription.asJaniModel(), properties);
                     }
                 case BuilderType::Jit:
                     return storm::builder::jit::ExplicitJitJaniModelBuilder<ValueType>::canHandle(modelDescription.asJaniModel());
@@ -59,8 +59,9 @@ namespace storm {
         
 
         
-        template bool canHandle<double>(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription);
-        template bool canHandle<storm::RationalNumber>(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription);
+        template bool canHandle<double>(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription, boost::optional<std::vector<storm::jani::Property>> const& properties);
+        template bool canHandle<storm::RationalNumber>(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription, boost::optional<std::vector<storm::jani::Property>> const& properties);
+        template bool canHandle<storm::RationalFunction>(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription, boost::optional<std::vector<storm::jani::Property>> const& properties);
         
     }
 }
\ No newline at end of file
diff --git a/src/storm/builder/BuilderType.h b/src/storm/builder/BuilderType.h
index a5732a950..22b08158c 100644
--- a/src/storm/builder/BuilderType.h
+++ b/src/storm/builder/BuilderType.h
@@ -1,5 +1,9 @@
 #pragma once
 
+#include <vector>
+#include <boost/optional.hpp>
+
+#include "storm/storage/jani/Property.h"
 #include "storm/storage/SymbolicModelDescription.h"
 
 namespace storm {
@@ -17,6 +21,6 @@ namespace storm {
         storm::jani::ModelFeatures getSupportedJaniFeatures(BuilderType const& builderType);
         
         template <typename ValueType>
-        bool canHandle(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription);
+        bool canHandle(BuilderType const& builderType, storm::storage::SymbolicModelDescription const& modelDescription, boost::optional<std::vector<storm::jani::Property>> const& properties = boost::none);
     }
 }
\ No newline at end of file
diff --git a/src/storm/utility/Engine.cpp b/src/storm/utility/Engine.cpp
index a2b315822..345dc6a8e 100644
--- a/src/storm/utility/Engine.cpp
+++ b/src/storm/utility/Engine.cpp
@@ -14,6 +14,7 @@
 #include "storm/modelchecker/CheckTask.h"
 
 #include "storm/storage/SymbolicModelDescription.h"
+#include "storm/storage/jani/Property.h"
 
 #include "storm/utility/macros.h"
 
@@ -144,21 +145,74 @@ namespace storm {
             return false;
         }
 
+        template <>
+        bool canHandle<storm::RationalFunction>(storm::utility::Engine const& engine, storm::storage::SymbolicModelDescription::ModelType const& modelType, storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalFunction> const& checkTask) {
+            // Define types to improve readability
+            typedef storm::storage::SymbolicModelDescription::ModelType ModelType;
+            // The Dd library does not make much of a difference (in case of exact or parametric models we will switch to sylvan anyway).
+            // Therefore, we always use sylvan here
+            storm::dd::DdType const ddType = storm::dd::DdType::Sylvan;
+            switch (engine) {
+                case Engine::Sparse:
+                case Engine::DdSparse:
+                    switch (modelType) {
+                        case ModelType::DTMC:
+                            return storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>>::canHandleStatic(checkTask);
+                        case ModelType::CTMC:
+                            return storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<storm::RationalFunction>>::canHandleStatic(checkTask);
+                        case ModelType::MDP:
+                        case ModelType::MA:
+                        case ModelType::POMDP:
+                            return false;
+                    }
+                case Engine::Hybrid:
+                    switch (modelType) {
+                        case ModelType::DTMC:
+                            return storm::modelchecker::HybridDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<ddType, storm::RationalFunction>>::canHandleStatic(checkTask);
+                        case ModelType::CTMC:
+                            return storm::modelchecker::HybridCtmcCslModelChecker<storm::models::symbolic::Ctmc<ddType, storm::RationalFunction>>::canHandleStatic(checkTask);
+                        case ModelType::MDP:
+                        case ModelType::MA:
+                        case ModelType::POMDP:
+                            return false;
+                    }
+                case Engine::Dd:
+                    switch (modelType) {
+                        case ModelType::DTMC:
+                            return storm::modelchecker::SymbolicDtmcPrctlModelChecker<storm::models::symbolic::Dtmc<ddType, storm::RationalFunction>>::canHandleStatic(checkTask);
+                        case ModelType::MDP:
+                        case ModelType::CTMC:
+                        case ModelType::MA:
+                        case ModelType::POMDP:
+                            return false;
+                    }
+                default:
+                    STORM_LOG_ERROR("The selected engine" << engine << " is not considered.");
+            }
+            STORM_LOG_ERROR("The selected combination of engine (" << engine << ") and model type (" << modelType << ") does not seem to be supported for this value type.");
+            return false;
+        }
         
         template <typename ValueType>
-        bool canHandle(storm::utility::Engine const& engine, storm::storage::SymbolicModelDescription const& modelDescription, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& checkTask) {
-            // Check handability based on model type
-            if (!canHandle(engine, modelDescription.getModelType(), checkTask)) {
-                return false;
+        bool canHandle(storm::utility::Engine const& engine, std::vector<storm::jani::Property> const& properties, storm::storage::SymbolicModelDescription const& modelDescription) {
+            // Check handability of properties based on model type
+            for (auto const& p : properties) {
+                for (auto const& f : {p.getRawFormula(), p.getFilter().getStatesFormula()}) {
+                    auto task = storm::modelchecker::CheckTask<storm::logic::Formula, ValueType>(*f, true);
+                    if (!canHandle(engine, modelDescription.getModelType(), task)) {
+                        STORM_LOG_INFO("Engine " << engine << " can not handle formula '" << *f << "'.");
+                        return false;
+                    }
+                }
             }
             // Check whether the model builder can handle the model description
-            return storm::builder::canHandle<ValueType>(getBuilderType(engine), modelDescription);
+            return storm::builder::canHandle<ValueType>(getBuilderType(engine), modelDescription, properties);
         }
         
         // explicit template instantiations.
-        template bool canHandle<double>(storm::utility::Engine const&, storm::storage::SymbolicModelDescription const&, storm::modelchecker::CheckTask<storm::logic::Formula, double> const&);
-        template bool canHandle<storm::RationalNumber>(storm::utility::Engine const&, storm::storage::SymbolicModelDescription const&, storm::modelchecker::CheckTask<storm::logic::Formula, storm::RationalNumber> const&);
-        
-        
+        template bool canHandle<double>(storm::utility::Engine const&, std::vector<storm::jani::Property> const&, storm::storage::SymbolicModelDescription const&);
+        template bool canHandle<storm::RationalNumber>(storm::utility::Engine const&, std::vector<storm::jani::Property> const&, storm::storage::SymbolicModelDescription const&);
+        template bool canHandle<storm::RationalFunction>(storm::utility::Engine const&, std::vector<storm::jani::Property> const&, storm::storage::SymbolicModelDescription const&);
+
     }
 }
\ No newline at end of file
diff --git a/src/storm/utility/Engine.h b/src/storm/utility/Engine.h
index dff20c8e6..3254749a9 100644
--- a/src/storm/utility/Engine.h
+++ b/src/storm/utility/Engine.h
@@ -10,6 +10,10 @@
 namespace storm {
     
     // Forward Declarations
+    namespace jani {
+        class Property;
+    }
+    
     namespace logic {
         class Formula;
     }
@@ -56,12 +60,12 @@ namespace storm {
         storm::builder::BuilderType getBuilderType(storm::utility::Engine const& engine);
         
         /*!
-         * Returns false if the given model description and checkTask can certainly not be handled by the given engine.
+         * Returns false if the given model description and one of the given properties can certainly not be handled by the given engine.
          * Notice that the set of handable model checking queries is only overapproximated, i.e. if this returns true,
          * the query could still be not supported by the engine. This behavior is due to the fact that we sometimes need
          * to actually build the model in order to decide whether it is supported.
          */
         template <typename ValueType>
-        bool canHandle(storm::utility::Engine const& engine, storm::modelchecker::CheckTask<storm::logic::Formula, ValueType> const& checkTask, storm::storage::SymbolicModelDescription const& modelDescription);
+        bool canHandle(storm::utility::Engine const& engine, std::vector<storm::jani::Property> const& properties, storm::storage::SymbolicModelDescription const& modelDescription);
     }
 }
\ No newline at end of file