diff --git a/src/storm-dft/settings/modules/DFTSettings.cpp b/src/storm-dft/settings/modules/DFTSettings.cpp
index 8b62833a1..e20df83ec 100644
--- a/src/storm-dft/settings/modules/DFTSettings.cpp
+++ b/src/storm-dft/settings/modules/DFTSettings.cpp
@@ -29,7 +29,8 @@ namespace storm {
             const std::string DFTSettings::propExpectedTimeOptionName = "expectedtime";
             const std::string DFTSettings::propExpectedTimeOptionShortName = "mttf";
             const std::string DFTSettings::propProbabilityOptionName = "probability";
-            const std::string DFTSettings::propTimeBoundOptionName = "timebound";
+            const std::string DFTSettings::propTimeboundOptionName = "timebound";
+            const std::string DFTSettings::propTimepointsOptionName = "timepoints";
             const std::string DFTSettings::minValueOptionName = "min";
             const std::string DFTSettings::maxValueOptionName = "max";
             const std::string DFTSettings::transformToGspnOptionName = "gspn";
@@ -50,7 +51,8 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, approximationHeuristicOptionName, false, "Set the heuristic used for approximation.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("heuristic", "Sets which heuristic is used for approximation. Must be in {depth, probability}. Default is").setDefaultValueString("depth").addValidatorString(ArgumentValidatorFactory::createMultipleChoiceValidator({"depth", "rateratio"})).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, propExpectedTimeOptionName, false, "Compute expected time of system failure.").setShortName(propExpectedTimeOptionShortName).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, propProbabilityOptionName, false, "Compute probability of system failure.").build());
-                this->addOption(storm::settings::OptionBuilder(moduleName, propTimeBoundOptionName, false, "Compute probability of system failure up to given timebound.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("time", "The timebound to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterValidator(0.0)).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, propTimeboundOptionName, false, "Compute probability of system failure up to given timebound.").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("time", "The timebound to use.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterValidator(0.0)).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, propTimepointsOptionName, false, "Compute probability of system failure up to given timebound for a set of given timepoints [starttime, starttime+inc, starttime+2inc, ... ,endtime]").addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("starttime", "The timebound to start from.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("endtime", "The timebound to end with.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("inc", "The value to increment with to get the next timepoint.").addValidatorDouble(ArgumentValidatorFactory::createDoubleGreaterEqualValidator(0.0)).build()).build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, minValueOptionName, false, "Compute minimal value in case of non-determinism.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, maxValueOptionName, false, "Compute maximal value in case of non-determinism.").build());
 #ifdef STORM_HAVE_Z3
@@ -119,13 +121,28 @@ namespace storm {
             }
             
             bool DFTSettings::usePropTimebound() const {
-                return this->getOption(propTimeBoundOptionName).getHasOptionBeenSet();
+                return this->getOption(propTimeboundOptionName).getHasOptionBeenSet();
             }
-            
+
             double DFTSettings::getPropTimebound() const {
-                return this->getOption(propTimeBoundOptionName).getArgumentByName("time").getValueAsDouble();
+                return this->getOption(propTimeboundOptionName).getArgumentByName("time").getValueAsDouble();
             }
-            
+
+            bool DFTSettings::usePropTimepoints() const {
+                return this->getOption(propTimepointsOptionName).getHasOptionBeenSet();
+            }
+
+            std::vector<double> DFTSettings::getPropTimepoints() const {
+                double starttime = this->getOption(propTimepointsOptionName).getArgumentByName("starttime").getValueAsDouble();
+                double endtime = this->getOption(propTimepointsOptionName).getArgumentByName("endtime").getValueAsDouble();
+                double inc = this->getOption(propTimepointsOptionName).getArgumentByName("inc").getValueAsDouble();
+                std::vector<double> timepoints;
+                for (double time = starttime; time <= endtime; time += inc) {
+                    timepoints.push_back(time);
+                }
+                return timepoints;
+            }
+
             bool DFTSettings::isComputeMinimalValue() const {
                 return this->getOption(minValueOptionName).getHasOptionBeenSet();
             }
@@ -156,13 +173,6 @@ namespace storm {
             }
 
             bool DFTSettings::check() const {
-                // Ensure that only one property is given.
-                if (usePropExpectedTime()) {
-                    STORM_LOG_THROW(!usePropProbability() && !usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given.");
-                } else if (usePropProbability()) {
-                    STORM_LOG_THROW(!usePropTimebound(), storm::exceptions::InvalidSettingsException, "More than one property given.");
-                }
-                
                 // Ensure that at most one of min or max is set
                 STORM_LOG_THROW(!isComputeMinimalValue() || !isComputeMaximalValue(), storm::exceptions::InvalidSettingsException, "Min and max can not both be set.");
                 return true;
diff --git a/src/storm-dft/settings/modules/DFTSettings.h b/src/storm-dft/settings/modules/DFTSettings.h
index 0d8695e2a..662039e0f 100644
--- a/src/storm-dft/settings/modules/DFTSettings.h
+++ b/src/storm-dft/settings/modules/DFTSettings.h
@@ -110,7 +110,28 @@ namespace storm {
                  * @return True iff the option was set.
                  */
                 bool usePropTimebound() const;
-                
+
+                /*!
+                 * Retrieves the timebound for the timebound property.
+                 *
+                 * @return The timebound.
+                 */
+                double getPropTimebound() const;
+
+                /*!
+                 * Retrieves whether the property timepoints should be used.
+                 *
+                 * @return True iff the option was set.
+                 */
+                bool usePropTimepoints() const;
+
+                /*!
+                 * Retrieves the settings for the timepoints property.
+                 *
+                 * @return The timepoints.
+                 */
+                std::vector<double> getPropTimepoints() const;
+
                 /*!
                  * Retrieves whether the minimal value should be computed for non-determinism.
                  *
@@ -124,13 +145,6 @@ namespace storm {
                  * @return True iff the option was set.
                  */
                 bool isComputeMaximalValue() const;
-                
-                /*!
-                 * Retrieves the timebound for the timebound property.
-                 *
-                 * @return The timebound.
-                 */
-                double getPropTimebound() const;
 
                 /*!
                  * Retrieves whether the DFT should be transformed into a GSPN.
@@ -184,7 +198,8 @@ namespace storm {
                 static const std::string propExpectedTimeOptionName;
                 static const std::string propExpectedTimeOptionShortName;
                 static const std::string propProbabilityOptionName;
-                static const std::string propTimeBoundOptionName;
+                static const std::string propTimeboundOptionName;
+                static const std::string propTimepointsOptionName;
                 static const std::string minValueOptionName;
                 static const std::string maxValueOptionName;
 #ifdef STORM_HAVE_Z3