diff --git a/src/storm/storage/jani/Assignment.cpp b/src/storm/storage/jani/Assignment.cpp
index 74f801906..0632f294d 100644
--- a/src/storm/storage/jani/Assignment.cpp
+++ b/src/storm/storage/jani/Assignment.cpp
@@ -27,6 +27,10 @@ namespace storm  {
             return lValue.isArrayAccess();
         }
         
+        storm::jani::LValue& Assignment::getLValue() {
+            return lValue;
+        }
+        
         storm::jani::LValue const& Assignment::getLValue() const {
             return lValue;
         }
diff --git a/src/storm/storage/jani/Assignment.h b/src/storm/storage/jani/Assignment.h
index 5179215e7..f2a18c8a9 100644
--- a/src/storm/storage/jani/Assignment.h
+++ b/src/storm/storage/jani/Assignment.h
@@ -31,9 +31,13 @@ namespace storm {
             
             /*!
              * Retrieves the lValue that is written in this assignment.
-             * @return
              */
             storm::jani::LValue const& getLValue() const;
+
+            /*!
+             * Retrieves the lValue that is written in this assignment.
+             */
+            storm::jani::LValue& getLValue();
             
             /*!
              * Retrieves the Variable that is written in this assignment.
diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp
index 9737d768f..b9c1e6449 100644
--- a/src/storm/storage/jani/Automaton.cpp
+++ b/src/storm/storage/jani/Automaton.cpp
@@ -281,6 +281,10 @@ namespace storm {
             return edges;
         }
         
+        EdgeContainer& Automaton::getEdgeContainer() {
+            return edges;
+        }
+        
         void Automaton::addEdge(Edge const& edge) {
             STORM_LOG_THROW(edge.getSourceLocationIndex() < locations.size(), storm::exceptions::InvalidArgumentException, "Cannot add edge with unknown source location index '" << edge.getSourceLocationIndex() << "'.");
             assert(validate());
@@ -293,8 +297,6 @@ namespace storm {
             for (uint64_t locationIndex = edge.getSourceLocationIndex() + 1; locationIndex < locationToStartingIndex.size(); ++locationIndex) {
                 ++locationToStartingIndex[locationIndex];
             }
-            
-
         }
         
         std::vector<Edge>& Automaton::getEdges() {
@@ -476,8 +478,8 @@ namespace storm {
             return false;
         }
         
-        void Automaton::liftTransientEdgeDestinationAssignments() {
-            edges.liftTransientDestinationAssignments();
+        void Automaton::liftTransientEdgeDestinationAssignments(uint64_t maxLevel) {
+            edges.liftTransientDestinationAssignments(maxLevel);
         }
 
         bool Automaton::validate() const {
@@ -488,8 +490,8 @@ namespace storm {
             return true;
         }
 
-        bool Automaton::usesAssignmentLevels() const {
-            return edges.usesAssignmentLevels();
+        bool Automaton::usesAssignmentLevels(bool onlyTransient) const {
+            return edges.usesAssignmentLevels(onlyTransient);
         }
         
         bool Automaton::isLinear() const {
diff --git a/src/storm/storage/jani/Automaton.h b/src/storm/storage/jani/Automaton.h
index 6e51d6440..abd459735 100644
--- a/src/storm/storage/jani/Automaton.h
+++ b/src/storm/storage/jani/Automaton.h
@@ -197,7 +197,15 @@ namespace storm {
              */
             ConstEdges getEdgesFromLocation(uint64_t locationIndex, uint64_t actionIndex) const;
             
+            /*!
+             * Retrieves the container of all edges of this automaton.
+             */
             EdgeContainer const& getEdgeContainer() const;
+
+            /*!
+             * Retrieves the container of all edges of this automaton.
+             */
+            EdgeContainer& getEdgeContainer();
             
             /*!
              * Adds the template edge to the list of edges
@@ -317,12 +325,12 @@ namespace storm {
             /*!
              * Lifts the common edge destination assignments to edge assignments.
              */
-            void liftTransientEdgeDestinationAssignments();
+            void liftTransientEdgeDestinationAssignments(uint64_t maxLevel = 0);
             
             /*!
              * Retrieves whether the automaton uses an assignment level other than zero.
              */
-            bool usesAssignmentLevels() const;
+            bool usesAssignmentLevels(bool onlyTransient = false) const;
 
             void simplifyIndexedAssignments();
             
diff --git a/src/storm/storage/jani/Edge.cpp b/src/storm/storage/jani/Edge.cpp
index 33834b2c4..cbe78c699 100644
--- a/src/storm/storage/jani/Edge.cpp
+++ b/src/storm/storage/jani/Edge.cpp
@@ -67,6 +67,10 @@ namespace storm {
             return destinations;
         }
         
+        std::vector<EdgeDestination>& Edge::getDestinations() {
+            return destinations;
+        }
+        
         std::size_t Edge::getNumberOfDestinations() const {
             return destinations.size();
         }
@@ -100,8 +104,8 @@ namespace storm {
             return templateEdge->hasTransientEdgeDestinationAssignments();
         }
         
-        bool Edge::usesAssignmentLevels() const {
-            return templateEdge->usesAssignmentLevels();
+        bool Edge::usesAssignmentLevels(bool onlyTransient) const {
+            return templateEdge->usesAssignmentLevels(onlyTransient);
         }
 
         void Edge::simplifyIndexedAssignments(VariableSet const& localVars) {
@@ -117,6 +121,14 @@ namespace storm {
             }
         }
 
+        uint64_t const& Edge::getLowestAssignmentLevel() const {
+            return templateEdge->getLowestAssignmentLevel();
+        }
+
+        uint64_t const& Edge::getHighestAssignmentLevel() const {
+            return templateEdge->getHighestAssignmentLevel();
+        }
+        
         void Edge::setTemplateEdge(std::shared_ptr<TemplateEdge> const& newTe) {
             templateEdge = newTe;
             uint64_t i = 0;
diff --git a/src/storm/storage/jani/Edge.h b/src/storm/storage/jani/Edge.h
index 002b97d40..d47edf14f 100644
--- a/src/storm/storage/jani/Edge.h
+++ b/src/storm/storage/jani/Edge.h
@@ -70,6 +70,11 @@ namespace storm {
              */
             std::vector<EdgeDestination> const& getDestinations() const;
             
+            /*!
+             * Retrieves the destinations of this edge.
+             */
+            std::vector<EdgeDestination>& getDestinations();
+            
             /*!
              * Retrieves the number of destinations of this edge.
              */
@@ -103,7 +108,7 @@ namespace storm {
             /*!
              * Retrieves whether the edge uses an assignment level other than zero.
              */
-            bool usesAssignmentLevels() const;
+            bool usesAssignmentLevels(bool onlyTransient = false) const;
 
             /*!
              *
@@ -112,9 +117,21 @@ namespace storm {
             void simplifyIndexedAssignments(VariableSet const& localVars);
             
             std::shared_ptr<TemplateEdge> const& getTemplateEdge();
-
             void setTemplateEdge(std::shared_ptr<TemplateEdge> const& newTe);
 
+            /*!
+             * Retrieves the lowest assignment level occurring in each assignment.
+             * If no assignment exists, this value is the highest possible integer
+             */
+            uint64_t const& getLowestAssignmentLevel() const;
+            
+            /*!
+             * Retrieves the highest assignment level occurring in each assignment
+             * If no assignment exists, this value is always zero
+             */
+            uint64_t const& getHighestAssignmentLevel() const;
+            
+
             void assertValid() const;
             
         private:
diff --git a/src/storm/storage/jani/EdgeContainer.cpp b/src/storm/storage/jani/EdgeContainer.cpp
index d735bc80d..83db856ad 100644
--- a/src/storm/storage/jani/EdgeContainer.cpp
+++ b/src/storm/storage/jani/EdgeContainer.cpp
@@ -86,9 +86,9 @@ namespace storm {
             edges.clear();
         }
 
-        void EdgeContainer::liftTransientDestinationAssignments() {
+        void EdgeContainer::liftTransientDestinationAssignments(uint64_t maxLevel) {
             for (auto& templateEdge : templates) {
-                templateEdge->liftTransientDestinationAssignments();
+                templateEdge->liftTransientDestinationAssignments(maxLevel);
             }
         }
 
@@ -111,9 +111,9 @@ namespace storm {
         }
 
 
-        bool EdgeContainer::usesAssignmentLevels() const {
+        bool EdgeContainer::usesAssignmentLevels(bool onlyTransient) const {
             for (auto const& edge : edges) {
-                if (edge.usesAssignmentLevels()) {
+                if (edge.usesAssignmentLevels(onlyTransient)) {
                     return true;
                 }
             }
diff --git a/src/storm/storage/jani/EdgeContainer.h b/src/storm/storage/jani/EdgeContainer.h
index c2bdfe80c..550fc80e0 100644
--- a/src/storm/storage/jani/EdgeContainer.h
+++ b/src/storm/storage/jani/EdgeContainer.h
@@ -107,12 +107,12 @@ namespace storm {
             std::set<uint64_t> getActionIndices() const;
 
             void substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution);
-            void liftTransientDestinationAssignments();
+            void liftTransientDestinationAssignments(uint64_t maxLevel = 0);
             void pushAssignmentsToDestinations();
             void insertEdge(Edge const& e, uint64_t locStart, uint64_t locEnd);
             void insertTemplateEdge(std::shared_ptr<TemplateEdge> const& te);
             bool isLinear() const;
-            bool usesAssignmentLevels() const;
+            bool usesAssignmentLevels(bool onlyTransient = false) const;
             void finalize(Model const& containingModel);
 
             void changeAssignmentVariables(std::map<Variable const*, std::reference_wrapper<Variable const>> const& remapping);
diff --git a/src/storm/storage/jani/Location.cpp b/src/storm/storage/jani/Location.cpp
index 5ab431734..7831436a7 100644
--- a/src/storm/storage/jani/Location.cpp
+++ b/src/storm/storage/jani/Location.cpp
@@ -23,6 +23,10 @@ namespace storm {
             return assignments;
         }
         
+        OrderedAssignments& Location::getAssignments() {
+            return assignments;
+        }
+        
         void Location::addTransientAssignment(storm::jani::Assignment const& assignment) {
             STORM_LOG_THROW(assignment.isTransient(), storm::exceptions::InvalidArgumentException, "Must not add non-transient assignment to location.");
             assignments.add(assignment);
diff --git a/src/storm/storage/jani/Location.h b/src/storm/storage/jani/Location.h
index 75e53d575..1fc3cd65d 100644
--- a/src/storm/storage/jani/Location.h
+++ b/src/storm/storage/jani/Location.h
@@ -30,6 +30,11 @@ namespace storm {
              */
             OrderedAssignments const& getAssignments() const;
             
+            /*!
+             * Retrieves the assignments of this location.
+             */
+            OrderedAssignments& getAssignments();
+            
             /*!
              * Adds the given transient assignment to this location.
              */
diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp
index 3f34b72d4..502c821c0 100644
--- a/src/storm/storage/jani/Model.cpp
+++ b/src/storm/storage/jani/Model.cpp
@@ -948,7 +948,7 @@ namespace storm {
         
         void Model::eliminateArrays(bool keepNonTrivialArrayAccess) {
             ArrayEliminator arrayEliminator;
-            arrayEliminator.eliminate(*this);
+            arrayEliminator.eliminate(*this, keepNonTrivialArrayAccess);
         }
         
         void Model::setInitialStatesRestriction(storm::expressions::Expression const& initialStatesRestriction) {
@@ -1164,9 +1164,9 @@ namespace storm {
             }
         }
         
-        void Model::liftTransientEdgeDestinationAssignments() {
+        void Model::liftTransientEdgeDestinationAssignments(uint64_t maxLevel) {
             for (auto& automaton : this->getAutomata()) {
-                automaton.liftTransientEdgeDestinationAssignments();
+                automaton.liftTransientEdgeDestinationAssignments(maxLevel);
             }
         }
         
@@ -1179,9 +1179,9 @@ namespace storm {
             return false;
         }
         
-        bool Model::usesAssignmentLevels() const {
+        bool Model::usesAssignmentLevels(bool onlyTransient) const {
             for (auto const& automaton : this->getAutomata()) {
-                if (automaton.usesAssignmentLevels()) {
+                if (automaton.usesAssignmentLevels(onlyTransient)) {
                     return true;
                 }
             }
diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h
index ed0d0638a..7ccc011a4 100644
--- a/src/storm/storage/jani/Model.h
+++ b/src/storm/storage/jani/Model.h
@@ -456,8 +456,9 @@ namespace storm {
             
             /*!
              * Lifts the common edge destination assignments to edge assignments.
+             * @param maxLevel the maximum level of assignments that are to be lifted.
              */
-            void liftTransientEdgeDestinationAssignments();
+            void liftTransientEdgeDestinationAssignments(uint64_t maxLevel = 0);
             
             /*!
              * Retrieves whether there is any transient edge destination assignment in the model.
@@ -466,8 +467,9 @@ namespace storm {
             
             /*!
              * Retrieves whether the model uses an assignment level other than zero.
+             * @param onlyTransient if set, only transient assignments are considered
              */
-            bool usesAssignmentLevels() const;
+            bool usesAssignmentLevels(bool onlyTransient = false) const;
             
             /*!
              * Checks the model for linearity. A model is linear if all expressions appearing in guards and assignments
diff --git a/src/storm/storage/jani/OrderedAssignments.cpp b/src/storm/storage/jani/OrderedAssignments.cpp
index 27ccd2761..11f59a5d0 100644
--- a/src/storm/storage/jani/OrderedAssignments.cpp
+++ b/src/storm/storage/jani/OrderedAssignments.cpp
@@ -80,11 +80,19 @@ namespace storm {
             return true;
         }
         
-        bool OrderedAssignments::hasMultipleLevels() const {
+        bool OrderedAssignments::hasMultipleLevels(bool onlyTransient) const {
             if (allAssignments.empty()) {
                 return false;
             }
-            return getLowestLevel() != 0 || getHighestLevel() != 0;
+            if (onlyTransient) {
+                for (auto const& a : allAssignments) {
+                    if (a->isTransient()) {
+                        return a->getLevel() != 0 || getHighestLevel(true) != 0;
+                    }
+                }
+                return false; // no transient assignments
+            }
+            return getLowestLevel(false) != 0 || getHighestLevel(false) != 0;
         }
         
         bool OrderedAssignments::empty() const {
@@ -101,13 +109,31 @@ namespace storm {
             return allAssignments.size();
         }
         
-        int_fast64_t OrderedAssignments::getLowestLevel() const {
+        int_fast64_t OrderedAssignments::getLowestLevel(bool onlyTransient) const {
             assert(!allAssignments.empty());
+            if (onlyTransient) {
+                for (auto const& a : allAssignments) {
+                    if (a->getLValue().isTransient()) {
+                        return a->getLevel();
+                    }
+                }
+                // assert that at least one transient variable is contained.
+                assert(false);
+            }
             return allAssignments.front()->getLevel();
         }
         
-        int_fast64_t OrderedAssignments::getHighestLevel() const {
+        int_fast64_t OrderedAssignments::getHighestLevel(bool onlyTransient) const {
             assert(!allAssignments.empty());
+            if (onlyTransient) {
+                for (auto aIt = allAssignments.rbegin(); aIt != allAssignments.rend(); ++aIt) {
+                    if ((*aIt)->getLValue().isTransient()) {
+                        return (*aIt)->getLevel();
+                    }
+                }
+                // assert that at least one transient variable is contained.
+                assert(false);
+            }
             return allAssignments.back()->getLevel();
         }
         
@@ -271,6 +297,15 @@ namespace storm {
             return result;
         }
         
+        bool OrderedAssignments::checkOrder() const {
+            for (std::vector<std::shared_ptr<Assignment>>::const_iterator it = allAssignments.cbegin(); it != allAssignments.cend(); ++it) {
+                if (it != lowerBound(**it, allAssignments)) {
+                    return false;
+                }
+            }
+            return true;
+        }
+        
         std::ostream& operator<<(std::ostream& stream, OrderedAssignments const& assignments) {
             stream << "[";
             for(auto const& e : assignments.allAssignments) {
diff --git a/src/storm/storage/jani/OrderedAssignments.h b/src/storm/storage/jani/OrderedAssignments.h
index aa81f59a3..54ac16e0d 100644
--- a/src/storm/storage/jani/OrderedAssignments.h
+++ b/src/storm/storage/jani/OrderedAssignments.h
@@ -44,7 +44,7 @@ namespace storm {
              * 
              * @return True if more than one level occurs in the assignment set.
              */
-            bool hasMultipleLevels() const;
+            bool hasMultipleLevels(bool onlyTransient = false) const;
 
             /**
              * Produces a new OrderedAssignments object with simplified leveling
@@ -73,13 +73,13 @@ namespace storm {
              * Retrieves the lowest level among all assignments. Note that this may only be called if there is at least
              * one assignment.
              */
-            int_fast64_t getLowestLevel() const;
+            int_fast64_t getLowestLevel(bool onlyTransient = false) const;
 
             /*!
              * Retrieves the highest level among all assignments. Note that this may only be called if there is at least
              * one assignment.
              */
-            int_fast64_t getHighestLevel() const;
+            int_fast64_t getHighestLevel(bool onlyTransient = false) const;
 
             /*!
              * Retrieves whether the given assignment is contained in this set of assignments.
@@ -144,7 +144,12 @@ namespace storm {
             friend std::ostream& operator<<(std::ostream& stream, OrderedAssignments const& assignments);
 
             OrderedAssignments clone() const;
-
+            
+            /*!
+             * Checks whether this ordered assignment is in the correct order.
+             */
+            bool checkOrder() const;
+            
         private:
             uint64_t isReadBeforeAssignment(LValue const& lValue, uint64_t assignmentNumber, uint64_t start = 0) const;
             uint64_t isWrittenBeforeAssignment(LValue const& LValue, uint64_t assignmentNumber, uint64_t start = 0) const;
diff --git a/src/storm/storage/jani/TemplateEdge.cpp b/src/storm/storage/jani/TemplateEdge.cpp
index 889d25214..79644f8a6 100644
--- a/src/storm/storage/jani/TemplateEdge.cpp
+++ b/src/storm/storage/jani/TemplateEdge.cpp
@@ -9,12 +9,12 @@
 namespace storm {
     namespace jani {
         
-        TemplateEdge::TemplateEdge(storm::expressions::Expression const& guard) : guard(guard) {
+        TemplateEdge::TemplateEdge(storm::expressions::Expression const& guard) : guard(guard), lowestAssignmentLevel(std::numeric_limits<uint64_t>::max()), highestAssignmentLevel(0) {
             // Intentionally left empty.
         }
 
         TemplateEdge::TemplateEdge(storm::expressions::Expression const& guard, OrderedAssignments const& assignments, std::vector<TemplateEdgeDestination> const& destinations)
-                : guard(guard), destinations(destinations), assignments(assignments) {
+                : guard(guard), destinations(destinations), assignments(assignments), lowestAssignmentLevel(std::numeric_limits<uint64_t>::max()), highestAssignmentLevel(0) {
             // Intentionally left empty.
         }
         
@@ -27,7 +27,18 @@ namespace storm {
         }
         
         void TemplateEdge::finalize(Model const& containingModel) {
+            if (assignments.empty()) {
+                lowestAssignmentLevel = std::numeric_limits<uint64_t>::max();
+                highestAssignmentLevel = 0;
+            } else {
+                lowestAssignmentLevel = assignments.getLowestLevel();
+                highestAssignmentLevel = assignments.getHighestLevel();
+            }
             for (auto const& destination : getDestinations()) {
+                if (!destination.getOrderedAssignments().empty()) {
+                    lowestAssignmentLevel = std::min<uint64_t>(lowestAssignmentLevel, destination.getOrderedAssignments().getLowestLevel());
+                    highestAssignmentLevel = std::max<uint64_t>(highestAssignmentLevel, destination.getOrderedAssignments().getHighestLevel());
+                }
                 for (auto const& assignment : destination.getOrderedAssignments().getAllAssignments()) {
                     Variable const& var = assignment.getLValue().isVariable() ? assignment.getLValue().getVariable() : assignment.getLValue().getArray();
                     if (containingModel.getGlobalVariables().hasVariable(var.getExpressionVariable())) {
@@ -53,6 +64,10 @@ namespace storm {
             return destinations;
         }
         
+        std::vector<TemplateEdgeDestination>& TemplateEdge::getDestinations() {
+            return destinations;
+        }
+        
         TemplateEdgeDestination const& TemplateEdge::getDestination(uint64_t index) const {
             return destinations[index];
         }
@@ -60,6 +75,10 @@ namespace storm {
         OrderedAssignments const& TemplateEdge::getAssignments() const {
             return assignments;
         }
+
+        OrderedAssignments& TemplateEdge::getAssignments() {
+            return assignments;
+        }
         
         void TemplateEdge::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) {
             guard = substituteJaniExpression(guard, substitution);
@@ -80,7 +99,7 @@ namespace storm {
             assignments.changeAssignmentVariables(remapping);
         }
 
-        void TemplateEdge::liftTransientDestinationAssignments() {
+        void TemplateEdge::liftTransientDestinationAssignments(uint64_t maxLevel) {
             if (!destinations.empty()) {
                 auto const& destination = *destinations.begin();
                 
@@ -88,11 +107,13 @@ namespace storm {
                 
                 for (auto const& assignment : destination.getOrderedAssignments().getTransientAssignments()) {
                     // Check if we can lift the assignment to the edge.
-                    bool canBeLifted = true;
-                    for (auto const& destination : destinations) {
-                        if (!destination.hasAssignment(assignment)) {
-                            canBeLifted = false;
-                            break;
+                    bool canBeLifted = assignment.getLevel() <= maxLevel;
+                    if (canBeLifted) {
+                        for (auto const& destination : destinations) {
+                            if (!destination.hasAssignment(assignment)) {
+                                canBeLifted = false;
+                                break;
+                            }
                         }
                     }
                     
@@ -143,18 +164,25 @@ namespace storm {
             return false;
         }
         
-        bool TemplateEdge::usesAssignmentLevels() const {
-            if (assignments.hasMultipleLevels()) {
+        bool TemplateEdge::usesAssignmentLevels(bool onlyTransient) const {
+            if (assignments.hasMultipleLevels(onlyTransient)) {
                 return true;
             }
             for (auto const& destination : this->getDestinations()) {
-                if (destination.usesAssignmentLevels()) {
+                if (destination.usesAssignmentLevels(onlyTransient)) {
                     return true;
                 }
             }
             return false;
         }
-
+        
+        uint64_t const& TemplateEdge::getLowestAssignmentLevel() const {
+            return lowestAssignmentLevel;
+        }
+        
+        uint64_t const& TemplateEdge::getHighestAssignmentLevel() const {
+            return highestAssignmentLevel;
+        }
 
         bool TemplateEdge::hasEdgeDestinationAssignments() const {
             for (auto const& destination : destinations) {
diff --git a/src/storm/storage/jani/TemplateEdge.h b/src/storm/storage/jani/TemplateEdge.h
index dac58144b..4e0d2a027 100644
--- a/src/storm/storage/jani/TemplateEdge.h
+++ b/src/storm/storage/jani/TemplateEdge.h
@@ -32,9 +32,11 @@ namespace storm {
 
             std::size_t getNumberOfDestinations() const;
             std::vector<TemplateEdgeDestination> const& getDestinations() const;
+            std::vector<TemplateEdgeDestination>& getDestinations();
             TemplateEdgeDestination const& getDestination(uint64_t index) const;
             
             OrderedAssignments const& getAssignments() const;
+            OrderedAssignments& getAssignments();
             
             /*!
              * Adds a transient assignment to this edge.
@@ -66,7 +68,7 @@ namespace storm {
              * assignments are no longer contained in the destination. Note that this may modify the semantics of the
              * model if assignment levels are being used somewhere in the model.
              */
-            void liftTransientDestinationAssignments();
+            void liftTransientDestinationAssignments(uint64_t maxLevel = 0);
             
             /**
              * Shifts the assingments from the edges to the destinations.
@@ -86,8 +88,20 @@ namespace storm {
             /*!
              * Retrieves whether the edge uses an assignment level other than zero.
              */
-            bool usesAssignmentLevels() const;
+            bool usesAssignmentLevels(bool onlyTransient = false) const;
 
+            /*!
+             * Retrieves the lowest assignment level occurring in each assignment.
+             * If no assignment exists, this value is the highest possible integer
+             */
+            uint64_t const& getLowestAssignmentLevel() const;
+            
+            /*!
+             * Retrieves the highest assignment level occurring in each assignment
+             * If no assignment exists, this value is always zero
+             */
+            uint64_t const& getHighestAssignmentLevel() const;
+            
             /*!
              * Checks the template edge for linearity.
              */
@@ -110,6 +124,8 @@ namespace storm {
             /// The assignments made when taking this edge.
             OrderedAssignments assignments;
             
+            uint64_t lowestAssignmentLevel, highestAssignmentLevel;
+            
             /// A set of global variables that is written by at least one of the edge's destinations. This set is
             /// initialized by the call to <code>finalize</code>.
             boost::container::flat_set<storm::expressions::Variable> writtenGlobalVariables;
diff --git a/src/storm/storage/jani/TemplateEdgeDestination.cpp b/src/storm/storage/jani/TemplateEdgeDestination.cpp
index b30bbda92..df0225636 100644
--- a/src/storm/storage/jani/TemplateEdgeDestination.cpp
+++ b/src/storm/storage/jani/TemplateEdgeDestination.cpp
@@ -27,6 +27,10 @@ namespace storm {
             return assignments;
         }
         
+        OrderedAssignments& TemplateEdgeDestination::getOrderedAssignments() {
+            return assignments;
+        }
+        
         bool TemplateEdgeDestination::removeAssignment(Assignment const& assignment) {
             return assignments.remove(assignment);
         }
@@ -43,8 +47,8 @@ namespace storm {
             return assignments.hasTransientAssignment();
         }
         
-        bool TemplateEdgeDestination::usesAssignmentLevels() const {
-            return assignments.hasMultipleLevels();
+        bool TemplateEdgeDestination::usesAssignmentLevels(bool onlyTransient) const {
+            return assignments.hasMultipleLevels(onlyTransient);
         }
         
         bool TemplateEdgeDestination::isLinear() const {
diff --git a/src/storm/storage/jani/TemplateEdgeDestination.h b/src/storm/storage/jani/TemplateEdgeDestination.h
index e6ad889b8..39e91fbd7 100644
--- a/src/storm/storage/jani/TemplateEdgeDestination.h
+++ b/src/storm/storage/jani/TemplateEdgeDestination.h
@@ -23,6 +23,7 @@ namespace storm {
             void changeAssignmentVariables(std::map<Variable const*, std::reference_wrapper<Variable const>> const& remapping);
 
             OrderedAssignments const& getOrderedAssignments() const;
+            OrderedAssignments& getOrderedAssignments();
             
             // Convenience methods to access the assignments.
             bool hasAssignment(Assignment const& assignment) const;
@@ -37,7 +38,7 @@ namespace storm {
             /*!
              * Retrieves whether the edge uses an assignment level other than zero.
              */
-            bool usesAssignmentLevels() const;
+            bool usesAssignmentLevels(bool onlyTransient = false) const;
 
             /*!
              * Checks whether the templ. edge destination contains one or more assignments
diff --git a/src/storm/storage/jani/VariableSet.cpp b/src/storm/storage/jani/VariableSet.cpp
index 973630a2c..ee8a798e2 100644
--- a/src/storm/storage/jani/VariableSet.cpp
+++ b/src/storm/storage/jani/VariableSet.cpp
@@ -132,6 +132,33 @@ namespace storm {
             return *newVariable;
         }
         
+        std::vector<std::shared_ptr<ArrayVariable>> VariableSet::dropAllArrayVariables() {
+            if (!arrayVariables.empty()) {
+                for (auto const& arrVar : arrayVariables) {
+                    nameToVariable.erase(arrVar->getName());
+                    variableToVariable.erase(arrVar->getExpressionVariable());
+                }
+                std::vector<std::shared_ptr<Variable>> newVariables;
+                for (auto const& v : variables) {
+                    if (!v->isArrayVariable()) {
+                        newVariables.push_back(v);
+                    }
+                }
+                variables = std::move(newVariables);
+                newVariables.clear();
+                for (auto const& v : transientVariables) {
+                    if (!v->isArrayVariable()) {
+                        newVariables.push_back(v);
+                    }
+                }
+                transientVariables = std::move(newVariables);
+            }
+            
+            std::vector<std::shared_ptr<ArrayVariable>> result = std::move(arrayVariables);
+            arrayVariables.clear();
+            return result;
+        }
+        
         bool VariableSet::hasVariable(std::string const& name) const {
             return nameToVariable.find(name) != nameToVariable.end();
         }
diff --git a/src/storm/storage/jani/VariableSet.h b/src/storm/storage/jani/VariableSet.h
index 9940d37a2..227535e6f 100644
--- a/src/storm/storage/jani/VariableSet.h
+++ b/src/storm/storage/jani/VariableSet.h
@@ -109,6 +109,11 @@ namespace storm {
              */
             ArrayVariable const& addVariable(ArrayVariable const& variable);
 
+            /*!
+             * Removes all array variables in this set
+             */
+            std::vector<std::shared_ptr<ArrayVariable>> dropAllArrayVariables();
+            
             /*!
              * Retrieves whether this variable set contains a variable with the given name.
              */
diff --git a/src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.cpp b/src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.cpp
index a75a7cfed..cfd421c59 100644
--- a/src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.cpp
+++ b/src/storm/storage/jani/expressions/JaniExpressionSubstitutionVisitor.cpp
@@ -6,15 +6,22 @@ namespace storm {
     
     namespace jani {
         storm::expressions::Expression substituteJaniExpression(storm::expressions::Expression const& expression, std::map<storm::expressions::Variable, storm::expressions::Expression> const& identifierToExpressionMap) {
-            return JaniExpressionSubstitutionVisitor<std::map<storm::expressions::Variable, storm::expressions::Expression>>(identifierToExpressionMap).substitute(expression);
+            return storm::expressions::JaniExpressionSubstitutionVisitor<std::map<storm::expressions::Variable, storm::expressions::Expression>>(identifierToExpressionMap).substitute(expression);
         }
         
         storm::expressions::Expression substituteJaniExpression(storm::expressions::Expression const& expression, std::unordered_map<storm::expressions::Variable, storm::expressions::Expression> const& identifierToExpressionMap) {
-            return JaniExpressionSubstitutionVisitor<std::unordered_map<storm::expressions::Variable, storm::expressions::Expression>>(identifierToExpressionMap).substitute(expression);
+            return storm::expressions::JaniExpressionSubstitutionVisitor<std::unordered_map<storm::expressions::Variable, storm::expressions::Expression>>(identifierToExpressionMap).substitute(expression);
         }
     }
     
+
     namespace expressions {
+        
+        template<typename MapType>
+        JaniExpressionSubstitutionVisitor<MapType>::JaniExpressionSubstitutionVisitor(MapType const& variableToExpressionMapping) : SubstitutionVisitor<MapType>(variableToExpressionMapping) {
+            // Intentionally left empty.
+        }
+        
         template<typename MapType>
         boost::any JaniExpressionSubstitutionVisitor<MapType>::visit(ValueArrayExpression const& expression, boost::any const& data) {
             uint64_t size = expression.size()->evaluateAsInt();