diff --git a/src/cli/cli.cpp b/src/cli/cli.cpp
index 0909b25de..758ac9a2a 100644
--- a/src/cli/cli.cpp
+++ b/src/cli/cli.cpp
@@ -236,15 +236,15 @@ namespace storm {
                 if (settings.isSymbolicSet()) {
 #ifdef STORM_HAVE_CARL
                     if (settings.isParametricSet()) {
-                        buildAndCheckSymbolicModel<storm::RationalFunction>(program.get(), formulas);
+                        buildAndCheckSymbolicModel<storm::RationalFunction>(program.get(), formulas, true);
                     } else {
 #endif
-                        buildAndCheckSymbolicModel<double>(program.get(), formulas);
+                        buildAndCheckSymbolicModel<double>(program.get(), formulas, true);
 #ifdef STORM_HAVE_CARL
                     }
 #endif
                 } else if (settings.isExplicitSet()) {
-                    buildAndCheckExplicitModel<double>(formulas);
+                    buildAndCheckExplicitModel<double>(formulas, true);
                 } else {
                     STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "No input model.");
                 }
diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h
index c93279179..bbb9d6404 100644
--- a/src/cli/entrypoints.h
+++ b/src/cli/entrypoints.h
@@ -9,10 +9,10 @@ namespace storm {
     namespace cli {
 
         template<typename ValueType>
-        void verifySparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) {
+        void verifySparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas, bool onlyInitialStatesRelevant = false) {
             for (auto const& formula : formulas) {
                 std::cout << std::endl << "Model checking property: " << *formula << " ...";
-                std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, formula));
+                std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, formula, onlyInitialStatesRelevant));
                 if (result) {
                     std::cout << " done." << std::endl;
                     std::cout << "Result (initial states): ";
@@ -26,12 +26,12 @@ namespace storm {
 
 #ifdef STORM_HAVE_CARL
         template<>
-        inline void verifySparseModel(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) {
+        inline void verifySparseModel(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas, bool onlyInitialStatesRelevant) {
 
             for (auto const& formula : formulas) {
                 STORM_LOG_THROW(model->getType() == storm::models::ModelType::Dtmc, storm::exceptions::InvalidSettingsException, "Currently parametric verification is only available for DTMCs.");
                 std::cout << std::endl << "Model checking property: " << *formula << " ...";
-                std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, formula));
+                std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySparseModel(model, formula, onlyInitialStatesRelevant));
                 if (result) {
                     std::cout << " done." << std::endl;
                     std::cout << "Result (initial states): ";
@@ -50,15 +50,15 @@ namespace storm {
 #endif
 
         template<storm::dd::DdType DdType>
-        void verifySymbolicModelWithAbstractionRefinementEngine(storm::prism::Program const& program, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) {
+        void verifySymbolicModelWithAbstractionRefinementEngine(storm::prism::Program const& program, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas, bool onlyInitialStatesRelevant = false) {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "Abstraction Refinement is not yet implemented.");
         }
 
         template<storm::dd::DdType DdType>
-        void verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) {
+        void verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas, bool onlyInitialStatesRelevant = false) {
             for (auto const& formula : formulas) {
                 std::cout << std::endl << "Model checking property: " << *formula << " ...";
-                std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithHybridEngine(model, formula));
+                std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithHybridEngine(model, formula, onlyInitialStatesRelevant));
 
                 if (result) {
                     std::cout << " done." << std::endl;
@@ -72,10 +72,10 @@ namespace storm {
         }
 
         template<storm::dd::DdType DdType>
-        void verifySymbolicModelWithSymbolicEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) {
+        void verifySymbolicModelWithSymbolicEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas, bool onlyInitialStatesRelevant = false) {
             for (auto const& formula : formulas) {
                 std::cout << std::endl << "Model checking property: " << *formula << " ...";
-                std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithDdEngine(model, formula));
+                std::unique_ptr<storm::modelchecker::CheckResult> result(storm::verifySymbolicModelWithDdEngine(model, formula, onlyInitialStatesRelevant));
                 if (result) {
                     std::cout << " done." << std::endl;
                     std::cout << "Result (initial states): ";
@@ -114,12 +114,12 @@ namespace storm {
     }
     
         template<typename ValueType, storm::dd::DdType LibraryType>
-        void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) {
+        void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas, bool onlyInitialStatesRelevant = false) {
 
             storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
 
             if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::AbstractionRefinement) {
-                verifySymbolicModelWithAbstractionRefinementEngine<LibraryType>(program, formulas);
+                verifySymbolicModelWithAbstractionRefinementEngine<LibraryType>(program, formulas, onlyInitialStatesRelevant);
             } else {
                 storm::storage::ModelFormulasPair modelFormulasPair = buildSymbolicModel<ValueType, LibraryType>(program, formulas);
                 STORM_LOG_THROW(modelFormulasPair.model != nullptr, storm::exceptions::InvalidStateException,
@@ -133,7 +133,6 @@ namespace storm {
 
                 // Verify the model, if a formula was given.
                 if (!formulas.empty()) {
-
                     if (modelFormulasPair.model->isSparseModel()) {
                         if (storm::settings::generalSettings().isCounterexampleSet()) {
                             // If we were requested to generate a counterexample, we now do so for each formula.
@@ -141,15 +140,15 @@ namespace storm {
                                 generateCounterexample<ValueType>(program, modelFormulasPair.model->as<storm::models::sparse::Model<ValueType>>(), formula);
                             }
                         } else {
-                            verifySparseModel<ValueType>(modelFormulasPair.model->as<storm::models::sparse::Model<ValueType>>(), modelFormulasPair.formulas);
+                            verifySparseModel<ValueType>(modelFormulasPair.model->as<storm::models::sparse::Model<ValueType>>(), modelFormulasPair.formulas, onlyInitialStatesRelevant);
                         }
                     } else if (modelFormulasPair.model->isSymbolicModel()) {
                         if (storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Hybrid) {
                             verifySymbolicModelWithHybridEngine(modelFormulasPair.model->as<storm::models::symbolic::Model<LibraryType>>(),
-                                                                modelFormulasPair.formulas);
+                                                                modelFormulasPair.formulas, onlyInitialStatesRelevant);
                         } else {
                             verifySymbolicModelWithSymbolicEngine(modelFormulasPair.model->as<storm::models::symbolic::Model<LibraryType>>(),
-                                                                  modelFormulasPair.formulas);
+                                                                  modelFormulasPair.formulas, onlyInitialStatesRelevant);
                         }
                     } else {
                         STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Invalid input model type.");
@@ -159,16 +158,16 @@ namespace storm {
         }
         
         template<typename ValueType>
-        void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) {
+        void buildAndCheckSymbolicModel(storm::prism::Program const& program, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas, bool onlyInitialStatesRelevant = false) {
             if (storm::settings::generalSettings().getDdLibraryType() == storm::dd::DdType::CUDD) {
-                buildAndCheckSymbolicModel<ValueType, storm::dd::DdType::CUDD>(program, formulas);
+                buildAndCheckSymbolicModel<ValueType, storm::dd::DdType::CUDD>(program, formulas, onlyInitialStatesRelevant);
             } else if (storm::settings::generalSettings().getDdLibraryType() == storm::dd::DdType::Sylvan) {
-                buildAndCheckSymbolicModel<ValueType, storm::dd::DdType::Sylvan>(program, formulas);
+                buildAndCheckSymbolicModel<ValueType, storm::dd::DdType::Sylvan>(program, formulas, onlyInitialStatesRelevant);
             }
         }
 
         template<typename ValueType>
-        void buildAndCheckExplicitModel(std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) {
+        void buildAndCheckExplicitModel(std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas, bool onlyInitialStatesRelevant = false) {
             storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
 
             STORM_LOG_THROW(settings.isExplicitSet(), storm::exceptions::InvalidStateException, "Unable to build explicit model without model files.");
@@ -183,7 +182,7 @@ namespace storm {
             // Verify the model, if a formula was given.
             if (!formulas.empty()) {
                 STORM_LOG_THROW(model->isSparseModel(), storm::exceptions::InvalidStateException, "Expected sparse model.");
-                verifySparseModel<ValueType>(model->as<storm::models::sparse::Model<ValueType>>(), formulas);
+                verifySparseModel<ValueType>(model->as<storm::models::sparse::Model<ValueType>>(), formulas, onlyInitialStatesRelevant);
             }
         }
     }
diff --git a/src/modelchecker/CheckTask.h b/src/modelchecker/CheckTask.h
index acd039b8b..cf66f4f06 100644
--- a/src/modelchecker/CheckTask.h
+++ b/src/modelchecker/CheckTask.h
@@ -28,8 +28,8 @@ namespace storm {
             /*!
              * Creates a task object with the default options for the given formula.
              */
-            CheckTask(FormulaType const& formula) : formula(formula) {
-                this->onlyInitialStatesRelevant = false;
+            CheckTask(FormulaType const& formula, bool onlyInitialStatesRelevant = false) : formula(formula) {
+                this->onlyInitialStatesRelevant = onlyInitialStatesRelevant;
                 this->produceStrategies = true;
                 this->qualitative = false;
                 
diff --git a/src/utility/storm.h b/src/utility/storm.h
index 86a43caab..d4a042bc6 100644
--- a/src/utility/storm.h
+++ b/src/utility/storm.h
@@ -236,23 +236,23 @@ namespace storm {
 #endif
 
     template<typename ValueType, storm::dd::DdType DdType>
-    std::unique_ptr<storm::modelchecker::CheckResult> verifyModel(std::shared_ptr<storm::models::ModelBase> model, std::shared_ptr<const storm::logic::Formula> const& formula) {
+    std::unique_ptr<storm::modelchecker::CheckResult> verifyModel(std::shared_ptr<storm::models::ModelBase> model, std::shared_ptr<const storm::logic::Formula> const& formula, bool onlyInitialStatesRelevant) {
         storm::settings::modules::GeneralSettings const& settings = storm::settings::generalSettings();
         switch(settings.getEngine()) {
             case storm::settings::modules::GeneralSettings::Engine::Sparse: {
                 std::shared_ptr<storm::models::sparse::Model<ValueType>> sparseModel = model->template as<storm::models::sparse::Model<ValueType>>();
                 STORM_LOG_THROW(sparseModel != nullptr, storm::exceptions::InvalidArgumentException, "Sparse engine requires a sparse input model");
-                return verifySparseModel(sparseModel, formula);
+                return verifySparseModel(sparseModel, formula, onlyInitialStatesRelevant);
             }
             case storm::settings::modules::GeneralSettings::Engine::Hybrid: {
                 std::shared_ptr<storm::models::symbolic::Model<DdType>> ddModel = model->template as<storm::models::symbolic::Model<DdType>>();
                 STORM_LOG_THROW(ddModel != nullptr, storm::exceptions::InvalidArgumentException, "Hybrid engine requires a dd input model");
-                return verifySymbolicModelWithHybridEngine(ddModel, formula);
+                return verifySymbolicModelWithHybridEngine(ddModel, formula, onlyInitialStatesRelevant);
             }
             case storm::settings::modules::GeneralSettings::Engine::Dd: {
                 std::shared_ptr<storm::models::symbolic::Model<DdType>> ddModel = model->template as<storm::models::symbolic::Model<DdType>>();
                 STORM_LOG_THROW(ddModel != nullptr, storm::exceptions::InvalidArgumentException, "Dd engine requires a dd input model");
-                return verifySymbolicModelWithDdEngine(ddModel, formula);
+                return verifySymbolicModelWithDdEngine(ddModel, formula, onlyInitialStatesRelevant);
             }
             case storm::settings::modules::GeneralSettings::Engine::AbstractionRefinement: {
                 STORM_LOG_ASSERT(false, "This position should not be reached, as at this point no model has been built.");
@@ -261,18 +261,19 @@ namespace storm {
     }
 
     template<typename ValueType>
-    std::unique_ptr<storm::modelchecker::CheckResult> verifySparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::shared_ptr<const storm::logic::Formula> const& formula) {
+    std::unique_ptr<storm::modelchecker::CheckResult> verifySparseModel(std::shared_ptr<storm::models::sparse::Model<ValueType>> model, std::shared_ptr<const storm::logic::Formula> const& formula, bool onlyInitialStatesRelevant = false) {
 
         std::unique_ptr<storm::modelchecker::CheckResult> result;
+        storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant);
         if (model->getType() == storm::models::ModelType::Dtmc) {
             std::shared_ptr<storm::models::sparse::Dtmc<ValueType>> dtmc = model->template as<storm::models::sparse::Dtmc<ValueType>>();
             storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<ValueType>> modelchecker(*dtmc);
-            if (modelchecker.canHandle(*formula)) {
-                result = modelchecker.check(*formula);
+            if (modelchecker.canHandle(task)) {
+                result = modelchecker.check(task);
             } else {
                 storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<ValueType>> modelchecker2(*dtmc);
-                if (modelchecker2.canHandle(*formula)) {
-                    result = modelchecker2.check(*formula);
+                if (modelchecker2.canHandle(task)) {
+                    result = modelchecker2.check(task);
                 }
             }
         } else if (model->getType() == storm::models::ModelType::Mdp) {
@@ -280,20 +281,20 @@ namespace storm {
 #ifdef STORM_HAVE_CUDA
             if (settings.isCudaSet()) {
                     storm::modelchecker::TopologicalValueIterationMdpPrctlModelChecker<ValueType> modelchecker(*mdp);
-                    result = modelchecker.check(*formula);
+                    result = modelchecker.check(task);
                 } else {
                     storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> modelchecker(*mdp);
-                    result = modelchecker.check(*formula);
+                    result = modelchecker.check(task);
                 }
 #else
             storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<ValueType>> modelchecker(*mdp);
-            result = modelchecker.check(*formula);
+            result = modelchecker.check(task);
 #endif
         } else if (model->getType() == storm::models::ModelType::Ctmc) {
             std::shared_ptr<storm::models::sparse::Ctmc<ValueType>> ctmc = model->template as<storm::models::sparse::Ctmc<ValueType>>();
 
             storm::modelchecker::SparseCtmcCslModelChecker<storm::models::sparse::Ctmc<ValueType>> modelchecker(*ctmc);
-            result = modelchecker.check(*formula);
+            result = modelchecker.check(task);
         }
         return result;
 
@@ -317,13 +318,14 @@ namespace storm {
     }
 
     template<>
-    inline std::unique_ptr<storm::modelchecker::CheckResult> verifySparseModel(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<const storm::logic::Formula> const& formula) {
+    inline std::unique_ptr<storm::modelchecker::CheckResult> verifySparseModel(std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> model, std::shared_ptr<const storm::logic::Formula> const& formula, bool onlyInitialStatesRelevant) {
         std::unique_ptr<storm::modelchecker::CheckResult> result;
         std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalFunction>> dtmc = model->template as<storm::models::sparse::Dtmc<storm::RationalFunction>>();
 
         storm::modelchecker::SparseDtmcEliminationModelChecker<storm::models::sparse::Dtmc<storm::RationalFunction>> modelchecker(*dtmc);
-        if (modelchecker.canHandle(*formula)) {
-            result = modelchecker.check(*formula);
+        storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant);
+        if (modelchecker.canHandle(task)) {
+            result = modelchecker.check(task);
         } else {
             STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "The parametric engine currently does not support this property.");
         }
@@ -333,25 +335,26 @@ namespace storm {
 #endif
 
     template<storm::dd::DdType DdType>
-    std::unique_ptr<storm::modelchecker::CheckResult> verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::shared_ptr<const storm::logic::Formula> const& formula) {
+    std::unique_ptr<storm::modelchecker::CheckResult> verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::shared_ptr<const storm::logic::Formula> const& formula, bool onlyInitialStatesRelevant = false) {
         std::unique_ptr<storm::modelchecker::CheckResult> result;
+        storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant);
         if (model->getType() == storm::models::ModelType::Dtmc) {
             std::shared_ptr<storm::models::symbolic::Dtmc<DdType>> dtmc = model->template as<storm::models::symbolic::Dtmc<DdType>>();
             storm::modelchecker::HybridDtmcPrctlModelChecker<DdType, double> modelchecker(*dtmc);
-            if (modelchecker.canHandle(*formula)) {
-                result = modelchecker.check(*formula);
+            if (modelchecker.canHandle(task)) {
+                result = modelchecker.check(task);
             }
         } else if (model->getType() == storm::models::ModelType::Ctmc) {
             std::shared_ptr<storm::models::symbolic::Ctmc<DdType>> ctmc = model->template as<storm::models::symbolic::Ctmc<DdType>>();
             storm::modelchecker::HybridCtmcCslModelChecker<DdType, double> modelchecker(*ctmc);
-            if (modelchecker.canHandle(*formula)) {
-                result = modelchecker.check(*formula);
+            if (modelchecker.canHandle(task)) {
+                result = modelchecker.check(task);
             }
         } else if (model->getType() == storm::models::ModelType::Mdp) {
             std::shared_ptr<storm::models::symbolic::Mdp<DdType>> mdp = model->template as<storm::models::symbolic::Mdp<DdType>>();
             storm::modelchecker::HybridMdpPrctlModelChecker<DdType, double> modelchecker(*mdp);
-            if (modelchecker.canHandle(*formula)) {
-                result = modelchecker.check(*formula);
+            if (modelchecker.canHandle(task)) {
+                result = modelchecker.check(task);
             }
         } else {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented.");
@@ -361,19 +364,20 @@ namespace storm {
 
 
     template<storm::dd::DdType DdType>
-    std::unique_ptr<storm::modelchecker::CheckResult> verifySymbolicModelWithDdEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::shared_ptr<const storm::logic::Formula> const& formula) {
+    std::unique_ptr<storm::modelchecker::CheckResult> verifySymbolicModelWithDdEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::shared_ptr<const storm::logic::Formula> const& formula, bool onlyInitialStatesRelevant) {
         std::unique_ptr<storm::modelchecker::CheckResult> result;
+        storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant);
         if (model->getType() == storm::models::ModelType::Dtmc) {
             std::shared_ptr<storm::models::symbolic::Dtmc<DdType>> dtmc = model->template as<storm::models::symbolic::Dtmc<DdType>>();
             storm::modelchecker::SymbolicDtmcPrctlModelChecker<DdType, double> modelchecker(*dtmc);
-            if (modelchecker.canHandle(*formula)) {
-                result = modelchecker.check(*formula);
+            if (modelchecker.canHandle(task)) {
+                result = modelchecker.check(task);
             }
         } else if (model->getType() == storm::models::ModelType::Mdp) {
             std::shared_ptr<storm::models::symbolic::Mdp<DdType>> mdp = model->template as<storm::models::symbolic::Mdp<DdType>>();
             storm::modelchecker::SymbolicMdpPrctlModelChecker<DdType, double> modelchecker(*mdp);
-            if (modelchecker.canHandle(*formula)) {
-                result = modelchecker.check(*formula);
+            if (modelchecker.canHandle(task)) {
+                result = modelchecker.check(task);
             }
         } else {
             STORM_LOG_THROW(false, storm::exceptions::NotImplementedException, "This functionality is not yet implemented.");