diff --git a/src/builder/DdJaniModelBuilder.cpp b/src/builder/DdJaniModelBuilder.cpp
index 96baa2077..d3bb66863 100644
--- a/src/builder/DdJaniModelBuilder.cpp
+++ b/src/builder/DdJaniModelBuilder.cpp
@@ -7,7 +7,6 @@
 #include "src/logic/Formulas.h"
 
 #include "src/storage/jani/Model.h"
-#include "src/storage/jani/RenameComposition.h"
 #include "src/storage/jani/AutomatonComposition.h"
 #include "src/storage/jani/ParallelComposition.h"
 #include "src/storage/jani/CompositionActionInformationVisitor.h"
@@ -209,12 +208,7 @@ namespace storm {
                 automata.insert(it, composition.getAutomatonName());
                 return boost::none;
             }
-            
-            boost::any visit(storm::jani::RenameComposition const& composition, boost::any const& data) override {
-                composition.getSubcomposition().accept(*this, data);
-                return boost::none;
-            }
-            
+
             boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override {
                 for (auto const& subcomposition : composition.getSubcompositions()) {
                     subcomposition->accept(*this, boost::none);
@@ -500,436 +494,7 @@ namespace storm {
             result.setValue(metaVariableNameToValueMap, 1);
             return result;
         }
-        
-//        template <storm::dd::DdType Type, typename ValueType>
-//        class SeparateEdgesSystemComposer : public SystemComposer<Type, ValueType> {
-//        public:
-//            // This structure represents an edge.
-//            struct EdgeDd {
-//                EdgeDd(storm::dd::Add<Type> const& guard = storm::dd::Add<Type>(), storm::dd::Add<Type, ValueType> const& transitions = storm::dd::Add<Type, ValueType>(), std::set<storm::expressions::Variable> const& writtenGlobalVariables = {}, std::set<storm::expressions::Variable> const& globalVariablesWrittenMultipleTimes = {}) : guard(guard), transitions(transitions), writtenGlobalVariables(writtenGlobalVariables), globalVariablesWrittenMultipleTimes(globalVariablesWrittenMultipleTimes) {
-//                    // Intentionally left empty.
-//                }
-//                
-//                EdgeDd(EdgeDd const& other) : guard(other.guard), transitions(other.transitions), writtenGlobalVariables(other.writtenGlobalVariables), globalVariablesWrittenMultipleTimes(other.globalVariablesWrittenMultipleTimes) {
-//                    // Intentionally left empty.
-//                }
-//                
-//                EdgeDd& operator=(EdgeDd const& other) {
-//                    if (this != &other) {
-//                        globalVariablesWrittenMultipleTimes = other.globalVariablesWrittenMultipleTimes;
-//                        writtenGlobalVariables = other.writtenGlobalVariables;
-//                        guard = other.guard;
-//                        transitions = other.transitions;
-//                    }
-//                    return *this;
-//                }
-//                
-//                storm::dd::Add<Type, ValueType> guard;
-//                storm::dd::Add<Type, ValueType> transitions;
-//                std::set<storm::expressions::Variable> writtenGlobalVariables;
-//                std::set<storm::expressions::Variable> globalVariablesWrittenMultipleTimes;
-//            };
-//            
-//            // This structure represents a subcomponent of a composition.
-//            struct AutomatonDd {
-//                AutomatonDd(storm::dd::Add<Type, ValueType> const& identity) : identity(identity) {
-//                    // Intentionally left empty.
-//                }
-//                
-//                std::map<uint64_t, std::vector<EdgeDd>> actionIndexToEdges;
-//                storm::dd::Add<Type, ValueType> identity;
-//            };
-//            
-//            SeparateEdgesSystemComposer(storm::jani::Model const& model, CompositionVariables<Type, ValueType> const& variables) : SystemComposer<Type, ValueType>(model, variables) {
-//                // Intentionally left empty.
-//            }
-//            
-//            ComposerResult<Type, ValueType> compose() override {
-//                AutomatonDd globalAutomaton = boost::any_cast<AutomatonDd>(this->model.getSystemComposition().accept(*this, boost::none));
-//                return buildSystemFromAutomaton(globalAutomaton);
-//            }
-//            
-//            boost::any visit(storm::jani::AutomatonComposition const& composition, boost::any const& data) override {
-//                return buildAutomatonDd(composition.getAutomatonName());
-//            }
-//            
-//            boost::any visit(storm::jani::RenameComposition const& composition, boost::any const& data) override {
-//                AutomatonDd subautomaton = boost::any_cast<AutomatonDd>(composition.getSubcomposition().accept(*this, boost::none));
-//                
-//                // Build a mapping from indices to indices for the renaming.
-//                std::map<uint64_t, uint64_t> renamingIndexToIndex;
-//                for (auto const& entry : composition.getRenaming()) {
-//                    if (this->model.getActionIndex(entry.first) != this->model.getSilentActionIndex()) {
-//                        // Distinguish the cases where we hide the action or properly rename it.
-//                        if (entry.second) {
-//                            renamingIndexToIndex.emplace(this->model.getActionIndex(entry.first), this->model.getActionIndex(entry.second.get()));
-//                        } else {
-//                            renamingIndexToIndex.emplace(this->model.getActionIndex(entry.first), this->model.getSilentActionIndex());
-//                        }
-//                    } else {
-//                        STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Renaming composition must not rename the silent action.");
-//                    }
-//                }
-//                
-//                // Finally, apply the renaming.
-//                AutomatonDd result(subautomaton.identity);
-//                for (auto const& actionEdges : subautomaton.actionIndexToEdges) {
-//                    auto it = renamingIndexToIndex.find(actionEdges.first);
-//                    if (it != renamingIndexToIndex.end()) {
-//                        // If we are to rename the action, do so.
-//                        result.actionIndexToEdges[it->second].insert(result.actionIndexToEdges[it->second].end(), actionEdges.second.begin(), actionEdges.second.end());
-//                    } else {
-//                        // Otherwise copy over the edges.
-//                        result.actionIndexToEdges[it->first].insert(result.actionIndexToEdges[it->first].begin(), actionEdges.second.begin(), actionEdges.second.end());
-//                    }
-//                }
-//                return result;
-//            }
-//            
-//            boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override {
-//                AutomatonDd leftSubautomaton = boost::any_cast<AutomatonDd>(composition.getLeftSubcomposition().accept(*this, boost::none));
-//                AutomatonDd rightSubautomaton = boost::any_cast<AutomatonDd>(composition.getRightSubcomposition().accept(*this, boost::none));
-//                
-//                // Build the set of synchronizing action indices.
-//                std::set<uint64_t> synchronizingActionIndices;
-//                for (auto const& entry : composition.getSynchronizationAlphabet()) {
-//                    if (this->model.getActionIndex(entry) != this->model.getSilentActionIndex()) {
-//                        synchronizingActionIndices.insert(this->model.getActionIndex(entry));
-//                    } else {
-//                        STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Parallel composition must not synchronize over silent action.");
-//                    }
-//                }
-//                
-//                // Perform the composition.
-//                
-//                // First, consider all actions in the left subcomposition.
-//                AutomatonDd result(leftSubautomaton.identity * rightSubautomaton.identity);
-//                uint64_t index = 0;
-//                for (auto const& actionEdges : leftSubautomaton.actionIndexToEdges) {
-//                    // If we need to synchronize over this action, do so now.
-//                    if (synchronizingActionIndices.find(actionEdges.first) != synchronizingActionIndices.end()) {
-//                        auto rightIt = rightSubautomaton.actionIndexToEdges.find(actionEdges.first);
-//                        if (rightIt != rightSubautomaton.actionIndexToEdges.end()) {
-//                            for (auto const& edge1 : actionEdges.second) {
-//                                for (auto const& edge2 : rightIt->second) {
-//                                    EdgeDd edgeDd = composeEdgesInParallel(edge1, edge2);
-//                                    if (!edgeDd.guard.isZero()) {
-//                                        result.actionIndexToEdges[actionEdges.first].push_back(edgeDd);
-//                                    }
-//                                    index++;
-//                                }
-//                            }
-//                        }
-//                    } else {
-//                        // Extend all edges by the missing identity (unsynchronizing) and copy them over.
-//                        for (auto const& edge : actionEdges.second) {
-//                            result.actionIndexToEdges[actionEdges.first].push_back(extendEdgeWithIdentity(edge, rightSubautomaton.identity));
-//                        }
-//                    }
-//                }
-//                
-//                // Then, consider all actions in the right subcomposition. All synchronizing actions can be ignored, because
-//                // we would have dealt with them earlier if there was a suitable synchronization partner. Since there is none,
-//                // such transitions can not be taken and we can drop them.
-//                for (auto const& actionEdges : rightSubautomaton.actionIndexToEdges) {
-//                    if (synchronizingActionIndices.find(actionEdges.first) == synchronizingActionIndices.end()) {
-//                        for (auto const& edge : actionEdges.second) {
-//                            result.actionIndexToEdges[actionEdges.first].push_back(extendEdgeWithIdentity(edge, leftSubautomaton.identity));
-//                        }
-//                    }
-//                }
-//                
-//                return result;
-//            }
-//            
-//        private:
-//            storm::dd::Add<Type, ValueType> combineEdgesBySummation(std::vector<EdgeDd> const& edges, CompositionVariables<Type, ValueType> const& variables) {
-//                storm::dd::Add<Type, ValueType> result = variables.manager->template getAddZero<ValueType>();
-//                for (auto const& edge : edges) {
-//                    // Simply add all actions, but make sure to include the missing global variable identities.
-//                    result += edge.transitions * computeMissingGlobalVariableIdentities(edge, variables);
-//                }
-//                return result;
-//            }
-//            
-//            std::pair<uint64_t, storm::dd::Add<Type, ValueType>> combineEdgesByNondeterministicChoice(std::vector<EdgeDd>& edges) {
-//                // Complete all edges by adding the missing global variable identities.
-//                for (auto& edge : edges) {
-//                    edge.transitions *= computeMissingGlobalVariableIdentities(edge, this->variables);
-//                }
-//                
-//                // Sum all guards, so we can read off the maximal number of nondeterministic choices in any given state.
-//                storm::dd::Add<Type, ValueType> sumOfGuards = this->variables.manager->template getAddZero<ValueType>();
-//                for (auto const& edge : edges) {
-//                    sumOfGuards += edge.guard;
-//                }
-//                uint_fast64_t maxChoices = static_cast<uint_fast64_t>(sumOfGuards.getMax());
-//                STORM_LOG_TRACE("Found " << maxChoices << " local choices.");
-//                
-//                // Depending on the maximal number of nondeterminstic choices, we need to use some variables to encode the nondeterminism.
-//                if (maxChoices == 0) {
-//                    return std::make_pair(0, this->variables.manager->template getAddZero<ValueType>());
-//                } else if (maxChoices == 1) {
-//                    return std::make_pair(0, combineEdgesBySummation(edges, this->variables));
-//                } else {
-//                    // Calculate number of required variables to encode the nondeterminism.
-//                    uint_fast64_t numberOfBinaryVariables = static_cast<uint_fast64_t>(std::ceil(storm::utility::math::log2(maxChoices)));
-//                    
-//                    storm::dd::Add<Type, ValueType> allEdges = this->variables.manager->template getAddZero<ValueType>();
-//                    
-//                    storm::dd::Bdd<Type> equalsNumberOfChoicesDd;
-//                    std::vector<storm::dd::Add<Type, ValueType>> choiceDds(maxChoices, this->variables.manager->template getAddZero<ValueType>());
-//                    std::vector<storm::dd::Bdd<Type>> remainingDds(maxChoices, this->variables.manager->getBddZero());
-//                    
-//                    for (uint_fast64_t currentChoices = 1; currentChoices <= maxChoices; ++currentChoices) {
-//                        // Determine the set of states with exactly currentChoices choices.
-//                        equalsNumberOfChoicesDd = sumOfGuards.equals(this->variables.manager->getConstant(static_cast<double>(currentChoices)));
-//                        
-//                        // If there is no such state, continue with the next possible number of choices.
-//                        if (equalsNumberOfChoicesDd.isZero()) {
-//                            continue;
-//                        }
-//                        
-//                        // Reset the previously used intermediate storage.
-//                        for (uint_fast64_t j = 0; j < currentChoices; ++j) {
-//                            choiceDds[j] = this->variables.manager->template getAddZero<ValueType>();
-//                            remainingDds[j] = equalsNumberOfChoicesDd;
-//                        }
-//                        
-//                        for (std::size_t j = 0; j < edges.size(); ++j) {
-//                            // Check if edge guard overlaps with equalsNumberOfChoicesDd. That is, there are states with exactly currentChoices
-//                            // choices such that one outgoing choice is given by the j-th edge.
-//                            storm::dd::Bdd<Type> guardChoicesIntersection = edges[j].guard.toBdd() && equalsNumberOfChoicesDd;
-//                            
-//                            // If there is no such state, continue with the next command.
-//                            if (guardChoicesIntersection.isZero()) {
-//                                continue;
-//                            }
-//                            
-//                            // Split the currentChoices nondeterministic choices.
-//                            for (uint_fast64_t k = 0; k < currentChoices; ++k) {
-//                                // Calculate the overlapping part of command guard and the remaining DD.
-//                                storm::dd::Bdd<Type> remainingGuardChoicesIntersection = guardChoicesIntersection && remainingDds[k];
-//                                
-//                                // Check if we can add some overlapping parts to the current index.
-//                                if (!remainingGuardChoicesIntersection.isZero()) {
-//                                    // Remove overlapping parts from the remaining DD.
-//                                    remainingDds[k] = remainingDds[k] && !remainingGuardChoicesIntersection;
-//                                    
-//                                    // Combine the overlapping part of the guard with command updates and add it to the resulting DD.
-//                                    choiceDds[k] += remainingGuardChoicesIntersection.template toAdd<ValueType>() * edges[j].transitions;
-//                                }
-//                                
-//                                // Remove overlapping parts from the command guard DD
-//                                guardChoicesIntersection = guardChoicesIntersection && !remainingGuardChoicesIntersection;
-//                                
-//                                // If the guard DD has become equivalent to false, we can stop here.
-//                                if (guardChoicesIntersection.isZero()) {
-//                                    break;
-//                                }
-//                            }
-//                        }
-//                        
-//                        // Add the meta variables that encode the nondeterminisim to the different choices.
-//                        for (uint_fast64_t j = 0; j < currentChoices; ++j) {
-//                            allEdges += encodeIndex(j, 0, numberOfBinaryVariables, this->variables) * choiceDds[j];
-//                        }
-//                        
-//                        // Delete currentChoices out of overlapping DD
-//                        sumOfGuards = sumOfGuards * (!equalsNumberOfChoicesDd).template toAdd<ValueType>();
-//                    }
-//                    
-//                    return std::make_pair(numberOfBinaryVariables, allEdges);
-//                }
-//            }
-//            
-//            storm::dd::Bdd<Type> computeIllegalFragmentFromEdges(std::map<uint64_t, std::vector<EdgeDd>> const& actionIndexToEdges) {
-//                // Create the illegal fragment. For this, we need to find the edges that write global variables multiple times.
-//                storm::dd::Bdd<Type> illegalFragment = this->variables.manager->getBddZero();
-//                for (auto const& action : actionIndexToEdges) {
-//                    for (auto const& edge : action.second) {
-//                        if (!edge.globalVariablesWrittenMultipleTimes.empty()) {
-//                            for (auto const& variable : edge.globalVariablesWrittenMultipleTimes) {
-//                                STORM_LOG_WARN("The global variable '" << variable.getName() << "' is written along multiple synchronizing edges. If such a transition is contained in the reachable state space, an error is raised.");
-//                                illegalFragment |= edge.guard.toBdd();
-//                            }
-//                        }
-//                    }
-//                }
-//                return illegalFragment;
-//            }
-//            
-//            ComposerResult<Type, ValueType> buildSystemFromAutomaton(AutomatonDd& automatonDd) {
-//                // If the model is an MDP, we need to encode the nondeterminism using additional variables.
-//                if (this->model.getModelType() == storm::jani::ModelType::MDP) {
-//                    std::map<uint64_t, std::pair<uint64_t, storm::dd::Add<Type, ValueType>>> actionIndexToUsedVariablesAndDd;
-//                    
-//                    // Combine the edges of each action individually and keep track of how many local nondeterminism variables
-//                    // were used.
-//                    uint64_t highestNumberOfUsedNondeterminismVariables = 0;
-//                    for (auto& action : automatonDd.actionIndexToEdges) {
-//                        std::pair<uint64_t, storm::dd::Add<Type, ValueType>> usedVariablesAndDd = combineEdgesByNondeterministicChoice(action.second);
-//                        actionIndexToUsedVariablesAndDd.emplace(action.first, usedVariablesAndDd);
-//                        highestNumberOfUsedNondeterminismVariables = std::max(highestNumberOfUsedNondeterminismVariables, usedVariablesAndDd.first);
-//                    }
-//                    
-//                    storm::dd::Add<Type, ValueType> result = this->variables.manager->template getAddZero<ValueType>();
-//                    for (auto const& element : actionIndexToUsedVariablesAndDd) {
-//                        result += element.second.second * encodeAction(element.first != this->model.getSilentActionIndex() ? boost::optional<uint64_t>(element.first) : boost::none, this->variables) * encodeIndex(0, element.second.first, highestNumberOfUsedNondeterminismVariables - element.second.first, this->variables);
-//                    }
-//                    
-//                    return ComposerResult<Type, ValueType>(result, computeIllegalFragmentFromEdges(automatonDd.actionIndexToEdges), highestNumberOfUsedNondeterminismVariables);
-//                } else if (this->model.getModelType() == storm::jani::ModelType::DTMC || this->model.getModelType() == storm::jani::ModelType::CTMC) {
-//                    storm::dd::Add<Type, ValueType> result = this->variables.manager->template getAddZero<ValueType>();
-//                    for (auto const& action : automatonDd.actionIndexToEdges) {
-//                        result += combineEdgesBySummation(action.second, this->variables);
-//                    }
-//                    return ComposerResult<Type, ValueType>(result, computeIllegalFragmentFromEdges(automatonDd.actionIndexToEdges), 0);
-//                }
-//                
-//                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Illegal model type.");
-//            }
-//            
-//            storm::dd::Add<Type, ValueType> computeMissingGlobalVariableIdentities(EdgeDd const& edge, CompositionVariables<Type, ValueType> const& variables) {
-//                std::set<storm::expressions::Variable> missingIdentities;
-//                std::set_difference(variables.allGlobalVariables.begin(), variables.allGlobalVariables.end(), edge.writtenGlobalVariables.begin(), edge.writtenGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin()));
-//                storm::dd::Add<Type, ValueType> identityEncoding = variables.manager->template getAddOne<ValueType>();
-//                for (auto const& variable : missingIdentities) {
-//                    identityEncoding *= variables.variableToIdentityMap.at(variable);
-//                }
-//                return identityEncoding;
-//            }
-//            
-//            EdgeDd extendEdgeWithIdentity(EdgeDd const& edge, storm::dd::Add<Type, ValueType> const& identity) {
-//                EdgeDd result(edge);
-//                result.transitions *= identity;
-//                return result;
-//            }
-//            
-//            EdgeDd composeEdgesInParallel(EdgeDd const& edge1, EdgeDd const& edge2) {
-//                EdgeDd result;
-//                
-//                // Compose the guards.
-//                result.guard = edge1.guard * edge2.guard;
-//                
-//                // If the composed guard is already zero, we can immediately return an empty result.
-//                if (result.guard.isZero()) {
-//                    result.transitions = edge1.transitions.getDdManager().template getAddZero<ValueType>();
-//                    return result;
-//                }
-//                
-//                // Compute the set of variables written multiple times by the composition.
-//                std::set<storm::expressions::Variable> oldVariablesWrittenMultipleTimes;
-//                std::set_union(edge1.globalVariablesWrittenMultipleTimes.begin(), edge1.globalVariablesWrittenMultipleTimes.end(), edge2.globalVariablesWrittenMultipleTimes.begin(), edge2.globalVariablesWrittenMultipleTimes.end(), std::inserter(oldVariablesWrittenMultipleTimes, oldVariablesWrittenMultipleTimes.begin()));
-//                
-//                std::set<storm::expressions::Variable> newVariablesWrittenMultipleTimes;
-//                std::set_intersection(edge1.writtenGlobalVariables.begin(), edge1.writtenGlobalVariables.end(), edge2.writtenGlobalVariables.begin(), edge2.writtenGlobalVariables.end(), std::inserter(newVariablesWrittenMultipleTimes, newVariablesWrittenMultipleTimes.begin()));
-//                
-//                std::set<storm::expressions::Variable> variablesWrittenMultipleTimes;
-//                std::set_union(oldVariablesWrittenMultipleTimes.begin(), oldVariablesWrittenMultipleTimes.end(), newVariablesWrittenMultipleTimes.begin(), newVariablesWrittenMultipleTimes.end(), std::inserter(variablesWrittenMultipleTimes, variablesWrittenMultipleTimes.begin()));
-//                
-//                result.globalVariablesWrittenMultipleTimes = std::move(variablesWrittenMultipleTimes);
-//                
-//                // Compute the set of variables written by the composition.
-//                std::set<storm::expressions::Variable> variablesWritten;
-//                std::set_union(edge1.writtenGlobalVariables.begin(), edge1.writtenGlobalVariables.end(), edge2.writtenGlobalVariables.begin(), edge2.writtenGlobalVariables.end(), std::inserter(variablesWritten, variablesWritten.begin()));
-//                
-//                result.writtenGlobalVariables = variablesWritten;
-//                
-//                // Compose the guards.
-//                result.guard = edge1.guard * edge2.guard;
-//                
-//                // Compose the transitions.
-//                result.transitions = edge1.transitions * edge2.transitions;
-//                
-//                return result;
-//            }
-//            
-//            /*!
-//             * Builds the DD for the given edge.
-//             */
-//            EdgeDd buildEdgeDd(storm::jani::Automaton const& automaton, storm::jani::Edge const& edge) {
-//                STORM_LOG_TRACE("Translating guard " << edge.getGuard());
-//                storm::dd::Add<Type, ValueType> guard = this->variables.rowExpressionAdapter->translateExpression(edge.getGuard());// * this->variables.automatonToRangeMap.at(automaton.getName());
-//                STORM_LOG_WARN_COND(!guard.isZero(), "The guard '" << edge.getGuard() << "' is unsatisfiable.");
-//                
-//                if (!guard.isZero()) {
-//                    // Create the DDs representing the individual updates.
-//                    std::vector<EdgeDestinationDd<Type, ValueType>> destinationDds;
-//                    for (storm::jani::EdgeDestination const& destination : edge.getDestinations()) {
-//                        destinationDds.push_back(buildEdgeDestinationDd(automaton, destination, guard, this->variables));
-//                        
-//                        STORM_LOG_WARN_COND(!destinationDds.back().transitions.isZero(), "Destination does not have any effect.");
-//                    }
-//
-//                    // Start by gathering all variables that were written in at least one update.
-//                    std::set<storm::expressions::Variable> globalVariablesInSomeUpdate;
-//                    
-//                    // If the edge is not labeled with the silent action, we have to analyze which portion of the global
-//                    // variables was written by any of the updates and make all update results equal w.r.t. this set. If
-//                    // the edge is labeled with the silent action, we can already multiply the identities of all global variables.
-//                    if (edge.getActionIndex() != this->model.getSilentActionIndex()) {
-//                        for (auto const& edgeDestinationDd : destinationDds) {
-//                            globalVariablesInSomeUpdate.insert(edgeDestinationDd.writtenGlobalVariables.begin(), edgeDestinationDd.writtenGlobalVariables.end());
-//                        }
-//                    } else {
-//                        globalVariablesInSomeUpdate = this->variables.allGlobalVariables;
-//                    }
-//                    
-//                    // Then, multiply the missing identities.
-//                    for (auto& destinationDd : destinationDds) {
-//                        std::set<storm::expressions::Variable> missingIdentities;
-//                        std::set_difference(globalVariablesInSomeUpdate.begin(), globalVariablesInSomeUpdate.end(), destinationDd.writtenGlobalVariables.begin(), destinationDd.writtenGlobalVariables.end(), std::inserter(missingIdentities, missingIdentities.begin()));
-//                        
-//                        for (auto const& variable : missingIdentities) {
-//                            STORM_LOG_TRACE("Multiplying identity for variable " << variable.getName() << " to destination DD.");
-//                            destinationDd.transitions *= this->variables.variableToIdentityMap.at(variable);
-//                        }
-//                    }
-//                    
-//                    // Now combine the destination DDs to the edge DD.
-//                    storm::dd::Add<Type, ValueType> transitions = this->variables.manager->template getAddZero<ValueType>();
-//                    for (auto const& destinationDd : destinationDds) {
-//                        transitions += destinationDd.transitions;
-//                    }
-//                    
-//                    // Add the source location and the guard.
-//                    transitions *= this->variables.manager->getEncoding(this->variables.automatonToLocationVariableMap.at(automaton.getName()).first, edge.getSourceLocationIndex()).template toAdd<ValueType>() * guard;
-//                    
-//                    // If we multiply the ranges of global variables, make sure everything stays within its bounds.
-//                    if (!globalVariablesInSomeUpdate.empty()) {
-//                        transitions *= this->variables.globalVariableRanges;
-//                    }
-//                    
-//                    // If the edge has a rate, we multiply it to the DD.
-//                    if (edge.hasRate()) {
-//                        transitions *= this->variables.rowExpressionAdapter->translateExpression(edge.getRate());
-//                    }
-//                    return EdgeDd(guard, transitions, globalVariablesInSomeUpdate);
-//                } else {
-//                    return EdgeDd(this->variables.manager->template getAddZero<ValueType>(), this->variables.manager->template getAddZero<ValueType>());
-//                }
-//            }
-//            
-//            /*!
-//             * Builds the DD for the automaton with the given name.
-//             */
-//            AutomatonDd buildAutomatonDd(std::string const& automatonName) {
-//                AutomatonDd result(this->variables.automatonToIdentityMap.at(automatonName));
-//                
-//                storm::jani::Automaton const& automaton = this->model.getAutomaton(automatonName);
-//                for (auto const& edge : automaton.getEdges()) {
-//                    // Build the edge and add it if it adds transitions.
-//                    EdgeDd edgeDd = buildEdgeDd(automaton, edge);
-//                    if (!edgeDd.guard.isZero()) {
-//                        result.actionIndexToEdges[edge.getActionIndex()].push_back(edgeDd);
-//                    }
-//                }
-//                
-//                return result;
-//            }
-//        };
-        
+                
         template <storm::dd::DdType Type, typename ValueType>
         class CombinedEdgesSystemComposer : public SystemComposer<Type, ValueType> {
         public:
@@ -1069,39 +634,6 @@ namespace storm {
                 return buildAutomatonDd(composition.getAutomatonName(), actionIndexToLocalNondeterminismVariableOffset);
             }
             
-            boost::any visit(storm::jani::RenameComposition const& composition, boost::any const& data) override {
-                // Build a mapping from indices to indices for the renaming.
-                std::map<uint64_t, uint64_t> renamingIndexToIndex;
-                for (auto const& entry : composition.getRenaming()) {
-                    if (actionInformation.getActionIndex(entry.first) != this->model.getSilentActionIndex()) {
-                        // Distinguish the cases where we hide the action or properly rename it.
-                        if (entry.second) {
-                            renamingIndexToIndex.emplace(actionInformation.getActionIndex(entry.first), actionInformation.getActionIndex(entry.second.get()));
-                        } else {
-                            renamingIndexToIndex.emplace(actionInformation.getActionIndex(entry.first), this->model.getSilentActionIndex());
-                        }
-                    } else {
-                        STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Renaming composition must not rename the silent action.");
-                    }
-                }
-                
-                // Prepare the new offset mapping.
-                std::map<uint64_t, uint64_t> const& actionIndexToLocalNondeterminismVariableOffset = boost::any_cast<std::map<uint64_t, uint64_t> const&>(data);
-                std::map<uint64_t, uint64_t> newSynchronizingActionToOffsetMap = actionIndexToLocalNondeterminismVariableOffset;
-                for (auto const& indexPair : renamingIndexToIndex) {
-                    // FIXME: Check correct? Introduce zero if not contained?
-                    auto it = actionIndexToLocalNondeterminismVariableOffset.find(indexPair.second);
-                    STORM_LOG_THROW(it != actionIndexToLocalNondeterminismVariableOffset.end(), storm::exceptions::InvalidArgumentException, "Invalid action index " << indexPair.second << ".");
-                    newSynchronizingActionToOffsetMap[indexPair.first] = it->second;
-                }
-                
-                // Then, we translate the subcomposition.
-                AutomatonDd subautomaton = boost::any_cast<AutomatonDd>(composition.getSubcomposition().accept(*this, newSynchronizingActionToOffsetMap));
-
-                // Now perform the renaming and return result.
-                return rename(subautomaton, renamingIndexToIndex);
-            }
-            
             boost::any visit(storm::jani::ParallelComposition const& composition, boost::any const& data) override {
                 std::map<uint64_t, uint64_t> const& actionIndexToLocalNondeterminismVariableOffset = boost::any_cast<std::map<uint64_t, uint64_t> const&>(data);
                 
@@ -1379,37 +911,6 @@ namespace storm {
                 }
             }
             
-            AutomatonDd rename(AutomatonDd const& automaton, std::map<uint64_t, uint64_t> const& indexToIndex) {
-                AutomatonDd result(automaton.identity, automaton.transientLocationAssignments);
-                
-                for (auto const& action : automaton.actionIndexToAction) {
-                    auto renamingIt = indexToIndex.find(action.first);
-                    if (renamingIt != indexToIndex.end()) {
-                        // If the action is to be renamed and an action with the target index already exists, we need
-                        // to combine the action DDs.
-                        auto itNewActions = result.actionIndexToAction.find(renamingIt->second);
-                        if (itNewActions != result.actionIndexToAction.end()) {
-                            itNewActions->second = combineUnsynchronizedActions(action.second, itNewActions->second);
-                        } else {
-                            // In this case, we can simply copy the action over.
-                            result.actionIndexToAction[renamingIt->second] = action.second;
-                        }
-                    } else {
-                        // If the action is not to be renamed, we need to copy it over. However, if some other action
-                        // was renamed to the very same action name before, we need to combine the transitions.
-                        auto itNewActions = result.actionIndexToAction.find(action.first);
-                        if (itNewActions != result.actionIndexToAction.end()) {
-                            itNewActions->second = combineUnsynchronizedActions(action.second, itNewActions->second);
-                        } else {
-                            // In this case, we can simply copy the action over.
-                            result.actionIndexToAction[action.first] = action.second;
-                        }
-                    }
-                }
-                
-                return result;
-            }
-            
             void performTransientAssignments(storm::jani::detail::ConstAssignments const& transientAssignments, std::function<void (storm::jani::Assignment const&)> const& callback) {
                 auto transientVariableIt = this->transientVariables.begin();
                 auto transientVariableIte = this->transientVariables.end();
diff --git a/src/generator/JaniNextStateGenerator.cpp b/src/generator/JaniNextStateGenerator.cpp
index 384a37a33..59d0eab9b 100644
--- a/src/generator/JaniNextStateGenerator.cpp
+++ b/src/generator/JaniNextStateGenerator.cpp
@@ -23,7 +23,7 @@ namespace storm {
         
         template<typename ValueType, typename StateType>
         JaniNextStateGenerator<ValueType, StateType>::JaniNextStateGenerator(storm::jani::Model const& model, NextStateGeneratorOptions const& options, bool flag) : NextStateGenerator<ValueType, StateType>(model.getExpressionManager(), options), model(model), rewardVariables(), hasStateActionRewards(false) {
-            STORM_LOG_THROW(model.hasDefaultComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions.");
+            STORM_LOG_THROW(model.hasStandardComposition(), storm::exceptions::WrongFormatException, "The explicit next-state generator currently does not support custom system compositions.");
             STORM_LOG_THROW(!model.hasNonGlobalTransientVariable(), storm::exceptions::InvalidSettingsException, "The explicit next-state generator currently does not support automata-local transient variables.");
             STORM_LOG_THROW(!this->options.isBuildChoiceLabelsSet(), storm::exceptions::InvalidSettingsException, "JANI next-state generator cannot generate choice labels.");
             
diff --git a/src/storage/jani/Composition.cpp b/src/storage/jani/Composition.cpp
index 7059c7c85..7ba39eaba 100644
--- a/src/storage/jani/Composition.cpp
+++ b/src/storage/jani/Composition.cpp
@@ -9,4 +9,4 @@ namespace storm {
         }
         
     }
-}
\ No newline at end of file
+}
diff --git a/src/storage/jani/Composition.h b/src/storage/jani/Composition.h
index e1f1f85b6..4af139349 100644
--- a/src/storage/jani/Composition.h
+++ b/src/storage/jani/Composition.h
@@ -15,6 +15,6 @@ namespace storm {
             
             friend std::ostream& operator<<(std::ostream& stream, Composition const& composition);
         };
-        
+                
     }
-}
\ No newline at end of file
+}
diff --git a/src/storage/jani/CompositionActionInformationVisitor.cpp b/src/storage/jani/CompositionActionInformationVisitor.cpp
index 9a98a5d1f..5b6f42a6f 100644
--- a/src/storage/jani/CompositionActionInformationVisitor.cpp
+++ b/src/storage/jani/CompositionActionInformationVisitor.cpp
@@ -56,33 +56,6 @@ namespace storm {
             return result;
         }
         
-        boost::any CompositionActionInformationVisitor::visit(RenameComposition const& composition, boost::any const& data) {
-            std::set<uint64_t> usedActions = boost::any_cast<std::set<uint64_t>>(composition.getSubcomposition().accept(*this, boost::none));
-            
-            std::set<uint64_t> newUsedActions;
-            for (auto const& index : usedActions) {
-                auto renamingIt = composition.getRenaming().find(indexToNameMap.at(index));
-                if (renamingIt != composition.getRenaming().end()) {
-                    if (renamingIt->second) {
-                        newUsedActions.insert(addOrGetActionIndex(renamingIt->second.get()));
-
-                        auto actionIndexIt = nameToIndexMap.find(renamingIt->second.get());
-                        if (actionIndexIt != nameToIndexMap.end()) {
-                            newUsedActions.insert(actionIndexIt->second);
-                        } else {
-                            nameToIndexMap[renamingIt->second.get()] = nextFreeActionIndex;
-                            indexToNameMap[nextFreeActionIndex] = renamingIt->second.get();
-                            ++nextFreeActionIndex;
-                        }
-                    }
-                } else {
-                    newUsedActions.insert(index);
-                }
-            }
-            
-            return newUsedActions;
-        }
-        
         boost::any CompositionActionInformationVisitor::visit(ParallelComposition const& composition, boost::any const& data) {
             std::vector<std::set<uint64_t>> subresults;
             for (auto const& subcomposition : composition.getSubcompositions()) {
@@ -97,7 +70,6 @@ namespace storm {
             // Determine all actions that do not take part in synchronization vectors.
             std::set<uint64_t> result;
             for (uint64_t subresultIndex = 0; subresultIndex < subresults.size(); ++subresultIndex) {
-                
                 std::set<uint64_t> actionsInSynch;
                 std::set<uint64_t> localEffectiveSynchVectors;
                 for (uint64_t synchVectorIndex = 0; synchVectorIndex < composition.getNumberOfSynchronizationVectors(); ++synchVectorIndex) {
@@ -128,7 +100,9 @@ namespace storm {
             
             // Now add all outputs of synchronization vectors.
             for (auto const& synchVector : composition.getSynchronizationVectors()) {
-                result.insert(addOrGetActionIndex(synchVector.getOutput()));
+                if (synchVector.getOutput() != storm::jani::Model::getSilentActionName()) {
+                    result.insert(addOrGetActionIndex(synchVector.getOutput()));
+                }
             }
             
             return result;
diff --git a/src/storage/jani/CompositionActionInformationVisitor.h b/src/storage/jani/CompositionActionInformationVisitor.h
index 23b2555e3..572d481d7 100644
--- a/src/storage/jani/CompositionActionInformationVisitor.h
+++ b/src/storage/jani/CompositionActionInformationVisitor.h
@@ -33,7 +33,6 @@ namespace storm {
             ActionInformation getActionInformation(storm::jani::Composition const& composition);
             
             virtual boost::any visit(AutomatonComposition const& composition, boost::any const& data) override;
-            virtual boost::any visit(RenameComposition const& composition, boost::any const& data) override;
             virtual boost::any visit(ParallelComposition const& composition, boost::any const& data) override;
             
         private:
diff --git a/src/storage/jani/CompositionInformationVisitor.cpp b/src/storage/jani/CompositionInformationVisitor.cpp
index b07911ca6..6c65e9613 100644
--- a/src/storage/jani/CompositionInformationVisitor.cpp
+++ b/src/storage/jani/CompositionInformationVisitor.cpp
@@ -6,11 +6,11 @@
 namespace storm {
     namespace jani {
         
-        CompositionInformation::CompositionInformation() : automatonNameToMultiplicity(), nonsilentActions(), renameComposition(false), nonStandardParallelComposition(false) {
+        CompositionInformation::CompositionInformation() : automatonNameToMultiplicity(), nonsilentActions(), nonStandardParallelComposition(false) {
             // Intentionally left empty.
         }
         
-        CompositionInformation::CompositionInformation(std::map<std::string, uint64_t> const& automatonNameToMultiplicity, std::set<std::string> const& nonsilentActions, bool containsRenameComposition, bool nonStandardParallelComposition) : automatonNameToMultiplicity(automatonNameToMultiplicity), nonsilentActions(nonsilentActions), renameComposition(containsRenameComposition), nonStandardParallelComposition(nonStandardParallelComposition) {
+        CompositionInformation::CompositionInformation(std::map<std::string, uint64_t> const& automatonNameToMultiplicity, std::set<std::string> const& nonsilentActions, bool nonStandardParallelComposition) : automatonNameToMultiplicity(automatonNameToMultiplicity), nonsilentActions(nonsilentActions), nonStandardParallelComposition(nonStandardParallelComposition) {
             // Intentionally left empty.
         }
         
@@ -26,29 +26,6 @@ namespace storm {
             return nonsilentActions;
         }
         
-        std::set<std::string> CompositionInformation::renameNonsilentActions(std::set<std::string> const& nonsilentActions, std::map<std::string, boost::optional<std::string>> const& renaming) {
-            std::set<std::string> newNonsilentActions;
-            for (auto const& entry : nonsilentActions) {
-                auto it = renaming.find(entry);
-                if (it != renaming.end()) {
-                    if (it->second) {
-                        newNonsilentActions.insert(it->second.get());
-                    }
-                } else {
-                    newNonsilentActions.insert(entry);
-                }
-            }
-            return newNonsilentActions;
-        }
-        
-        void CompositionInformation::setContainsRenameComposition() {
-            renameComposition = true;
-        }
-        
-        bool CompositionInformation::containsRenameComposition() const {
-            return renameComposition;
-        }
-        
         void CompositionInformation::setContainsNonStandardParallelComposition() {
             nonStandardParallelComposition = true;
         }
@@ -87,28 +64,21 @@ namespace storm {
             return result;
         }
         
-        boost::any CompositionInformationVisitor::visit(RenameComposition const& composition, boost::any const& data) {
-            CompositionInformation subresult = boost::any_cast<CompositionInformation>(composition.getSubcomposition().accept(*this, data));
-            std::set<std::string> nonsilentActions = CompositionInformation::renameNonsilentActions(subresult.getNonsilentActions(), composition.getRenaming());
-            return CompositionInformation(subresult.getAutomatonToMultiplicityMap(), nonsilentActions, true, subresult.containsNonStandardParallelComposition());
-        }
-        
         boost::any CompositionInformationVisitor::visit(ParallelComposition const& composition, boost::any const& data) {
             std::vector<CompositionInformation> subinformation;
             
+            std::set<std::string> nonsilentSubActions;
             for (auto const& subcomposition : composition.getSubcompositions()) {
                 subinformation.push_back(boost::any_cast<CompositionInformation>(subcomposition->accept(*this, data)));
+                nonsilentSubActions.insert(subinformation.back().getNonsilentActions().begin(), subinformation.back().getNonsilentActions().end());
             }
             
             std::map<std::string, uint64_t> joinedAutomatonToMultiplicityMap;
-            bool containsRenameComposition = false;
             bool containsNonStandardParallelComposition = false;
             
             for (auto const& subinfo : subinformation) {
-                containsRenameComposition |= subinfo.containsRenameComposition();
                 containsNonStandardParallelComposition |= subinfo.containsNonStandardParallelComposition();
                 joinedAutomatonToMultiplicityMap = CompositionInformation::joinMultiplicityMaps(joinedAutomatonToMultiplicityMap, subinfo.getAutomatonToMultiplicityMap());
-                
             }
             
             // Keep track of the synchronization vectors that are effective, meaning that the subcompositions all have
@@ -124,28 +94,65 @@ namespace storm {
                 auto const& subinfo = subinformation[infoIndex];
                 
                 std::set<uint64_t> enabledSynchVectors;
-                for (auto const& nonsilentAction : subinfo.getNonsilentActions()) {
-                    bool appearsInSomeSynchVector = false;
-                    for (uint64_t synchVectorIndex = 0; synchVectorIndex < composition.getNumberOfSynchronizationVectors(); ++synchVectorIndex) {
-                        auto const& synchVector = composition.getSynchronizationVector(synchVectorIndex);
-                        if (synchVector.getInput(infoIndex) == nonsilentAction) {
-                            appearsInSomeSynchVector = true;
-                            enabledSynchVectors.insert(synchVectorIndex);
+                std::set<std::string> actionsInSynch;
+                for (uint64_t synchVectorIndex = 0; synchVectorIndex < composition.getNumberOfSynchronizationVectors(); ++synchVectorIndex) {
+                    auto const& synchVector = composition.getSynchronizationVector(synchVectorIndex);
+                    if (synchVector.getInput(infoIndex) != SynchronizationVector::getNoActionInput()) {
+                        for (auto const& nonsilentAction : subinfo.getNonsilentActions()) {
+                            if (synchVector.getInput(infoIndex) == nonsilentAction) {
+                                enabledSynchVectors.insert(synchVectorIndex);
+                                actionsInSynch.insert(nonsilentAction);
+                            }
                         }
-                    }
-                    
-                    if (!appearsInSomeSynchVector) {
-                        nonsilentActions.insert(nonsilentAction);
+                    } else {
+                        enabledSynchVectors.insert(synchVectorIndex);
                     }
                 }
                 
+                std::set_difference(subinfo.getNonsilentActions().begin(), subinfo.getNonsilentActions().end(), actionsInSynch.begin(), actionsInSynch.end(), std::inserter(nonsilentActions, nonsilentActions.begin()));
+
                 std::set<uint64_t> newEffectiveSynchVectors;
                 std::set_intersection(effectiveSynchVectors.begin(), effectiveSynchVectors.end(), enabledSynchVectors.begin(), enabledSynchVectors.end(), std::inserter(newEffectiveSynchVectors, newEffectiveSynchVectors.begin()));
                 effectiveSynchVectors = std::move(newEffectiveSynchVectors);
             }
 
-            return CompositionInformation(joinedAutomatonToMultiplicityMap, nonsilentActions, containsRenameComposition, containsNonStandardParallelComposition);
+            // Finally check whether it's a non-standard parallel composition. We do that by first constructing a set of
+            // all effective synchronization vectors and then checking whether this set is fully contained within the
+            // set of expected synchronization vectors.
+            
+            std::set<storm::jani::SynchronizationVector, storm::jani::SynchronizationVectorLexicographicalLess> synchVectorSet;
+            for (auto synchVectorIndex : effectiveSynchVectors) {
+                synchVectorSet.insert(composition.getSynchronizationVector(synchVectorIndex));
+            }
+
+            // Construct the set of expected synchronization vectors.
+            std::set<storm::jani::SynchronizationVector, storm::jani::SynchronizationVectorLexicographicalLess> expectedSynchVectorSetUnderApprox;
+            std::set<storm::jani::SynchronizationVector, storm::jani::SynchronizationVectorLexicographicalLess> expectedSynchVectorSetOverApprox;
+            for (auto action : nonsilentSubActions) {
+                std::vector<std::string> input;
+                uint64_t numberOfParticipatingAutomata = 0;
+                for (auto const& subcomposition : subinformation) {
+                    if (subcomposition.getNonsilentActions().find(action) != subcomposition.getNonsilentActions().end()) {
+                        input.push_back(action);
+                        ++numberOfParticipatingAutomata;
+                    } else {
+                        input.push_back(SynchronizationVector::getNoActionInput());
+                    }
+                }
+                
+                storm::jani::SynchronizationVector newSynchVector(input, action);
+                expectedSynchVectorSetOverApprox.insert(newSynchVector);
+                if (numberOfParticipatingAutomata > 1) {
+                    expectedSynchVectorSetUnderApprox.insert(newSynchVector);
+                }
+            }
+            
+            containsNonStandardParallelComposition |= !std::includes(expectedSynchVectorSetOverApprox.begin(), expectedSynchVectorSetOverApprox.end(), synchVectorSet.begin(), synchVectorSet.end(), SynchronizationVectorLexicographicalLess());
+
+            containsNonStandardParallelComposition |= !std::includes(synchVectorSet.begin(), synchVectorSet.end(), expectedSynchVectorSetUnderApprox.begin(), expectedSynchVectorSetUnderApprox.end(), SynchronizationVectorLexicographicalLess());
+
+            return CompositionInformation(joinedAutomatonToMultiplicityMap, nonsilentActions, containsNonStandardParallelComposition);
         }
         
     }
-}
\ No newline at end of file
+}
diff --git a/src/storage/jani/CompositionInformationVisitor.h b/src/storage/jani/CompositionInformationVisitor.h
index 786078e2e..804fa3ba0 100644
--- a/src/storage/jani/CompositionInformationVisitor.h
+++ b/src/storage/jani/CompositionInformationVisitor.h
@@ -16,16 +16,12 @@ namespace storm {
         class CompositionInformation {
         public:
             CompositionInformation();
-            CompositionInformation(std::map<std::string, uint64_t> const& automatonNameToMultiplicity, std::set<std::string> const& nonsilentActions, bool containsRenaming, bool nonStandardParallelComposition);
+            CompositionInformation(std::map<std::string, uint64_t> const& automatonNameToMultiplicity, std::set<std::string> const& nonsilentActions, bool nonStandardParallelComposition);
 
             void increaseAutomatonMultiplicity(std::string const& automatonName, uint64_t count = 1);
             
             void addNonsilentAction(std::string const& actionName);
             std::set<std::string> const& getNonsilentActions() const;
-            static std::set<std::string> renameNonsilentActions(std::set<std::string> const& nonsilentActions, std::map<std::string, boost::optional<std::string>> const& renaming);
-            
-            void setContainsRenameComposition();
-            bool containsRenameComposition() const;
             
             void setContainsNonStandardParallelComposition();
             bool containsNonStandardParallelComposition() const;
@@ -39,10 +35,7 @@ namespace storm {
             
             /// The set of non-silent actions contained in the composition.
             std::set<std::string> nonsilentActions;
-            
-            /// A flag indicating whether the composition contains a renaming composition.
-            bool renameComposition;
-            
+                        
             /// A flag indicating whether the composition contains any non-standard parallel composition.
             bool nonStandardParallelComposition;
         };
@@ -54,9 +47,8 @@ namespace storm {
             CompositionInformation getInformation(Composition const& composition, Model const& model);
             
             virtual boost::any visit(AutomatonComposition const& composition, boost::any const& data) override;
-            virtual boost::any visit(RenameComposition const& composition, boost::any const& data) override;
             virtual boost::any visit(ParallelComposition const& composition, boost::any const& data) override;
         };
         
     }
-}
\ No newline at end of file
+}
diff --git a/src/storage/jani/CompositionVisitor.h b/src/storage/jani/CompositionVisitor.h
index d8c62a788..c346826e2 100644
--- a/src/storage/jani/CompositionVisitor.h
+++ b/src/storage/jani/CompositionVisitor.h
@@ -7,15 +7,13 @@ namespace storm {
         
         class Composition;
         class AutomatonComposition;
-        class RenameComposition;
         class ParallelComposition;
         
         class CompositionVisitor {
         public:
             virtual boost::any visit(AutomatonComposition const& composition, boost::any const& data) = 0;
-            virtual boost::any visit(RenameComposition const& composition, boost::any const& data) = 0;
             virtual boost::any visit(ParallelComposition const& composition, boost::any const& data) = 0;
         };
         
     }
-}
\ No newline at end of file
+}
diff --git a/src/storage/jani/Compositions.h b/src/storage/jani/Compositions.h
index ea74f3ac4..b32464d91 100644
--- a/src/storage/jani/Compositions.h
+++ b/src/storage/jani/Compositions.h
@@ -1,3 +1,2 @@
 #include "src/storage/jani/AutomatonComposition.h"
-#include "src/storage/jani/RenameComposition.h"
 #include "src/storage/jani/ParallelComposition.h"
diff --git a/src/storage/jani/Model.cpp b/src/storage/jani/Model.cpp
index 50603f5b9..f0a6cb9ba 100644
--- a/src/storage/jani/Model.cpp
+++ b/src/storage/jani/Model.cpp
@@ -13,7 +13,7 @@
 namespace storm {
     namespace jani {
         
-        static const std::string SILENT_ACTION_NAME = "";
+        const std::string Model::SILENT_ACTION_NAME = "";
         
         Model::Model() {
             // Intentionally left empty.
@@ -238,6 +238,7 @@ namespace storm {
                 std::string const& actionName = this->getAction(actionIndex).getName();
                 std::vector<std::string> synchVectorInputs;
                 uint64_t numberOfParticipatingAutomata = 0;
+                int i = 0;
                 for (auto const& actionIndices : automatonActionIndices) {
                     if (actionIndices.find(actionIndex) != actionIndices.end()) {
                         ++numberOfParticipatingAutomata;
@@ -245,6 +246,7 @@ namespace storm {
                     } else {
                         synchVectorInputs.push_back(storm::jani::SynchronizationVector::getNoActionInput());
                     }
+                    ++i;
                 }
                 
                 // Only add the synchronization vector if there is more than one participating automaton.
@@ -273,11 +275,7 @@ namespace storm {
             }
             return result;
         }
-        
-        std::string const& Model::getSilentActionName() const {
-            return actions[silentActionIndex].getName();
-        }
-        
+                
         uint64_t Model::getSilentActionIndex() const {
             return silentActionIndex;
         }
@@ -459,10 +457,10 @@ namespace storm {
             
         }
         
-        bool Model::hasDefaultComposition() const {
+        bool Model::hasStandardComposition() const {
             CompositionInformationVisitor visitor;
             CompositionInformation info = visitor.getInformation(this->getSystemComposition(), *this);
-            if (info.containsNonStandardParallelComposition() || info.containsRenameComposition()) {
+            if (info.containsNonStandardParallelComposition()) {
                 return false;
             }
             for (auto const& multiplicity : info.getAutomatonToMultiplicityMap()) {
@@ -515,5 +513,13 @@ namespace storm {
             return true;
         }
         
+        std::string const& Model::getSilentActionName() {
+            return Model::SILENT_ACTION_NAME;
+        }
+        
+        bool Model::isSilentAction(std::string const& name) {
+            return name == Model::SILENT_ACTION_NAME;
+        }
+
     }
 }
diff --git a/src/storage/jani/Model.h b/src/storage/jani/Model.h
index b239c7f52..f36f1842f 100644
--- a/src/storage/jani/Model.h
+++ b/src/storage/jani/Model.h
@@ -232,11 +232,6 @@ namespace storm {
              */
             std::set<std::string> getActionNames(bool includeSilent = true) const;
             
-            /*!
-             * Retrieves the name of the silent action.
-             */
-            std::string const& getSilentActionName() const;
-            
             /*!
              * Retrieves the index of the silent action.
              */
@@ -309,10 +304,10 @@ namespace storm {
             std::vector<storm::expressions::Expression> getAllRangeExpressions() const;
             
             /*!
-             * Retrieves whether this model has the default composition, that is it composes all automata in parallel
+             * Retrieves whether this model has the standard composition, that is it composes all automata in parallel
              * and synchronizes over all common actions.
              */
-            bool hasDefaultComposition() const;
+            bool hasStandardComposition() const;
             
             /*!
              * After adding all components to the model, this method has to be called. It recursively calls
@@ -333,7 +328,20 @@ namespace storm {
              */
             bool undefinedConstantsAreGraphPreserving() const;
             
+            /*!
+             * Retrieves the name of the silent action.
+             */
+            static std::string const& getSilentActionName();
+            
+            /*!
+             * Checks whether the provided action name belongs to the silent action.
+             */
+            static bool isSilentAction(std::string const& name);
+            
         private:
+            /// The name of the silent action.
+            static const std::string SILENT_ACTION_NAME;
+            
             /// The model name.
             std::string name;
             
diff --git a/src/storage/jani/ParallelComposition.cpp b/src/storage/jani/ParallelComposition.cpp
index 09573ebc7..374eee402 100644
--- a/src/storage/jani/ParallelComposition.cpp
+++ b/src/storage/jani/ParallelComposition.cpp
@@ -65,6 +65,15 @@ namespace storm {
             return boost::none;
         }
         
+        uint64_t SynchronizationVector::getPositionOfFirstParticipatingAction() const {
+            for (uint64_t result = 0; result < this->size(); ++result) {
+                if (this->getInput(result) != getNoActionInput()) {
+                    return result;
+                }
+            }
+            STORM_LOG_THROW(false, storm::exceptions::WrongFormatException, "Synchronization vector must have at least one participating action.");
+        }
+        
         bool SynchronizationVector::isNoActionInput(std::string const& action) {
             return action == noAction;
         }
@@ -83,13 +92,48 @@ namespace storm {
             return stream;
         }
         
+        bool operator==(SynchronizationVector const& vector1, SynchronizationVector const& vector2) {
+            if (vector1.getOutput() != vector2.getOutput()) {
+                return false;
+            }
+            if (vector1.getInput() != vector1.getInput()) {
+                return false;
+            }
+            return true;
+        }
+        
+        bool operator!=(SynchronizationVector const& vector1, SynchronizationVector const& vector2) {
+            return !(vector1 == vector2);
+        }
+        
+        bool SynchronizationVectorLexicographicalLess::operator()(SynchronizationVector const& vector1, SynchronizationVector const& vector2) {
+            STORM_LOG_THROW(vector1.size() == vector2.size(), storm::exceptions::WrongFormatException, "Cannot compare synchronization vectors of different size.");
+            for (uint64_t i = 0; i < vector1.size(); ++i) {
+                if (vector1.getInput(i) < vector2.getInput(i)) {
+                    return true;
+                } else if (vector1.getInput(i) > vector2.getInput(i)) {
+                    return false;
+                }
+            }
+            if (vector1.getOutput() < vector2.getOutput()) {
+                return true;
+            } else if (vector1.getOutput() > vector2.getOutput()) {
+                return false;
+            }
+            return false;
+        }
+        
+        ParallelComposition::ParallelComposition(std::shared_ptr<Composition> const& subcomposition, std::vector<SynchronizationVector> const& synchronizationVectors) : ParallelComposition(std::vector<std::shared_ptr<Composition>>{subcomposition}, synchronizationVectors) {
+            // Intentionally left empty.
+        }
+        
         ParallelComposition::ParallelComposition(std::vector<std::shared_ptr<Composition>> const& subcompositions, std::vector<SynchronizationVector> const& synchronizationVectors) : subcompositions(subcompositions), synchronizationVectors(synchronizationVectors) {
-            STORM_LOG_THROW(subcompositions.size() > 1, storm::exceptions::WrongFormatException, "At least two automata required for parallel composition.");
+            STORM_LOG_THROW(!subcompositions.empty(), storm::exceptions::WrongFormatException, "At least one automaton required for parallel composition.");
             this->checkSynchronizationVectors();
         }
         
         ParallelComposition::ParallelComposition(std::vector<std::shared_ptr<Composition>> const& subcompositions, std::set<std::string> const& synchronizationAlphabet) : subcompositions(subcompositions), synchronizationVectors() {
-            STORM_LOG_THROW(subcompositions.size() > 1, storm::exceptions::WrongFormatException, "At least two automata required for parallel composition.");
+            STORM_LOG_THROW(!subcompositions.empty(), storm::exceptions::WrongFormatException, "At least one automaton required for parallel composition.");
 
             // Manually construct the synchronization vectors for all elements of the synchronization alphabet.
             for (auto const& action : synchronizationAlphabet) {
@@ -143,6 +187,17 @@ namespace storm {
                     }
                 }
             }
+            
+            for (auto const& vector : synchronizationVectors) {
+                bool hasInput = false;
+                for (auto const& input : vector.getInput()) {
+                    if (input != SynchronizationVector::getNoActionInput()) {
+                        hasInput = true;
+                        break;
+                    }
+                }
+                STORM_LOG_THROW(hasInput, storm::exceptions::WrongFormatException, "Synchronization vector must have at least one proper input.");
+            }
         }
         
         boost::any ParallelComposition::accept(CompositionVisitor& visitor, boost::any const& data) const {
diff --git a/src/storage/jani/ParallelComposition.h b/src/storage/jani/ParallelComposition.h
index 581d6b06c..4cd62587d 100644
--- a/src/storage/jani/ParallelComposition.h
+++ b/src/storage/jani/ParallelComposition.h
@@ -18,11 +18,12 @@ namespace storm {
             
             std::size_t size() const;
             std::vector<std::string> const& getInput() const;
-            static std::string const& getNoActionInput();
             std::string const& getInput(uint64_t index) const;
             std::string const& getOutput() const;
-            static bool isNoActionInput(std::string const& action);
 
+            static std::string const& getNoActionInput();
+            static bool isNoActionInput(std::string const& action);
+            
             /*!
              * Retrieves the action name that is the last participating action before the given input index. If there is
              * no such action none is returned.
@@ -30,11 +31,16 @@ namespace storm {
             boost::optional<std::string> getPrecedingParticipatingAction(uint64_t index) const;
 
             /*!
-             * Retrieves the position with the last participating action before the given input index. If there is
+             * Retrieves the position of the last participating action before the given input index. If there is
              * no such action none is returned.
              */
             boost::optional<uint64_t> getPositionOfPrecedingParticipatingAction(uint64_t index) const;
 
+            /*!
+             * Retrieves the position of the first participating action.
+             */
+            uint64_t getPositionOfFirstParticipatingAction() const;
+
         private:
             // A marker that can be used as one of the inputs. The semantics is that no action of the corresponding
             // automaton takes part in the synchronization.
@@ -47,10 +53,22 @@ namespace storm {
             std::string output;
         };
         
+        bool operator==(SynchronizationVector const& vector1, SynchronizationVector const& vector2);
+        bool operator!=(SynchronizationVector const& vector1, SynchronizationVector const& vector2);
+        
+        struct SynchronizationVectorLexicographicalLess {
+            bool operator()(SynchronizationVector const& vector1, SynchronizationVector const& vector2);
+        };
+        
         std::ostream& operator<<(std::ostream& stream, SynchronizationVector const& synchronizationVector);
         
         class ParallelComposition : public Composition {
         public:
+            /*!
+             * Creates a parallel composition of the subcomposition and the provided synchronization vectors.
+             */
+            ParallelComposition(std::shared_ptr<Composition> const& subcomposition, std::vector<SynchronizationVector> const& synchronizationVectors);
+
             /*!
              * Creates a parallel composition of the subcompositions and the provided synchronization vectors.
              */
diff --git a/src/storage/jani/RenameComposition.cpp b/src/storage/jani/RenameComposition.cpp
deleted file mode 100644
index c54febb03..000000000
--- a/src/storage/jani/RenameComposition.cpp
+++ /dev/null
@@ -1,48 +0,0 @@
-#include "src/storage/jani/RenameComposition.h"
-
-#include <vector>
-#include <sstream>
-
-#include <boost/algorithm/string/join.hpp>
-
-namespace storm {
-    namespace jani {
-        
-        RenameComposition::RenameComposition(std::shared_ptr<Composition> const& subcomposition, std::map<std::string, boost::optional<std::string>> const& renaming) : subcomposition(subcomposition), renaming(renaming) {
-            // Intentionally left empty.
-        }
-        
-        Composition const& RenameComposition::getSubcomposition() const {
-            return *subcomposition;
-        }
-        
-        boost::any RenameComposition::accept(CompositionVisitor& visitor, boost::any const& data) const {
-            return visitor.visit(*this, data);
-        }
-        
-        std::map<std::string, boost::optional<std::string>> const& RenameComposition::getRenaming() const {
-            return renaming;
-        }
-        
-        void RenameComposition::write(std::ostream& stream) const {
-            std::vector<std::string> renamingStrings;
-            
-            for (auto const& entry : renaming) {
-                std::stringstream stream;
-                stream << entry.first << " -> ";
-                if (entry.second) {
-                    stream << entry.second.get();
-                } else {
-                    stream << "tau";
-                }
-                renamingStrings.push_back(stream.str());
-            }
-            
-            stream << "(";
-            subcomposition->write(stream);
-            stream << ")/{" << boost::join(renamingStrings, ", ") << "} ";
-        }
-
-        
-    }
-}
diff --git a/src/storage/jani/RenameComposition.h b/src/storage/jani/RenameComposition.h
deleted file mode 100644
index 169a8d738..000000000
--- a/src/storage/jani/RenameComposition.h
+++ /dev/null
@@ -1,42 +0,0 @@
-#pragma once
-
-#include <memory>
-#include <map>
-
-#include <boost/optional.hpp>
-
-#include "src/storage/jani/Composition.h"
-
-namespace storm {
-    namespace jani {
-        
-        class RenameComposition : public Composition {
-        public:
-            RenameComposition(std::shared_ptr<Composition> const& subcomposition, std::map<std::string, boost::optional<std::string>> const& renaming = {});
-            
-            /*!
-             * Retrieves the subcomposition of this rename composition.
-             */
-            Composition const& getSubcomposition() const;
-            
-            /*!
-             * Retrieves the renaming of actions. If some action name is mapped to none, this indicates the action is to
-             * be renamed to the silent action.
-             */
-            std::map<std::string, boost::optional<std::string>> const& getRenaming() const;
-            
-            virtual boost::any accept(CompositionVisitor& visitor, boost::any const& data) const override;
-            
-            virtual void write(std::ostream& stream) const override;
-            
-        private:
-            // The subcomposition.
-            std::shared_ptr<Composition> subcomposition;
-            
-            // The renaming to perform. If one cation is mapped to none, this means that the action is to be renamed to
-            // the silent action.
-            std::map<std::string, boost::optional<std::string>> renaming;
-        };
-        
-    }
-}
\ No newline at end of file
diff --git a/src/storage/prism/CompositionToJaniVisitor.cpp b/src/storage/prism/CompositionToJaniVisitor.cpp
index 0a8b1cce7..baa380e15 100644
--- a/src/storage/prism/CompositionToJaniVisitor.cpp
+++ b/src/storage/prism/CompositionToJaniVisitor.cpp
@@ -19,22 +19,20 @@ namespace storm {
         }
         
         boost::any CompositionToJaniVisitor::visit(RenamingComposition const& composition, boost::any const& data) {
-            std::map<std::string, boost::optional<std::string>> newRenaming;
+            std::vector<storm::jani::SynchronizationVector> synchronizationVectors;
             for (auto const& renamingPair : composition.getActionRenaming()) {
-                newRenaming.emplace(renamingPair.first, renamingPair.second);
+                synchronizationVectors.push_back(storm::jani::SynchronizationVector({renamingPair.first}, renamingPair.second));
             }
-            auto subcomposition = boost::any_cast<std::shared_ptr<storm::jani::Composition>>(composition.getSubcomposition().accept(*this, data));
-            std::shared_ptr<storm::jani::Composition> result = std::make_shared<storm::jani::RenameComposition>(subcomposition, newRenaming);
+            std::shared_ptr<storm::jani::Composition> result = std::make_shared<storm::jani::ParallelComposition>(boost::any_cast<std::shared_ptr<storm::jani::Composition>>(composition.getSubcomposition().accept(*this, data)), synchronizationVectors);
             return result;
         }
         
         boost::any CompositionToJaniVisitor::visit(HidingComposition const& composition, boost::any const& data) {
-            std::map<std::string, boost::optional<std::string>> newRenaming;
+            std::vector<storm::jani::SynchronizationVector> synchronizationVectors;
             for (auto const& action : composition.getActionsToHide()) {
-                newRenaming.emplace(action, boost::none);
+                synchronizationVectors.push_back(storm::jani::SynchronizationVector({action}, storm::jani::Model::getSilentActionName()));
             }
-            auto subcomposition = boost::any_cast<std::shared_ptr<storm::jani::Composition>>(composition.getSubcomposition().accept(*this, data));
-            std::shared_ptr<storm::jani::Composition> result = std::make_shared<storm::jani::RenameComposition>(subcomposition, newRenaming);
+            std::shared_ptr<storm::jani::Composition> result = std::make_shared<storm::jani::ParallelComposition>(boost::any_cast<std::shared_ptr<storm::jani::Composition>>(composition.getSubcomposition().accept(*this, data)), synchronizationVectors);
             return result;
         }