diff --git a/src/storm/generator/JaniNextStateGenerator.cpp b/src/storm/generator/JaniNextStateGenerator.cpp
index cf7a7b43e..6bba78c1a 100644
--- a/src/storm/generator/JaniNextStateGenerator.cpp
+++ b/src/storm/generator/JaniNextStateGenerator.cpp
@@ -14,6 +14,7 @@
 #include "storm/storage/jani/AutomatonComposition.h"
 #include "storm/storage/jani/ParallelComposition.h"
 #include "storm/storage/jani/CompositionInformationVisitor.h"
+#include "storm/storage/jani/traverser/AssignmentLevelFinder.h"
 
 #include "storm/storage/sparse/JaniChoiceOrigins.h"
 
@@ -26,6 +27,7 @@
 #include "storm/exceptions/InvalidSettingsException.h"
 #include "storm/exceptions/WrongFormatException.h"
 #include "storm/exceptions/InvalidArgumentException.h"
+#include "storm/exceptions/UnexpectedException.h"
 
 namespace storm {
     namespace generator {
@@ -38,12 +40,16 @@ namespace storm {
         template<typename ValueType, typename StateType>
         JaniNextStateGenerator<ValueType, StateType>::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool) : NextStateGenerator<ValueType, StateType>(model.getExpressionManager(), options), model(model), rewardVariables(), hasStateActionRewards(false) {
             STORM_LOG_THROW(!model.hasNonGlobalTransientVariable(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support automata-local transient variables.");
-            STORM_LOG_THROW(!model.usesAssignmentLevels(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support assignment levels.");
             STORM_LOG_THROW(!this->options.isBuildChoiceLabelsSet(), storm::exceptions::InvalidSettingsException, "JANI next-state generator cannot generate choice labels.");
 
-            // Lift the transient edge destinations. We can do so, as we know that there are no assignment levels (because that's not supported anyway).
+            if (this->model.containsArrayVariables()) {
+                arrayEliminatorData = this->model.eliminateArrays(true);
+            }
+            
+            // Lift the transient edge destinations of the first assignment level.
+            uint64_t lowestAssignmentLevel = storm::jani::AssignmentLevelFinder().getLowestAssignmentLevel(this->model);
             if (this->model.hasTransientEdgeDestinationAssignments()) {
-                this->model.liftTransientEdgeDestinationAssignments();
+                this->model.liftTransientEdgeDestinationAssignments(lowestAssignmentLevel);
             }
             STORM_LOG_THROW(!this->model.hasTransientEdgeDestinationAssignments(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support transient edge destination assignments.");
             
@@ -54,6 +60,34 @@ namespace storm {
             this->checkValid();
             this->variableInformation = VariableInformation(model, this->parallelAutomata, options.isAddOutOfBoundsStateSet());
             
+            // Find for each replaced array variable the corresponding references in the variable information
+            for (auto const& arrayReplacements : arrayEliminatorData.replacements) {
+                std::vector<uint64_t> varInfoIndices;
+                for (auto const& replacedVar : arrayReplacements.second) {
+                    if (replacedVar->getExpressionVariable().hasIntegerType()) {
+                        uint64_t index = 0;
+                        for (auto const& intInfo : this->variableInformation.integerVariables) {
+                            if (intInfo.variable == replacedVar->getExpressionVariable()) {
+                                varInfoIndices.push_back(index);
+                                break;
+                            }
+                            ++index;
+                        }
+                    } else if (replacedVar->getExpressionVariable().hasBooleanType()) {
+                        uint64_t index = 0;
+                        for (auto const& boolInfo : this->variableInformation.booleanVariables) {
+                            if (boolInfo.variable == replacedVar->getExpressionVariable()) {
+                                varInfoIndices.push_back(index);
+                            }
+                            ++index;
+                        }
+                    } else {
+                        STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unhandled type of base variable.");
+                    }
+                }
+                arrayVariableToElementInformations.emplace(arrayReplacements.first, std::move(varInfoIndices));
+            }
+            
             // Create a proper evalator.
             this->evaluator = std::make_unique<storm::expressions::ExpressionEvaluator<ValueType>>(model.getManager());
             
@@ -230,7 +264,7 @@ namespace storm {
         }
         
         template<typename ValueType, typename StateType>
-        CompressedState JaniNextStateGenerator<ValueType, StateType>::applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& destination, storm::generator::LocationVariableInformation const& locationVariable) {
+        CompressedState JaniNextStateGenerator<ValueType, StateType>::applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& destination, storm::generator::LocationVariableInformation const& locationVariable, uint64_t assignmentLevel, storm::expressions::ExpressionEvaluator<ValueType> const& expressionEvaluator) {
             CompressedState newState(state);
             
             // Update the location of the state.
@@ -240,22 +274,28 @@ namespace storm {
             auto assignmentIt = destination.getOrderedAssignments().getNonTransientAssignments().begin();
             auto assignmentIte = destination.getOrderedAssignments().getNonTransientAssignments().end();
             
+            if (assignmentLevel > 0) {
+                while (assignmentIt != assignmentIte && assignmentIt->getLevel() < assignmentLevel) {
+                    ++assignmentIt;
+                }
+            }
+            
             // Iterate over all boolean assignments and carry them out.
             auto boolIt = this->variableInformation.booleanVariables.begin();
-            for (; assignmentIt != assignmentIte && assignmentIt->getAssignedExpression().hasBooleanType(); ++assignmentIt) {
+            for (; assignmentIt != assignmentIte && assignmentIt->getAssignedExpression().hasBooleanType() && assignmentIt->getLevel() == assignmentLevel && assignmentIt->getLValue().isVariable(); ++assignmentIt) {
                 while (assignmentIt->getExpressionVariable() != boolIt->variable) {
                     ++boolIt;
                 }
-                newState.set(boolIt->bitOffset, this->evaluator->asBool(assignmentIt->getAssignedExpression()));
+                newState.set(boolIt->bitOffset, expressionEvaluator.asBool(assignmentIt->getAssignedExpression()));
             }
             
             // Iterate over all integer assignments and carry them out.
             auto integerIt = this->variableInformation.integerVariables.begin();
-            for (; assignmentIt != assignmentIte && assignmentIt->getAssignedExpression().hasIntegerType(); ++assignmentIt) {
+            for (; assignmentIt != assignmentIte && assignmentIt->getAssignedExpression().hasIntegerType() && assignmentIt->getLevel() == assignmentLevel && assignmentIt->getLValue().isVariable(); ++assignmentIt) {
                 while (assignmentIt->getExpressionVariable() != integerIt->variable) {
                     ++integerIt;
                 }
-                int_fast64_t assignedValue = this->evaluator->asInt(assignmentIt->getAssignedExpression());
+                int_fast64_t assignedValue = expressionEvaluator.asInt(assignmentIt->getAssignedExpression());
                 if (this->options.isAddOutOfBoundsStateSet()) {
                     if (assignedValue < integerIt->lowerBound || assignedValue > integerIt->upperBound) {
                         return this->outOfBoundsState;
@@ -268,10 +308,36 @@ namespace storm {
                 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 << ").");
             }
+            // Iterate over all array access assignments and carry them out.
+            for (; assignmentIt != assignmentIte && assignmentIt->getLValue().isArrayAccess() && assignmentIt->getLevel() == assignmentLevel; ++assignmentIt) {
+                int_fast64_t arrayIndex = expressionEvaluator.asInt(assignmentIt->getLValue().getArrayIndex());
+                if (assignmentIt->getAssignedExpression().hasIntegerType()) {
+                    std::vector<uint64_t> const& intInfoIndices = arrayVariableToElementInformations.at(assignmentIt->getLValue().getArray().getExpressionVariable());
+                    STORM_LOG_THROW(arrayIndex < intInfoIndices.size(), storm::exceptions::WrongFormatException, "Array access " << assignmentIt->getLValue() << " evaluates to array index " << arrayIndex << " which is out of bounds as the array size is " << intInfoIndices.size());
+                    IntegerVariableInformation const& intInfo = this->variableInformation.integerVariables[intInfoIndices[arrayIndex]];
+                    int_fast64_t assignedValue = expressionEvaluator.asInt(assignmentIt->getAssignedExpression());
+                    if (this->options.isAddOutOfBoundsStateSet()) {
+                        if (assignedValue < intInfo.lowerBound || assignedValue > intInfo.upperBound) {
+                            return this->outOfBoundsState;
+                        }
+                    } else if (this->options.isExplorationChecksSet()) {
+                        STORM_LOG_THROW(assignedValue >= intInfo.lowerBound, storm::exceptions::WrongFormatException, "The update " << assignmentIt->getExpressionVariable().getName() << " := " << assignmentIt->getAssignedExpression() << " leads to an out-of-bounds value (" << assignedValue << ") for the variable '" << assignmentIt->getExpressionVariable().getName() << "'.");
+                        STORM_LOG_THROW(assignedValue <= intInfo.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(intInfo.bitOffset, intInfo.bitWidth, assignedValue - intInfo.lowerBound);
+                    STORM_LOG_ASSERT(static_cast<int_fast64_t>(newState.getAsInt(intInfo.bitOffset, intInfo.bitWidth)) + intInfo.lowerBound == assignedValue, "Writing to the bit vector bucket failed (read " << newState.getAsInt(intInfo.bitOffset, intInfo.bitWidth) << " but wrote " << assignedValue << ").");
+                } else if (assignmentIt->getAssignedExpression().hasBooleanType()) {
+                    std::vector<uint64_t> const& boolInfoIndices = arrayVariableToElementInformations.at(assignmentIt->getLValue().getArray().getExpressionVariable());
+                    STORM_LOG_THROW(arrayIndex < boolInfoIndices.size(), storm::exceptions::WrongFormatException, "Array access " << assignmentIt->getLValue() << " evaluates to array index " << arrayIndex << " which is out of bounds as the array size is " << boolInfoIndices.size());
+                    BooleanVariableInformation const& boolInfo = this->variableInformation.booleanVariables[boolInfoIndices[arrayIndex]];
+                    newState.set(boolInfo.bitOffset, expressionEvaluator.asBool(assignmentIt->getAssignedExpression()));
+                } else {
+                    STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "Unhandled type of base variable.");
+                }
+            }
             
             // Check that we processed all assignments.
-            STORM_LOG_ASSERT(assignmentIt == assignmentIte, "Not all assignments were consumed.");
-            
+            STORM_LOG_ASSERT(assignmentIt == assignmentIte || assignmentIt->getLevel() > assignmentLevel, "Not all assignments were consumed.");
             return newState;
         }
         
@@ -389,9 +455,16 @@ namespace storm {
                 if (probability != storm::utility::zero<ValueType>()) {
                     // Obtain target state index and add it to the list of known states. If it has not yet been
                     // seen, we also add it to the set of states that have yet to be explored.
-                    auto newState = applyUpdate(state, destination, this->variableInformation.locationVariables[automatonIndex]);
-                    
-                    StateType stateIndex = stateToIdCallback(applyUpdate(state, destination, this->variableInformation.locationVariables[automatonIndex]));
+                    uint64_t assignmentLevel = edge.getLowestAssignmentLevel(); // Might be the largest possible integer, if there is no assignment
+                    uint64_t const& highestLevel = edge.getHighestAssignmentLevel();
+                    CompressedState newState = applyUpdate(state, destination, this->variableInformation.locationVariables[automatonIndex], assignmentLevel, *this->evaluator);
+                    while (assignmentLevel < highestLevel) {
+                        ++assignmentLevel;
+                        auto nextLevelEvaluator = storm::expressions::ExpressionEvaluator<ValueType>(model.getManager());
+                        unpackStateIntoEvaluator(newState, this->variableInformation, nextLevelEvaluator);
+                        newState = applyUpdate(newState, destination, this->variableInformation.locationVariables[automatonIndex], assignmentLevel, nextLevelEvaluator);
+                    }
+                    StateType stateIndex = stateToIdCallback(newState);
                     
                     // Update the choice by adding the probability/target state to it.
                     probability = exitRate ? exitRate.get() * probability : probability;
@@ -441,42 +514,107 @@ namespace storm {
                 currentDistribution.add(state, storm::utility::one<ValueType>());
                 
                 EdgeIndexSet edgeIndices;
+                uint64_t assignmentLevel = std::numeric_limits<uint64_t>::max();
+                uint64_t highestLevel = 0;
                 for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) {
-                    auto const& indexAndEdge = *iteratorList[i];
-                    
                     if (this->getOptions().isBuildChoiceOriginsSet()) {
-                        edgeIndices.insert(model.encodeAutomatonAndEdgeIndices(edgeCombination[i].first, indexAndEdge.first));
+                        edgeIndices.insert(model.encodeAutomatonAndEdgeIndices(edgeCombination[i].first, iteratorList[i]->first));
                     }
-                    
-                    storm::jani::Edge const& edge = *indexAndEdge.second;
-                    
-                    for (auto const& destination : edge.getDestinations()) {
-                        for (auto const& stateProbability : currentDistribution) {
-                            // Compute the new state under the current update and add it to the set of new target states.
-                            CompressedState newTargetState = applyUpdate(stateProbability.getState(), destination, this->variableInformation.locationVariables[edgeCombination[i].first]);
-                            
-                            // If the new state was already found as a successor state, update the probability
-                            // and otherwise insert it.
-                            ValueType probability = stateProbability.getValue() * this->evaluator->asRational(destination.getProbability());
+                    assignmentLevel = std::min(assignmentLevel, iteratorList[i]->second->getLowestAssignmentLevel());
+                    highestLevel = std::max(highestLevel, iteratorList[i]->second->getHighestAssignmentLevel());
+                }
+                
+                if (assignmentLevel >= highestLevel) {
+                    // When all assignments have the same level, we can perform the assignments of the different automata sequentially
+                    for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) {
+                        auto const& indexAndEdge = *iteratorList[i];
+                        storm::jani::Edge const& edge = *indexAndEdge.second;
+                        
+                        for (auto const& destination : edge.getDestinations()) {
+                            for (auto const& stateProbability : currentDistribution) {
+                                // Compute the new state under the current update and add it to the set of new target states.
+                                CompressedState newTargetState = applyUpdate(stateProbability.getState(), destination, this->variableInformation.locationVariables[edgeCombination[i].first], assignmentLevel, *this->evaluator);
+                                
+                                // If the new state was already found as a successor state, update the probability
+                                // and otherwise insert it.
+                                ValueType probability = stateProbability.getValue() * this->evaluator->asRational(destination.getProbability());
+                                if (edge.hasRate()) {
+                                    probability *= this->evaluator->asRational(edge.getRate());
+                                }
+                                if (probability != storm::utility::zero<ValueType>()) {
+                                    nextDistribution.add(newTargetState, probability);
+                                }
+                            }
+                        }
+                        
+                        // Create the state-action reward for the newly created choice.
+                        auto valueIt = stateActionRewards.begin();
+                        performTransientAssignments(edge.getAssignments().getTransientAssignments(), [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } );
+                        
+                        nextDistribution.compress();
+                        
+                        // If there is one more command to come, shift the target states one time step back.
+                        if (i < iteratorList.size() - 1) {
+                            currentDistribution = std::move(nextDistribution);
+                        }
+                    }
+                } else {
+                    // If there are different assignment levels, we need to expand the possible destinations which causes an exponential blowup...
+                    uint64_t destinationId = 0;
+                    bool lastDestinationId = false;
+                    do {
+                        
+                        // First assignment level
+                        std::vector<storm::jani::EdgeDestination const*> destinations;
+                        std::vector<LocationVariableInformation const*> locationVars;
+                        destinations.reserve(iteratorList.size());
+                        locationVars.reserve(iteratorList.size());
+                        CompressedState successorState = state;
+                        ValueType successorProbability = storm::utility::one<ValueType>();
+
+                        uint64_t destinationIndex = destinationId;
+                        for (uint_fast64_t i = 0; i < iteratorList.size(); ++i) {
+                            storm::jani::Edge const& edge = *iteratorList[i]->second;
+                            destinations.push_back(&edge.getDestination(destinationIndex % edge.getNumberOfDestinations()));
+                            locationVars.push_back(&this->variableInformation.locationVariables[edgeCombination[i].first]);
+                            std::cout << destinationIndex % edge.getNumberOfDestinations();
+                            if (i == iteratorList.size() - 1 && (destinationIndex % edge.getNumberOfDestinations()) == edge.getNumberOfDestinations() - 1) {
+                                lastDestinationId = true;
+                            }
+                            destinationIndex /= edge.getNumberOfDestinations();
+                            ValueType probability = this->evaluator->asRational(destinations.back()->getProbability());
                             if (edge.hasRate()) {
-                                probability *= this->evaluator->asRational(edge.getRate());
+                                successorProbability *= probability * this->evaluator->asRational(edge.getRate());
+                            } else {
+                                successorProbability *= probability;
                             }
-                            if (probability != storm::utility::zero<ValueType>()) {
-                                nextDistribution.add(newTargetState, probability);
+                            if (storm::utility::isZero(successorProbability)) {
+                                break;
                             }
+                            // Create the state-action reward for the newly created choice.
+                            auto valueIt = stateActionRewards.begin();
+                            performTransientAssignments(edge.getAssignments().getTransientAssignments(), [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } );
+                            successorState = applyUpdate(successorState, *destinations.back(), *locationVars.back(), assignmentLevel, *this->evaluator);
                         }
-                    }
-                    
-                    // Create the state-action reward for the newly created choice.
-                    auto valueIt = stateActionRewards.begin();
-                    performTransientAssignments(edge.getAssignments().getTransientAssignments(), [&valueIt] (ValueType const& value) { *valueIt += value; ++valueIt; } );
-                    
-                    nextDistribution.compress();
-                    
-                    // If there is one more command to come, shift the target states one time step back.
-                    if (i < iteratorList.size() - 1) {
-                        currentDistribution = std::move(nextDistribution);
-                    }
+                        
+                        if (!storm::utility::isZero(successorProbability)) {
+                            // remaining assignment levels
+                            while (assignmentLevel < highestLevel) {
+                                ++assignmentLevel;
+                                auto currentLevelEvaluator = storm::expressions::ExpressionEvaluator<ValueType>(model.getManager());
+                                unpackStateIntoEvaluator(successorState, this->variableInformation, currentLevelEvaluator);
+                                auto locationVarIt = locationVars.begin();
+                                for (auto const& destPtr : destinations) {
+                                    successorState = applyUpdate(successorState, *destPtr, **locationVarIt, assignmentLevel, currentLevelEvaluator);
+                                    ++locationVarIt;
+                                }
+                            }
+                            nextDistribution.add(successorState, successorProbability);
+                        }
+                        
+                        ++destinationId;
+                    } while (!lastDestinationId);
+                    std::cout << std::endl;
                 }
                 
                 // At this point, we applied all commands of the current command combination and newTargetStates
@@ -664,6 +802,7 @@ namespace storm {
             auto rewardVariableIt = rewardVariables.begin();
             auto rewardVariableIte = rewardVariables.end();
             for (auto const& assignment : transientAssignments) {
+                STORM_LOG_ASSERT(assignment.getLValue().isVariable(), "Transient assignments to non-variable LValues are not supported.");
                 while (rewardVariableIt != rewardVariableIte && *rewardVariableIt < assignment.getExpressionVariable()) {
                     callback(storm::utility::zero<ValueType>());
                     ++rewardVariableIt;
diff --git a/src/storm/generator/JaniNextStateGenerator.h b/src/storm/generator/JaniNextStateGenerator.h
index bd6b0c922..c80452f8c 100644
--- a/src/storm/generator/JaniNextStateGenerator.h
+++ b/src/storm/generator/JaniNextStateGenerator.h
@@ -5,6 +5,7 @@
 #include "storm/generator/NextStateGenerator.h"
 
 #include "storm/storage/jani/Model.h"
+#include "storm/storage/jani/ArrayEliminator.h"
 #include "storm/storage/jani/OrderedAssignments.h"
 
 namespace storm {
@@ -66,9 +67,10 @@ namespace storm {
              * @params state The state to which to apply the new values.
              * @params update The update to apply.
              * @params locationVariable The location variable that is being updated.
+             * @params assignmentLevel The assignmentLevel that is to be considered for the update.
              * @return The resulting state.
              */
-            CompressedState applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& update, storm::generator::LocationVariableInformation const& locationVariable);
+            CompressedState applyUpdate(CompressedState const& state, storm::jani::EdgeDestination const& update, storm::generator::LocationVariableInformation const& locationVariable, uint64_t assignmentlevel, storm::expressions::ExpressionEvaluator<ValueType> const& expressionEvaluator);
             
             /*!
              * Retrieves all choices possible from the given state.
@@ -137,6 +139,13 @@ namespace storm {
             
             /// A flag that stores whether at least one of the selected reward models has state-action rewards.
             bool hasStateActionRewards;
+            
+            /// Data from eliminating arrays
+            storm::jani::ArrayEliminatorData arrayEliminatorData;
+            
+            /// Maps each array variable to the index of the base variable in this->variableInformation
+            std::unordered_map<storm::expressions::Variable, std::vector<uint64_t>> arrayVariableToElementInformations;
+
         };
         
     }
diff --git a/src/storm/storage/jani/traverser/ArrayEliminator.cpp b/src/storm/storage/jani/ArrayEliminator.cpp
similarity index 52%
rename from src/storm/storage/jani/traverser/ArrayEliminator.cpp
rename to src/storm/storage/jani/ArrayEliminator.cpp
index 15da40a42..fb50de59f 100644
--- a/src/storm/storage/jani/traverser/ArrayEliminator.cpp
+++ b/src/storm/storage/jani/ArrayEliminator.cpp
@@ -1,4 +1,4 @@
-#include "storm/storage/jani/traverser/ArrayEliminator.h"
+#include "storm/storage/jani/ArrayEliminator.h"
 
 #include <unordered_map>
 
@@ -10,6 +10,7 @@
 #include "storm/storage/expressions/ExpressionManager.h"
 
 #include "storm/exceptions/NotSupportedException.h"
+#include "storm/exceptions/UnexpectedException.h"
 
 namespace storm {
     namespace jani {
@@ -105,11 +106,188 @@ namespace storm {
                 }
                 
                 virtual boost::any visit(storm::expressions::ArrayAccessExpression const& expression, boost::any const& data) override {
-                    STORM_LOG_WARN("Array access expression on rhs of array assignment. This is not expected since nested arrays are currently not supported.");
+                    STORM_LOG_WARN("Found Array access expression within an array expression. This is not expected since nested arrays are currently not supported.");
                     return 0;
                 }
             };
             
+            class ArrayExpressionEliminationVisitor : public storm::expressions::ExpressionVisitor, public storm::expressions::JaniExpressionVisitor {
+            public:
+                typedef std::shared_ptr<storm::expressions::BaseExpression const> BaseExprPtr;
+                
+                ArrayExpressionEliminationVisitor(std::unordered_map<storm::expressions::Variable, std::vector<storm::jani::Variable const*>> const& replacements, std::unordered_map<storm::expressions::Variable, std::size_t> const& sizes) : replacements(replacements), arraySizes(sizes) {}
+                virtual ~ArrayExpressionEliminationVisitor() = default;
+    
+                storm::expressions::Expression eliminate(storm::expressions::Expression const& expression, storm::expressions::Expression const& outOfBoundsExpression)  {
+                    auto res = eliminate(expression, false);
+                    if (outOfBoundsError) {
+                        return outOfBoundsExpression;
+                    } else {
+                        return res;
+                    }
+                }
+                
+                storm::expressions::Expression eliminate(storm::expressions::Expression const& expression, bool failIfOutOfBounds = true) {
+                    outOfBoundsError = false;
+                    // here, data is the accessed index of the most recent array access expression. Initially, there is none.
+                    auto res = storm::expressions::Expression(boost::any_cast<BaseExprPtr>(expression.accept(*this, boost::any())));
+                    STORM_LOG_THROW(!failIfOutOfBounds || !outOfBoundsError, storm::exceptions::UnexpectedException, "Out of bounds array access occured while eliminating expression " << expression);
+                    return res.simplify();
+                }
+                
+                virtual boost::any visit(storm::expressions::IfThenElseExpression const& expression, boost::any const& data) override {
+                    // for the condition expression, outer array accesses should not matter.
+                    BaseExprPtr conditionExpression = boost::any_cast<BaseExprPtr>(expression.getCondition()->accept(*this, boost::any()));
+                    BaseExprPtr thenExpression = boost::any_cast<BaseExprPtr>(expression.getThenExpression()->accept(*this, data));
+                    BaseExprPtr elseExpression = boost::any_cast<BaseExprPtr>(expression.getElseExpression()->accept(*this, data));
+        
+                    // If the arguments did not change, we simply push the expression itself.
+                    if (conditionExpression.get() == expression.getCondition().get() && thenExpression.get() == expression.getThenExpression().get() && elseExpression.get() == expression.getElseExpression().get()) {
+                        return expression.getSharedPointer();
+                    } else {
+                        return std::const_pointer_cast<storm::expressions::BaseExpression const>(std::shared_ptr<storm::expressions::BaseExpression>(new storm::expressions::IfThenElseExpression(expression.getManager(), thenExpression->getType(), conditionExpression, thenExpression, elseExpression)));
+                    }
+                }
+        
+                virtual boost::any visit(storm::expressions::BinaryBooleanFunctionExpression const& expression, boost::any const& data) override {
+                    STORM_LOG_ASSERT(data.empty(), "BinaryBooleanFunctionExpressions should not be direct subexpressions of array access expressions. However, the expression " << expression << " is.");
+                    BaseExprPtr firstExpression = boost::any_cast<BaseExprPtr>(expression.getFirstOperand()->accept(*this, data));
+                    BaseExprPtr secondExpression = boost::any_cast<BaseExprPtr>(expression.getSecondOperand()->accept(*this, data));
+        
+                    // If the arguments did not change, we simply push the expression itself.
+                    if (firstExpression.get() == expression.getFirstOperand().get() && secondExpression.get() == expression.getSecondOperand().get()) {
+                        return expression.getSharedPointer();
+                    } else {
+                        return std::const_pointer_cast<storm::expressions::BaseExpression const>(std::shared_ptr<storm::expressions::BaseExpression>(new storm::expressions::BinaryBooleanFunctionExpression(expression.getManager(), expression.getType(), firstExpression, secondExpression, expression.getOperatorType())));
+                    }
+                }
+        
+                virtual boost::any visit(storm::expressions::BinaryNumericalFunctionExpression const& expression, boost::any const& data) override {
+                    STORM_LOG_ASSERT(data.empty(), "BinaryNumericalFunctionExpression should not be direct subexpressions of array access expressions. However, the expression " << expression << " is.");
+                    BaseExprPtr firstExpression = boost::any_cast<BaseExprPtr>(expression.getFirstOperand()->accept(*this, data));
+                    BaseExprPtr secondExpression = boost::any_cast<BaseExprPtr>(expression.getSecondOperand()->accept(*this, data));
+                    
+                    // If the arguments did not change, we simply push the expression itself.
+                    if (firstExpression.get() == expression.getFirstOperand().get() && secondExpression.get() == expression.getSecondOperand().get()) {
+                        return expression.getSharedPointer();
+                    } else {
+                        return std::const_pointer_cast<storm::expressions::BaseExpression const>(std::shared_ptr<storm::expressions::BaseExpression>(new storm::expressions::BinaryNumericalFunctionExpression(expression.getManager(), expression.getType(), firstExpression, secondExpression, expression.getOperatorType())));
+                    }
+                }
+        
+                virtual boost::any visit(storm::expressions::BinaryRelationExpression const& expression, boost::any const& data) override {
+                    STORM_LOG_ASSERT(data.empty(), "BinaryRelationExpression should not be direct subexpressions of array access expressions. However, the expression " << expression << " is.");
+                    BaseExprPtr firstExpression = boost::any_cast<BaseExprPtr>(expression.getFirstOperand()->accept(*this, data));
+                    BaseExprPtr secondExpression = boost::any_cast<BaseExprPtr>(expression.getSecondOperand()->accept(*this, data));
+                    
+                    // If the arguments did not change, we simply push the expression itself.
+                    if (firstExpression.get() == expression.getFirstOperand().get() && secondExpression.get() == expression.getSecondOperand().get()) {
+                        return expression.getSharedPointer();
+                    } else {
+                        return std::const_pointer_cast<storm::expressions::BaseExpression const>(std::shared_ptr<storm::expressions::BaseExpression>(new storm::expressions::BinaryRelationExpression(expression.getManager(), expression.getType(), firstExpression, secondExpression, expression.getRelationType())));
+                    }
+                }
+                
+                virtual boost::any visit(storm::expressions::VariableExpression const& expression, boost::any const& data) override {
+                    if (expression.getType().isArrayType()) {
+                        STORM_LOG_THROW(!data.empty(), storm::exceptions::NotSupportedException, "Unable to translate array variable to basic variable, since it does not seem to be within an array access expression.");
+                        uint64_t index = boost::any_cast<uint64_t>(data);
+                        STORM_LOG_ASSERT(replacements.find(expression.getVariable()) != replacements.end(), "Unable to find array variable " << expression << " in array replacements.");
+                        auto const& arrayVarReplacements = replacements.at(expression.getVariable());
+                        STORM_LOG_ASSERT(index < arrayVarReplacements.size(), "No replacement for array variable, since index " << index << " is out of bounds.");
+                        return arrayVarReplacements[index]->getExpressionVariable().getExpression().getBaseExpressionPointer();
+                    } else {
+                        return expression.getSharedPointer();
+                    }
+                }
+        
+                virtual boost::any visit(storm::expressions::UnaryBooleanFunctionExpression const& expression, boost::any const& data) override {
+                    STORM_LOG_ASSERT(data.empty(), "UnaryBooleanFunctionExpression should not be direct subexpressions of array access expressions. However, the expression " << expression << " is.");
+                    BaseExprPtr operandExpression = boost::any_cast<BaseExprPtr>(expression.getOperand()->accept(*this, data));
+                    
+                    // If the argument did not change, we simply push the expression itself.
+                    if (operandExpression.get() == expression.getOperand().get()) {
+                        return expression.getSharedPointer();
+                    } else {
+                        return std::const_pointer_cast<storm::expressions::BaseExpression const>(std::shared_ptr<storm::expressions::BaseExpression>(new storm::expressions::UnaryBooleanFunctionExpression(expression.getManager(), expression.getType(), operandExpression, expression.getOperatorType())));
+                    }
+                }
+        
+                virtual boost::any visit(storm::expressions::UnaryNumericalFunctionExpression const& expression, boost::any const& data) override {
+                    STORM_LOG_ASSERT(data.empty(), "UnaryBooleanFunctionExpression should not be direct subexpressions of array access expressions. However, the expression " << expression << " is.");
+        
+                    BaseExprPtr operandExpression = boost::any_cast<BaseExprPtr>(expression.getOperand()->accept(*this, data));
+                    
+                    // If the argument did not change, we simply push the expression itself.
+                    if (operandExpression.get() == expression.getOperand().get()) {
+                        return expression.getSharedPointer();
+                    } else {
+                        return std::const_pointer_cast<storm::expressions::BaseExpression const>(std::shared_ptr<storm::expressions::BaseExpression>(new storm::expressions::UnaryNumericalFunctionExpression(expression.getManager(), expression.getType(), operandExpression, expression.getOperatorType())));
+                    }
+                }
+                
+                virtual boost::any visit(storm::expressions::BooleanLiteralExpression const& expression, boost::any const&) override {
+                    return expression.getSharedPointer();
+                }
+                
+                virtual boost::any visit(storm::expressions::IntegerLiteralExpression const& expression, boost::any const&) override {
+                    return expression.getSharedPointer();
+                }
+                
+                virtual boost::any visit(storm::expressions::RationalLiteralExpression const& expression, boost::any const&) override {
+                    return expression.getSharedPointer();
+                }
+                
+                virtual boost::any visit(storm::expressions::ValueArrayExpression const& expression, boost::any const& data) override {
+                    STORM_LOG_THROW(!data.empty(), storm::exceptions::NotSupportedException, "Unable to translate ValueArrayExpression to element expression since it does not seem to be within an array access expression.");
+                    uint64_t index = boost::any_cast<uint64_t>(data);
+                    STORM_LOG_ASSERT(expression.size()->isIntegerLiteralExpression(), "unexpected kind of size expression of ValueArrayExpression (" << expression.size()->toExpression() << ").");
+                    if (index < static_cast<uint64_t>(expression.size()->evaluateAsInt())) {
+                        return expression.at(index);
+                    } else {
+                        outOfBoundsError = true;
+                        return expression.at(0);
+                    }
+                }
+                
+                virtual boost::any visit(storm::expressions::ConstructorArrayExpression const& expression, boost::any const& data) override {
+                    STORM_LOG_THROW(!data.empty(), storm::exceptions::NotSupportedException, "Unable to translate ValueArrayExpression to element expression since it does not seem to be within an array access expression.");
+                    uint64_t index = boost::any_cast<uint64_t>(data);
+                    if (expression.size()->containsVariables()) {
+                        STORM_LOG_WARN("Ignoring length of constructorArrayExpression " << expression << " as it still contains variables.");
+                    } else if (index >= static_cast<uint64_t>(expression.size()->evaluateAsInt())) {
+                        outOfBoundsError = true;
+                    }
+                    return expression.at(index);
+                }
+                
+                virtual boost::any visit(storm::expressions::ArrayAccessExpression const& expression, boost::any const& data) override {
+                    if (expression.getSecondOperand()->containsVariables()) {
+                        //get the size of the array expression
+                        uint64_t size = MaxArraySizeExpressionVisitor().getMaxSize(expression.getFirstOperand()->toExpression(), arraySizes);
+                        STORM_LOG_THROW(size > 0, storm::exceptions::NotSupportedException, "Unable to get size of array expression for array access " << expression << ".");
+                        uint64_t index = size - 1;
+                        storm::expressions::Expression result = boost::any_cast<BaseExprPtr>(expression.getFirstOperand()->accept(*this, index))->toExpression();
+                        while (index > 0) {
+                            --index;
+                            result = storm::expressions::ite(
+                                    expression.getSecondOperand()->toExpression() == expression.getManager().integer(index),
+                                    boost::any_cast<BaseExprPtr>(expression.getFirstOperand()->accept(*this, index))->toExpression(),
+                                    result);
+                        }
+                        return result.getBaseExpressionPointer();
+                    } else {
+                        uint64_t index = expression.getSecondOperand()->evaluateAsInt();
+                        return boost::any_cast<BaseExprPtr>(expression.getFirstOperand()->accept(*this, index));
+                    }
+                }
+                
+            private:
+                std::unordered_map<storm::expressions::Variable, std::vector<storm::jani::Variable const*>> const& replacements;
+                std::unordered_map<storm::expressions::Variable, std::size_t> const& arraySizes;
+                bool outOfBoundsError;
+            };
+            
             class MaxArraySizeDeterminer : public ConstJaniTraverser {
             public:
                 
@@ -127,7 +305,7 @@ namespace storm {
                     return result;
                 }
                 
-                virtual void traverse(Assignment const& assignment, boost::any const& data) const override {
+                virtual void traverse(Assignment const& assignment, boost::any const& data) override {
                     if (assignment.lValueIsVariable() && assignment.getExpressionVariable().getType().isArrayType()) {
                         auto& map = *boost::any_cast<MapPtr>(data);
                         std::size_t newSize = MaxArraySizeExpressionVisitor().getMaxSize(assignment.getAssignedExpression(), map);
@@ -138,7 +316,7 @@ namespace storm {
                     }
                 }
                 
-                virtual void traverse(ArrayVariable const& variable, boost::any const& data) const override {
+                virtual void traverse(ArrayVariable const& variable, boost::any const& data) override {
                     if (variable.hasInitExpression()) {
                         auto& map = *boost::any_cast<MapPtr>(data);
                         std::size_t newSize = MaxArraySizeExpressionVisitor().getMaxSize(variable.getInitExpression(), map);
@@ -156,19 +334,21 @@ namespace storm {
 
                 typedef ArrayEliminatorData ResultType;
                 
-                ArrayVariableReplacer(storm::expressions::ExpressionManager& expressionManager, bool keepNonTrivialArrayAccess) : expressionManager(expressionManager) , keepNonTrivialArrayAccess(keepNonTrivialArrayAccess) {}
+                ArrayVariableReplacer(storm::expressions::ExpressionManager& expressionManager, bool keepNonTrivialArrayAccess, std::unordered_map<storm::expressions::Variable, std::size_t> const& arrayVarToSizesMap) : expressionManager(expressionManager) , keepNonTrivialArrayAccess(keepNonTrivialArrayAccess), arraySizes(arrayVarToSizesMap) {}
                 
                 virtual ~ArrayVariableReplacer() = default;
-                ResultType replace(Model& model, std::unordered_map<storm::expressions::Variable, std::size_t> const& arrayVarToSizesMap) {
+                ResultType replace(Model& model) {
+
                     ResultType result;
-                    for (auto const& arraySize : arrayVarToSizesMap) {
+                    arrayExprEliminator = std::make_unique<ArrayExpressionEliminationVisitor>(result.replacements, arraySizes);
+                    for (auto const& arraySize : arraySizes) {
                         result.replacements.emplace(arraySize.first, std::vector<storm::jani::Variable const*>(arraySize.second, nullptr));
                     }
                     traverse(model, &result);
                     return result;
                 }
 
-                virtual void traverse(Model& model, boost::any const& data) const override {
+                virtual void traverse(Model& model, boost::any const& data) override {
                     
                     // Insert fresh basic variables for global array variables
                     auto& replacements = boost::any_cast<ResultType*>(data)->replacements;
@@ -183,20 +363,20 @@ namespace storm {
                     auto& eliminatedArrayVariables = boost::any_cast<ResultType*>(data)->eliminatedArrayVariables;
                     eliminatedArrayVariables.insert(eliminatedArrayVariables.end(), elVars.begin(), elVars.end());
                     
+                    // Make new variable replacements known to the expression eliminator
+                    arrayExprEliminator = std::make_unique<ArrayExpressionEliminationVisitor>(replacements, arraySizes);
+                    
                     for (auto& aut : model.getAutomata()) {
                         traverse(aut, data);
                     }
                     
-                    // traverse remaining components
-                    for (auto& c : model.getConstants()) {
-                        traverse(c, data);
-                    }
+                    // traversal of remaining components
                     if (model.hasInitialStatesRestriction()) {
-                        //model.setInitialStatesRestriction();
+                        model.setInitialStatesRestriction(arrayExprEliminator->eliminate(model.getInitialStatesRestriction()));
                     }
                 }
                 
-                virtual void traverse(Automaton& automaton, boost::any const& data) const override {
+                virtual void traverse(Automaton& automaton, boost::any const& data) override {
                     // No need to traverse the init restriction.
                     
                     // Insert fresh basic variables for local array variables
@@ -212,23 +392,23 @@ namespace storm {
                     auto& eliminatedArrayVariables = boost::any_cast<ResultType*>(data)->eliminatedArrayVariables;
                     eliminatedArrayVariables.insert(eliminatedArrayVariables.end(), elVars.begin(), elVars.end());
 
+                    // Make new variable replacements known to the expression eliminator
+                    arrayExprEliminator = std::make_unique<ArrayExpressionEliminationVisitor>(replacements, arraySizes);
+                    
                     for (auto& loc : automaton.getLocations()) {
                         JaniTraverser::traverse(loc, data);
                     }
                     JaniTraverser::traverse(automaton.getEdgeContainer(), data);
-                }
-                
-                void traverse(Constant& constant, boost::any const& data) const {
-                    if (constant.isDefined()) {
-                        // todo:
-                        //traverse(constant.getExpression(), data);
+                    
+                    if (automaton.hasInitialStatesRestriction()) {
+                        automaton.setInitialStatesRestriction(arrayExprEliminator->eliminate(automaton.getInitialStatesRestriction()));
                     }
                 }
-
-                virtual void traverse(OrderedAssignments& orderedAssignments, boost::any const& data) const override {
+                
+                virtual void traverse(OrderedAssignments& orderedAssignments, boost::any const& data) override {
                     auto const& replacements = boost::any_cast<ResultType*>(data)->replacements;
 
-                    // Replace array occurrences in LValues.
+                    // Replace array occurrences in LValues and assigned expressions.
                     std::vector<Assignment> newAssignments;
                     uint64_t level = 0;
                     std::unordered_map<storm::expressions::Variable, std::vector<Assignment const*>> collectedArrayAccessAssignments;
@@ -253,12 +433,14 @@ namespace storm {
                             STORM_LOG_ASSERT(assignment.getAssignedExpression().getType().isArrayType(), "Assigning a non-array expression to an array variable...");
                             std::vector<storm::jani::Variable const*> const& arrayVariableReplacements = replacements.at(assignment.getExpressionVariable());
                             for (uint64_t index = 0; index < arrayVariableReplacements.size(); ++index) {
-                                auto arrayAccessExpression = std::make_shared<storm::expressions::ArrayAccessExpression>(expressionManager, assignment.getAssignedExpression().getType().getElementType(), assignment.getAssignedExpression().getBaseExpressionPointer(), expressionManager.integer(index).getBaseExpressionPointer());
-                                newAssignments.emplace_back(LValue(*arrayVariableReplacements[index]), arrayAccessExpression->toExpression(), level);
+                                auto const& replacement = *arrayVariableReplacements[index];
+                                auto arrayAccessExpression = std::make_shared<storm::expressions::ArrayAccessExpression>(expressionManager, assignment.getAssignedExpression().getType().getElementType(), assignment.getAssignedExpression().getBaseExpressionPointer(), expressionManager.integer(index).getBaseExpressionPointer())->toExpression();
+                                arrayAccessExpression = arrayExprEliminator->eliminate(arrayAccessExpression, getOutOfBoundsValue(replacement));
+                                newAssignments.emplace_back(LValue(replacement), arrayAccessExpression, level);
                             }
                             continue;
                         }
-                        newAssignments.push_back(assignment);
+                        newAssignments.emplace_back(assignment.getLValue(), arrayExprEliminator->eliminate(assignment.getAssignedExpression()), assignment.getLevel());
                     }
                     for (auto const& arrayAssignments : collectedArrayAccessAssignments) {
                         insertLValueArrayAccessReplacements(arrayAssignments.second, replacements.at(arrayAssignments.first), level, newAssignments);
@@ -276,7 +458,7 @@ namespace storm {
                     std::string name = arrayVariable.getExpressionVariable().getName() + "_at_" + std::to_string(index);
                     storm::expressions::Expression initValue;
                     if (arrayVariable.hasInitExpression()) {
-                        initValue = std::make_shared<storm::expressions::ArrayAccessExpression>(expressionManager, arrayVariable.getExpressionVariable().getType().getElementType(), arrayVariable.getInitExpression().getBaseExpressionPointer(), expressionManager.integer(index).getBaseExpressionPointer())->toExpression();
+                        initValue = arrayExprEliminator->eliminate(std::make_shared<storm::expressions::ArrayAccessExpression>(expressionManager, arrayVariable.getExpressionVariable().getType().getElementType(), arrayVariable.getInitExpression().getBaseExpressionPointer(), expressionManager.integer(index).getBaseExpressionPointer())->toExpression());
                     }
                     if (arrayVariable.getElementType() == ArrayVariable::ElementType::Int) {
                         storm::expressions::Variable exprVariable = expressionManager.declareIntegerVariable(name);
@@ -324,31 +506,50 @@ namespace storm {
                     if (onlyConstantIndices) {
                         for (auto const& aa : arrayAccesses) {
                             LValue lvalue(*arrayVariableReplacements.at(aa->getLValue().getArrayIndex().evaluateAsInt()));
-                            newAssignments.emplace_back(lvalue, aa->getAssignedExpression(), level);
+                            newAssignments.emplace_back(lvalue, arrayExprEliminator->eliminate(aa->getAssignedExpression()), level);
                         }
                     } else {
                         for (uint64_t index = 0; index < arrayVariableReplacements.size(); ++index) {
                             storm::expressions::Expression assignedExpression = arrayVariableReplacements[index]->getExpressionVariable().getExpression();
                             auto indexExpression = expressionManager.integer(index);
                             for (auto const& aa : arrayAccesses) {
-                                assignedExpression = storm::expressions::ite(aa->getLValue().getArrayIndex() == indexExpression, aa->getAssignedExpression(), assignedExpression);
+                                assignedExpression = storm::expressions::ite(aa->getLValue().getArrayIndex() == indexExpression, arrayExprEliminator->eliminate(aa->getAssignedExpression()), assignedExpression);
                                 newAssignments.emplace_back(LValue(*arrayVariableReplacements[index]), assignedExpression, level);
                             }
                         }
                     }
                 }
                 
+                storm::expressions::Expression getOutOfBoundsValue(Variable const& var) const {
+                    if (var.hasInitExpression()) {
+                        return var.getInitExpression();
+                    }
+                    if (var.isBooleanVariable()) {
+                        return expressionManager.boolean(false);
+                    }
+                    if (var.isBoundedIntegerVariable()) {
+                        return var.asBoundedIntegerVariable().getLowerBound();
+                    }
+                    if (var.isUnboundedIntegerVariable()) {
+                        return expressionManager.integer(0);
+                    }
+                    if (var.isRealVariable()) {
+                        return expressionManager.rational(0.0);
+                    }
+                    STORM_LOG_THROW(false, storm::exceptions::UnexpectedException, "unhandled variabe type");
+                    return storm::expressions::Expression();
+                }
+                
+                std::unique_ptr<ArrayExpressionEliminationVisitor> arrayExprEliminator;
                 storm::expressions::ExpressionManager& expressionManager;
                 bool const keepNonTrivialArrayAccess;
+                std::unordered_map<storm::expressions::Variable, std::size_t> const& arraySizes;
             };
-            
-            
-        
         } // namespace detail
         
         ArrayEliminatorData ArrayEliminator::eliminate(Model& model, bool keepNonTrivialArrayAccess) {
             auto sizes = detail::MaxArraySizeDeterminer().getMaxSizes(model);
-            ArrayEliminatorData result = detail::ArrayVariableReplacer(model.getExpressionManager(), keepNonTrivialArrayAccess).replace(model, sizes);
+            ArrayEliminatorData result = detail::ArrayVariableReplacer(model.getExpressionManager(), keepNonTrivialArrayAccess, sizes).replace(model);
             
             model.finalize();
             return result;
diff --git a/src/storm/storage/jani/traverser/ArrayEliminator.h b/src/storm/storage/jani/ArrayEliminator.h
similarity index 100%
rename from src/storm/storage/jani/traverser/ArrayEliminator.h
rename to src/storm/storage/jani/ArrayEliminator.h
diff --git a/src/storm/storage/jani/Model.cpp b/src/storm/storage/jani/Model.cpp
index 502c821c0..6ff5cd28a 100644
--- a/src/storm/storage/jani/Model.cpp
+++ b/src/storm/storage/jani/Model.cpp
@@ -946,9 +946,13 @@ namespace storm {
             return false;
         }
         
-        void Model::eliminateArrays(bool keepNonTrivialArrayAccess) {
+        ArrayEliminatorData Model::eliminateArrays(bool keepNonTrivialArrayAccess) {
             ArrayEliminator arrayEliminator;
-            arrayEliminator.eliminate(*this, keepNonTrivialArrayAccess);
+            return arrayEliminator.eliminate(*this, keepNonTrivialArrayAccess);
+        }
+        
+        void Model::eliminateArrays() {
+            eliminateArrays(false);
         }
         
         void Model::setInitialStatesRestriction(storm::expressions::Expression const& initialStatesRestriction) {
diff --git a/src/storm/storage/jani/Model.h b/src/storm/storage/jani/Model.h
index 7ccc011a4..937f58f42 100644
--- a/src/storm/storage/jani/Model.h
+++ b/src/storm/storage/jani/Model.h
@@ -33,6 +33,7 @@ namespace storm {
         class Automaton;
         class Exporter;
         class SynchronizationVector;
+        class ArrayEliminatorData;
         
         class Model {
         public:
@@ -365,8 +366,10 @@ namespace storm {
             /*!
              * Eliminates occurring array variables and expressions by replacing array variables by multiple basic variables.
              * @param keepNonTrivialArrayAccess if set, array access expressions in LValues and expressions are only replaced, if the index expression is constant.
+             * @return data from the elimination. If non-trivial array accesses are kept, pointers to remaining array variables point to this data.
              */
-            void eliminateArrays(bool keepNonTrivialArrayAccess = false);
+            ArrayEliminatorData eliminateArrays(bool keepNonTrivialArrayAccess);
+            void eliminateArrays();
             
             /*!
              * Retrieves whether there is an expression restricting the legal initial values of the global variables.
diff --git a/src/storm/storage/jani/OrderedAssignments.cpp b/src/storm/storage/jani/OrderedAssignments.cpp
index 11f59a5d0..c81e7df0d 100644
--- a/src/storm/storage/jani/OrderedAssignments.cpp
+++ b/src/storm/storage/jani/OrderedAssignments.cpp
@@ -185,6 +185,9 @@ namespace storm {
             std::vector<Assignment> newAssignments;
             for (auto const& assignment : allAssignments) {
                 newAssignments.push_back(*assignment);
+                if (assignment->isTransient() && !assignment->getAssignedExpression().containsVariables()) {
+                    // Since we do not support
+                }
                 if (synchronous && !localVars.hasVariable(assignment->getLValue().isVariable() ? assignment->getLValue().getVariable() : assignment->getLValue().getArray())) {
                     continue;
                 }
diff --git a/src/storm/storage/jani/expressions/ArrayAccessExpression.cpp b/src/storm/storage/jani/expressions/ArrayAccessExpression.cpp
index 1f3980fc9..6590845db 100644
--- a/src/storm/storage/jani/expressions/ArrayAccessExpression.cpp
+++ b/src/storm/storage/jani/expressions/ArrayAccessExpression.cpp
@@ -19,6 +19,7 @@ namespace storm {
         
         boost::any ArrayAccessExpression::accept(ExpressionVisitor& visitor, boost::any const& data) const {
             auto janiVisitor = dynamic_cast<JaniExpressionVisitor*>(&visitor);
+            STORM_LOG_ASSERT(janiVisitor != nullptr, "Visitor of jani expression should be of type JaniVisitor.");
             STORM_LOG_THROW(janiVisitor != nullptr, storm::exceptions::UnexpectedException, "Visitor of jani expression should be of type JaniVisitor.");
             return janiVisitor->visit(*this, data);
         }
@@ -29,7 +30,7 @@ namespace storm {
             } else {
                 stream << "(" << *getFirstOperand() << ")";
             }
-            stream << "[" << getSecondOperand() << "]";
+            stream << "[" << *getSecondOperand() << "]";
         }
     }
 }
\ No newline at end of file
diff --git a/src/storm/storage/jani/traverser/AssignmentLevelFinder.cpp b/src/storm/storage/jani/traverser/AssignmentLevelFinder.cpp
new file mode 100644
index 000000000..442ba4bd4
--- /dev/null
+++ b/src/storm/storage/jani/traverser/AssignmentLevelFinder.cpp
@@ -0,0 +1,19 @@
+#include "storm/storage/jani/traverser/AssignmentLevelFinder.h"
+
+
+namespace storm {
+    namespace jani {
+        
+        uint64_t AssignmentLevelFinder::getLowestAssignmentLevel(Model const& model) {
+            uint64_t res = std::numeric_limits<uint64_t>::max();
+            ConstJaniTraverser::traverse(model, &res);
+            return res;
+        }
+        
+        void AssignmentLevelFinder::traverse(Assignment const& assignment, boost::any const& data) {
+            auto& res = *boost::any_cast<uint64_t*>(data);
+            res = std::min<uint64_t>(res, assignment.getLevel());
+        }
+    }
+}
+
diff --git a/src/storm/storage/jani/traverser/AssignmentLevelFinder.h b/src/storm/storage/jani/traverser/AssignmentLevelFinder.h
new file mode 100644
index 000000000..7a5a4a4fc
--- /dev/null
+++ b/src/storm/storage/jani/traverser/AssignmentLevelFinder.h
@@ -0,0 +1,19 @@
+#pragma once
+
+#include "storm/storage/jani/traverser/JaniTraverser.h"
+
+namespace storm {
+    namespace jani {
+        class AssignmentLevelFinder : public ConstJaniTraverser {
+        public:
+            
+            AssignmentLevelFinder() = default;
+            virtual ~AssignmentLevelFinder() = default;
+            
+            uint64_t getLowestAssignmentLevel(Model const& model);
+            
+            virtual void traverse(Assignment const& assignment, boost::any const& data) override;
+        };
+    }
+}
+
diff --git a/src/storm/storage/jani/traverser/AssignmentsFinder.cpp b/src/storm/storage/jani/traverser/AssignmentsFinder.cpp
index 8ad36776b..db7cfccf8 100644
--- a/src/storm/storage/jani/traverser/AssignmentsFinder.cpp
+++ b/src/storm/storage/jani/traverser/AssignmentsFinder.cpp
@@ -13,7 +13,7 @@ namespace storm {
             return res;
         }
         
-        void AssignmentsFinder::traverse(Location const& location, boost::any const& data) const {
+        void AssignmentsFinder::traverse(Location const& location, boost::any const& data) {
             auto resVar = boost::any_cast<std::pair<Variable const*, ResultType*>>(data);
             for (auto const& assignment : location.getAssignments()) {
                 if (assignment.getVariable() == *resVar.first) {
@@ -23,7 +23,7 @@ namespace storm {
             ConstJaniTraverser::traverse(location, data);
         }
         
-        void AssignmentsFinder::traverse(TemplateEdge const& templateEdge, boost::any const& data) const {
+        void AssignmentsFinder::traverse(TemplateEdge const& templateEdge, boost::any const& data) {
             auto resVar = boost::any_cast<std::pair<Variable const*, ResultType*>>(data);
             for (auto const& assignment : templateEdge.getAssignments()) {
                 if (assignment.getVariable() == *resVar.first) {
@@ -33,7 +33,7 @@ namespace storm {
             ConstJaniTraverser::traverse(templateEdge, data);
         }
         
-        void AssignmentsFinder::traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data) const {
+        void AssignmentsFinder::traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data) {
             auto resVar = boost::any_cast<std::pair<Variable const*, ResultType*>>(data);
             for (auto const& assignment : templateEdgeDestination.getOrderedAssignments()) {
                 if (assignment.getVariable() == *resVar.first) {
diff --git a/src/storm/storage/jani/traverser/AssignmentsFinder.h b/src/storm/storage/jani/traverser/AssignmentsFinder.h
index b6bcd376e..514d29208 100644
--- a/src/storm/storage/jani/traverser/AssignmentsFinder.h
+++ b/src/storm/storage/jani/traverser/AssignmentsFinder.h
@@ -20,9 +20,9 @@ namespace storm {
             
             virtual ~AssignmentsFinder() = default;
             
-            virtual void traverse(Location const& location, boost::any const& data) const override;
-            virtual void traverse(TemplateEdge const& templateEdge, boost::any const& data) const override;
-            virtual void traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data) const override;
+            virtual void traverse(Location const& location, boost::any const& data) override;
+            virtual void traverse(TemplateEdge const& templateEdge, boost::any const& data) override;
+            virtual void traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data) override;
         };
     }
 }
diff --git a/src/storm/storage/jani/traverser/JaniTraverser.cpp b/src/storm/storage/jani/traverser/JaniTraverser.cpp
index bd1b9bbf1..787682ede 100644
--- a/src/storm/storage/jani/traverser/JaniTraverser.cpp
+++ b/src/storm/storage/jani/traverser/JaniTraverser.cpp
@@ -4,7 +4,7 @@
 namespace storm {
     namespace jani {
         
-        void JaniTraverser::traverse(Model& model, boost::any const& data) const {
+        void JaniTraverser::traverse(Model& model, boost::any const& data) {
             for (auto& act : model.getActions()) {
                 traverse(act, data);
             }
@@ -20,11 +20,11 @@ namespace storm {
             }
         }
         
-        void JaniTraverser::traverse(Action const& action, boost::any const& data) const {
+        void JaniTraverser::traverse(Action const& action, boost::any const& data) {
             // Intentionally left empty.
         }
-            
-        void JaniTraverser::traverse(Automaton& automaton, boost::any const& data) const {
+        
+        void JaniTraverser::traverse(Automaton& automaton, boost::any const& data) {
             traverse(automaton.getVariables(), data);
             for (auto& loc : automaton.getLocations()) {
                 traverse(loc, data);
@@ -34,14 +34,14 @@ namespace storm {
                 traverse(automaton.getInitialStatesRestriction(), data);
             }
         }
-            
-        void JaniTraverser::traverse(Constant& constant, boost::any const& data) const {
+        
+        void JaniTraverser::traverse(Constant& constant, boost::any const& data) {
             if (constant.isDefined()) {
                 traverse(constant.getExpression(), data);
             }
         }
-            
-        void JaniTraverser::traverse(VariableSet& variableSet, boost::any const& data) const {
+        
+        void JaniTraverser::traverse(VariableSet& variableSet, boost::any const& data) {
             for (auto& v : variableSet.getBooleanVariables()) {
                 traverse(v, data);
             }
@@ -58,18 +58,18 @@ namespace storm {
                 traverse(v, data);
             }
         }
-            
-        void JaniTraverser::traverse(Location& location, boost::any const& data) const {
+        
+        void JaniTraverser::traverse(Location& location, boost::any const& data) {
             traverse(location.getAssignments(), data);
         }
-            
-        void JaniTraverser::traverse(BooleanVariable& variable, boost::any const& data) const {
+        
+        void JaniTraverser::traverse(BooleanVariable& variable, boost::any const& data) {
             if (variable.hasInitExpression()) {
                 traverse(variable.getInitExpression(), data);
             }
         }
         
-        void JaniTraverser::traverse(BoundedIntegerVariable& variable, boost::any const& data) const {
+        void JaniTraverser::traverse(BoundedIntegerVariable& variable, boost::any const& data) {
             if (variable.hasInitExpression()) {
                 traverse(variable.getInitExpression(), data);
             }
@@ -77,19 +77,19 @@ namespace storm {
             traverse(variable.getUpperBound(), data);
         }
         
-        void JaniTraverser::traverse(UnboundedIntegerVariable& variable, boost::any const& data) const {
+        void JaniTraverser::traverse(UnboundedIntegerVariable& variable, boost::any const& data) {
             if (variable.hasInitExpression()) {
                 traverse(variable.getInitExpression(), data);
             }
         }
         
-        void JaniTraverser::traverse(RealVariable& variable, boost::any const& data) const {
+        void JaniTraverser::traverse(RealVariable& variable, boost::any const& data) {
              if (variable.hasInitExpression()) {
                 traverse(variable.getInitExpression(), data);
             }
         }
         
-        void JaniTraverser::traverse(ArrayVariable& variable, boost::any const& data) const {
+        void JaniTraverser::traverse(ArrayVariable& variable, boost::any const& data) {
             if (variable.hasInitExpression()) {
                 traverse(variable.getInitExpression(), data);
             }
@@ -99,7 +99,7 @@ namespace storm {
             }
         }
         
-        void JaniTraverser::traverse(EdgeContainer& edgeContainer, boost::any const& data) const {
+        void JaniTraverser::traverse(EdgeContainer& edgeContainer, boost::any const& data) {
             for (auto& templateEdge : edgeContainer.getTemplateEdges()) {
                 traverse(*templateEdge, data);
             }
@@ -108,19 +108,19 @@ namespace storm {
             }
         }
         
-        void JaniTraverser::traverse(TemplateEdge& templateEdge, boost::any const& data) const {
+        void JaniTraverser::traverse(TemplateEdge& templateEdge, boost::any const& data) {
             traverse(templateEdge.getGuard(), data);
             for (auto& dest : templateEdge.getDestinations()) {
                 traverse(dest, data);
             }
             traverse(templateEdge.getAssignments(), data);
         }
-            
-        void JaniTraverser::traverse(TemplateEdgeDestination& templateEdgeDestination, boost::any const& data) const {
+        
+        void JaniTraverser::traverse(TemplateEdgeDestination& templateEdgeDestination, boost::any const& data) {
             traverse(templateEdgeDestination.getOrderedAssignments(), data);
         }
-            
-        void JaniTraverser::traverse(Edge& edge, boost::any const& data) const {
+        
+        void JaniTraverser::traverse(Edge& edge, boost::any const& data) {
             if (edge.hasRate()) {
                 traverse(edge.getRate(), data);
             }
@@ -128,34 +128,34 @@ namespace storm {
                 traverse(dest, data);
             }
         }
-            
-        void JaniTraverser::traverse(EdgeDestination& edgeDestination, boost::any const& data) const {
+        
+        void JaniTraverser::traverse(EdgeDestination& edgeDestination, boost::any const& data) {
             traverse(edgeDestination.getProbability(), data);
         }
-            
-        void JaniTraverser::traverse(OrderedAssignments& orderedAssignments, boost::any const& data) const {
+        
+        void JaniTraverser::traverse(OrderedAssignments& orderedAssignments, boost::any const& data) {
             for (auto& assignment : orderedAssignments) {
                 traverse(assignment, data);
             }
             STORM_LOG_ASSERT(orderedAssignments.checkOrder(), "Order of ordered assignment has been violated.");
         }
-            
-        void JaniTraverser::traverse(Assignment& assignment, boost::any const& data) const {
+        
+        void JaniTraverser::traverse(Assignment& assignment, boost::any const& data) {
             traverse(assignment.getAssignedExpression(), data);
             traverse(assignment.getLValue(), data);
         }
         
-        void JaniTraverser::traverse(LValue& lValue, boost::any const& data) const {
+        void JaniTraverser::traverse(LValue& lValue, boost::any const& data) {
             if (lValue.isArrayAccess()) {
                 traverse(lValue.getArrayIndex(), data);
             }
         }
         
-        void JaniTraverser::traverse(storm::expressions::Expression const& expression, boost::any const& data) const {
+        void JaniTraverser::traverse(storm::expressions::Expression const& expression, boost::any const& data) {
             // intentionally left empty.
         }
         
-        void ConstJaniTraverser::traverse(Model const& model, boost::any const& data) const {
+        void ConstJaniTraverser::traverse(Model const& model, boost::any const& data) {
             for (auto const& act : model.getActions()) {
                 traverse(act, data);
             }
@@ -171,11 +171,11 @@ namespace storm {
             }
         }
         
-        void ConstJaniTraverser::traverse(Action const& action, boost::any const& data) const {
+        void ConstJaniTraverser::traverse(Action const& action, boost::any const& data) {
             // Intentionally left empty.
         }
-            
-        void ConstJaniTraverser::traverse(Automaton const& automaton, boost::any const& data) const {
+        
+        void ConstJaniTraverser::traverse(Automaton const& automaton, boost::any const& data) {
             traverse(automaton.getVariables(), data);
             for (auto const& loc : automaton.getLocations()) {
                 traverse(loc, data);
@@ -185,14 +185,14 @@ namespace storm {
                 traverse(automaton.getInitialStatesRestriction(), data);
             }
         }
-            
-        void ConstJaniTraverser::traverse(Constant const& constant, boost::any const& data) const {
+        
+        void ConstJaniTraverser::traverse(Constant const& constant, boost::any const& data) {
             if (constant.isDefined()) {
                 traverse(constant.getExpression(), data);
             }
         }
-            
-        void ConstJaniTraverser::traverse(VariableSet const& variableSet, boost::any const& data) const {
+        
+        void ConstJaniTraverser::traverse(VariableSet const& variableSet, boost::any const& data) {
             for (auto const& v : variableSet.getBooleanVariables()) {
                 traverse(v, data);
             }
@@ -209,18 +209,18 @@ namespace storm {
                 traverse(v, data);
             }
         }
-            
-        void ConstJaniTraverser::traverse(Location const& location, boost::any const& data) const {
+        
+        void ConstJaniTraverser::traverse(Location const& location, boost::any const& data) {
             traverse(location.getAssignments(), data);
         }
-            
-        void ConstJaniTraverser::traverse(BooleanVariable const& variable, boost::any const& data) const {
+        
+        void ConstJaniTraverser::traverse(BooleanVariable const& variable, boost::any const& data) {
             if (variable.hasInitExpression()) {
                 traverse(variable.getInitExpression(), data);
             }
         }
         
-        void ConstJaniTraverser::traverse(BoundedIntegerVariable const& variable, boost::any const& data) const {
+        void ConstJaniTraverser::traverse(BoundedIntegerVariable const& variable, boost::any const& data) {
             if (variable.hasInitExpression()) {
                 traverse(variable.getInitExpression(), data);
             }
@@ -228,19 +228,19 @@ namespace storm {
             traverse(variable.getUpperBound(), data);
         }
         
-        void ConstJaniTraverser::traverse(UnboundedIntegerVariable const& variable, boost::any const& data) const {
+        void ConstJaniTraverser::traverse(UnboundedIntegerVariable const& variable, boost::any const& data) {
             if (variable.hasInitExpression()) {
                 traverse(variable.getInitExpression(), data);
             }
         }
         
-        void ConstJaniTraverser::traverse(RealVariable const& variable, boost::any const& data) const {
+        void ConstJaniTraverser::traverse(RealVariable const& variable, boost::any const& data) {
              if (variable.hasInitExpression()) {
                 traverse(variable.getInitExpression(), data);
             }
         }
         
-        void ConstJaniTraverser::traverse(ArrayVariable const& variable, boost::any const& data) const {
+        void ConstJaniTraverser::traverse(ArrayVariable const& variable, boost::any const& data) {
             if (variable.hasInitExpression()) {
                 traverse(variable.getInitExpression(), data);
             }
@@ -250,7 +250,7 @@ namespace storm {
             }
         }
         
-        void ConstJaniTraverser::traverse(EdgeContainer const& edgeContainer, boost::any const& data) const {
+        void ConstJaniTraverser::traverse(EdgeContainer const& edgeContainer, boost::any const& data) {
             for (auto const& templateEdge : edgeContainer.getTemplateEdges()) {
                 traverse(*templateEdge, data);
             }
@@ -259,19 +259,19 @@ namespace storm {
             }
         }
         
-        void ConstJaniTraverser::traverse(TemplateEdge const& templateEdge, boost::any const& data) const {
+        void ConstJaniTraverser::traverse(TemplateEdge const& templateEdge, boost::any const& data) {
             traverse(templateEdge.getGuard(), data);
             for (auto const& dest : templateEdge.getDestinations()) {
                 traverse(dest, data);
             }
             traverse(templateEdge.getAssignments(), data);
         }
-            
-        void ConstJaniTraverser::traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data) const {
+        
+        void ConstJaniTraverser::traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data) {
             traverse(templateEdgeDestination.getOrderedAssignments(), data);
         }
-            
-        void ConstJaniTraverser::traverse(Edge const& edge, boost::any const& data) const {
+        
+        void ConstJaniTraverser::traverse(Edge const& edge, boost::any const& data) {
             if (edge.hasRate()) {
                 traverse(edge.getRate(), data);
             }
@@ -279,29 +279,29 @@ namespace storm {
                 traverse(dest, data);
             }
         }
-            
-        void ConstJaniTraverser::traverse(EdgeDestination const& edgeDestination, boost::any const& data) const {
+        
+        void ConstJaniTraverser::traverse(EdgeDestination const& edgeDestination, boost::any const& data) {
             traverse(edgeDestination.getProbability(), data);
         }
-            
-        void ConstJaniTraverser::traverse(OrderedAssignments const& orderedAssignments, boost::any const& data) const {
+        
+        void ConstJaniTraverser::traverse(OrderedAssignments const& orderedAssignments, boost::any const& data) {
             for (auto const& assignment : orderedAssignments) {
                 traverse(assignment, data);
             }
         }
-            
-        void ConstJaniTraverser::traverse(Assignment const& assignment, boost::any const& data) const {
+        
+        void ConstJaniTraverser::traverse(Assignment const& assignment, boost::any const& data) {
             traverse(assignment.getAssignedExpression(), data);
             traverse(assignment.getLValue(), data);
         }
-            
-        void ConstJaniTraverser::traverse(LValue const& lValue, boost::any const& data) const {
+        
+        void ConstJaniTraverser::traverse(LValue const& lValue, boost::any const& data) {
             if (lValue.isArrayAccess()) {
                 traverse(lValue.getArrayIndex(), data);
             }
         }
         
-        void ConstJaniTraverser::traverse(storm::expressions::Expression const& expression, boost::any const& data) const {
+        void ConstJaniTraverser::traverse(storm::expressions::Expression const& expression, boost::any const& data) {
             // intentionally left empty.
         }
         
diff --git a/src/storm/storage/jani/traverser/JaniTraverser.h b/src/storm/storage/jani/traverser/JaniTraverser.h
index 25cc4530d..685c76a85 100644
--- a/src/storm/storage/jani/traverser/JaniTraverser.h
+++ b/src/storm/storage/jani/traverser/JaniTraverser.h
@@ -11,54 +11,54 @@ namespace storm {
         public:
             virtual ~JaniTraverser() = default;
             
-            virtual void traverse(Model& model, boost::any const& data) const;
+            virtual void traverse(Model& model, boost::any const& data);
             
-            virtual void traverse(Action const& action, boost::any const& data) const;
-            virtual void traverse(Automaton& automaton, boost::any const& data) const;
-            virtual void traverse(Constant& constant, boost::any const& data) const;
-            virtual void traverse(VariableSet& variableSet, boost::any const& data) const;
-            virtual void traverse(Location& location, boost::any const& data) const;
-            virtual void traverse(BooleanVariable& variable, boost::any const& data) const;
-            virtual void traverse(BoundedIntegerVariable& variable, boost::any const& data) const;
-            virtual void traverse(UnboundedIntegerVariable& variable, boost::any const& data) const;
-            virtual void traverse(RealVariable& variable, boost::any const& data) const;
-            virtual void traverse(ArrayVariable& variable, boost::any const& data) const;
-            virtual void traverse(EdgeContainer& edgeContainer, boost::any const& data) const;
-            virtual void traverse(TemplateEdge& templateEdge, boost::any const& data) const;
-            virtual void traverse(TemplateEdgeDestination& templateEdgeDestination, boost::any const& data) const;
-            virtual void traverse(Edge& edge, boost::any const& data) const;
-            virtual void traverse(EdgeDestination& edgeDestination, boost::any const& data) const;
-            virtual void traverse(OrderedAssignments& orderedAssignments, boost::any const& data) const;
-            virtual void traverse(Assignment& assignment, boost::any const& data) const;
-            virtual void traverse(LValue& lValue, boost::any const& data) const;
-            virtual void traverse(storm::expressions::Expression const& expression, boost::any const& data) const;
+            virtual void traverse(Action const& action, boost::any const& data);
+            virtual void traverse(Automaton& automaton, boost::any const& data);
+            virtual void traverse(Constant& constant, boost::any const& data);
+            virtual void traverse(VariableSet& variableSet, boost::any const& data);
+            virtual void traverse(Location& location, boost::any const& data);
+            virtual void traverse(BooleanVariable& variable, boost::any const& data);
+            virtual void traverse(BoundedIntegerVariable& variable, boost::any const& data);
+            virtual void traverse(UnboundedIntegerVariable& variable, boost::any const& data);
+            virtual void traverse(RealVariable& variable, boost::any const& data);
+            virtual void traverse(ArrayVariable& variable, boost::any const& data);
+            virtual void traverse(EdgeContainer& edgeContainer, boost::any const& data);
+            virtual void traverse(TemplateEdge& templateEdge, boost::any const& data);
+            virtual void traverse(TemplateEdgeDestination& templateEdgeDestination, boost::any const& data);
+            virtual void traverse(Edge& edge, boost::any const& data);
+            virtual void traverse(EdgeDestination& edgeDestination, boost::any const& data);
+            virtual void traverse(OrderedAssignments& orderedAssignments, boost::any const& data);
+            virtual void traverse(Assignment& assignment, boost::any const& data);
+            virtual void traverse(LValue& lValue, boost::any const& data);
+            virtual void traverse(storm::expressions::Expression const& expression, boost::any const& data);
         };
         
         class ConstJaniTraverser {
         public:
             virtual ~ConstJaniTraverser() = default;
             
-            virtual void traverse(Model const& model, boost::any const& data) const;
+            virtual void traverse(Model const& model, boost::any const& data);
             
-            virtual void traverse(Action const& action, boost::any const& data) const;
-            virtual void traverse(Automaton const& automaton, boost::any const& data) const;
-            virtual void traverse(Constant const& constant, boost::any const& data) const;
-            virtual void traverse(VariableSet const& variableSet, boost::any const& data) const;
-            virtual void traverse(Location const& location, boost::any const& data) const;
-            virtual void traverse(BooleanVariable const& variable, boost::any const& data) const;
-            virtual void traverse(BoundedIntegerVariable const& variable, boost::any const& data) const;
-            virtual void traverse(UnboundedIntegerVariable const& variable, boost::any const& data) const;
-            virtual void traverse(RealVariable const& variable, boost::any const& data) const;
-            virtual void traverse(ArrayVariable const& variable, boost::any const& data) const;
-            virtual void traverse(EdgeContainer const& edgeContainer, boost::any const& data) const;
-            virtual void traverse(TemplateEdge const& templateEdge, boost::any const& data) const;
-            virtual void traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data) const;
-            virtual void traverse(Edge const& edge, boost::any const& data) const;
-            virtual void traverse(EdgeDestination const& edgeDestination, boost::any const& data) const;
-            virtual void traverse(OrderedAssignments const& orderedAssignments, boost::any const& data) const;
-            virtual void traverse(Assignment const& assignment, boost::any const& data) const;
-            virtual void traverse(LValue const& lValue, boost::any const& data) const;
-            virtual void traverse(storm::expressions::Expression const& expression, boost::any const& data) const;
+            virtual void traverse(Action const& action, boost::any const& data);
+            virtual void traverse(Automaton const& automaton, boost::any const& data);
+            virtual void traverse(Constant const& constant, boost::any const& data);
+            virtual void traverse(VariableSet const& variableSet, boost::any const& data);
+            virtual void traverse(Location const& location, boost::any const& data);
+            virtual void traverse(BooleanVariable const& variable, boost::any const& data);
+            virtual void traverse(BoundedIntegerVariable const& variable, boost::any const& data);
+            virtual void traverse(UnboundedIntegerVariable const& variable, boost::any const& data);
+            virtual void traverse(RealVariable const& variable, boost::any const& data);
+            virtual void traverse(ArrayVariable const& variable, boost::any const& data);
+            virtual void traverse(EdgeContainer const& edgeContainer, boost::any const& data);
+            virtual void traverse(TemplateEdge const& templateEdge, boost::any const& data);
+            virtual void traverse(TemplateEdgeDestination const& templateEdgeDestination, boost::any const& data);
+            virtual void traverse(Edge const& edge, boost::any const& data);
+            virtual void traverse(EdgeDestination const& edgeDestination, boost::any const& data);
+            virtual void traverse(OrderedAssignments const& orderedAssignments, boost::any const& data);
+            virtual void traverse(Assignment const& assignment, boost::any const& data);
+            virtual void traverse(LValue const& lValue, boost::any const& data);
+            virtual void traverse(storm::expressions::Expression const& expression, boost::any const& data);
         };
     }
 }