diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp
index 325cfb3a5..8b54e0eba 100644
--- a/src/builder/DdJaniModelBuilder.cpp
+++ b/src/builder/DdJaniModelBuilder.cpp
@@ -15,6 +15,8 @@
 #include "src/storage/dd/Bdd.h"
 #include "src/adapters/AddExpressionAdapter.h"
 
+#include "src/storage/expressions/ExpressionManager.h"
+
 #include "src/models/symbolic/Dtmc.h"
 #include "src/models/symbolic/Ctmc.h"
 #include "src/models/symbolic/Mdp.h"
@@ -28,6 +30,7 @@
 #include "src/utility/dd.h"
 #include "src/utility/math.h"
 #include "src/exceptions/WrongFormatException.h"
+#include "src/exceptions/InvalidSettingsException.h"
 #include "src/exceptions/InvalidArgumentException.h"
 #include "src/exceptions/InvalidStateException.h"
 #include "src/exceptions/NotSupportedException.h"
@@ -36,7 +39,7 @@ namespace storm {
     namespace builder {
         
         template <storm::dd::DdType Type, typename ValueType>
-        DdJaniModelBuilder<Type, ValueType>::Options::Options() : buildAllRewardModels(true), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() {
+        DdJaniModelBuilder<Type, ValueType>::Options::Options(bool buildAllLabels, bool buildAllRewardModels) : buildAllLabels(buildAllLabels), buildAllRewardModels(buildAllRewardModels), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() {
             // Intentionally left empty.
         }
         
@@ -47,7 +50,7 @@ namespace storm {
         }
         
         template <storm::dd::DdType Type, typename ValueType>
-        DdJaniModelBuilder<Type, ValueType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) : buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() {
+        DdJaniModelBuilder<Type, ValueType>::Options::Options(std::vector<std::shared_ptr<storm::logic::Formula const>> const& formulas) : buildAllLabels(false), buildAllRewardModels(false), rewardModelsToBuild(), constantDefinitions(), terminalStates(), negatedTerminalStates() {
             if (formulas.empty()) {
                 this->buildAllRewardModels = true;
             } else {
@@ -75,6 +78,12 @@ namespace storm {
                 std::set<std::string> referencedRewardModels = formula.getReferencedRewardModels();
                 rewardModelsToBuild.insert(referencedRewardModels.begin(), referencedRewardModels.end());
             }
+            
+            // Extract all the labels used in the formula.
+            std::vector<std::shared_ptr<storm::logic::AtomicLabelFormula const>> atomicLabelFormulas = formula.getAtomicLabelFormulas();
+            for (auto const& formula : atomicLabelFormulas) {
+                addLabel(formula->getLabel());
+            }
         }
         
         template <storm::dd::DdType Type, typename ValueType>
@@ -112,7 +121,18 @@ namespace storm {
         bool DdJaniModelBuilder<Type, ValueType>::Options::isBuildAllRewardModelsSet() const {
             return buildAllRewardModels;
         }
+
+        template <storm::dd::DdType Type, typename ValueType>
+        bool DdJaniModelBuilder<Type, ValueType>::Options::isBuildAllLabelsSet() const {
+            return buildAllLabels;
+        }
         
+        template <storm::dd::DdType Type, typename ValueType>
+        void DdJaniModelBuilder<Type, ValueType>::Options::addLabel(std::string const& labelName) {
+            STORM_LOG_THROW(!buildAllLabels, storm::exceptions::InvalidSettingsException, "Cannot add label, because all labels are built anyway.");
+            labelNames.insert(labelName);
+        }
+
         template <storm::dd::DdType Type, typename ValueType>
         struct CompositionVariables {
             CompositionVariables() : manager(std::make_shared<storm::dd::DdManager<Type>>()),
@@ -138,8 +158,9 @@ namespace storm {
             // All pairs of row/column meta variables.
             std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> rowColumnMetaVariablePairs;
             
-            // A mapping from automata to the meta variable encoding their location.
-            std::map<std::string, std::pair<storm::expressions::Variable, storm::expressions::Variable>> automatonToLocationVariableMap;
+            // A mapping from automata to the meta variables encoding their location.
+            std::map<std::string, storm::expressions::Variable> automatonToLocationVariableMap;
+            std::map<std::string, std::pair<storm::expressions::Variable, storm::expressions::Variable>> automatonToLocationDdVariableMap;
             
             // A mapping from action indices to the meta variables used to encode these actions.
             std::map<uint64_t, storm::expressions::Variable> actionVariablesMap;
@@ -245,9 +266,14 @@ namespace storm {
                 
                 for (auto const& automaton : this->model.getAutomata()) {
                     // Start by creating a meta variable for the location of the automaton.
+                    storm::expressions::Variable locationExpressionVariable = model.getManager().declareFreshIntegerVariable(false, "loc");
+                    result.automatonToLocationVariableMap[automaton.getName()] = locationExpressionVariable;
                     std::pair<storm::expressions::Variable, storm::expressions::Variable> variablePair = result.manager->addMetaVariable("l_" + automaton.getName(), 0, automaton.getNumberOfLocations() - 1);
-                    result.automatonToLocationVariableMap[automaton.getName()] = variablePair;
+                    result.automatonToLocationDdVariableMap[automaton.getName()] = variablePair;
                     result.rowColumnMetaVariablePairs.push_back(variablePair);
+
+                    result.variableToRowMetaVariableMap->emplace(locationExpressionVariable, variablePair.first);
+                    result.variableToColumnMetaVariableMap->emplace(locationExpressionVariable, variablePair.second);
                     
                     // Add the location variable to the row/column variables.
                     result.rowMetaVariables.insert(variablePair.first);
@@ -277,7 +303,7 @@ namespace storm {
                     storm::dd::Bdd<Type> range = result.manager->getBddOne();
                     
                     // Add the identity and ranges of the location variables to the ones of the automaton.
-                    std::pair<storm::expressions::Variable, storm::expressions::Variable> const& locationVariables = result.automatonToLocationVariableMap[automaton.getName()];
+                    std::pair<storm::expressions::Variable, storm::expressions::Variable> const& locationVariables = result.automatonToLocationDdVariableMap[automaton.getName()];
                     storm::dd::Add<Type, ValueType> variableIdentity = result.manager->template getIdentity<ValueType>(locationVariables.first).equals(result.manager->template getIdentity<ValueType>(locationVariables.second)).template toAdd<ValueType>() * result.manager->getRange(locationVariables.first).template toAdd<ValueType>() * result.manager->getRange(locationVariables.second).template toAdd<ValueType>();
                     identity &= variableIdentity.toBdd();
                     range &= result.manager->getRange(locationVariables.first);
@@ -458,7 +484,7 @@ namespace storm {
                 }
             }
             
-            transitions *= variables.manager->getEncoding(variables.automatonToLocationVariableMap.at(automaton.getName()).second, destination.getLocationIndex()).template toAdd<ValueType>();
+            transitions *= variables.manager->getEncoding(variables.automatonToLocationDdVariableMap.at(automaton.getName()).second, destination.getLocationIndex()).template toAdd<ValueType>();
             
             return EdgeDestinationDd<Type, ValueType>(transitions, assignedGlobalVariables);
         }
@@ -1081,7 +1107,7 @@ namespace storm {
                     }
                     
                     // Add the source location and the guard.
-                    transitions *= this->variables.manager->getEncoding(this->variables.automatonToLocationVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd<ValueType>() * guard;
+                    transitions *= this->variables.manager->getEncoding(this->variables.automatonToLocationDdVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd<ValueType>() * guard;
                     
                     // If we multiply the ranges of global variables, make sure everything stays within its bounds.
                     if (!globalVariablesInSomeDestination.empty()) {
@@ -1475,7 +1501,7 @@ namespace storm {
                 for (uint64_t locationIndex = 0; locationIndex < automaton.getNumberOfLocations(); ++locationIndex) {
                     auto const& location = automaton.getLocation(locationIndex);
                     performTransientAssignments(location.getAssignments().getTransientAssignments(), [this,&automatonName,locationIndex,&result] (storm::jani::Assignment const& assignment) {
-                        storm::dd::Add<Type, ValueType> assignedValues = this->variables.manager->getEncoding(this->variables.automatonToLocationVariableMap.at(automatonName).first, locationIndex).template toAdd<ValueType>() * this->variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression());
+                        storm::dd::Add<Type, ValueType> assignedValues = this->variables.manager->getEncoding(this->variables.automatonToLocationDdVariableMap.at(automatonName).first, locationIndex).template toAdd<ValueType>() * this->variables.rowExpressionAdapter->translateExpression(assignment.getAssignedExpression());
                         auto it = result.transientLocationAssignments.find(assignment.getExpressionVariable());
                         if (it != result.transientLocationAssignments.end()) {
                             it->second += assignedValues;
@@ -1557,17 +1583,18 @@ namespace storm {
             storm::dd::Bdd<Type> deadlockStates;
             storm::dd::Add<Type, ValueType> transitionMatrix;
             std::unordered_map<std::string, storm::models::symbolic::StandardRewardModel<Type, ValueType>> rewardModels;
+            std::map<std::string, storm::expressions::Expression> labelToExpressionMap;
         };
         
         template <storm::dd::DdType Type, typename ValueType>
         std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> createModel(storm::jani::ModelType const& modelType, CompositionVariables<Type, ValueType> const& variables, ModelComponents<Type, ValueType> const& modelComponents) {
             
             if (modelType == storm::jani::ModelType::DTMC) {
-                return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Dtmc<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, std::map<std::string, storm::expressions::Expression>(), modelComponents.rewardModels));
+                return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Dtmc<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, modelComponents.labelToExpressionMap, modelComponents.rewardModels));
             } else if (modelType == storm::jani::ModelType::CTMC) {
-                return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Ctmc<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, std::map<std::string, storm::expressions::Expression>(), modelComponents.rewardModels));
+                return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Ctmc<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, modelComponents.labelToExpressionMap, modelComponents.rewardModels));
             } else if (modelType == storm::jani::ModelType::MDP) {
-                return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Mdp<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, variables.allNondeterminismVariables, std::map<std::string, storm::expressions::Expression>(), modelComponents.rewardModels));
+                return std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>>(new storm::models::symbolic::Mdp<Type, ValueType>(variables.manager, modelComponents.reachableStates, modelComponents.initialStates, modelComponents.deadlockStates, modelComponents.transitionMatrix, variables.rowMetaVariables, variables.rowExpressionAdapter, variables.columnMetaVariables, variables.columnExpressionAdapter, variables.rowColumnMetaVariablePairs, variables.allNondeterminismVariables, modelComponents.labelToExpressionMap, modelComponents.rewardModels));
             } else {
                 STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Invalid model type.");
             }
@@ -1635,7 +1662,7 @@ namespace storm {
             for (auto const& automaton : model.getAutomata()) {
                 storm::dd::Bdd<Type> initialLocationIndices = variables.manager->getBddZero();
                 for (auto const& locationIndex : automaton.getInitialLocationIndices()) {
-                    initialLocationIndices |= variables.manager->getEncoding(variables.automatonToLocationVariableMap.at(automaton.getName()).first, locationIndex);
+                    initialLocationIndices |= variables.manager->getEncoding(variables.automatonToLocationDdVariableMap.at(automaton.getName()).first, locationIndex);
                 }
                 initialStates &= initialLocationIndices;
             }
@@ -1698,7 +1725,7 @@ namespace storm {
             std::vector<storm::expressions::Variable> result;
             if (options.isBuildAllRewardModelsSet()) {
                 for (auto const& variable : model.getGlobalVariables()) {
-                    if (variable.isTransient()) {
+                    if (variable.isTransient() && (variable.isRealVariable() || variable.isUnboundedIntegerVariable())) {
                         result.push_back(variable.getExpressionVariable());
                     }
                 }
@@ -1709,7 +1736,7 @@ namespace storm {
                         result.push_back(globalVariables.getVariable(rewardModelName).getExpressionVariable());
                     } else {
                         STORM_LOG_THROW(rewardModelName.empty(), storm::exceptions::InvalidArgumentException, "Cannot build unknown reward model '" << rewardModelName << "'.");
-                        STORM_LOG_THROW(globalVariables.getNumberOfTransientVariables() == 1, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is ambiguous.");
+                        STORM_LOG_THROW(globalVariables.getNumberOfRealTransientVariables() + globalVariables.getNumberOfUnboundedIntegerTransientVariables() == 1, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is ambiguous.");
                     }
                 }
                 
@@ -1748,6 +1775,21 @@ namespace storm {
             return result;
         }
         
+        template <storm::dd::DdType Type, typename ValueType>
+        std::map<std::string, storm::expressions::Expression> buildLabelExpressions(storm::jani::Model const& model, CompositionVariables<Type, ValueType> const& variables, typename DdJaniModelBuilder<Type, ValueType>::Options const& options) {
+            std::map<std::string, storm::expressions::Expression> result;
+            
+            for (auto const& variable : model.getGlobalVariables().getTransientVariables()) {
+                if (variable->isBooleanVariable()) {
+                    if (options.buildAllLabels || options.labelNames.find(variable->getName()) != options.labelNames.end()) {
+                        result[variable->getName()] = model.getLabelExpression(variable->asBooleanVariable(), variables.automatonToLocationVariableMap);
+                    }
+                }
+            }
+            
+            return result;
+        }
+        
         template <storm::dd::DdType Type, typename ValueType>
         std::shared_ptr<storm::models::symbolic::Model<Type, ValueType>> DdJaniModelBuilder<Type, ValueType>::build(storm::jani::Model const& model, Options const& options) {
             if (model.hasUndefinedConstants()) {
@@ -1814,6 +1856,9 @@ namespace storm {
             // Build the reward models.
             modelComponents.rewardModels = buildRewardModels(system, rewardVariables);
             
+            // Build the label to expressions mapping.
+            modelComponents.labelToExpressionMap = buildLabelExpressions(model, variables, options);
+            
             // Finally, create the model.
             return createModel(model.getModelType(), variables, modelComponents);
         }
diff --git a/src/builder/DdJaniModelBuilder.h b/src/builder/DdJaniModelBuilder.h
index dd99f5fcb..85c62b0bd 100644
--- a/src/builder/DdJaniModelBuilder.h
+++ b/src/builder/DdJaniModelBuilder.h
@@ -25,7 +25,7 @@ namespace storm {
                 /*!
                  * Creates an object representing the default building options.
                  */
-                Options();
+                Options(bool buildAllLabels = false, bool buildAllRewardModels = false);
                 
                 /*! Creates an object representing the suggested building options assuming that the given formula is the
                  * only one to check. Additional formulas may be preserved by calling <code>preserveFormula</code>.
@@ -63,7 +63,23 @@ namespace storm {
                  * Retrieves the names of the reward models to build.
                  */
                 std::set<std::string> const& getRewardModelNames() const;
+
+                /*!
+                 * Adds the given label to the ones that are supposed to be built.
+                 */
+                void addLabel(std::string const& labelName);
+
+                /*!
+                 * Retrieves whether the flag to build all labels is set.
+                 */
+                bool isBuildAllLabelsSet() const;
+
+                /// A flag that indicates whether all labels are to be built. In this case, the label names are to be ignored.
+                bool buildAllLabels;
                 
+                /// A set of labels to build.
+                std::set<std::string> labelNames;
+
                 /*!
                  * Retrieves whether the flag to build all reward models is set.
                  */
@@ -98,4 +114,4 @@ namespace storm {
         };
         
     }
-}
\ No newline at end of file
+}
diff --git a/src/generator/CompressedState.cpp b/src/generator/CompressedState.cpp
index d7707d740..820b2000e 100644
--- a/src/generator/CompressedState.cpp
+++ b/src/generator/CompressedState.cpp
@@ -10,6 +10,13 @@ namespace storm {
         
         template<typename ValueType>
         void unpackStateIntoEvaluator(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<ValueType>& evaluator) {
+            for (auto const& locationVariable : variableInformation.locationVariables) {
+                if (locationVariable.bitWidth != 0) {
+                    evaluator.setIntegerValue(locationVariable.variable, state.getAsInt(locationVariable.bitOffset, locationVariable.bitWidth));
+                } else {
+                    evaluator.setIntegerValue(locationVariable.variable, 0);
+                }
+            }
             for (auto const& booleanVariable : variableInformation.booleanVariables) {
                 evaluator.setBooleanValue(booleanVariable.variable, state.get(booleanVariable.bitOffset));
             }
@@ -20,6 +27,13 @@ namespace storm {
         
         storm::expressions::SimpleValuation unpackStateIntoValuation(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionManager const& manager) {
             storm::expressions::SimpleValuation result(manager.getSharedPointer());
+            for (auto const& locationVariable : variableInformation.locationVariables) {
+                if (locationVariable.bitWidth != 0) {
+                    result.setIntegerValue(locationVariable.variable, state.getAsInt(locationVariable.bitOffset, locationVariable.bitWidth));
+                } else {
+                    result.setIntegerValue(locationVariable.variable, 0);
+                }
+            }
             for (auto const& booleanVariable : variableInformation.booleanVariables) {
                 result.setBooleanValue(booleanVariable.variable, state.get(booleanVariable.bitOffset));
             }
diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp
index b84ffca3c..bc166cba3 100644
--- a/src/generator/JaniNextStateGenerator.cpp
+++ b/src/generator/JaniNextStateGenerator.cpp
@@ -32,6 +32,9 @@ namespace storm {
             this->checkValid();
             this->variableInformation = VariableInformation(model);
             
+            // Create a proper evalator.
+            this->evaluator = std::make_unique<storm::expressions::ExpressionEvaluator<ValueType>>(model.getManager());
+            
             if (this->options.isBuildAllRewardModelsSet()) {
                 for (auto const& variable : model.getGlobalVariables()) {
                     if (variable.isTransient()) {
@@ -46,14 +49,22 @@ namespace storm {
                         rewardVariables.push_back(globalVariables.getVariable(rewardModelName).getExpressionVariable());
                     } else {
                         STORM_LOG_THROW(rewardModelName.empty(), storm::exceptions::InvalidArgumentException, "Cannot build unknown reward model '" << rewardModelName << "'.");
-                        STORM_LOG_THROW(globalVariables.getNumberOfTransientVariables() == 1, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is ambiguous.");
+                        STORM_LOG_THROW(globalVariables.getNumberOfRealTransientVariables() + globalVariables.getNumberOfUnboundedIntegerTransientVariables() == 1, storm::exceptions::InvalidArgumentException, "Reference to standard reward model is ambiguous.");
                     }
                 }
                 
                 // If no reward model was yet added, but there was one that was given in the options, we try to build the
                 // standard reward model.
                 if (rewardVariables.empty() && !this->options.getRewardModelNames().empty()) {
-                    rewardVariables.push_back(globalVariables.getTransientVariables().front()->getExpressionVariable());
+                    bool foundTransientVariable = false;
+                    for (auto const& transientVariable : globalVariables.getTransientVariables()) {
+                        if (transientVariable->isUnboundedIntegerVariable() || transientVariable->isRealVariable()) {
+                            rewardVariables.push_back(transientVariable->getExpressionVariable());
+                            foundTransientVariable = true;
+                            break;
+                        }
+                    }
+                    STORM_LOG_ASSERT(foundTransientVariable, "Expected to find a fitting transient variable.");
                 }
             }
             
@@ -62,11 +73,28 @@ namespace storm {
             
             // If there are terminal states we need to handle, we now need to translate all labels to expressions.
             if (this->options.hasTerminalStates()) {
+                std::map<std::string, storm::expressions::Variable> locationVariables;
+                auto locationVariableIt = this->variableInformation.locationVariables.begin();
+                for (auto const& automaton : this->model.getAutomata()) {
+                    locationVariables[automaton.getName()] = locationVariableIt->variable;
+                    ++locationVariableIt;
+                }
+                
                 for (auto const& expressionOrLabelAndBool : this->options.getTerminalStates()) {
                     if (expressionOrLabelAndBool.first.isExpression()) {
                         this->terminalStates.push_back(std::make_pair(expressionOrLabelAndBool.first.getExpression(), expressionOrLabelAndBool.second));
                     } else {
-                        STORM_LOG_THROW(expressionOrLabelAndBool.first.getLabel() == "init" || expressionOrLabelAndBool.first.getLabel() == "deadlock", storm::exceptions::InvalidSettingsException, "Terminal states refer to illegal label '" << expressionOrLabelAndBool.first.getLabel() << "'.");
+                        // If it's a label, i.e. refers to a transient boolean variable we need to derive the expression
+                        // for the label so we can cut off the exploration there.
+                        if (expressionOrLabelAndBool.first.getLabel() != "init" && expressionOrLabelAndBool.first.getLabel() != "deadlock") {
+                            STORM_LOG_THROW(model.getGlobalVariables().hasVariable(expressionOrLabelAndBool.first.getLabel()) , storm::exceptions::InvalidSettingsException, "Terminal states refer to illegal label '" << expressionOrLabelAndBool.first.getLabel() << "'.");
+                            
+                            storm::jani::Variable const& variable = model.getGlobalVariables().getVariable(expressionOrLabelAndBool.first.getLabel());
+                            STORM_LOG_THROW(variable.isBooleanVariable(), storm::exceptions::InvalidSettingsException, "Terminal states refer to non-boolean variable '" << expressionOrLabelAndBool.first.getLabel() << "'.");
+                            STORM_LOG_THROW(variable.isTransient(), storm::exceptions::InvalidSettingsException, "Terminal states refer to non-transient variable '" << expressionOrLabelAndBool.first.getLabel() << "'.");
+
+                            this->terminalStates.push_back(std::make_pair(this->model.getLabelExpression(variable.asBooleanVariable(), locationVariables), expressionOrLabelAndBool.second));
+                        }
                     }
                 }
             }
@@ -116,7 +144,11 @@ namespace storm {
             
             auto resultIt = result.begin();
             for (auto it = this->variableInformation.locationVariables.begin(), ite = this->variableInformation.locationVariables.end(); it != ite; ++it, ++resultIt) {
-                *resultIt = getLocation(state, *it);
+                if (it->bitWidth == 0) {
+                    *resultIt = 0;
+                } else {
+                    *resultIt = state.getAsInt(it->bitOffset, it->bitWidth);
+                }
             }
             
             return result;
@@ -221,7 +253,7 @@ namespace storm {
                 while (assignmentIt->getExpressionVariable() != boolIt->variable) {
                     ++boolIt;
                 }
-                newState.set(boolIt->bitOffset, this->evaluator.asBool(assignmentIt->getAssignedExpression()));
+                newState.set(boolIt->bitOffset, this->evaluator->asBool(assignmentIt->getAssignedExpression()));
             }
             
             // Iterate over all integer assignments and carry them out.
@@ -230,7 +262,7 @@ namespace storm {
                 while (assignmentIt->getExpressionVariable() != integerIt->variable) {
                     ++integerIt;
                 }
-                int_fast64_t assignedValue = this->evaluator.asInt(assignmentIt->getAssignedExpression());
+                int_fast64_t assignedValue = this->evaluator->asInt(assignmentIt->getAssignedExpression());
                 STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << assignmentIt->getExpressionVariable().getName() << " := " << assignmentIt->getAssignedExpression() << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getExpressionVariable().getName() << "'.");
                 newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound);
                 STORM_LOG_ASSERT(static_cast<int_fast64_t>(newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth)) + integerIt->lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << newState.getAsInt(integerIt->bitOffset, integerIt->bitWidth) << " but wrote " << assignedValue << ").");
@@ -266,7 +298,7 @@ namespace storm {
             // If a terminal expression was set and we must not expand this state, return now.
             if (!this->terminalStates.empty()) {
                 for (auto const& expressionBool : this->terminalStates) {
-                    if (this->evaluator.asBool(expressionBool.first) == expressionBool.second) {
+                    if (this->evaluator->asBool(expressionBool.first) == expressionBool.second) {
                         return result;
                     }
                 }
@@ -356,14 +388,14 @@ namespace storm {
                     }
                     
                     // Skip the command, if it is not enabled.
-                    if (!this->evaluator.asBool(edge.getGuard())) {
+                    if (!this->evaluator->asBool(edge.getGuard())) {
                         continue;
                     }
                     
                     // Determine the exit rate if it's a Markovian edge.
                     boost::optional<ValueType> exitRate = boost::none;
                     if (edge.hasRate()) {
-                        exitRate = this->evaluator.asRational(edge.getRate());
+                        exitRate = this->evaluator->asRational(edge.getRate());
                     }
                     
                     result.push_back(Choice<ValueType>(edge.getActionIndex(), static_cast<bool>(exitRate)));
@@ -377,7 +409,7 @@ namespace storm {
                         StateType stateIndex = stateToIdCallback(applyUpdate(state, destination, this->variableInformation.locationVariables[automatonIndex]));
                         
                         // Update the choice by adding the probability/target state to it.
-                        ValueType probability = this->evaluator.asRational(destination.getProbability());
+                        ValueType probability = this->evaluator->asRational(destination.getProbability());
                         probability = exitRate ? exitRate.get() * probability : probability;
                         choice.addProbability(stateIndex, probability);
                         probabilitySum += probability;
@@ -437,9 +469,9 @@ namespace storm {
                                     // and otherwise insert it.
                                     auto targetStateIt = newTargetStates->find(newTargetState);
                                     if (targetStateIt != newTargetStates->end()) {
-                                        targetStateIt->second += stateProbabilityPair.second * this->evaluator.asRational(destination.getProbability());
+                                        targetStateIt->second += stateProbabilityPair.second * this->evaluator->asRational(destination.getProbability());
                                     } else {
-                                        newTargetStates->emplace(newTargetState, stateProbabilityPair.second * this->evaluator.asRational(destination.getProbability()));
+                                        newTargetStates->emplace(newTargetState, stateProbabilityPair.second * this->evaluator->asRational(destination.getProbability()));
                                     }
                                 }
                                 
@@ -525,7 +557,7 @@ namespace storm {
                 
                 std::vector<storm::jani::Edge const*> edgePointers;
                 for (auto const& edge : edges) {
-                    if (this->evaluator.asBool(edge.getGuard())) {
+                    if (this->evaluator->asBool(edge.getGuard())) {
                         edgePointers.push_back(&edge);
                     }
                 }
@@ -574,7 +606,32 @@ namespace storm {
         
         template<typename ValueType, typename StateType>
         storm::models::sparse::StateLabeling JaniNextStateGenerator<ValueType, StateType>::label(storm::storage::BitVectorHashMap<StateType> const& states, std::vector<StateType> const& initialStateIndices, std::vector<StateType> const& deadlockStateIndices) {
-            return NextStateGenerator<ValueType, StateType>::label(states, initialStateIndices, deadlockStateIndices, {});
+            
+            // Prepare a mapping from automata names to the location variables.
+            std::map<std::string, storm::expressions::Variable> locationVariables;
+            auto locationVariableIt = this->variableInformation.locationVariables.begin();
+            for (auto const& automaton : model.getAutomata()) {
+                locationVariables[automaton.getName()] = locationVariableIt->variable;
+                ++locationVariableIt;
+            }
+            
+            // As in JANI we can use transient boolean variable assignments in locations to identify states, we need to
+            // create a list of boolean transient variables and the expressions that define them.
+            std::unordered_map<storm::expressions::Variable, storm::expressions::Expression> transientVariableToExpressionMap;
+            for (auto const& variable : model.getGlobalVariables().getTransientVariables()) {
+                if (variable->isBooleanVariable()) {
+                    if (this->options.isBuildAllLabelsSet() || this->options.getLabelNames().find(variable->getName()) != this->options.getLabelNames().end()) {
+                        transientVariableToExpressionMap[variable->getExpressionVariable()] = model.getLabelExpression(variable->asBooleanVariable(), locationVariables);
+                    }
+                }
+            }
+            
+            std::vector<std::pair<std::string, storm::expressions::Expression>> transientVariableExpressions;
+            for (auto const& element : transientVariableToExpressionMap) {
+                transientVariableExpressions.push_back(std::make_pair(element.first.getName(), element.second));
+            }
+            
+            return NextStateGenerator<ValueType, StateType>::label(states, initialStateIndices, deadlockStateIndices, transientVariableExpressions);
         }
         
         template<typename ValueType, typename StateType>
@@ -595,7 +652,7 @@ namespace storm {
                 if (rewardVariableIt == rewardVariableIte) {
                     break;
                 } else if (*rewardVariableIt == assignment.getExpressionVariable()) {
-                    callback(ValueType(this->evaluator.asRational(assignment.getAssignedExpression())));
+                    callback(ValueType(this->evaluator->asRational(assignment.getAssignedExpression())));
                     ++rewardVariableIt;
                 }
             }
diff --git a/src/generator/JaniNextStateGenerator.h b/src/generator/JaniNextStateGenerator.h
index 7855bc5cf..7d5907c21 100644
--- a/src/generator/JaniNextStateGenerator.h
+++ b/src/generator/JaniNextStateGenerator.h
@@ -105,7 +105,7 @@ namespace storm {
              * Checks the underlying model for validity for this next-state generator.
              */
             void checkValid() const;
-            
+                        
             /// The model used for the generation of next states.
             storm::jani::Model model;
             
diff --git a/src/generator/NextStateGenerator.cpp b/src/generator/NextStateGenerator.cpp
index 08fe61ba1..cf15f0a3f 100644
--- a/src/generator/NextStateGenerator.cpp
+++ b/src/generator/NextStateGenerator.cpp
@@ -224,12 +224,12 @@ namespace storm {
         }
         
         template<typename ValueType, typename StateType>
-        NextStateGenerator<ValueType, StateType>::NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, VariableInformation const& variableInformation, NextStateGeneratorOptions const& options) : options(options), expressionManager(expressionManager.getSharedPointer()), variableInformation(variableInformation), evaluator(expressionManager), state(nullptr) {
+        NextStateGenerator<ValueType, StateType>::NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, VariableInformation const& variableInformation, NextStateGeneratorOptions const& options) : options(options), expressionManager(expressionManager.getSharedPointer()), variableInformation(variableInformation), evaluator(nullptr), state(nullptr) {
             // Intentionally left empty.
         }
         
         template<typename ValueType, typename StateType>
-        NextStateGenerator<ValueType, StateType>::NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, NextStateGeneratorOptions const& options) : options(options), expressionManager(expressionManager.getSharedPointer()), variableInformation(), evaluator(expressionManager), state(nullptr) {
+        NextStateGenerator<ValueType, StateType>::NextStateGenerator(storm::expressions::ExpressionManager const& expressionManager, NextStateGeneratorOptions const& options) : options(options), expressionManager(expressionManager.getSharedPointer()), variableInformation(), evaluator(nullptr), state(nullptr) {
             // Intentionally left empty.
         }
         
@@ -246,7 +246,7 @@ namespace storm {
         template<typename ValueType, typename StateType>
         void NextStateGenerator<ValueType, StateType>::load(CompressedState const& state) {
             // Since almost all subsequent operations are based on the evaluator, we load the state into it now.
-            unpackStateIntoEvaluator(state, variableInformation, evaluator);
+            unpackStateIntoEvaluator(state, variableInformation, *evaluator);
             
             // Also, we need to store a pointer to the state itself, because we need to be able to access it when expanding it.
             this->state = &state;
@@ -257,7 +257,7 @@ namespace storm {
             if (expression.isTrue()) {
                 return true;
             }
-            return evaluator.asBool(expression);
+            return evaluator->asBool(expression);
         }
         
         template<typename ValueType, typename StateType>
@@ -282,11 +282,11 @@ namespace storm {
                 result.addLabel(label.first);
             }
             for (auto const& stateIndexPair : states) {
-                unpackStateIntoEvaluator(stateIndexPair.first, variableInformation, this->evaluator);
+                unpackStateIntoEvaluator(stateIndexPair.first, variableInformation, *this->evaluator);
                 
                 for (auto const& label : labelsAndExpressions) {
                     // Add label to state, if the corresponding expression is true.
-                    if (evaluator.asBool(label.second)) {
+                    if (evaluator->asBool(label.second)) {
                         result.addLabelToState(label.first, stateIndexPair.second);
                     }
                 }
diff --git a/src/generator/NextStateGenerator.h b/src/generator/NextStateGenerator.h
index b2989b256..b9b7bfe23 100644
--- a/src/generator/NextStateGenerator.h
+++ b/src/generator/NextStateGenerator.h
@@ -211,7 +211,7 @@ namespace storm {
             VariableInformation variableInformation;
             
             /// An evaluator used to evaluate expressions.
-            storm::expressions::ExpressionEvaluator<ValueType> evaluator;
+            std::unique_ptr<storm::expressions::ExpressionEvaluator<ValueType>> evaluator;
             
             /// The currently loaded state.
             CompressedState const* state;
diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp
index 6eceb0c26..e344ab13a 100644
--- a/src/generator/PrismNextStateGenerator.cpp
+++ b/src/generator/PrismNextStateGenerator.cpp
@@ -30,6 +30,9 @@ namespace storm {
             this->checkValid();
             this->variableInformation = VariableInformation(program);
             
+            // Create a proper evalator.
+            this->evaluator = std::make_unique<storm::expressions::ExpressionEvaluator<ValueType>>(program.getManager());
+            
             if (this->options.isBuildAllRewardModelsSet()) {
                 for (auto const& rewardModel : this->program.getRewardModels()) {
                     rewardModels.push_back(rewardModel);
@@ -186,8 +189,8 @@ namespace storm {
                 ValueType stateRewardValue = storm::utility::zero<ValueType>();
                 if (rewardModel.get().hasStateRewards()) {
                     for (auto const& stateReward : rewardModel.get().getStateRewards()) {
-                        if (this->evaluator.asBool(stateReward.getStatePredicateExpression())) {
-                            stateRewardValue += ValueType(this->evaluator.asRational(stateReward.getRewardValueExpression()));
+                        if (this->evaluator->asBool(stateReward.getStatePredicateExpression())) {
+                            stateRewardValue += ValueType(this->evaluator->asRational(stateReward.getRewardValueExpression()));
                         }
                     }
                 }
@@ -197,7 +200,7 @@ namespace storm {
             // If a terminal expression was set and we must not expand this state, return now.
             if (!this->terminalStates.empty()) {
                 for (auto const& expressionBool : this->terminalStates) {
-                    if (this->evaluator.asBool(expressionBool.first) == expressionBool.second) {
+                    if (this->evaluator->asBool(expressionBool.first) == expressionBool.second) {
                         return result;
                     }
                 }
@@ -252,8 +255,8 @@ namespace storm {
                     if (rewardModel.get().hasStateActionRewards()) {
                         for (auto const& stateActionReward : rewardModel.get().getStateActionRewards()) {
                             for (auto const& choice : allChoices) {
-                                if (stateActionReward.getActionIndex() == choice.getActionIndex() && this->evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
-                                    stateActionRewardValue += ValueType(this->evaluator.asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass() / totalExitRate;
+                                if (stateActionReward.getActionIndex() == choice.getActionIndex() && this->evaluator->asBool(stateActionReward.getStatePredicateExpression())) {
+                                    stateActionRewardValue += ValueType(this->evaluator->asRational(stateActionReward.getRewardValueExpression())) * choice.getTotalMass() / totalExitRate;
                                 }
                             }
                             
@@ -295,7 +298,7 @@ namespace storm {
                 while (assignmentIt->getVariable() != boolIt->variable) {
                     ++boolIt;
                 }
-                newState.set(boolIt->bitOffset, this->evaluator.asBool(assignmentIt->getExpression()));
+                newState.set(boolIt->bitOffset, this->evaluator->asBool(assignmentIt->getExpression()));
             }
             
             // Iterate over all integer assignments and carry them out.
@@ -304,7 +307,7 @@ namespace storm {
                 while (assignmentIt->getVariable() != integerIt->variable) {
                     ++integerIt;
                 }
-                int_fast64_t assignedValue = this->evaluator.asInt(assignmentIt->getExpression());
+                int_fast64_t assignedValue = this->evaluator->asInt(assignmentIt->getExpression());
                 STORM_LOG_THROW(assignedValue <= integerIt->upperBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'.");
                 STORM_LOG_THROW(assignedValue >= integerIt->lowerBound, storm::exceptions::WrongFormatException, "The update " << update << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getVariableName() << "'.");
                 newState.setFromInt(integerIt->bitOffset, integerIt->bitWidth, assignedValue - integerIt->lowerBound);
@@ -343,7 +346,7 @@ namespace storm {
                 // Look up commands by their indices and add them if the guard evaluates to true in the given state.
                 for (uint_fast64_t commandIndex : commandIndices) {
                     storm::prism::Command const& command = module.getCommand(commandIndex);
-                    if (this->evaluator.asBool(command.getGuardExpression())) {
+                    if (this->evaluator->asBool(command.getGuardExpression())) {
                         commands.push_back(command);
                     }
                 }
@@ -376,7 +379,7 @@ namespace storm {
                     if (command.isLabeled()) continue;
                     
                     // Skip the command, if it is not enabled.
-                    if (!this->evaluator.asBool(command.getGuardExpression())) {
+                    if (!this->evaluator->asBool(command.getGuardExpression())) {
                         continue;
                     }
                     
@@ -398,7 +401,7 @@ namespace storm {
                         StateType stateIndex = stateToIdCallback(applyUpdate(state, update));
                         
                         // Update the choice by adding the probability/target state to it.
-                        ValueType probability = this->evaluator.asRational(update.getLikelihoodExpression());
+                        ValueType probability = this->evaluator->asRational(update.getLikelihoodExpression());
                         choice.addProbability(stateIndex, probability);
                         probabilitySum += probability;
                     }
@@ -408,8 +411,8 @@ namespace storm {
                         ValueType stateActionRewardValue = storm::utility::zero<ValueType>();
                         if (rewardModel.get().hasStateActionRewards()) {
                             for (auto const& stateActionReward : rewardModel.get().getStateActionRewards()) {
-                                if (stateActionReward.getActionIndex() == choice.getActionIndex() && this->evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
-                                    stateActionRewardValue += ValueType(this->evaluator.asRational(stateActionReward.getRewardValueExpression()));
+                                if (stateActionReward.getActionIndex() == choice.getActionIndex() && this->evaluator->asBool(stateActionReward.getStatePredicateExpression())) {
+                                    stateActionRewardValue += ValueType(this->evaluator->asRational(stateActionReward.getRewardValueExpression()));
                                 }
                             }
                         }
@@ -462,9 +465,9 @@ namespace storm {
                                     // and otherwise insert it.
                                     auto targetStateIt = newTargetStates->find(newTargetState);
                                     if (targetStateIt != newTargetStates->end()) {
-                                        targetStateIt->second += stateProbabilityPair.second * this->evaluator.asRational(update.getLikelihoodExpression());
+                                        targetStateIt->second += stateProbabilityPair.second * this->evaluator->asRational(update.getLikelihoodExpression());
                                     } else {
-                                        newTargetStates->emplace(newTargetState, stateProbabilityPair.second * this->evaluator.asRational(update.getLikelihoodExpression()));
+                                        newTargetStates->emplace(newTargetState, stateProbabilityPair.second * this->evaluator->asRational(update.getLikelihoodExpression()));
                                     }
                                 }
                             }
@@ -509,8 +512,8 @@ namespace storm {
                             ValueType stateActionRewardValue = storm::utility::zero<ValueType>();
                             if (rewardModel.get().hasStateActionRewards()) {
                                 for (auto const& stateActionReward : rewardModel.get().getStateActionRewards()) {
-                                    if (stateActionReward.getActionIndex() == choice.getActionIndex() && this->evaluator.asBool(stateActionReward.getStatePredicateExpression())) {
-                                        stateActionRewardValue += ValueType(this->evaluator.asRational(stateActionReward.getRewardValueExpression()));
+                                    if (stateActionReward.getActionIndex() == choice.getActionIndex() && this->evaluator->asBool(stateActionReward.getStatePredicateExpression())) {
+                                        stateActionRewardValue += ValueType(this->evaluator->asRational(stateActionReward.getRewardValueExpression()));
                                     }
                                 }
                             }
diff --git a/src/generator/VariableInformation.cpp b/src/generator/VariableInformation.cpp
index 125e6089d..c1a00e4e6 100644
--- a/src/generator/VariableInformation.cpp
+++ b/src/generator/VariableInformation.cpp
@@ -2,6 +2,7 @@
 
 #include "src/storage/prism/Program.h"
 #include "src/storage/jani/Model.h"
+#include "src/storage/expressions/ExpressionManager.h"
 
 #include "src/utility/macros.h"
 #include "src/exceptions/InvalidArgumentException.h"
@@ -19,7 +20,7 @@ namespace storm {
             // Intentionally left empty.
         }
         
-        LocationVariableInformation::LocationVariableInformation(uint64_t highestValue, uint_fast64_t bitOffset, uint_fast64_t bitWidth) : highestValue(highestValue), bitOffset(bitOffset), bitWidth(bitWidth) {
+        LocationVariableInformation::LocationVariableInformation(storm::expressions::Variable const& variable, uint64_t highestValue, uint_fast64_t bitOffset, uint_fast64_t bitWidth) : variable(variable), highestValue(highestValue), bitOffset(bitOffset), bitWidth(bitWidth) {
             // Intentionally left empty.
         }
         
@@ -74,7 +75,7 @@ namespace storm {
             }
             for (auto const& automaton : model.getAutomata()) {
                 uint_fast64_t bitwidth = static_cast<uint_fast64_t>(std::ceil(std::log2(automaton.getNumberOfLocations())));
-                locationVariables.emplace_back(automaton.getNumberOfLocations() - 1, totalBitOffset, bitwidth);
+                locationVariables.emplace_back(model.getManager().declareFreshIntegerVariable(false, "loc"), automaton.getNumberOfLocations() - 1, totalBitOffset, bitwidth);
                 totalBitOffset += bitwidth;
                 
                 for (auto const& variable : automaton.getVariables().getBooleanVariables()) {
diff --git a/src/generator/VariableInformation.h b/src/generator/VariableInformation.h
index 1aa8ee95c..0bbef3a6e 100644
--- a/src/generator/VariableInformation.h
+++ b/src/generator/VariableInformation.h
@@ -56,7 +56,10 @@ namespace storm {
         
         // A structure storing information about the location variables of the model.
         struct LocationVariableInformation {
-            LocationVariableInformation(uint64_t highestValue, uint_fast64_t bitOffset, uint_fast64_t bitWidth);
+            LocationVariableInformation(storm::expressions::Variable const& variable, uint64_t highestValue, uint_fast64_t bitOffset, uint_fast64_t bitWidth);
+
+            // The expression variable for this location.
+            storm::expressions::Variable variable;
 
             // The highest possible location value.
             uint64_t highestValue;
@@ -98,4 +101,4 @@ namespace storm {
     }
 }
 
-#endif /* STORM_GENERATOR_VARIABLEINFORMATION_H_ */
\ No newline at end of file
+#endif /* STORM_GENERATOR_VARIABLEINFORMATION_H_ */
diff --git a/src/storage/BitVector.h b/src/storage/BitVector.h
index c8b81709f..ecdd03536 100644
--- a/src/storage/BitVector.h
+++ b/src/storage/BitVector.h
@@ -472,7 +472,7 @@ namespace storm {
              * value is equal to a call to size(), then there is no bit set after the specified position.
              *
              * @param startingIndex The index at which to start the search for the next bit that is set. The
-             * bit at this index itself is already considered.
+             * bit at this index itself is included in the search range.
              * @return The index of the next bit that is set after the given index.
              */
             uint_fast64_t getNextSetIndex(uint_fast64_t startingIndex) const;
diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp
index 343d88d78..ee2317df8 100644
--- a/src/storage/jani/Model.cpp
+++ b/src/storage/jani/Model.cpp
@@ -7,6 +7,7 @@
 
 #include "src/utility/macros.h"
 #include "src/exceptions/WrongFormatException.h"
+#include "src/exceptions/InvalidArgumentException.h"
 #include "src/exceptions/InvalidOperationException.h"
 #include "src/exceptions/InvalidTypeException.h"
 
@@ -456,7 +457,39 @@ namespace storm {
             STORM_LOG_ASSERT(getModelType() != storm::jani::ModelType::UNDEFINED, "Model type not set");
             STORM_LOG_ASSERT(!automata.empty(), "No automata set");
             STORM_LOG_ASSERT(composition != nullptr, "Composition is not set");
+        }
+        
+        storm::expressions::Expression Model::getLabelExpression(BooleanVariable const& transientVariable, std::map<std::string, storm::expressions::Variable> const& automatonToLocationVariableMap) const {
+            STORM_LOG_THROW(transientVariable.isTransient(), storm::exceptions::InvalidArgumentException, "Expected transient variable.");
+            
+            storm::expressions::Expression result;
+            bool negate = transientVariable.getInitExpression().isTrue();
+            
+            for (auto const& automaton : this->getAutomata()) {
+                storm::expressions::Variable const& locationVariable = automatonToLocationVariableMap.at(automaton.getName());
+                for (auto const& location : automaton.getLocations()) {
+                    for (auto const& assignment : location.getAssignments().getTransientAssignments()) {
+                        if (assignment.getExpressionVariable() == transientVariable.getExpressionVariable()) {
+                            auto newExpression = (locationVariable == this->getManager().integer(automaton.getLocationIndex(location.getName()))) && (negate ? !assignment.getAssignedExpression() : assignment.getAssignedExpression());
+                            if (result.isInitialized()) {
+                                result = result || newExpression;
+                            } else {
+                                result = newExpression;
+                            }
+                        }
+                    }
+                }
+            }
             
+            if (result.isInitialized()) {
+                if (negate) {
+                    result = !result;
+                }
+            } else {
+                result = this->getManager().boolean(negate);
+            }
+            
+            return result;
         }
         
         bool Model::hasStandardComposition() const {
diff --git a/src/storage/jani/Model.h b/src/storage/jani/Model.h
index 9a941a48f..35a74ead0 100644
--- a/src/storage/jani/Model.h
+++ b/src/storage/jani/Model.h
@@ -326,6 +326,12 @@ namespace storm {
              */
             void checkValid() const;
             
+            /*!
+             * Creates the expression that characterizes all states in which the provided transient boolean variable is
+             * true. The provided location variables are used to encode the location of the automata.
+             */
+            storm::expressions::Expression getLabelExpression(BooleanVariable const& transientVariable, std::map<std::string, storm::expressions::Variable> const& automatonToLocationVariableMap) const;
+            
             /*!
              * Checks that undefined constants (parameters) of the model preserve the graph of the underlying model.
              * That is, undefined constants may only appear in the probability expressions of edge destinations as well
diff --git a/src/storage/jani/VariableSet.cpp b/src/storage/jani/VariableSet.cpp
index a5468f63a..582fee73b 100644
--- a/src/storage/jani/VariableSet.cpp
+++ b/src/storage/jani/VariableSet.cpp
@@ -176,6 +176,26 @@ namespace storm {
             return result;
         }
         
+        uint_fast64_t VariableSet::getNumberOfRealTransientVariables() const {
+            uint_fast64_t result = 0;
+            for (auto const& variable : variables) {
+                if (variable->isTransient() && variable->isRealVariable()) {
+                    ++result;
+                }
+            }
+            return result;
+        }
+        
+        uint_fast64_t VariableSet::getNumberOfUnboundedIntegerTransientVariables() const {
+            uint_fast64_t result = 0;
+            for (auto const& variable : variables) {
+                if (variable->isTransient() && variable->isUnboundedIntegerVariable()) {
+                    ++result;
+                }
+            }
+            return result;
+        }
+        
         std::vector<std::shared_ptr<Variable const>> VariableSet::getTransientVariables() const {
             std::vector<std::shared_ptr<Variable const>> result;
             for (auto const& variable : variables) {
diff --git a/src/storage/jani/VariableSet.h b/src/storage/jani/VariableSet.h
index 1c947669e..031d56652 100644
--- a/src/storage/jani/VariableSet.h
+++ b/src/storage/jani/VariableSet.h
@@ -173,6 +173,16 @@ namespace storm {
              */
             uint_fast64_t getNumberOfTransientVariables() const;
             
+            /*!
+             * Retrieves the number of real transient variables in this variable set.
+             */
+            uint_fast64_t getNumberOfRealTransientVariables() const;
+
+            /*!
+             * Retrieves the number of unbounded integer transient variables in this variable set.
+             */
+            uint_fast64_t getNumberOfUnboundedIntegerTransientVariables() const;
+
             /*!
              * Retrieves a vector of transient variables in this variable set.
              */