diff --git a/src/builder/DdPrismModelBuilder.cpp b/src/builder/DdPrismModelBuilder.cpp
index 1c1d599a5..4f6ab3871 100644
--- a/src/builder/DdPrismModelBuilder.cpp
+++ b/src/builder/DdPrismModelBuilder.cpp
@@ -190,18 +190,18 @@ namespace storm {
             };
             
         template <storm::dd::DdType Type>
-        DdPrismModelBuilder<Type>::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates() {
+        DdPrismModelBuilder<Type>::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
             // Intentionally left empty.
         }
         
         template <storm::dd::DdType Type>
-        DdPrismModelBuilder<Type>::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()), terminalStates() {
+        DdPrismModelBuilder<Type>::Options::Options(storm::logic::Formula const& formula) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()), terminalStates(), negatedTerminalStates() {
             this->preserveFormula(formula);
             this->setTerminalStatesFromFormula(formula);
         }
         
         template <storm::dd::DdType Type>
-        DdPrismModelBuilder<Type>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates() {
+        DdPrismModelBuilder<Type>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
             if (formulas.empty()) {
                 this->buildAllRewardModels = true;
                 this->buildAllLabels = true;
@@ -221,6 +221,9 @@ namespace storm {
             if (terminalStates) {
                 terminalStates.reset();
             }
+            if (negatedTerminalStates) {
+                negatedTerminalStates.reset();
+            }
 
             // If we are not required to build all reward models, we determine the reward models we need to build.
             if (!buildAllRewardModels) {
@@ -261,10 +264,16 @@ namespace storm {
                     this->setTerminalStatesFromFormula(sub);
                 }
             } else if (formula.isUntilFormula()) {
-                storm::logic::Formula const& right = formula.asUntilFormula().getLeftSubformula();
+                storm::logic::Formula const& right = formula.asUntilFormula().getRightSubformula();
                 if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) {
                     this->setTerminalStatesFromFormula(right);
                 }
+                storm::logic::Formula const& left = formula.asUntilFormula().getLeftSubformula();
+                if (left.isAtomicExpressionFormula()) {
+                    negatedTerminalStates = left.asAtomicExpressionFormula().getExpression();
+                } else if (left.isAtomicLabelFormula()) {
+                    negatedTerminalStates = left.asAtomicLabelFormula().getLabel();
+                }
             } else if (formula.isProbabilityOperatorFormula()) {
                 storm::logic::Formula const& sub = formula.asProbabilityOperatorFormula().getSubformula();
                 if (sub.isEventuallyFormula() || sub.isUntilFormula()) {
@@ -1023,16 +1032,33 @@ namespace storm {
             storm::dd::Add<Type> stateActionDd = system.stateActionDd;
             
             // If we were asked to treat some states as terminal states, we cut away their transitions now.
-            if (options.terminalStates) {
-                storm::expressions::Expression terminalExpression;
-                if (options.terminalStates.get().type() == typeid(storm::expressions::Expression)) {
-                    terminalExpression = boost::get<storm::expressions::Expression>(options.terminalStates.get());
-                } else {
-                    std::string const& labelName = boost::get<std::string>(options.terminalStates.get());
-                    terminalExpression = preparedProgram.getLabelExpression(labelName);
+            if (options.terminalStates || options.negatedTerminalStates) {
+                storm::dd::Add<Type> terminalStatesAdd = generationInfo.manager->getAddZero();
+                if (options.terminalStates) {
+                    storm::expressions::Expression terminalExpression;
+                    if (options.terminalStates.get().type() == typeid(storm::expressions::Expression)) {
+                        terminalExpression = boost::get<storm::expressions::Expression>(options.terminalStates.get());
+                    } else {
+                        std::string const& labelName = boost::get<std::string>(options.terminalStates.get());
+                        terminalExpression = preparedProgram.getLabelExpression(labelName);
+                    }
+                
+                    STORM_LOG_TRACE("Making the states satisfying " << terminalExpression << " terminal.");
+                    terminalStatesAdd = generationInfo.rowExpressionAdapter->translateExpression(terminalExpression);
                 }
-                STORM_LOG_TRACE("Making the states satisfying " << terminalExpression << " terminal.");
-                storm::dd::Add<Type> terminalStatesAdd = generationInfo.rowExpressionAdapter->translateExpression(terminalExpression);
+                if (options.negatedTerminalStates) {
+                    storm::expressions::Expression nonTerminalExpression;
+                    if (options.negatedTerminalStates.get().type() == typeid(storm::expressions::Expression)) {
+                        nonTerminalExpression = boost::get<storm::expressions::Expression>(options.negatedTerminalStates.get());
+                    } else {
+                        std::string const& labelName = boost::get<std::string>(options.terminalStates.get());
+                        nonTerminalExpression = preparedProgram.getLabelExpression(labelName);
+                    }
+                    
+                    STORM_LOG_TRACE("Making the states *not* satisfying " << nonTerminalExpression << " terminal.");
+                    terminalStatesAdd |= !generationInfo.rowExpressionAdapter->translateExpression(nonTerminalExpression);
+                }
+                
                 transitionMatrix *= !terminalStatesAdd;
             }
             
diff --git a/src/builder/DdPrismModelBuilder.h b/src/builder/DdPrismModelBuilder.h
index 20f6e76f0..4669432a8 100644
--- a/src/builder/DdPrismModelBuilder.h
+++ b/src/builder/DdPrismModelBuilder.h
@@ -99,9 +99,13 @@ namespace storm {
                 // An optional set of expressions for which labels need to be built.
                 boost::optional<std::vector<storm::expressions::Expression>> expressionLabels;
                 
-                // An optional expression or label that characterizes the terminal states of the model. If this is set,
-                // the outgoing transitions of these states are replaced with a self-loop.
+                // An optional expression or label that (a subset of) characterizes the terminal states of the model.
+                // If this is set, the outgoing transitions of these states are replaced with a self-loop.
                 boost::optional<boost::variant<storm::expressions::Expression, std::string>> terminalStates;
+                
+                // An optional expression or label whose negation characterizes (a subset of) the terminal states of the
+                // model. If this is set, the outgoing transitions of these states are replaced with a self-loop.
+                boost::optional<boost::variant<storm::expressions::Expression, std::string>> negatedTerminalStates;
             };
             
             /*!
diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp
index cf02700eb..cfc7d8577 100644
--- a/src/builder/ExplicitPrismModelBuilder.cpp
+++ b/src/builder/ExplicitPrismModelBuilder.cpp
@@ -106,17 +106,17 @@ namespace storm {
         }
 
         template <typename ValueType, typename IndexType>
-        ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options() : buildCommandLabels(false), buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates() {
+        ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options() : buildCommandLabels(false), buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
             // Intentionally left empty.
         }
         
         template <typename ValueType, typename IndexType>
-        ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()), terminalStates() {
+        ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options(storm::logic::Formula const& formula) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()), terminalStates(), negatedTerminalStates() {
             this->preserveFormula(formula);
         }
         
         template <typename ValueType, typename IndexType>
-        ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates() {
+        ExplicitPrismModelBuilder<ValueType, IndexType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula>> const& formulas) : buildCommandLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
             if (formulas.empty()) {
                 this->buildAllRewardModels = true;
                 this->buildAllLabels = true;
@@ -142,10 +142,16 @@ namespace storm {
                     this->setTerminalStatesFromFormula(sub);
                 }
             } else if (formula.isUntilFormula()) {
-                storm::logic::Formula const& right = formula.asUntilFormula().getLeftSubformula();
+                storm::logic::Formula const& right = formula.asUntilFormula().getRightSubformula();
                 if (right.isAtomicExpressionFormula() || right.isAtomicLabelFormula()) {
                     this->setTerminalStatesFromFormula(right);
                 }
+                storm::logic::Formula const& left = formula.asUntilFormula().getLeftSubformula();
+                if (left.isAtomicExpressionFormula()) {
+                    negatedTerminalStates = left.asAtomicExpressionFormula().getExpression();
+                } else if (left.isAtomicLabelFormula()) {
+                    negatedTerminalStates = left.asAtomicLabelFormula().getLabel();
+                }
             } else if (formula.isProbabilityOperatorFormula()) {
                 storm::logic::Formula const& sub = formula.asProbabilityOperatorFormula().getSubformula();
                 if (sub.isEventuallyFormula() || sub.isUntilFormula()) {
@@ -160,6 +166,9 @@ namespace storm {
             if (terminalStates) {
                 terminalStates.reset();
             }
+            if (negatedTerminalStates) {
+                negatedTerminalStates.reset();
+            }
             
             // If we are not required to build all reward models, we determine the reward models we need to build.
             if (!buildAllRewardModels) {
@@ -932,7 +941,8 @@ namespace storm {
                 rewardModelBuilders.emplace_back(deterministicModel, rewardModel.get().hasStateRewards(), rewardModel.get().hasStateActionRewards(), rewardModel.get().hasTransitionRewards());
             }
             
-            // If we were asked to treat some states as terminal states, we cut away their transitions now.
+            // If we were asked to treat some states as terminal states, we determine an expression characterizing the
+            // terminal states of the model that we pass on to the matrix building routine.
             boost::optional<storm::expressions::Expression> terminalExpression;
             if (options.terminalStates) {
                 if (options.terminalStates.get().type() == typeid(storm::expressions::Expression)) {
@@ -942,9 +952,27 @@ namespace storm {
                     terminalExpression = program.getLabelExpression(labelName);
                 }
             }
+            if (options.negatedTerminalStates) {
+                if (options.negatedTerminalStates.get().type() == typeid(storm::expressions::Expression)) {
+                    if (terminalExpression) {
+                        terminalExpression = terminalExpression.get() || !boost::get<storm::expressions::Expression>(options.negatedTerminalStates.get());
+                    } else {
+                        terminalExpression = !boost::get<storm::expressions::Expression>(options.negatedTerminalStates.get());
+                    }
+                } else {
+                    std::string const& labelName = boost::get<std::string>(options.negatedTerminalStates.get());
+                    if (terminalExpression) {
+                        terminalExpression = terminalExpression.get() || !program.getLabelExpression(labelName);
+                    } else {
+                        terminalExpression = !program.getLabelExpression(labelName);
+                    }
+                }
+            }
+            if (terminalExpression) {
+                STORM_LOG_TRACE("Making the states satisfying " << terminalExpression.get() << " terminal.");
+            }
             
             modelComponents.choiceLabeling = buildMatrices(program, variableInformation, selectedRewardModels, stateInformation, options.buildCommandLabels, deterministicModel, discreteTimeModel, transitionMatrixBuilder, rewardModelBuilders, terminalExpression);
-            
             modelComponents.transitionMatrix = transitionMatrixBuilder.build();
             
             // Now finalize all reward models.
diff --git a/src/builder/ExplicitPrismModelBuilder.h b/src/builder/ExplicitPrismModelBuilder.h
index 313b1652c..1356394d8 100644
--- a/src/builder/ExplicitPrismModelBuilder.h
+++ b/src/builder/ExplicitPrismModelBuilder.h
@@ -193,9 +193,13 @@ namespace storm {
                 // An optional set of expressions for which labels need to be built.
                 boost::optional<std::vector<storm::expressions::Expression>> expressionLabels;
                 
-                // An optional expression or label that characterizes the terminal states of the model. If this is set,
-                // the outgoing transitions of these states are replaced with a self-loop.
+                // An optional expression or label that characterizes (a subset of) the terminal states of the model. If
+                // this is set, the outgoing transitions of these states are replaced with a self-loop.
                 boost::optional<boost::variant<storm::expressions::Expression, std::string>> terminalStates;
+                
+                // An optional expression or label whose negation characterizes (a subset of) the terminal states of the
+                // model. If this is set, the outgoing transitions of these states are replaced with a self-loop.
+                boost::optional<boost::variant<storm::expressions::Expression, std::string>> negatedTerminalStates;
             };
             
             /*!