diff --git a/src/storm/abstraction/MenuGameRefiner.h b/src/storm/abstraction/MenuGameRefiner.h
index 3250b97ab..1157a8985 100644
--- a/src/storm/abstraction/MenuGameRefiner.h
+++ b/src/storm/abstraction/MenuGameRefiner.h
@@ -11,7 +11,7 @@
 #include "storm/abstraction/QuantitativeResultMinMax.h"
 
 #include "storm/storage/expressions/Expression.h"
-#include "storm/storage/expressions/PredicateSplitter.h"
+#include "storm/storage/expressions/FullPredicateSplitter.h"
 #include "storm/storage/expressions/EquivalenceChecker.h"
 
 #include "storm/storage/dd/DdType.h"
@@ -143,7 +143,7 @@ namespace storm {
             storm::settings::modules::AbstractionSettings::PivotSelectionHeuristic pivotSelectionHeuristic;
             
             /// An object that can be used for splitting predicates.
-            mutable storm::expressions::PredicateSplitter splitter;
+            mutable storm::expressions::FullPredicateSplitter splitter;
             
             /// An object that can be used to determine whether predicates are equivalent.
             mutable storm::expressions::EquivalenceChecker equivalenceChecker;
diff --git a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp
index d2f948d69..b35376b6b 100644
--- a/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp
+++ b/src/storm/abstraction/jani/JaniMenuGameAbstractor.cpp
@@ -32,7 +32,7 @@ namespace storm {
             using storm::settings::modules::AbstractionSettings;
             
             template <storm::dd::DdType DdType, typename ValueType>
-            JaniMenuGameAbstractor<DdType, ValueType>::JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : model(model), smtSolverFactory(smtSolverFactory), abstractionInformation(model.getManager(), model.getAllExpressionVariables(), smtSolverFactory->create(model.getManager())), automata(), initialStateAbstractor(abstractionInformation, {model.getInitialStatesExpression()}, this->smtSolverFactory), validBlockAbstractor(abstractionInformation, smtSolverFactory), currentGame(nullptr), refinementPerformed(false) {
+            JaniMenuGameAbstractor<DdType, ValueType>::JaniMenuGameAbstractor(storm::jani::Model const& model, std::shared_ptr<storm::utility::solver::SmtSolverFactory> const& smtSolverFactory) : model(model), smtSolverFactory(smtSolverFactory), abstractionInformation(model.getManager(), model.getAllExpressionVariables(), smtSolverFactory->create(model.getManager())), automata(), initialStateAbstractor(abstractionInformation, {model.getInitialStatesExpression()}, this->smtSolverFactory), validBlockAbstractor(abstractionInformation, smtSolverFactory), currentGame(nullptr), refinementPerformed(true) {
                 
                 // For now, we assume that there is a single module. If the program has more than one module, it needs
                 // to be flattened before the procedure.
diff --git a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
index a5ef4c2f5..ae6a17ab4 100644
--- a/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
+++ b/src/storm/modelchecker/abstraction/GameBasedMdpModelChecker.cpp
@@ -8,7 +8,7 @@
 #include "storm/models/symbolic/Mdp.h"
 
 #include "storm/storage/expressions/ExpressionManager.h"
-#include "storm/storage/expressions/VariableSetAbstractor.h"
+#include "storm/storage/expressions/VariableSetPredicateSplitter.h"
 
 #include "storm/storage/dd/DdManager.h"
 
@@ -78,8 +78,22 @@ namespace storm {
         template<storm::dd::DdType Type, typename ModelType>
         std::unique_ptr<CheckResult> GameBasedMdpModelChecker<Type, ModelType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) {
             storm::logic::UntilFormula const& pathFormula = checkTask.getFormula();
-            std::map<std::string, storm::expressions::Expression> labelToExpressionMapping = preprocessedModel.asPrismProgram().getLabelToExpressionMapping();
-            return performGameBasedAbstractionRefinement(checkTask.substituteFormula<storm::logic::Formula>(pathFormula), pathFormula.getLeftSubformula().toExpression(preprocessedModel.getManager(), labelToExpressionMapping), pathFormula.getRightSubformula().toExpression(preprocessedModel.getManager(), labelToExpressionMapping));
+            std::map<std::string, storm::expressions::Expression> labelToExpressionMapping;
+            if (preprocessedModel.isPrismProgram()) {
+                labelToExpressionMapping = preprocessedModel.asPrismProgram().getLabelToExpressionMapping();
+            } else {
+                storm::jani::Model const& janiModel = preprocessedModel.asJaniModel();
+                for (auto const& variable : janiModel.getGlobalVariables().getBooleanVariables()) {
+                    if (variable.isTransient()) {
+                        labelToExpressionMapping[variable.getName()] = janiModel.getLabelExpression(variable.asBooleanVariable());
+                    }
+                }
+            }
+            
+            storm::expressions::Expression constraintExpression = pathFormula.getLeftSubformula().toExpression(preprocessedModel.getManager(), labelToExpressionMapping);
+            storm::expressions::Expression targetStateExpression = pathFormula.getRightSubformula().toExpression(preprocessedModel.getManager(), labelToExpressionMapping);
+            
+            return performGameBasedAbstractionRefinement(checkTask.substituteFormula<storm::logic::Formula>(pathFormula), constraintExpression, targetStateExpression);
         }
         
         template<storm::dd::DdType Type, typename ModelType>
@@ -88,8 +102,19 @@ namespace storm {
             std::map<std::string, storm::expressions::Expression> labelToExpressionMapping;
             if (preprocessedModel.isPrismProgram()) {
                 labelToExpressionMapping = preprocessedModel.asPrismProgram().getLabelToExpressionMapping();
+            } else {
+                storm::jani::Model const& janiModel = preprocessedModel.asJaniModel();
+                for (auto const& variable : janiModel.getGlobalVariables().getBooleanVariables()) {
+                    if (variable.isTransient()) {
+                        labelToExpressionMapping[variable.getName()] = janiModel.getLabelExpression(variable.asBooleanVariable());
+                    }
+                }
             }
-            return performGameBasedAbstractionRefinement(checkTask.substituteFormula<storm::logic::Formula>(pathFormula), preprocessedModel.getManager().boolean(true), pathFormula.getSubformula().toExpression(preprocessedModel.getManager(), labelToExpressionMapping));
+            
+            storm::expressions::Expression constraintExpression = preprocessedModel.getManager().boolean(true);
+            storm::expressions::Expression targetStateExpression = pathFormula.getSubformula().toExpression(preprocessedModel.getManager(), labelToExpressionMapping);
+            
+            return performGameBasedAbstractionRefinement(checkTask.substituteFormula<storm::logic::Formula>(pathFormula), constraintExpression, targetStateExpression);
         }
         
         template<storm::dd::DdType Type, typename ValueType>
@@ -326,7 +351,7 @@ namespace storm {
                 auto iterationStart = std::chrono::high_resolution_clock::now();
                 STORM_LOG_TRACE("Starting iteration " << iterations << ".");
 
-                // (1) build initial abstraction based on the the constraint expression (if not 'true') and the target state expression.
+                // (1) build the abstraction.
                 auto abstractionStart = std::chrono::high_resolution_clock::now();
                 storm::abstraction::MenuGame<Type, ValueType> game = abstractor->abstract();
                 auto abstractionEnd = std::chrono::high_resolution_clock::now();
@@ -447,17 +472,13 @@ namespace storm {
         std::vector<storm::expressions::Expression> GameBasedMdpModelChecker<Type, ModelType>::getInitialPredicates(storm::expressions::Expression const& constraintExpression, storm::expressions::Expression const& targetStateExpression) {
             std::vector<storm::expressions::Expression> initialPredicates;
             if (preprocessedModel.isJaniModel()) {
-                storm::expressions::VariableSetAbstractor abstractor(preprocessedModel.asJaniModel().getAllLocationExpressionVariables());
+                storm::expressions::VariableSetPredicateSplitter splitter(preprocessedModel.asJaniModel().getAllLocationExpressionVariables());
 
-                storm::expressions::Expression abstractedExpression = abstractor.abstract(targetStateExpression);
-                if (abstractedExpression.isInitialized() && !abstractedExpression.isTrue() && !abstractedExpression.isFalse()) {
-                    initialPredicates.push_back(abstractedExpression);
-                }
-                
-                abstractedExpression = abstractor.abstract(constraintExpression);
-                if (abstractedExpression.isInitialized() && !abstractedExpression.isTrue() && !abstractedExpression.isFalse()) {
-                    initialPredicates.push_back(abstractedExpression);
-                }
+                std::vector<storm::expressions::Expression> splitExpressions = splitter.split(targetStateExpression);
+                initialPredicates.insert(initialPredicates.end(), splitExpressions.begin(), splitExpressions.end());
+
+                splitExpressions = splitter.split(constraintExpression);
+                initialPredicates.insert(initialPredicates.end(), splitExpressions.begin(), splitExpressions.end());
             } else {
                 if (!targetStateExpression.isTrue() && !targetStateExpression.isFalse()) {
                     initialPredicates.push_back(targetStateExpression);
diff --git a/src/storm/storage/expressions/PredicateSplitter.cpp b/src/storm/storage/expressions/FullPredicateSplitter.cpp
similarity index 55%
rename from src/storm/storage/expressions/PredicateSplitter.cpp
rename to src/storm/storage/expressions/FullPredicateSplitter.cpp
index 39ac62a6d..06b289847 100644
--- a/src/storm/storage/expressions/PredicateSplitter.cpp
+++ b/src/storm/storage/expressions/FullPredicateSplitter.cpp
@@ -1,4 +1,4 @@
-#include "storm/storage/expressions/PredicateSplitter.h"
+#include "storm/storage/expressions/FullPredicateSplitter.h"
 
 #include "storm/storage/expressions/Expression.h"
 #include "storm/storage/expressions/Expressions.h"
@@ -9,7 +9,7 @@
 namespace storm {
     namespace expressions {
         
-        std::vector<storm::expressions::Expression> PredicateSplitter::split(storm::expressions::Expression const& expression) {
+        std::vector<storm::expressions::Expression> FullPredicateSplitter::split(storm::expressions::Expression const& expression) {
             STORM_LOG_THROW(expression.hasBooleanType(), storm::exceptions::InvalidArgumentException, "Expected predicate of boolean type.");
             
             // Gather all atoms.
@@ -28,51 +28,51 @@ namespace storm {
             return atomicExpressions;
         }
         
-        boost::any PredicateSplitter::visit(IfThenElseExpression const& expression, boost::any const&) {
-            atomicExpressions.push_back(expression.shared_from_this());
+        boost::any FullPredicateSplitter::visit(IfThenElseExpression const& expression, boost::any const&) {
+            atomicExpressions.push_back(expression.toExpression());
             return boost::any();
         }
         
-        boost::any PredicateSplitter::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) {
+        boost::any FullPredicateSplitter::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) {
             expression.getFirstOperand()->accept(*this, data);
             expression.getSecondOperand()->accept(*this, data);
             return boost::any();
         }
         
-        boost::any PredicateSplitter::visit(BinaryNumericalFunctionExpression const&, boost::any const&) {
+        boost::any FullPredicateSplitter::visit(BinaryNumericalFunctionExpression const&, boost::any const&) {
             return boost::any();
         }
         
-        boost::any PredicateSplitter::visit(BinaryRelationExpression const& expression, boost::any const&) {
-            atomicExpressions.push_back(expression.shared_from_this());
+        boost::any FullPredicateSplitter::visit(BinaryRelationExpression const& expression, boost::any const&) {
+            atomicExpressions.push_back(expression.toExpression());
             return boost::any();
         }
         
-        boost::any PredicateSplitter::visit(VariableExpression const& expression, boost::any const&) {
+        boost::any FullPredicateSplitter::visit(VariableExpression const& expression, boost::any const&) {
             if (expression.hasBooleanType()) {
-                atomicExpressions.push_back(expression.shared_from_this());
+                atomicExpressions.push_back(expression.toExpression());
             }
             return boost::any();
         }
         
-        boost::any PredicateSplitter::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) {
+        boost::any FullPredicateSplitter::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) {
             expression.getOperand()->accept(*this, data);
             return boost::any();
         }
         
-        boost::any PredicateSplitter::visit(UnaryNumericalFunctionExpression const&, boost::any const&) {
+        boost::any FullPredicateSplitter::visit(UnaryNumericalFunctionExpression const&, boost::any const&) {
             return boost::any();
         }
         
-        boost::any PredicateSplitter::visit(BooleanLiteralExpression const&, boost::any const&) {
+        boost::any FullPredicateSplitter::visit(BooleanLiteralExpression const&, boost::any const&) {
             return boost::any();
         }
         
-        boost::any PredicateSplitter::visit(IntegerLiteralExpression const&, boost::any const&) {
+        boost::any FullPredicateSplitter::visit(IntegerLiteralExpression const&, boost::any const&) {
             return boost::any();
         }
         
-        boost::any PredicateSplitter::visit(RationalLiteralExpression const&, boost::any const&) {
+        boost::any FullPredicateSplitter::visit(RationalLiteralExpression const&, boost::any const&) {
             return boost::any();
         }
         
diff --git a/src/storm/storage/expressions/PredicateSplitter.h b/src/storm/storage/expressions/FullPredicateSplitter.h
similarity index 96%
rename from src/storm/storage/expressions/PredicateSplitter.h
rename to src/storm/storage/expressions/FullPredicateSplitter.h
index 5fe784a18..0b8a360f8 100644
--- a/src/storm/storage/expressions/PredicateSplitter.h
+++ b/src/storm/storage/expressions/FullPredicateSplitter.h
@@ -8,7 +8,7 @@ namespace storm {
     namespace expressions {
         class Expression;
         
-        class PredicateSplitter : public ExpressionVisitor {
+        class FullPredicateSplitter : public ExpressionVisitor {
         public:
             std::vector<storm::expressions::Expression> split(storm::expressions::Expression const& expression);
             
diff --git a/src/storm/storage/expressions/VariableSetAbstractor.cpp b/src/storm/storage/expressions/VariableSetAbstractor.cpp
deleted file mode 100644
index 5820db995..000000000
--- a/src/storm/storage/expressions/VariableSetAbstractor.cpp
+++ /dev/null
@@ -1,225 +0,0 @@
-#include "storm/storage/expressions/VariableSetAbstractor.h"
-
-#include "storm/storage/expressions/Expressions.h"
-
-#include "storm/utility/macros.h"
-#include "storm/exceptions/InvalidArgumentException.h"
-
-namespace storm {
-    namespace expressions {
-        
-        VariableSetAbstractor::VariableSetAbstractor(std::set<storm::expressions::Variable> const& variablesToAbstract) : variablesToAbstract(variablesToAbstract) {
-            // Intentionally left empty.
-        }
-        
-        storm::expressions::Expression VariableSetAbstractor::abstract(storm::expressions::Expression const& expression) {
-            std::set<storm::expressions::Variable> containedVariables = expression.getVariables();
-            bool onlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), containedVariables.begin(), containedVariables.end());
-            
-            if (onlyAbstractedVariables) {
-                return storm::expressions::Expression();
-            }
-            
-            std::set<storm::expressions::Variable> tmp;
-            std::set_intersection(containedVariables.begin(), containedVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin()));
-            bool hasAbstractedVariables = !tmp.empty();
-            
-            if (hasAbstractedVariables) {
-                return boost::any_cast<storm::expressions::Expression>(expression.accept(*this, boost::none));
-            } else {
-                return expression;
-            }
-        }
-        
-        boost::any VariableSetAbstractor::visit(IfThenElseExpression const& expression, boost::any const& data) {
-            std::set<storm::expressions::Variable> conditionVariables;
-            expression.getCondition()->gatherVariables(conditionVariables);
-            bool conditionOnlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), conditionVariables.begin(), conditionVariables.end());
-            
-            std::set<storm::expressions::Variable> tmp;
-            std::set_intersection(conditionVariables.begin(), conditionVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin()));
-            bool conditionHasAbstractedVariables = !tmp.empty();
-            
-            std::set<storm::expressions::Variable> thenVariables;
-            expression.getThenExpression()->gatherVariables(thenVariables);
-            bool thenOnlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), thenVariables.begin(), thenVariables.end());
-
-            tmp.clear();
-            std::set_intersection(thenVariables.begin(), thenVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin()));
-            bool thenHasAbstractedVariables = !tmp.empty();
-
-            std::set<storm::expressions::Variable> elseVariables;
-            expression.getElseExpression()->gatherVariables(elseVariables);
-            bool elseOnlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), elseVariables.begin(), elseVariables.end());
-
-            tmp.clear();
-            std::set_intersection(elseVariables.begin(), elseVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin()));
-            bool elseHasAbstractedVariables = !tmp.empty();
-
-            if (conditionHasAbstractedVariables || thenHasAbstractedVariables || elseHasAbstractedVariables) {
-                if (conditionOnlyAbstractedVariables && thenOnlyAbstractedVariables && elseOnlyAbstractedVariables) {
-                    return boost::any();
-                } else {
-                    STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot abstract from variable set in expression as it mixes variables of different types.");
-                }
-            } else {
-                return expression.toExpression();
-            }
-        }
-        
-        boost::any VariableSetAbstractor::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) {
-            std::set<storm::expressions::Variable> leftContainedVariables;
-            expression.getFirstOperand()->gatherVariables(leftContainedVariables);
-            bool leftOnlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), leftContainedVariables.begin(), leftContainedVariables.end());
-            
-            std::set<storm::expressions::Variable> tmp;
-            std::set_intersection(leftContainedVariables.begin(), leftContainedVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin()));
-            bool leftHasAbstractedVariables = !tmp.empty();
-            
-            std::set<storm::expressions::Variable> rightContainedVariables;
-            expression.getSecondOperand()->gatherVariables(rightContainedVariables);
-            bool rightOnlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), rightContainedVariables.begin(), rightContainedVariables.end());
-            
-            tmp.clear();
-            std::set_intersection(rightContainedVariables.begin(), rightContainedVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin()));
-            bool rightHasAbstractedVariables = !tmp.empty();
-            
-            if (leftOnlyAbstractedVariables && rightOnlyAbstractedVariables) {
-                return boost::any();
-            } else if (!leftHasAbstractedVariables && !rightHasAbstractedVariables) {
-                return expression;
-            } else {
-                if (leftHasAbstractedVariables && !rightHasAbstractedVariables) {
-                    return expression.getFirstOperand()->toExpression();
-                } else  if (rightHasAbstractedVariables && !leftHasAbstractedVariables) {
-                    return expression.getSecondOperand()->toExpression();
-                } else {
-                    storm::expressions::Expression leftResult = boost::any_cast<storm::expressions::Expression>(expression.getFirstOperand()->accept(*this, data));
-                    storm::expressions::Expression rightResult = boost::any_cast<storm::expressions::Expression>(expression.getFirstOperand()->accept(*this, data));
-                    
-                    switch (expression.getOperatorType()) {
-                        case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::And: return leftResult && rightResult;
-                        case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Or: return leftResult || rightResult;
-                        case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Xor: return leftResult ^ rightResult;
-                        case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Implies: return storm::expressions::implies(leftResult, rightResult);
-                        case storm::expressions::BinaryBooleanFunctionExpression::OperatorType::Iff: return storm::expressions::iff(leftResult, rightResult);
-                    }
-                }
-            }
-        }
-        
-        boost::any VariableSetAbstractor::visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) {
-            std::set<storm::expressions::Variable> leftContainedVariables;
-            expression.getFirstOperand()->gatherVariables(leftContainedVariables);
-            bool leftOnlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), leftContainedVariables.begin(), leftContainedVariables.end());
-            
-            std::set<storm::expressions::Variable> tmp;
-            std::set_intersection(leftContainedVariables.begin(), leftContainedVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin()));
-            bool leftHasAbstractedVariables = !tmp.empty();
-            
-            std::set<storm::expressions::Variable> rightContainedVariables;
-            expression.getSecondOperand()->gatherVariables(rightContainedVariables);
-            bool rightOnlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), rightContainedVariables.begin(), rightContainedVariables.end());
-            
-            tmp.clear();
-            std::set_intersection(rightContainedVariables.begin(), rightContainedVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin()));
-            bool rightHasAbstractedVariables = !tmp.empty();
-            
-            if (leftOnlyAbstractedVariables && rightOnlyAbstractedVariables) {
-                return boost::any();
-            } else if (!leftHasAbstractedVariables && !rightHasAbstractedVariables) {
-                return expression;
-            } else {
-                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot abstract from variable set in expression as it mixes variables of different types.");
-            }
-        }
-        
-        boost::any VariableSetAbstractor::visit(BinaryRelationExpression const& expression, boost::any const& data) {
-            std::set<storm::expressions::Variable> leftContainedVariables;
-            expression.getFirstOperand()->gatherVariables(leftContainedVariables);
-            bool leftOnlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), leftContainedVariables.begin(), leftContainedVariables.end());
-            
-            std::set<storm::expressions::Variable> tmp;
-            std::set_intersection(leftContainedVariables.begin(), leftContainedVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin()));
-            bool leftHasAbstractedVariables = !tmp.empty();
-
-            std::set<storm::expressions::Variable> rightContainedVariables;
-            expression.getSecondOperand()->gatherVariables(rightContainedVariables);
-            bool rightOnlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), rightContainedVariables.begin(), rightContainedVariables.end());
-            
-            tmp.clear();
-            std::set_intersection(rightContainedVariables.begin(), rightContainedVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin()));
-            bool rightHasAbstractedVariables = !tmp.empty();
-
-            if (leftOnlyAbstractedVariables && rightOnlyAbstractedVariables) {
-                return boost::any();
-            } else if (!leftHasAbstractedVariables && !rightHasAbstractedVariables) {
-                return expression;
-            } else {
-                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot abstract from variable set in expression as it mixes variables of different types.");
-            }
-        }
-        
-        boost::any VariableSetAbstractor::visit(VariableExpression const& expression, boost::any const& data) {
-            if (variablesToAbstract.find(expression.getVariable()) != variablesToAbstract.end()) {
-                return boost::any();
-            } else {
-                return expression.toExpression();
-            }
-        }
-        
-        boost::any VariableSetAbstractor::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) {
-            std::set<storm::expressions::Variable> containedVariables;
-            expression.gatherVariables(containedVariables);
-            bool onlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), containedVariables.begin(), containedVariables.end());
-            
-            if (onlyAbstractedVariables) {
-                return boost::any();
-            }
-            
-            std::set<storm::expressions::Variable> tmp;
-            std::set_intersection(containedVariables.begin(), containedVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin()));
-            bool hasAbstractedVariables = !tmp.empty();
-            if (hasAbstractedVariables) {
-                storm::expressions::Expression subexpression = boost::any_cast<storm::expressions::Expression>(expression.getOperand()->accept(*this, data));
-                switch (expression.getOperatorType()) {
-                    case storm::expressions::UnaryBooleanFunctionExpression::OperatorType::Not: return !subexpression;
-                }
-            } else {
-                return expression.toExpression();
-            }
-        }
-        
-        boost::any VariableSetAbstractor::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) {
-            std::set<storm::expressions::Variable> containedVariables;
-            expression.gatherVariables(containedVariables);
-            bool onlyAbstractedVariables = std::includes(variablesToAbstract.begin(), variablesToAbstract.end(), containedVariables.begin(), containedVariables.end());
-            
-            if (onlyAbstractedVariables) {
-                return boost::any();
-            }
-            
-            std::set<storm::expressions::Variable> tmp;
-            std::set_intersection(containedVariables.begin(), containedVariables.end(), variablesToAbstract.begin(), variablesToAbstract.end(), std::inserter(tmp, tmp.begin()));
-            bool hasAbstractedVariables = !tmp.empty();
-            if (hasAbstractedVariables) {
-                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Cannot abstract from variable set in expression as it mixes variables of different types.");
-            } else {
-                return expression.toExpression();
-            }
-        }
-        
-        boost::any VariableSetAbstractor::visit(BooleanLiteralExpression const& expression, boost::any const& data) {
-            return expression.toExpression();
-        }
-        
-        boost::any VariableSetAbstractor::visit(IntegerLiteralExpression const& expression, boost::any const& data) {
-            return expression.toExpression();
-        }
-        
-        boost::any VariableSetAbstractor::visit(RationalLiteralExpression const& expression, boost::any const& data) {
-            return expression.toExpression();
-        }
-        
-    }
-}
diff --git a/src/storm/storage/expressions/VariableSetPredicateSplitter.cpp b/src/storm/storage/expressions/VariableSetPredicateSplitter.cpp
new file mode 100644
index 000000000..a6906ac8a
--- /dev/null
+++ b/src/storm/storage/expressions/VariableSetPredicateSplitter.cpp
@@ -0,0 +1,180 @@
+#include "storm/storage/expressions/VariableSetPredicateSplitter.h"
+
+#include "storm/storage/expressions/Expressions.h"
+
+#include "storm/utility/macros.h"
+#include "storm/exceptions/InvalidArgumentException.h"
+
+namespace storm {
+    namespace expressions {
+        
+        VariableSetPredicateSplitter::VariableSetPredicateSplitter(std::set<storm::expressions::Variable> const& irrelevantVariables) : irrelevantVariables(irrelevantVariables) {
+            // Intentionally left empty.
+        }
+        
+        std::vector<storm::expressions::Expression> VariableSetPredicateSplitter::split(storm::expressions::Expression const& expression) {
+            STORM_LOG_THROW(expression.hasBooleanType(), storm::exceptions::InvalidArgumentException, "Expected predicate of boolean type.");
+            
+            // Gather all atoms.
+            resultPredicates.clear();
+            expression.accept(*this, boost::none);
+            
+            // Remove all boolean literals from the atoms.
+            std::vector<storm::expressions::Expression> expressionsToKeep;
+            for (auto const& atom : resultPredicates) {
+                if (!atom.isTrue() && !atom.isFalse()) {
+                    expressionsToKeep.push_back(atom);
+                }
+            }
+            resultPredicates = std::move(expressionsToKeep);
+            
+            return resultPredicates;
+        }
+        
+        boost::any VariableSetPredicateSplitter::visit(IfThenElseExpression const& expression, boost::any const& data) {
+            std::set<storm::expressions::Variable> conditionVariables;
+            expression.getCondition()->gatherVariables(conditionVariables);
+            bool conditionOnlyIrrelevantVariables = std::includes(irrelevantVariables.begin(), irrelevantVariables.end(), conditionVariables.begin(), conditionVariables.end());
+            
+            std::set<storm::expressions::Variable> tmp;
+            std::set_intersection(conditionVariables.begin(), conditionVariables.end(), irrelevantVariables.begin(), irrelevantVariables.end(), std::inserter(tmp, tmp.begin()));
+            bool conditionHasIrrelevantVariables = !tmp.empty();
+            
+            std::set<storm::expressions::Variable> thenVariables;
+            expression.getThenExpression()->gatherVariables(thenVariables);
+            bool thenOnlyIrrelevantVariables = std::includes(irrelevantVariables.begin(), irrelevantVariables.end(), thenVariables.begin(), thenVariables.end());
+
+            tmp.clear();
+            std::set_intersection(thenVariables.begin(), thenVariables.end(), irrelevantVariables.begin(), irrelevantVariables.end(), std::inserter(tmp, tmp.begin()));
+            bool thenHasIrrelevantVariables = !tmp.empty();
+
+            std::set<storm::expressions::Variable> elseVariables;
+            expression.getElseExpression()->gatherVariables(elseVariables);
+            bool elseOnlyIrrelevantVariables = std::includes(irrelevantVariables.begin(), irrelevantVariables.end(), elseVariables.begin(), elseVariables.end());
+
+            tmp.clear();
+            std::set_intersection(elseVariables.begin(), elseVariables.end(), irrelevantVariables.begin(), irrelevantVariables.end(), std::inserter(tmp, tmp.begin()));
+            bool elseHasIrrelevantVariables = !tmp.empty();
+
+            if (conditionHasIrrelevantVariables || thenHasIrrelevantVariables || elseHasIrrelevantVariables) {
+                STORM_LOG_THROW(conditionOnlyIrrelevantVariables && thenOnlyIrrelevantVariables && elseOnlyIrrelevantVariables, storm::exceptions::InvalidArgumentException, "Cannot split expression based on variable set as variables of different type are related.");
+            } else {
+                resultPredicates.push_back(expression.toExpression());
+            }
+            return boost::any();
+        }
+        
+        boost::any VariableSetPredicateSplitter::visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) {
+            std::set<storm::expressions::Variable> leftContainedVariables;
+            expression.getFirstOperand()->gatherVariables(leftContainedVariables);
+            bool leftOnlyIrrelevantVariables = std::includes(irrelevantVariables.begin(), irrelevantVariables.end(), leftContainedVariables.begin(), leftContainedVariables.end());
+            
+            std::set<storm::expressions::Variable> tmp;
+            std::set_intersection(leftContainedVariables.begin(), leftContainedVariables.end(), irrelevantVariables.begin(), irrelevantVariables.end(), std::inserter(tmp, tmp.begin()));
+            bool leftHasIrrelevantVariables = !tmp.empty();
+            
+            std::set<storm::expressions::Variable> rightContainedVariables;
+            expression.getSecondOperand()->gatherVariables(rightContainedVariables);
+            bool rightOnlyIrrelevantVariables = std::includes(irrelevantVariables.begin(), irrelevantVariables.end(), rightContainedVariables.begin(), rightContainedVariables.end());
+            
+            tmp.clear();
+            std::set_intersection(rightContainedVariables.begin(), rightContainedVariables.end(), irrelevantVariables.begin(), irrelevantVariables.end(), std::inserter(tmp, tmp.begin()));
+            bool rightHasIrrelevantVariables = !tmp.empty();
+            
+            if (leftOnlyIrrelevantVariables && rightOnlyIrrelevantVariables) {
+                return boost::any();
+            }
+            
+            if (!leftHasIrrelevantVariables && !rightHasIrrelevantVariables) {
+                resultPredicates.push_back(expression.toExpression());
+            }
+            
+            if (!leftHasIrrelevantVariables) {
+                resultPredicates.push_back(expression.getFirstOperand()->toExpression());
+            } else if (!leftOnlyIrrelevantVariables) {
+                return expression.getFirstOperand()->accept(*this, data);
+            }
+            
+            if (!rightHasIrrelevantVariables) {
+                resultPredicates.push_back(expression.getSecondOperand()->toExpression());
+            } else if (!rightOnlyIrrelevantVariables) {
+                return expression.getSecondOperand()->accept(*this, data);
+            }
+            return boost::any();
+        }
+        
+        boost::any VariableSetPredicateSplitter::visit(BinaryNumericalFunctionExpression const& expression, boost::any const& data) {
+            return boost::any();
+        }
+        
+        boost::any VariableSetPredicateSplitter::visit(BinaryRelationExpression const& expression, boost::any const& data) {
+            std::set<storm::expressions::Variable> leftContainedVariables;
+            expression.getFirstOperand()->gatherVariables(leftContainedVariables);
+            bool leftOnlyIrrelevantVariables = std::includes(irrelevantVariables.begin(), irrelevantVariables.end(), leftContainedVariables.begin(), leftContainedVariables.end());
+            
+            std::set<storm::expressions::Variable> tmp;
+            std::set_intersection(leftContainedVariables.begin(), leftContainedVariables.end(), irrelevantVariables.begin(), irrelevantVariables.end(), std::inserter(tmp, tmp.begin()));
+            bool leftHasIrrelevantVariables = !tmp.empty();
+
+            std::set<storm::expressions::Variable> rightContainedVariables;
+            expression.getSecondOperand()->gatherVariables(rightContainedVariables);
+            bool rightOnlyIrrelevantVariables = std::includes(irrelevantVariables.begin(), irrelevantVariables.end(), rightContainedVariables.begin(), rightContainedVariables.end());
+            
+            tmp.clear();
+            std::set_intersection(rightContainedVariables.begin(), rightContainedVariables.end(), irrelevantVariables.begin(), irrelevantVariables.end(), std::inserter(tmp, tmp.begin()));
+            bool rightHasIrrelevantVariables = !tmp.empty();
+
+            if (!leftHasIrrelevantVariables && !rightHasIrrelevantVariables) {
+                resultPredicates.push_back(expression.toExpression());
+            } else {
+                STORM_LOG_THROW(leftOnlyIrrelevantVariables && rightOnlyIrrelevantVariables, storm::exceptions::InvalidArgumentException, "Cannot abstract from variable set in expression as it mixes variables of different types.");
+            }
+            return boost::any();
+        }
+        
+        boost::any VariableSetPredicateSplitter::visit(VariableExpression const& expression, boost::any const& data) {
+            if (expression.hasBooleanType() && irrelevantVariables.find(expression.getVariable()) == irrelevantVariables.end()) {
+                resultPredicates.push_back(expression.toExpression());
+            }
+            return boost::any();
+        }
+        
+        boost::any VariableSetPredicateSplitter::visit(UnaryBooleanFunctionExpression const& expression, boost::any const& data) {
+            std::set<storm::expressions::Variable> containedVariables;
+            expression.gatherVariables(containedVariables);
+            bool onlyIrrelevantVariables = std::includes(irrelevantVariables.begin(), irrelevantVariables.end(), containedVariables.begin(), containedVariables.end());
+            
+            if (onlyIrrelevantVariables) {
+                return boost::any();
+            }
+            
+            std::set<storm::expressions::Variable> tmp;
+            std::set_intersection(containedVariables.begin(), containedVariables.end(), irrelevantVariables.begin(), irrelevantVariables.end(), std::inserter(tmp, tmp.begin()));
+            bool hasIrrelevantVariables = !tmp.empty();
+
+            if (hasIrrelevantVariables) {
+                expression.getOperand()->accept(*this, data);
+            } else {
+                resultPredicates.push_back(expression.toExpression());
+            }
+            return boost::any();
+        }
+        
+        boost::any VariableSetPredicateSplitter::visit(UnaryNumericalFunctionExpression const& expression, boost::any const& data) {
+            return boost::any();
+        }
+        
+        boost::any VariableSetPredicateSplitter::visit(BooleanLiteralExpression const& expression, boost::any const& data) {
+            return boost::any();
+        }
+        
+        boost::any VariableSetPredicateSplitter::visit(IntegerLiteralExpression const& expression, boost::any const& data) {
+            return boost::any();
+        }
+        
+        boost::any VariableSetPredicateSplitter::visit(RationalLiteralExpression const& expression, boost::any const& data) {
+            return boost::any();
+        }
+        
+    }
+}
diff --git a/src/storm/storage/expressions/VariableSetAbstractor.h b/src/storm/storage/expressions/VariableSetPredicateSplitter.h
similarity index 76%
rename from src/storm/storage/expressions/VariableSetAbstractor.h
rename to src/storm/storage/expressions/VariableSetPredicateSplitter.h
index e5d905598..da1b1db46 100644
--- a/src/storm/storage/expressions/VariableSetAbstractor.h
+++ b/src/storm/storage/expressions/VariableSetPredicateSplitter.h
@@ -1,6 +1,7 @@
 #pragma once
 
 #include <set>
+#include <vector>
 
 #include "storm/storage/expressions/ExpressionVisitor.h"
 
@@ -10,11 +11,11 @@ namespace storm {
         class Variable;
         class Expression;
         
-        class VariableSetAbstractor : public ExpressionVisitor {
+        class VariableSetPredicateSplitter : public ExpressionVisitor {
         public:
-            VariableSetAbstractor(std::set<storm::expressions::Variable> const& variablesToAbstract);
+            VariableSetPredicateSplitter(std::set<storm::expressions::Variable> const& irrelevantVariables);
             
-            storm::expressions::Expression abstract(storm::expressions::Expression const& expression);
+            std::vector<storm::expressions::Expression> split(storm::expressions::Expression const& expression);
             
             virtual boost::any visit(IfThenElseExpression const& expression, boost::any const& data) override;
             virtual boost::any visit(BinaryBooleanFunctionExpression const& expression, boost::any const& data) override;
@@ -28,7 +29,8 @@ namespace storm {
             virtual boost::any visit(RationalLiteralExpression const& expression, boost::any const& data) override;
             
         private:
-            std::set<storm::expressions::Variable> variablesToAbstract;
+            std::set<storm::expressions::Variable> irrelevantVariables;
+            std::vector<storm::expressions::Expression> resultPredicates;
         };
         
     }
diff --git a/src/storm/storage/jani/Automaton.cpp b/src/storm/storage/jani/Automaton.cpp
index ad6bf5c57..f3dac4889 100644
--- a/src/storm/storage/jani/Automaton.cpp
+++ b/src/storm/storage/jani/Automaton.cpp
@@ -354,10 +354,10 @@ namespace storm {
             if (!hasInitialStatesRestriction()) {
                 return false;
             }
-            if (getInitialStatesExpression().containsVariables()) {
+            if (getInitialStatesRestriction().containsVariables()) {
                 return true;
             } else {
-                return !getInitialStatesExpression().evaluateAsBool();
+                return !getInitialStatesRestriction().evaluateAsBool();
             }
         }