diff --git a/src/ir/Assignment.cpp b/src/ir/Assignment.cpp
index 095a922f3..232472857 100644
--- a/src/ir/Assignment.cpp
+++ b/src/ir/Assignment.cpp
@@ -24,6 +24,13 @@ Assignment::Assignment(std::string variableName, std::shared_ptr<storm::ir::expr
 	// Nothing to do here.
 }
 
+Assignment::Assignment(const Assignment& assignment, const std::map<std::string, std::string>& renaming, const std::map<std::string,uint_fast64_t>& bools, const std::map<std::string,uint_fast64_t>& ints)
+	: variableName(assignment.variableName), expression(assignment.expression->clone(renaming, bools, ints)) {
+	if (renaming.count(assignment.variableName) > 0) {
+		this->variableName = renaming.at(assignment.variableName);
+	}
+}
+
 // Returns the name of the variable associated with this assignment.
 std::string const& Assignment::getVariableName() const {
 	return variableName;
diff --git a/src/ir/Assignment.h b/src/ir/Assignment.h
index 019cc55eb..b17693bf0 100644
--- a/src/ir/Assignment.h
+++ b/src/ir/Assignment.h
@@ -33,6 +33,8 @@ public:
 	 */
 	Assignment(std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> expression);
 
+	Assignment(const Assignment& assignment, const std::map<std::string, std::string>& renaming, const std::map<std::string,uint_fast64_t>& bools, const std::map<std::string,uint_fast64_t>& ints);
+
 	/*!
 	 * Retrieves the name of the variable that this assignment targets.
 	 * @returns the name of the variable that this assignment targets.
diff --git a/src/ir/BooleanVariable.cpp b/src/ir/BooleanVariable.cpp
index b867a1aa1..4ef83a879 100644
--- a/src/ir/BooleanVariable.cpp
+++ b/src/ir/BooleanVariable.cpp
@@ -25,6 +25,9 @@ BooleanVariable::BooleanVariable(uint_fast64_t index, std::string variableName,
 	// Nothing to do here.
 }
 
+BooleanVariable::BooleanVariable(const BooleanVariable& var, const std::string& newName) : Variable(var, newName) {
+}
+
 // Build a string representation of the variable.
 std::string BooleanVariable::toString() const {
 	std::stringstream result;
diff --git a/src/ir/BooleanVariable.h b/src/ir/BooleanVariable.h
index 9c5ba17c0..fcf5ce602 100644
--- a/src/ir/BooleanVariable.h
+++ b/src/ir/BooleanVariable.h
@@ -8,10 +8,9 @@
 #ifndef STORM_IR_BOOLEANVARIABLE_H_
 #define STORM_IR_BOOLEANVARIABLE_H_
 
-#include "expressions/BooleanLiteral.h"
-
-#include "Variable.h"
+#include "src/ir/Variable.h"
 #include <memory>
+#include <map>
 
 namespace storm {
 
@@ -35,6 +34,9 @@ public:
 	 */
 	BooleanVariable(uint_fast64_t index, std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue = std::shared_ptr<storm::ir::expressions::BaseExpression>(nullptr));
 
+
+	BooleanVariable(const BooleanVariable& var, const std::string& newName);
+
 	/*!
 	 * Retrieves a string representation of this variable.
 	 * @returns a string representation of this variable.
diff --git a/src/ir/Command.cpp b/src/ir/Command.cpp
index bec67d4bf..b34ab60ed 100644
--- a/src/ir/Command.cpp
+++ b/src/ir/Command.cpp
@@ -20,10 +20,21 @@ Command::Command() : actionName(), guardExpression(), updates() {
 
 // Initializes all members according to the given values.
 Command::Command(std::string actionName, std::shared_ptr<storm::ir::expressions::BaseExpression> guardExpression, std::vector<storm::ir::Update> updates)
-		: actionName(actionName), guardExpression(guardExpression), updates(updates) {
+	: actionName(actionName), guardExpression(guardExpression), updates(updates) {
 	// Nothing to do here.
 }
 
+Command::Command(const Command& cmd, const std::map<std::string, std::string>& renaming, const std::map<std::string,uint_fast64_t>& bools, const std::map<std::string,uint_fast64_t>& ints)
+	: actionName(cmd.actionName), guardExpression(cmd.guardExpression->clone(renaming, bools, ints)) {
+	if (renaming.count(this->actionName) > 0) {
+		this->actionName = renaming.at(this->actionName);
+	}
+	this->updates.reserve(cmd.updates.size());
+	for (Update u : cmd.updates) {
+		this->updates.emplace_back(u, renaming, bools, ints);
+	}
+}
+
 // Return the action name.
 std::string const& Command::getActionName() const {
 	return this->actionName;
diff --git a/src/ir/Command.h b/src/ir/Command.h
index 9207c76f0..b4049307c 100644
--- a/src/ir/Command.h
+++ b/src/ir/Command.h
@@ -13,6 +13,7 @@
 
 #include <vector>
 #include <string>
+#include <map>
 
 namespace storm {
 
@@ -34,7 +35,8 @@ public:
 	 * @param guardExpression the expression that defines the guard of the command.
 	 */
 	Command(std::string actionName, std::shared_ptr<storm::ir::expressions::BaseExpression> guardExpression, std::vector<storm::ir::Update> updates);
-	
+
+	Command(const Command& cmd, const std::map<std::string, std::string>& renaming, const std::map<std::string,uint_fast64_t>& bools, const std::map<std::string,uint_fast64_t>& ints);
 	/*!
 	 * Retrieves the action name of this command.
 	 * @returns the action name of this command.
diff --git a/src/ir/IntegerVariable.cpp b/src/ir/IntegerVariable.cpp
index b07316b65..d96b2221b 100644
--- a/src/ir/IntegerVariable.cpp
+++ b/src/ir/IntegerVariable.cpp
@@ -27,6 +27,9 @@ IntegerVariable::IntegerVariable(uint_fast64_t index, std::string variableName,
 	}
 }
 
+IntegerVariable::IntegerVariable(const IntegerVariable& var, const std::string& newName) : Variable(var, newName) {
+}
+
 // Return lower bound for variable.
 std::shared_ptr<storm::ir::expressions::BaseExpression> IntegerVariable::getLowerBound() const {
 	return this->lowerBound;
diff --git a/src/ir/IntegerVariable.h b/src/ir/IntegerVariable.h
index a05ef1d7e..a31ece3e5 100644
--- a/src/ir/IntegerVariable.h
+++ b/src/ir/IntegerVariable.h
@@ -9,7 +9,7 @@
 #define STORM_IR_INTEGERVARIABLE_H_
 
 #include "expressions/BaseExpression.h"
-#include "Variable.h"
+#include "src/ir/Variable.h"
 #include <memory>
 
 namespace storm {
@@ -37,6 +37,8 @@ public:
 	 */
 	IntegerVariable(uint_fast64_t index, std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> lowerBound, std::shared_ptr<storm::ir::expressions::BaseExpression> upperBound, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue = std::shared_ptr<storm::ir::expressions::BaseExpression>(nullptr));
 
+	IntegerVariable(const IntegerVariable& var, const std::string& newName);
+	
 	/*!
 	 * Retrieves the lower bound for this integer variable.
 	 * @returns the lower bound for this integer variable.
diff --git a/src/ir/Module.cpp b/src/ir/Module.cpp
index 9a2337f8a..dcacfe198 100644
--- a/src/ir/Module.cpp
+++ b/src/ir/Module.cpp
@@ -10,6 +10,7 @@
 #include "src/exceptions/InvalidArgumentException.h"
 
 #include <sstream>
+#include <iostream>
 
 namespace storm {
 
@@ -30,17 +31,34 @@ Module::Module(std::string moduleName, std::vector<storm::ir::BooleanVariable> b
 	: moduleName(moduleName), booleanVariables(booleanVariables), integerVariables(integerVariables),
 	  booleanVariablesToIndexMap(booleanVariableToIndexMap),
 	  integerVariablesToIndexMap(integerVariableToIndexMap), commands(commands), actions(), actionsToCommandIndexMap() {
-	// Build actionsToCommandIndexMap
-	for (unsigned int id = 0; id < this->commands.size(); id++) {
-		std::string action = this->commands[id].getActionName();
-		if (action != "") {
-			if (this->actionsToCommandIndexMap.count(action) == 0) {
-				this->actionsToCommandIndexMap[action] = std::shared_ptr<std::set<uint_fast64_t>>(new std::set<uint_fast64_t>());
-			}
-			this->actionsToCommandIndexMap[action]->insert(id);
-			this->actions.insert(action);
-		}
-	}  
+	this->collectActions();
+}
+
+Module::Module(const Module& module, const std::string& moduleName, const std::map<std::string, std::string>& renaming, const VariableAdder& adder)
+	: moduleName(moduleName) {
+	this->booleanVariables.reserve(module.booleanVariables.size());
+	for (BooleanVariable it: module.booleanVariables) {
+		if (renaming.count(it.getName()) > 0) {
+			this->booleanVariables.emplace_back(it, renaming.at(it.getName()));
+			//this->booleanVariablesToIndexMap[renaming.at(it.getName())] = (*boolAdder)(it.getName(), it.getInitialValue());
+			this->booleanVariablesToIndexMap[renaming.at(it.getName())] = adder.addBooleanVariable(it.getName(), it.getInitialValue());
+		} else std::cerr << "ERROR: " << moduleName << "." << it.getName() << " was not renamed!" << std::endl;
+	}
+	this->integerVariables.reserve(module.integerVariables.size());
+	for (IntegerVariable it: module.integerVariables) {
+		if (renaming.count(it.getName()) > 0) {
+			this->integerVariables.emplace_back(it, renaming.at(it.getName()));
+			//this->integerVariablesToIndexMap[renaming.at(it.getName())] = (*intAdder)(it.getName(), it.getLowerBound(), it.getUpperBound(), it.getInitialValue());
+			this->integerVariablesToIndexMap[renaming.at(it.getName())] = adder.addIntegerVariable(it.getName(), it.getLowerBound(), it.getUpperBound(), it.getInitialValue());
+		} else std::cerr << "ERROR: " << moduleName << "." << it.getName() << " was not renamed!" << std::endl;
+	}
+	
+	this->commands.reserve(module.commands.size());
+	for (Command cmd: module.commands) {
+		this->commands.emplace_back(cmd, renaming, this->booleanVariablesToIndexMap, this->integerVariablesToIndexMap);
+	}
+
+	this->collectActions();
 }
 
 // Return the number of boolean variables.
@@ -125,6 +143,19 @@ std::shared_ptr<std::set<uint_fast64_t>> const Module::getCommandsByAction(std::
 	}
 }
 
+void Module::collectActions() {
+	for (unsigned int id = 0; id < this->commands.size(); id++) {
+		std::string action = this->commands[id].getActionName();
+		if (action != "") {
+			if (this->actionsToCommandIndexMap.count(action) == 0) {
+				this->actionsToCommandIndexMap[action] = std::shared_ptr<std::set<uint_fast64_t>>(new std::set<uint_fast64_t>());
+			}
+			this->actionsToCommandIndexMap[action]->insert(id);
+			this->actions.insert(action);
+		}
+	}
+}
+
 } // namespace ir
 
 } // namespace storm
diff --git a/src/ir/Module.h b/src/ir/Module.h
index 4070846f5..8991062ec 100644
--- a/src/ir/Module.h
+++ b/src/ir/Module.h
@@ -22,6 +22,11 @@ namespace storm {
 
 namespace ir {
 
+	struct VariableAdder {
+		virtual uint_fast64_t addIntegerVariable(const std::string& name, const std::shared_ptr<storm::ir::expressions::BaseExpression> lower, const std::shared_ptr<storm::ir::expressions::BaseExpression> upper, const std::shared_ptr<storm::ir::expressions::BaseExpression> init) const = 0;
+		virtual uint_fast64_t addBooleanVariable(const std::string& name, const std::shared_ptr<storm::ir::expressions::BaseExpression> init) const = 0;
+	};
+
 /*!
  * A class representing a module.
  */
@@ -45,6 +50,18 @@ public:
 			std::map<std::string, uint_fast64_t> integerVariableToIndexMap,
 			std::vector<storm::ir::Command> commands);
 
+	typedef uint_fast64_t (*addIntegerVariablePtr)(const std::string& name, const std::shared_ptr<storm::ir::expressions::BaseExpression> lower, const std::shared_ptr<storm::ir::expressions::BaseExpression> upper, const std::shared_ptr<storm::ir::expressions::BaseExpression> init);
+	typedef uint_fast64_t (*addBooleanVariablePtr)(const std::string& name, const std::shared_ptr<storm::ir::expressions::BaseExpression> init);
+	
+	/*!
+	 * Special copy constructor, implementing the module renaming functionality.
+	 * This will create a new module having all identifier renamed according to the given map.
+	 * @param module Module to be copied.
+	 * @param moduleName Name of the new module.
+	 * @param renaming Renaming map.
+	 */
+	Module(const Module& module, const std::string& moduleName, const std::map<std::string, std::string>& renaming, const VariableAdder& adder);
+
 	/*!
 	 * Retrieves the number of boolean variables in the module.
 	 * @returns the number of boolean variables in the module.
@@ -116,6 +133,9 @@ public:
 	std::shared_ptr<std::set<uint_fast64_t>> const getCommandsByAction(std::string const& action) const;
 
 private:
+
+	void collectActions();
+
 	// The name of the module.
 	std::string moduleName;
 
@@ -137,7 +157,7 @@ private:
 	// The set of actions present in this module.
 	std::set<std::string> actions;
 	
-	// A map of actions to the set of commands labelled with this action.
+	// A map of actions to the set of commands labeled with this action.
 	std::map<std::string, std::shared_ptr<std::set<uint_fast64_t>>> actionsToCommandIndexMap;
 };
 
diff --git a/src/ir/Update.cpp b/src/ir/Update.cpp
index edacb6fe9..2d0dc5d2a 100644
--- a/src/ir/Update.cpp
+++ b/src/ir/Update.cpp
@@ -26,6 +26,24 @@ Update::Update(std::shared_ptr<storm::ir::expressions::BaseExpression> likelihoo
 	// Nothing to do here.
 }
 
+Update::Update(const Update& update, const std::map<std::string, std::string>& renaming, const std::map<std::string,uint_fast64_t>& bools, const std::map<std::string,uint_fast64_t>& ints) {
+	for (auto it : update.booleanAssignments) {
+		if (renaming.count(it.first) > 0) {
+			this->booleanAssignments[renaming.at(it.first)] = Assignment(it.second, renaming, bools, ints);
+		} else {
+			this->booleanAssignments[it.first] = Assignment(it.second, renaming, bools, ints);
+		}
+	}
+	for (auto it : update.integerAssignments) {
+		if (renaming.count(it.first) > 0) {
+			this->integerAssignments[renaming.at(it.first)] = Assignment(it.second, renaming, bools, ints);
+		} else {
+			this->integerAssignments[it.first] = Assignment(it.second, renaming, bools, ints);
+		}
+	}
+	this->likelihoodExpression = update.likelihoodExpression->clone(renaming, bools, ints);
+}
+
 // Return the expression for the likelihood of the update.
 std::shared_ptr<storm::ir::expressions::BaseExpression> const& Update::getLikelihoodExpression() const {
 	return likelihoodExpression;
diff --git a/src/ir/Update.h b/src/ir/Update.h
index 54ddc5cd8..4ce6a2fbf 100644
--- a/src/ir/Update.h
+++ b/src/ir/Update.h
@@ -36,6 +36,8 @@ public:
 	 */
 	Update(std::shared_ptr<storm::ir::expressions::BaseExpression> likelihoodExpression, std::map<std::string, storm::ir::Assignment> booleanAssignments, std::map<std::string, storm::ir::Assignment> integerAssignments);
 
+	Update(const Update& update, const std::map<std::string, std::string>& renaming, const std::map<std::string,uint_fast64_t>& bools, const std::map<std::string,uint_fast64_t>& ints);
+
 	/*!
 	 * Retrieves the expression for the likelihood of this update.
 	 * @returns the expression for the likelihood of this update.
diff --git a/src/ir/Variable.cpp b/src/ir/Variable.cpp
index 19d7f211f..caef3aad0 100644
--- a/src/ir/Variable.cpp
+++ b/src/ir/Variable.cpp
@@ -8,6 +8,7 @@
 #include "Variable.h"
 
 #include <sstream>
+#include <map>
 
 namespace storm {
 
@@ -23,6 +24,10 @@ Variable::Variable(uint_fast64_t index, std::string variableName, std::shared_pt
 	// Nothing to do here.
 }
 
+Variable::Variable(const Variable& var, const std::string& newName) : Variable(var.index, newName, var.initialValue) {
+	// Nothing to do here
+}
+
 // Return the name of the variable.
 std::string const& Variable::getName() const {
 	return variableName;
diff --git a/src/ir/Variable.h b/src/ir/Variable.h
index 6f31280e2..2348346c3 100644
--- a/src/ir/Variable.h
+++ b/src/ir/Variable.h
@@ -35,6 +35,13 @@ public:
 	 */
 	Variable(uint_fast64_t index, std::string variableName, std::shared_ptr<storm::ir::expressions::BaseExpression> initialValue = std::shared_ptr<storm::ir::expressions::BaseExpression>());
 
+	/*!
+	 * Creates a copy of the given Variable and gives it a new name.
+	 * @param var Variable to copy.
+	 * @param newName New name of this variable.
+	 */
+	Variable(const Variable& var, const std::string& newName);
+
 	/*!
 	 * Retrieves the name of the variable.
 	 * @returns the name of the variable.
diff --git a/src/ir/expressions/BaseExpression.h b/src/ir/expressions/BaseExpression.h
index 3f93607ba..563037266 100644
--- a/src/ir/expressions/BaseExpression.h
+++ b/src/ir/expressions/BaseExpression.h
@@ -15,11 +15,11 @@
 
 #include <string>
 #include <vector>
+#include <map>
+#include <memory>
 
 namespace storm {
-
 namespace ir {
-
 namespace expressions {
 
 class BaseExpression {
@@ -39,6 +39,8 @@ public:
 
 	}
 
+	virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) = 0;
+
 	virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		if (type != int_) {
 			throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression of type '"
diff --git a/src/ir/expressions/BinaryBooleanFunctionExpression.h b/src/ir/expressions/BinaryBooleanFunctionExpression.h
index 85c927c60..dc1dc1147 100644
--- a/src/ir/expressions/BinaryBooleanFunctionExpression.h
+++ b/src/ir/expressions/BinaryBooleanFunctionExpression.h
@@ -31,6 +31,10 @@ public:
 
 	}
 
+	virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) {
+		return std::shared_ptr<BaseExpression>(new BinaryBooleanFunctionExpression(this->getLeft()->clone(renaming, bools, ints), this->getRight()->clone(renaming, bools, ints), this->functionType));
+	}
+
 	virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		bool resultLeft = this->getLeft()->getValueAsBool(variableValues);
 		bool resultRight = this->getRight()->getValueAsBool(variableValues);
diff --git a/src/ir/expressions/BinaryExpression.h b/src/ir/expressions/BinaryExpression.h
index c5b4ba9f5..de0b1d8ab 100644
--- a/src/ir/expressions/BinaryExpression.h
+++ b/src/ir/expressions/BinaryExpression.h
@@ -8,7 +8,7 @@
 #ifndef STORM_IR_EXPRESSIONS_BINARYEXPRESSION_H_
 #define STORM_IR_EXPRESSIONS_BINARYEXPRESSION_H_
 
-#include "BaseExpression.h"
+#include "src/ir/expressions/BaseExpression.h"
 #include <memory>
 
 namespace storm {
@@ -19,7 +19,8 @@ namespace expressions {
 
 class BinaryExpression : public BaseExpression {
 public:
-	BinaryExpression(ReturnType type, std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right) : BaseExpression(type), left(left), right(right) {
+	BinaryExpression(ReturnType type, std::shared_ptr<BaseExpression> left, std::shared_ptr<BaseExpression> right)
+		: BaseExpression(type), left(left), right(right) {
 
 	}
 
diff --git a/src/ir/expressions/BinaryNumericalFunctionExpression.h b/src/ir/expressions/BinaryNumericalFunctionExpression.h
index 153f4331d..49d2c9494 100644
--- a/src/ir/expressions/BinaryNumericalFunctionExpression.h
+++ b/src/ir/expressions/BinaryNumericalFunctionExpression.h
@@ -24,6 +24,10 @@ public:
 
 	}
 
+	virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) {
+		return std::shared_ptr<BaseExpression>(new BinaryNumericalFunctionExpression(this->getType(), this->getLeft()->clone(renaming, bools, ints), this->getRight()->clone(renaming, bools, ints), this->functionType));
+	}
+
 	virtual ~BinaryNumericalFunctionExpression() {
 
 	}
diff --git a/src/ir/expressions/BinaryRelationExpression.h b/src/ir/expressions/BinaryRelationExpression.h
index 1a60cd34d..38a09b179 100644
--- a/src/ir/expressions/BinaryRelationExpression.h
+++ b/src/ir/expressions/BinaryRelationExpression.h
@@ -28,6 +28,10 @@ public:
 
 	}
 
+	virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) {
+		return std::shared_ptr<BaseExpression>(new BinaryRelationExpression(this->getLeft()->clone(renaming, bools, ints), this->getRight()->clone(renaming, bools, ints), this->relationType));
+	}
+
 	virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		int_fast64_t resultLeft = this->getLeft()->getValueAsInt(variableValues);
 		int_fast64_t resultRight = this->getRight()->getValueAsInt(variableValues);
diff --git a/src/ir/expressions/BooleanConstantExpression.h b/src/ir/expressions/BooleanConstantExpression.h
index 858fe0c12..15dcd9d4b 100644
--- a/src/ir/expressions/BooleanConstantExpression.h
+++ b/src/ir/expressions/BooleanConstantExpression.h
@@ -29,6 +29,10 @@ public:
 
 	}
 
+	virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) {
+		return std::shared_ptr<BaseExpression>(this);
+	}
+
 	virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		if (!defined) {
 			throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
diff --git a/src/ir/expressions/BooleanLiteral.h b/src/ir/expressions/BooleanLiteral.h
index 04f40285f..696deb787 100644
--- a/src/ir/expressions/BooleanLiteral.h
+++ b/src/ir/expressions/BooleanLiteral.h
@@ -11,9 +11,7 @@
 #include "src/ir/expressions/BaseExpression.h"
 
 namespace storm {
-
 namespace ir {
-
 namespace expressions {
 
 class BooleanLiteral : public BaseExpression {
@@ -28,6 +26,10 @@ public:
 
 	}
 
+	virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) {
+		return std::shared_ptr<BaseExpression>(this);
+	}
+
 	virtual bool getValueAsBool(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		return value;
 	}
diff --git a/src/ir/expressions/DoubleConstantExpression.h b/src/ir/expressions/DoubleConstantExpression.h
index a027afa17..a0c31efbe 100644
--- a/src/ir/expressions/DoubleConstantExpression.h
+++ b/src/ir/expressions/DoubleConstantExpression.h
@@ -26,6 +26,10 @@ public:
 
 	}
 
+	virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) {
+		return std::shared_ptr<BaseExpression>(this);
+	}
+
 	virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		if (!defined) {
 			throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
diff --git a/src/ir/expressions/DoubleLiteral.h b/src/ir/expressions/DoubleLiteral.h
index 72c464100..efa0d1bb5 100644
--- a/src/ir/expressions/DoubleLiteral.h
+++ b/src/ir/expressions/DoubleLiteral.h
@@ -30,6 +30,10 @@ public:
 
 	}
 
+	virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) {
+		return std::shared_ptr<BaseExpression>(this);
+	}
+
 	virtual double getValueAsDouble(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		return value;
 	}
diff --git a/src/ir/expressions/IntegerConstantExpression.h b/src/ir/expressions/IntegerConstantExpression.h
index 8c58260f6..01d8f2d71 100644
--- a/src/ir/expressions/IntegerConstantExpression.h
+++ b/src/ir/expressions/IntegerConstantExpression.h
@@ -26,6 +26,10 @@ public:
 
 	}
 
+	virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) {
+		return std::shared_ptr<BaseExpression>(this);
+	}
+
 	virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		if (!defined) {
 			throw storm::exceptions::ExpressionEvaluationException() << "Cannot evaluate expression: "
diff --git a/src/ir/expressions/IntegerLiteral.h b/src/ir/expressions/IntegerLiteral.h
index a5130bd5e..8911f640a 100644
--- a/src/ir/expressions/IntegerLiteral.h
+++ b/src/ir/expressions/IntegerLiteral.h
@@ -28,6 +28,10 @@ public:
 
 	}
 
+	virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) {
+		return std::shared_ptr<BaseExpression>(this);
+	}
+
 	virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		return value;
 	}
@@ -35,7 +39,7 @@ public:
 	virtual void accept(ExpressionVisitor* visitor) {
 		visitor->visit(this);
 	}
-
+	
 	virtual std::string toString() const {
 		return boost::lexical_cast<std::string>(value);
 	}
diff --git a/src/ir/expressions/UnaryBooleanFunctionExpression.h b/src/ir/expressions/UnaryBooleanFunctionExpression.h
index 26b448548..73b9969a7 100644
--- a/src/ir/expressions/UnaryBooleanFunctionExpression.h
+++ b/src/ir/expressions/UnaryBooleanFunctionExpression.h
@@ -28,6 +28,10 @@ public:
 
 	}
 
+	virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) {
+		return std::shared_ptr<BaseExpression>(new UnaryBooleanFunctionExpression(this->getChild()->clone(renaming, bools, ints), this->functionType));
+	}
+
 	FunctionType getFunctionType() const {
 		return functionType;
 	}
diff --git a/src/ir/expressions/UnaryNumericalFunctionExpression.h b/src/ir/expressions/UnaryNumericalFunctionExpression.h
index 2a1f02125..0556892f2 100644
--- a/src/ir/expressions/UnaryNumericalFunctionExpression.h
+++ b/src/ir/expressions/UnaryNumericalFunctionExpression.h
@@ -28,6 +28,10 @@ public:
 
 	}
 
+	virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) {
+		return std::shared_ptr<BaseExpression>(new UnaryNumericalFunctionExpression(this->getType(), this->getChild()->clone(renaming, bools, ints), this->functionType));
+	}
+
 	virtual int_fast64_t getValueAsInt(std::pair<std::vector<bool>, std::vector<int_fast64_t>> const* variableValues) const {
 		if (this->getType() != int_) {
 			BaseExpression::getValueAsInt(variableValues);
diff --git a/src/ir/expressions/VariableExpression.h b/src/ir/expressions/VariableExpression.h
index 1b9dfd46b..bbdb11ea6 100644
--- a/src/ir/expressions/VariableExpression.h
+++ b/src/ir/expressions/VariableExpression.h
@@ -33,6 +33,23 @@ public:
 
 	}
 
+	virtual std::shared_ptr<BaseExpression> clone(const std::map<std::string, std::string>& renaming, const std::map<std::string, uint_fast64_t>& bools, const std::map<std::string, uint_fast64_t>& ints) {
+		if (renaming.count(this->variableName) > 0) {
+			std::string newName = renaming.at(this->variableName);
+			if (this->getType() == bool_) {
+				return std::shared_ptr<BaseExpression>(new VariableExpression(bool_, bools.at(newName), newName, this->lowerBound, this->upperBound));
+			} else if (this->getType() == int_) {
+				return std::shared_ptr<BaseExpression>(new VariableExpression(int_, ints.at(newName), newName, this->lowerBound, this->upperBound));
+			} else {
+				std::cerr << "ERROR: Renaming variable " << this->variableName << " that is neither bool nor int." << std::endl;
+				return std::shared_ptr<BaseExpression>(this);
+			}
+		} else {
+			return std::shared_ptr<BaseExpression>(this);
+		}
+	}
+
+
 	virtual void accept(ExpressionVisitor* visitor) {
 		visitor->visit(this);
 	}
diff --git a/src/parser/PrismParser.cpp b/src/parser/PrismParser.cpp
index e9bd368eb..948f32ad6 100644
--- a/src/parser/PrismParser.cpp
+++ b/src/parser/PrismParser.cpp
@@ -222,8 +222,28 @@ struct PrismParser::PrismGrammar : qi::grammar<Iterator, Program(), qi::locals<s
 		variableDefinition.name("variable declaration");
 
 		// This block defines all entities that are needed for parsing a module.
-		moduleDefinition = (qi::lit("module")[phoenix::clear(phoenix::ref(localBooleanVariables_)), phoenix::clear(phoenix::ref(localIntegerVariables_))] > freeIdentifierName > *(variableDefinition(qi::_a, qi::_b, qi::_c, qi::_d)) > +commandDefinition > qi::lit("endmodule"))[phoenix::bind(moduleNames_.add, qi::_1, qi::_1), qi::_val = phoenix::construct<Module>(qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2)];
+		moduleDefinition = (qi::lit("module")
+				[phoenix::clear(phoenix::ref(localBooleanVariables_)), phoenix::clear(phoenix::ref(localIntegerVariables_))]
+				>> freeIdentifierName >> *(variableDefinition(qi::_a, qi::_b, qi::_c, qi::_d)) > +commandDefinition > qi::lit("endmodule"))
+				[
+					phoenix::bind(moduleNames_.add, qi::_1, qi::_1),
+					qi::_val = phoenix::construct<Module>(qi::_1, qi::_a, qi::_b, qi::_c, qi::_d, qi::_2),
+					phoenix::bind(moduleMap_.add, qi::_1, qi::_val)
+				];
+
+		Module const * (qi::symbols<char, Module>::*moduleFinder)(const std::string&) const = &qi::symbols<char, Module>::find;
 		moduleDefinition.name("module");
+		moduleRenaming = (qi::lit("module")
+				[phoenix::clear(phoenix::ref(localRenamings_))]
+				>> freeIdentifierName >> qi::lit("=") > moduleNames_ > qi::lit("[") > *(
+						(identifierName > qi::lit("=") > identifierName)[phoenix::insert(phoenix::ref(localRenamings_), phoenix::construct<std::pair<std::string,std::string>>(qi::_1, qi::_2))]
+				) > qi::lit("]") > qi::lit("endmodule"))
+				[
+					phoenix::bind(moduleNames_.add, qi::_1, qi::_1),
+					qi::_val = phoenix::construct<Module>(*phoenix::bind(moduleFinder, moduleMap_, qi::_2), qi::_1, localRenamings_, VariableAdder(this)),
+					phoenix::bind(moduleMap_.add, qi::_1, qi::_val)
+
+				];
 		moduleDefinitionList %= +moduleDefinition;
 		moduleDefinitionList.name("module list");
 
@@ -268,6 +288,26 @@ struct PrismParser::PrismGrammar : qi::grammar<Iterator, Program(), qi::locals<s
 		if (keywords_.find(s) != nullptr) return false;
 		return true;
 	}
+
+	struct VariableAdder : public storm::ir::VariableAdder{
+		VariableAdder(PrismGrammar* grammar) : grammar(grammar) {};
+		PrismGrammar* grammar;
+		uint_fast64_t addIntegerVariable(const std::string& name, const std::shared_ptr<storm::ir::expressions::BaseExpression> lower, const std::shared_ptr<storm::ir::expressions::BaseExpression> upper, const std::shared_ptr<storm::ir::expressions::BaseExpression> init) const {
+			std::shared_ptr<VariableExpression> varExpr = std::shared_ptr<VariableExpression>(new VariableExpression(storm::ir::expressions::BaseExpression::int_, grammar->nextIntegerVariableIndex, name, lower, upper));
+			grammar->integerVariables_.add(name, varExpr);
+			grammar->integerVariableNames_.add(name, name);
+			grammar->nextIntegerVariableIndex++;
+			return grammar->nextIntegerVariableIndex-1;
+		}
+
+		uint_fast64_t addBooleanVariable(const std::string& name, const std::shared_ptr<storm::ir::expressions::BaseExpression> init) const {
+			std::shared_ptr<VariableExpression> varExpr = std::shared_ptr<VariableExpression>(new VariableExpression(storm::ir::expressions::BaseExpression::bool_, grammar->nextBooleanVariableIndex, name));
+			grammar->integerVariables_.add(name, varExpr);
+			grammar->integerVariableNames_.add(name, name);
+			grammar->nextBooleanVariableIndex++;
+			return grammar->nextBooleanVariableIndex-1;
+		}
+	};
 	
 	void prepareForSecondRun() {
 		// Clear constants.
@@ -317,6 +357,7 @@ struct PrismParser::PrismGrammar : qi::grammar<Iterator, Program(), qi::locals<s
 
 	// Rules for module definition.
 	qi::rule<Iterator, Module(), qi::locals<std::vector<BooleanVariable>, std::vector<IntegerVariable>, std::map<std::string, uint_fast64_t>, std::map<std::string, uint_fast64_t>>, Skipper> moduleDefinition;
+	qi::rule<Iterator, Module(), qi::locals<std::vector<BooleanVariable>, std::vector<IntegerVariable>, std::map<std::string, uint_fast64_t>, std::map<std::string, uint_fast64_t>>, Skipper> moduleRenaming;
 
 	// Rules for variable definitions.
 	qi::rule<Iterator, qi::unused_type(std::vector<BooleanVariable>&, std::vector<IntegerVariable>&, std::map<std::string, uint_fast64_t>&, std::map<std::string, uint_fast64_t>&), Skipper> variableDefinition;
@@ -469,6 +510,9 @@ struct PrismParser::PrismGrammar : qi::grammar<Iterator, Program(), qi::locals<s
 	// the intermediate representation.
 	struct qi::symbols<char, std::shared_ptr<BaseExpression>> integerVariables_, booleanVariables_;
 	struct qi::symbols<char, std::shared_ptr<BaseExpression>> integerConstants_, booleanConstants_, doubleConstants_;
+	struct qi::symbols<char, Module> moduleMap_;
+
+	std::map<std::string, std::string> localRenamings_;
 
 	// A structure representing the identity function over identifier names.
 	struct variableNamesStruct : qi::symbols<char, std::string> { } integerVariableNames_, booleanVariableNames_, commandNames_, labelNames_, allConstantNames_, moduleNames_,
diff --git a/src/parser/PrismParser.h b/src/parser/PrismParser.h
index f4a563e37..1fca04c55 100644
--- a/src/parser/PrismParser.h
+++ b/src/parser/PrismParser.h
@@ -13,6 +13,7 @@
 
 // Used for file input.
 #include <istream>
+#include <memory>
 
 namespace storm {