diff --git a/src/models/sparse/Ctmc.cpp b/src/models/sparse/Ctmc.cpp
index e495221b1..5217396ce 100644
--- a/src/models/sparse/Ctmc.cpp
+++ b/src/models/sparse/Ctmc.cpp
@@ -10,7 +10,7 @@ namespace storm {
             Ctmc<ValueType>::Ctmc(storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::models::sparse::StateLabeling const& stateLabeling,
                                   boost::optional<std::vector<ValueType>> const& optionalStateRewardVector,
                                   boost::optional<storm::storage::SparseMatrix<ValueType>> const& optionalTransitionRewardMatrix,
-                                  boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> const& optionalChoiceLabeling)
+                                  boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling)
             : DeterministicModel<ValueType>(storm::models::ModelType::Ctmc, rateMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) {
                 exitRates = createExitRateVector(this->getTransitionMatrix());
             }
@@ -19,7 +19,7 @@ namespace storm {
             Ctmc<ValueType>::Ctmc(storm::storage::SparseMatrix<ValueType>&& rateMatrix, storm::models::sparse::StateLabeling&& stateLabeling,
                                   boost::optional<std::vector<ValueType>>&& optionalStateRewardVector,
                                   boost::optional<storm::storage::SparseMatrix<ValueType>>&& optionalTransitionRewardMatrix,
-                                  boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>&& optionalChoiceLabeling)
+                                  boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling)
             : DeterministicModel<ValueType>(storm::models::ModelType::Ctmc, std::move(rateMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix), std::move(optionalChoiceLabeling)) {
                 // It is important to refer to the transition matrix here, because the given rate matrix has been move elsewhere.
                 exitRates = createExitRateVector(this->getTransitionMatrix());
diff --git a/src/models/sparse/Ctmc.h b/src/models/sparse/Ctmc.h
index 53be5048e..71e1eb074 100644
--- a/src/models/sparse/Ctmc.h
+++ b/src/models/sparse/Ctmc.h
@@ -29,7 +29,7 @@ namespace storm {
                 Ctmc(storm::storage::SparseMatrix<ValueType> const& rateMatrix, storm::models::sparse::StateLabeling const& stateLabeling,
                      boost::optional<std::vector<ValueType>> const& optionalStateRewardVector = boost::optional<std::vector<ValueType>>(),
                      boost::optional<storm::storage::SparseMatrix<ValueType>> const& optionalTransitionRewardMatrix = boost::optional<storm::storage::SparseMatrix<ValueType>>(),
-                     boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> const& optionalChoiceLabeling = boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
+                     boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling = boost::optional<std::vector<LabelSet>>());
                 
                 /*!
                  * Constructs a model by moving the given data.
@@ -43,7 +43,7 @@ namespace storm {
                 Ctmc(storm::storage::SparseMatrix<ValueType>&& rateMatrix, storm::models::sparse::StateLabeling&& stateLabeling,
                      boost::optional<std::vector<ValueType>>&& optionalStateRewardVector = boost::optional<std::vector<ValueType>>(),
                      boost::optional<storm::storage::SparseMatrix<ValueType>>&& optionalTransitionRewardMatrix = boost::optional<storm::storage::SparseMatrix<ValueType>>(),
-                     boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>&& optionalChoiceLabeling = boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
+                     boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling = boost::optional<std::vector<LabelSet>>());
                 
                 Ctmc(Ctmc<ValueType> const& ctmc) = default;
                 Ctmc& operator=(Ctmc<ValueType> const& ctmc) = default;
diff --git a/src/models/sparse/DeterministicModel.cpp b/src/models/sparse/DeterministicModel.cpp
index d24353d02..68d18ba77 100644
--- a/src/models/sparse/DeterministicModel.cpp
+++ b/src/models/sparse/DeterministicModel.cpp
@@ -11,7 +11,7 @@ namespace storm {
                                                               storm::models::sparse::StateLabeling const& stateLabeling,
                                                               boost::optional<std::vector<ValueType>> const& optionalStateRewardVector,
                                                               boost::optional<storm::storage::SparseMatrix<ValueType>> const& optionalTransitionRewardMatrix,
-                                                              boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> const& optionalChoiceLabeling)
+                                                              boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling)
             : Model<ValueType>(modelType, transitionMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) {
                 // Intentionally left empty.
             }
@@ -22,7 +22,7 @@ namespace storm {
                                                               storm::models::sparse::StateLabeling&& stateLabeling,
                                                               boost::optional<std::vector<ValueType>>&& optionalStateRewardVector,
                                                               boost::optional<storm::storage::SparseMatrix<ValueType>>&& optionalTransitionRewardMatrix,
-                                                              boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>&& optionalChoiceLabeling)
+                                                              boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling)
             : Model<ValueType>(modelType, std::move(transitionMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix), std::move(optionalChoiceLabeling)) {
                 // Intentionally left empty.
             }
diff --git a/src/models/sparse/DeterministicModel.h b/src/models/sparse/DeterministicModel.h
index 940048dc6..19ecb4a44 100644
--- a/src/models/sparse/DeterministicModel.h
+++ b/src/models/sparse/DeterministicModel.h
@@ -29,7 +29,7 @@ namespace storm {
                                    storm::models::sparse::StateLabeling const& stateLabeling,
                                    boost::optional<std::vector<ValueType>> const& optionalStateRewardVector = boost::optional<std::vector<ValueType>>(),
                                    boost::optional<storm::storage::SparseMatrix<ValueType>> const& optionalTransitionRewardMatrix = boost::optional<storm::storage::SparseMatrix<ValueType>>(),
-                                   boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> const& optionalChoiceLabeling = boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
+                                   boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling = boost::optional<std::vector<LabelSet>>());
                 
                 /*!
                  * Constructs a model by moving the given data.
@@ -46,7 +46,7 @@ namespace storm {
                                    storm::models::sparse::StateLabeling&& stateLabeling,
                                    boost::optional<std::vector<ValueType>>&& optionalStateRewardVector = boost::optional<std::vector<ValueType>>(),
                                    boost::optional<storm::storage::SparseMatrix<ValueType>>&& optionalTransitionRewardMatrix = boost::optional<storm::storage::SparseMatrix<ValueType>>(),
-                                   boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>&& optionalChoiceLabeling = boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
+                                   boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling = boost::optional<std::vector<LabelSet>>());
                 
                 DeterministicModel(DeterministicModel const& other) = default;
                 DeterministicModel& operator=(DeterministicModel const& other) = default;
diff --git a/src/models/sparse/Dtmc.cpp b/src/models/sparse/Dtmc.cpp
index d522743a3..05a67daf9 100644
--- a/src/models/sparse/Dtmc.cpp
+++ b/src/models/sparse/Dtmc.cpp
@@ -12,7 +12,7 @@ namespace storm {
                  storm::models::sparse::StateLabeling const& stateLabeling,
                  boost::optional<std::vector<ValueType>> const& optionalStateRewardVector,
                  boost::optional<storm::storage::SparseMatrix<ValueType>> const& optionalTransitionRewardMatrix,
-                 boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> const& optionalChoiceLabeling)
+                 boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling)
             : DeterministicModel<ValueType>(storm::models::ModelType::Dtmc, probabilityMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) {
                 STORM_LOG_THROW(this->checkValidityOfProbabilityMatrix(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid.");
                 STORM_LOG_THROW(!this->hasTransitionRewards() || this->getTransitionRewardMatrix().isSubmatrixOf(this->getTransitionMatrix()), storm::exceptions::InvalidArgumentException, "The transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist.");
@@ -22,7 +22,7 @@ namespace storm {
             Dtmc<ValueType>::Dtmc(storm::storage::SparseMatrix<ValueType>&& probabilityMatrix, storm::models::sparse::StateLabeling&& stateLabeling,
                  boost::optional<std::vector<ValueType>>&& optionalStateRewardVector,
                  boost::optional<storm::storage::SparseMatrix<ValueType>>&& optionalTransitionRewardMatrix,
-                 boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>&& optionalChoiceLabeling)
+                 boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling)
             : DeterministicModel<ValueType>(storm::models::ModelType::Dtmc, std::move(probabilityMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix), std::move(optionalChoiceLabeling)) {
                 STORM_LOG_THROW(this->checkValidityOfProbabilityMatrix(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid.");
                 STORM_LOG_THROW(!this->hasTransitionRewards() || this->getTransitionRewardMatrix().isSubmatrixOf(this->getTransitionMatrix()), storm::exceptions::InvalidArgumentException, "The transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist.");
@@ -41,7 +41,7 @@ namespace storm {
                 //					  	  	  	  	  	  storm::models::sparse::StateLabeling(this->getStateLabeling(), subSysStates),
                 //					  	  	  	  	  	  boost::optional<std::vector<ValueType>>(),
                 //					  	  	  	  	  	  boost::optional<storm::storage::SparseMatrix<ValueType>>(),
-                //					  	  	  	  	  	  boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
+                //					  	  	  	  	  	  boost::optional<std::vector<LabelSet>>());
                 //		}
                 //
                 //		// Does the vector have the right size?
@@ -164,16 +164,16 @@ namespace storm {
                 //			newTransitionRewards = newTransRewardsBuilder.build();
                 //		}
                 //
-                //		boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> newChoiceLabels;
+                //		boost::optional<std::vector<LabelSet>> newChoiceLabels;
                 //		if(this->hasChoiceLabeling()) {
                 //
                 //			// Get the choice label sets and move the needed values to the front.
-                //			std::vector<boost::container::flat_set<uint_fast64_t>> newChoice(this->getChoiceLabeling());
+                //			std::vector<LabelSet> newChoice(this->getChoiceLabeling());
                 //			storm::utility::vector::selectVectorValues(newChoice, subSysStates, this->getChoiceLabeling());
                 //
                 //			// Throw away all values after the last state and set the choice label set for s_b as empty.
                 //			newChoice.resize(newStateCount);
-                //			newChoice[newStateCount - 1] = boost::container::flat_set<uint_fast64_t>();
+                //			newChoice[newStateCount - 1] = LabelSet();
                 //
                 //			newChoiceLabels = newChoice;
                 //		}
diff --git a/src/models/sparse/Dtmc.h b/src/models/sparse/Dtmc.h
index 2ff6dd884..eb37c9432 100644
--- a/src/models/sparse/Dtmc.h
+++ b/src/models/sparse/Dtmc.h
@@ -27,7 +27,7 @@ namespace storm {
                      storm::models::sparse::StateLabeling const& stateLabeling,
                      boost::optional<std::vector<ValueType>> const& optionalStateRewardVector = boost::optional<std::vector<ValueType>>(),
                      boost::optional<storm::storage::SparseMatrix<ValueType>> const& optionalTransitionRewardMatrix = boost::optional<storm::storage::SparseMatrix<ValueType>>(),
-                     boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> const& optionalChoiceLabeling = boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
+                     boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling = boost::optional<std::vector<LabelSet>>());
                 
                 /*!
                  * Constructs a model by moving the given data.
@@ -41,7 +41,7 @@ namespace storm {
                 Dtmc(storm::storage::SparseMatrix<ValueType>&& probabilityMatrix, storm::models::sparse::StateLabeling&& stateLabeling,
                      boost::optional<std::vector<ValueType>>&& optionalStateRewardVector = boost::optional<std::vector<ValueType>>(),
                      boost::optional<storm::storage::SparseMatrix<ValueType>>&& optionalTransitionRewardMatrix = boost::optional<storm::storage::SparseMatrix<ValueType>>(),
-                     boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>&& optionalChoiceLabeling = boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
+                     boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling = boost::optional<std::vector<LabelSet>>());
                 
                 Dtmc(Dtmc<ValueType> const& dtmc) = default;
                 Dtmc& operator=(Dtmc<ValueType> const& dtmc) = default;
diff --git a/src/models/sparse/MarkovAutomaton.cpp b/src/models/sparse/MarkovAutomaton.cpp
index 4032452d8..d161a64f6 100644
--- a/src/models/sparse/MarkovAutomaton.cpp
+++ b/src/models/sparse/MarkovAutomaton.cpp
@@ -13,7 +13,7 @@ namespace storm {
                                                         std::vector<ValueType> const& exitRates,
                                                         boost::optional<std::vector<ValueType>> const& optionalStateRewardVector,
                                                         boost::optional<storm::storage::SparseMatrix<ValueType>> const& optionalTransitionRewardMatrix,
-                                                        boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> const& optionalChoiceLabeling)
+                                                        boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling)
             : NondeterministicModel<ValueType>(storm::models::ModelType::MarkovAutomaton, transitionMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling), markovianStates(markovianStates), exitRates(exitRates), closed(false) {
                 this->turnRatesToProbabilities();
                 STORM_LOG_THROW(!this->hasTransitionRewards() || this->getTransitionRewardMatrix().isSubmatrixOf(this->getTransitionMatrix()), storm::exceptions::InvalidArgumentException, "There are transition rewards for nonexistent transitions.");
@@ -26,7 +26,7 @@ namespace storm {
                                                         std::vector<ValueType> const& exitRates,
                                                         boost::optional<std::vector<ValueType>>&& optionalStateRewardVector,
                                                         boost::optional<storm::storage::SparseMatrix<ValueType>>&& optionalTransitionRewardMatrix,
-                                                        boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>&& optionalChoiceLabeling)
+                                                        boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling)
             : NondeterministicModel<ValueType>(storm::models::ModelType::MarkovAutomaton, std::move(transitionMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix), std::move(optionalChoiceLabeling)), markovianStates(markovianStates), exitRates(std::move(exitRates)), closed(false) {
                 this->turnRatesToProbabilities();
                 STORM_LOG_THROW(!this->hasTransitionRewards() || this->getTransitionRewardMatrix().isSubmatrixOf(this->getTransitionMatrix()), storm::exceptions::InvalidArgumentException, "There are transition rewards for nonexistent transitions.");
diff --git a/src/models/sparse/MarkovAutomaton.h b/src/models/sparse/MarkovAutomaton.h
index d051965cc..622da37b0 100644
--- a/src/models/sparse/MarkovAutomaton.h
+++ b/src/models/sparse/MarkovAutomaton.h
@@ -31,7 +31,7 @@ namespace storm {
                                 std::vector<ValueType> const& exitRates,
                                 boost::optional<std::vector<ValueType>> const& optionalStateRewardVector = boost::optional<std::vector<ValueType>>(),
                                 boost::optional<storm::storage::SparseMatrix<ValueType>> const& optionalTransitionRewardMatrix = boost::optional<storm::storage::SparseMatrix<ValueType>>(),
-                                boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> const& optionalChoiceLabeling = boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
+                                boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling = boost::optional<std::vector<LabelSet>>());
                 
                 /*!
                  * Constructs a model by moving the given data.
@@ -50,7 +50,7 @@ namespace storm {
                                 std::vector<ValueType> const& exitRates,
                                 boost::optional<std::vector<ValueType>>&& optionalStateRewardVector = boost::optional<std::vector<ValueType>>(),
                                 boost::optional<storm::storage::SparseMatrix<ValueType>>&& optionalTransitionRewardMatrix = boost::optional<storm::storage::SparseMatrix<ValueType>>(),
-                                boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>&& optionalChoiceLabeling = boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
+                                boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling = boost::optional<std::vector<LabelSet>>());
                 
                 MarkovAutomaton(MarkovAutomaton const& other) = default;
                 MarkovAutomaton& operator=(MarkovAutomaton const& other) = default;
diff --git a/src/models/sparse/Mdp.cpp b/src/models/sparse/Mdp.cpp
index f8775107b..1c8bd1b50 100644
--- a/src/models/sparse/Mdp.cpp
+++ b/src/models/sparse/Mdp.cpp
@@ -11,7 +11,7 @@ namespace storm {
                                 storm::models::sparse::StateLabeling const& stateLabeling,
                                 boost::optional<std::vector<ValueType>> const& optionalStateRewardVector,
                                 boost::optional<storm::storage::SparseMatrix<ValueType>> const& optionalTransitionRewardMatrix,
-                                boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> const& optionalChoiceLabeling)
+                                boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling)
             : NondeterministicModel<ValueType>(storm::models::ModelType::Mdp, transitionMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) {
                 STORM_LOG_THROW(this->checkValidityOfProbabilityMatrix(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid.");
                 STORM_LOG_THROW(!this->hasTransitionRewards() || this->getTransitionRewardMatrix().isSubmatrixOf(this->getTransitionMatrix()), storm::exceptions::InvalidArgumentException, "The transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist.");
@@ -23,20 +23,20 @@ namespace storm {
                                 storm::models::sparse::StateLabeling&& stateLabeling,
                                 boost::optional<std::vector<ValueType>>&& optionalStateRewardVector,
                                 boost::optional<storm::storage::SparseMatrix<ValueType>>&& optionalTransitionRewardMatrix,
-                                boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>&& optionalChoiceLabeling)
+                                boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling)
             : NondeterministicModel<ValueType>(storm::models::ModelType::Mdp, std::move(transitionMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix), std::move(optionalChoiceLabeling)) {
                 STORM_LOG_THROW(this->checkValidityOfProbabilityMatrix(), storm::exceptions::InvalidArgumentException, "The probability matrix is invalid.");
                 STORM_LOG_THROW(!this->hasTransitionRewards() || this->getTransitionRewardMatrix().isSubmatrixOf(this->getTransitionMatrix()), storm::exceptions::InvalidArgumentException, "The transition reward matrix is not a submatrix of the transition matrix, i.e. there are rewards for transitions that do not exist.");
             }
             
             template <typename ValueType>
-            Mdp<ValueType> Mdp<ValueType>::restrictChoiceLabels(boost::container::flat_set<uint_fast64_t> const& enabledChoiceLabels) const {
+            Mdp<ValueType> Mdp<ValueType>::restrictChoiceLabels(LabelSet const& enabledChoiceLabels) const {
                 STORM_LOG_THROW(this->hasChoiceLabeling(), storm::exceptions::InvalidArgumentException, "Restriction to label set is impossible for unlabeled model.");
                 
-                std::vector<boost::container::flat_set<uint_fast64_t>> const& choiceLabeling = this->getChoiceLabeling();
+                std::vector<LabelSet> const& choiceLabeling = this->getChoiceLabeling();
                 
                 storm::storage::SparseMatrixBuilder<ValueType> transitionMatrixBuilder(0, this->getTransitionMatrix().getColumnCount(), 0, true, true);
-                std::vector<boost::container::flat_set<uint_fast64_t>> newChoiceLabeling;
+                std::vector<LabelSet> newChoiceLabeling;
                 
                 // Check for each choice of each state, whether the choice labels are fully contained in the given label set.
                 uint_fast64_t currentRow = 0;
@@ -71,7 +71,7 @@ namespace storm {
                 Mdp<ValueType> restrictedMdp(transitionMatrixBuilder.build(), storm::models::sparse::StateLabeling(this->getStateLabeling()),
                                              this->hasStateRewards() ? boost::optional<std::vector<ValueType>>(this->getStateRewardVector()) : boost::optional<std::vector<ValueType>>(),
                                              this->hasTransitionRewards() ? boost::optional<storm::storage::SparseMatrix<ValueType>>(this->getTransitionRewardMatrix()) : boost::optional<storm::storage::SparseMatrix<ValueType>>(),
-                                             boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>(newChoiceLabeling));
+                                             boost::optional<std::vector<LabelSet>>(newChoiceLabeling));
                 return restrictedMdp;
             }
             
diff --git a/src/models/sparse/Mdp.h b/src/models/sparse/Mdp.h
index 4b62f7377..18879ee76 100644
--- a/src/models/sparse/Mdp.h
+++ b/src/models/sparse/Mdp.h
@@ -27,7 +27,7 @@ namespace storm {
                     storm::models::sparse::StateLabeling const& stateLabeling,
                     boost::optional<std::vector<ValueType>> const& optionalStateRewardVector = boost::optional<std::vector<ValueType>>(),
                     boost::optional<storm::storage::SparseMatrix<ValueType>> const& optionalTransitionRewardMatrix = boost::optional<storm::storage::SparseMatrix<ValueType>>(),
-                    boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> const& optionalChoiceLabeling = boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
+                    boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling = boost::optional<std::vector<LabelSet>>());
                 
                 /*!
                  * Constructs a model by moving the given data.
@@ -42,7 +42,7 @@ namespace storm {
                     storm::models::sparse::StateLabeling&& stateLabeling,
                     boost::optional<std::vector<ValueType>>&& optionalStateRewardVector = boost::optional<std::vector<ValueType>>(),
                     boost::optional<storm::storage::SparseMatrix<ValueType>>&& optionalTransitionRewardMatrix = boost::optional<storm::storage::SparseMatrix<ValueType>>(),
-                    boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>&& optionalChoiceLabeling = boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
+                    boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling = boost::optional<std::vector<LabelSet>>());
                 
                 Mdp(Mdp const& other) = default;
                 Mdp& operator=(Mdp const& other) = default;
@@ -61,7 +61,7 @@ namespace storm {
                  * and which ones need to be ignored.
                  * @return A restricted version of the current MDP that only uses choice labels from the given set.
                  */
-                Mdp<ValueType> restrictChoiceLabels(boost::container::flat_set<uint_fast64_t> const& enabledChoiceLabels) const;
+                Mdp<ValueType> restrictChoiceLabels(LabelSet const& enabledChoiceLabels) const;
                 
             private:
                 /*!
diff --git a/src/models/sparse/Model.cpp b/src/models/sparse/Model.cpp
index e1230d051..b2ca03c1d 100644
--- a/src/models/sparse/Model.cpp
+++ b/src/models/sparse/Model.cpp
@@ -12,7 +12,7 @@ namespace storm {
                                     storm::models::sparse::StateLabeling const& stateLabeling,
                                     boost::optional<std::vector<ValueType>> const& optionalStateRewardVector,
                                     boost::optional<storm::storage::SparseMatrix<ValueType>> const& optionalTransitionRewardMatrix,
-                                    boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> const& optionalChoiceLabeling)
+                                    boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling)
             : ModelBase(modelType),
             transitionMatrix(transitionMatrix),
             stateLabeling(stateLabeling),
@@ -28,7 +28,7 @@ namespace storm {
                                     storm::models::sparse::StateLabeling&& stateLabeling,
                                     boost::optional<std::vector<ValueType>>&& optionalStateRewardVector,
                                     boost::optional<storm::storage::SparseMatrix<ValueType>>&& optionalTransitionRewardMatrix,
-                                    boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>&& optionalChoiceLabeling)
+                                    boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling)
             : ModelBase(modelType),
             transitionMatrix(std::move(transitionMatrix)),
             stateLabeling(std::move(stateLabeling)),
@@ -109,7 +109,7 @@ namespace storm {
             }
             
             template <typename ValueType>
-            std::vector<boost::container::flat_set<uint_fast64_t>> const& Model<ValueType>::getChoiceLabeling() const {
+            std::vector<LabelSet> const& Model<ValueType>::getChoiceLabeling() const {
                 return choiceLabeling.get();
             }
             
@@ -159,7 +159,7 @@ namespace storm {
                     result += getTransitionRewardMatrix().getSizeInBytes();
                 }
                 if (hasChoiceLabeling()) {
-                    result += getChoiceLabeling().size() * sizeof(boost::container::flat_set<uint_fast64_t>);
+                    result += getChoiceLabeling().size() * sizeof(LabelSet);
                 }
                 return result;
             }
diff --git a/src/models/sparse/Model.h b/src/models/sparse/Model.h
index 103da9fba..5457370e6 100644
--- a/src/models/sparse/Model.h
+++ b/src/models/sparse/Model.h
@@ -16,6 +16,9 @@ namespace storm {
     namespace models {
         namespace sparse {
             
+            // The type used for storing a set of labels.
+            typedef boost::container::flat_set<uint_fast64_t> LabelSet;
+            
             /*!
              * Base class for all sparse models.
              */
@@ -45,7 +48,7 @@ namespace storm {
                       storm::models::sparse::StateLabeling const& stateLabeling,
                       boost::optional<std::vector<ValueType>> const& optionalStateRewardVector = boost::optional<std::vector<ValueType>>(),
                       boost::optional<storm::storage::SparseMatrix<ValueType>> const& optionalTransitionRewardMatrix = boost::optional<storm::storage::SparseMatrix<ValueType>>(),
-                      boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> const& optionalChoiceLabeling = boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
+                      boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling = boost::optional<std::vector<LabelSet>>());
                 
                 /*!
                  * Constructs a model by moving the given data.
@@ -62,7 +65,7 @@ namespace storm {
                       storm::models::sparse::StateLabeling&& stateLabeling,
                       boost::optional<std::vector<ValueType>>&& optionalStateRewardVector = boost::optional<std::vector<ValueType>>(),
                       boost::optional<storm::storage::SparseMatrix<ValueType>>&& optionalTransitionRewardMatrix = boost::optional<storm::storage::SparseMatrix<ValueType>>(),
-                      boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>&& optionalChoiceLabeling = boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
+                      boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling = boost::optional<std::vector<LabelSet>>());
                                 
                 /*!
                  * Retrieves the backward transition relation of the model, i.e. a set of transitions between states
@@ -175,7 +178,7 @@ namespace storm {
                  *
                  * @return The labels for the choices of the model.
                  */
-                std::vector<boost::container::flat_set<uint_fast64_t>> const& getChoiceLabeling() const;
+                std::vector<LabelSet> const& getChoiceLabeling() const;
                 
                 /*!
                  * Returns the state labeling associated with this model.
@@ -287,7 +290,7 @@ namespace storm {
                 boost::optional<storm::storage::SparseMatrix<ValueType>> transitionRewardMatrix;
                 
                 // If set, a vector representing the labels of choices.
-                boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> choiceLabeling;
+                boost::optional<std::vector<LabelSet>> choiceLabeling;
             };
             
         } // namespace sparse
diff --git a/src/models/sparse/NondeterministicModel.cpp b/src/models/sparse/NondeterministicModel.cpp
index 31dbaf699..40a5742c4 100644
--- a/src/models/sparse/NondeterministicModel.cpp
+++ b/src/models/sparse/NondeterministicModel.cpp
@@ -12,7 +12,7 @@ namespace storm {
                                                                     storm::models::sparse::StateLabeling const& stateLabeling,
                                                                     boost::optional<std::vector<ValueType>> const& optionalStateRewardVector,
                                                                     boost::optional<storm::storage::SparseMatrix<ValueType>> const& optionalTransitionRewardMatrix,
-                                                                    boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> const& optionalChoiceLabeling)
+                                                                    boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling)
             : Model<ValueType>(modelType, transitionMatrix, stateLabeling, optionalStateRewardVector, optionalTransitionRewardMatrix, optionalChoiceLabeling) {
                 // Intentionally left empty.
             }
@@ -23,7 +23,7 @@ namespace storm {
                                                                     storm::models::sparse::StateLabeling&& stateLabeling,
                                                                     boost::optional<std::vector<ValueType>>&& optionalStateRewardVector,
                                                                     boost::optional<storm::storage::SparseMatrix<ValueType>>&& optionalTransitionRewardMatrix,
-                                                                    boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>&& optionalChoiceLabeling)
+                                                                    boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling)
             : Model<ValueType>(modelType, std::move(transitionMatrix), std::move(stateLabeling), std::move(optionalStateRewardVector), std::move(optionalTransitionRewardMatrix),
                                std::move(optionalChoiceLabeling)) {
                 // Intentionally left empty.
diff --git a/src/models/sparse/NondeterministicModel.h b/src/models/sparse/NondeterministicModel.h
index 87d77111b..e5b8bc0b0 100644
--- a/src/models/sparse/NondeterministicModel.h
+++ b/src/models/sparse/NondeterministicModel.h
@@ -29,7 +29,7 @@ namespace storm {
                                       storm::models::sparse::StateLabeling const& stateLabeling,
                                       boost::optional<std::vector<ValueType>> const& optionalStateRewardVector = boost::optional<std::vector<ValueType>>(),
                                       boost::optional<storm::storage::SparseMatrix<ValueType>> const& optionalTransitionRewardMatrix = boost::optional<storm::storage::SparseMatrix<ValueType>>(),
-                                      boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>> const& optionalChoiceLabeling = boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
+                                      boost::optional<std::vector<LabelSet>> const& optionalChoiceLabeling = boost::optional<std::vector<LabelSet>>());
                 
                 /*!
                  * Constructs a model by moving the given data.
@@ -46,7 +46,7 @@ namespace storm {
                                       storm::models::sparse::StateLabeling&& stateLabeling,
                                       boost::optional<std::vector<ValueType>>&& optionalStateRewardVector = boost::optional<std::vector<ValueType>>(),
                                       boost::optional<storm::storage::SparseMatrix<ValueType>>&& optionalTransitionRewardMatrix = boost::optional<storm::storage::SparseMatrix<ValueType>>(),
-                                      boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>&& optionalChoiceLabeling = boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>());
+                                      boost::optional<std::vector<LabelSet>>&& optionalChoiceLabeling = boost::optional<std::vector<LabelSet>>());
                 
                 NondeterministicModel(NondeterministicModel const& other) = default;
                 NondeterministicModel& operator=(NondeterministicModel const& other) = default;
diff --git a/src/models/sparse/StochasticTwoPlayerGame.cpp b/src/models/sparse/StochasticTwoPlayerGame.cpp
new file mode 100644
index 000000000..8e6daa52a
--- /dev/null
+++ b/src/models/sparse/StochasticTwoPlayerGame.cpp
@@ -0,0 +1,41 @@
+#include "src/models/sparse/StochasticTwoPlayerGame.h"
+
+#include "src/adapters/CarlAdapter.h"
+
+namespace storm {
+    namespace models {
+        namespace sparse {
+            
+            template <typename ValueType>
+            StochasticTwoPlayerGame<ValueType>::StochasticTwoPlayerGame(storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& player1Matrix,
+                                                                        storm::storage::SparseMatrix<ValueType> const& player2Matrix,
+                                                                        storm::models::sparse::StateLabeling const& stateLabeling,
+                                                                        boost::optional<std::vector<ValueType>> const& optionalStateRewardVector,
+                                                                        boost::optional<std::vector<LabelSet>> const& optionalPlayer1ChoiceLabeling,
+                                                                        boost::optional<std::vector<LabelSet>> const& optionalPlayer2ChoiceLabeling)
+            : NondeterministicModel<ValueType>(storm::models::ModelType::S2pg, player2Matrix, stateLabeling, optionalStateRewardVector, boost::optional<storm::storage::SparseMatrix<ValueType>>(), optionalPlayer2ChoiceLabeling), player1Matrix(player1Matrix), player1Labels(optionalPlayer1ChoiceLabeling) {
+                // Intentionally left empty.
+            }
+            
+            
+            template <typename ValueType>
+            StochasticTwoPlayerGame<ValueType>::StochasticTwoPlayerGame(storm::storage::SparseMatrix<storm::storage::sparse::state_type>&& player1Matrix,
+                                                                        storm::storage::SparseMatrix<ValueType>&& player2Matrix,
+                                                                        storm::models::sparse::StateLabeling&& stateLabeling,
+                                                                        boost::optional<std::vector<ValueType>>&& optionalStateRewardVector,
+                                                                        boost::optional<std::vector<LabelSet>>&& optionalPlayer1ChoiceLabeling,
+                                                                        boost::optional<std::vector<LabelSet>>&& optionalPlayer2ChoiceLabeling)
+            : NondeterministicModel<ValueType>(storm::models::ModelType::S2pg, std::move(player2Matrix), std::move(stateLabeling), std::move(optionalStateRewardVector), boost::optional<storm::storage::SparseMatrix<ValueType>>(), std::move(optionalPlayer2ChoiceLabeling)), player1Matrix(std::move(player1Matrix)), player1Labels(std::move(optionalPlayer1ChoiceLabeling)) {
+                // Intentionally left empty.
+            }
+            
+            template class StochasticTwoPlayerGame<double>;
+            template class StochasticTwoPlayerGame<float>;
+            
+#ifdef STORM_HAVE_CARL
+            template class StochasticTwoPlayerGame<storm::RationalFunction>;
+#endif
+            
+        } // namespace sparse
+    } // namespace models
+} // namespace storm
\ No newline at end of file
diff --git a/src/models/sparse/StochasticTwoPlayerGame.h b/src/models/sparse/StochasticTwoPlayerGame.h
new file mode 100644
index 000000000..cbd2988ca
--- /dev/null
+++ b/src/models/sparse/StochasticTwoPlayerGame.h
@@ -0,0 +1,77 @@
+#ifndef STORM_MODELS_SPARSE_STOCHASTICTWOPLAYERGAME_H_
+#define STORM_MODELS_SPARSE_STOCHASTICTWOPLAYERGAME_H_
+
+#include "src/models/sparse/NondeterministicModel.h"
+#include "src/utility/OsDetection.h"
+
+namespace storm {
+    namespace models {
+        namespace sparse {
+            
+            /*!
+             * This class represents a (discrete-time) stochastic two-player game.
+             */
+            template <typename ValueType>
+            class StochasticTwoPlayerGame : public NondeterministicModel<ValueType> {
+            public:
+                /*!
+                 * Constructs a model from the given data.
+                 *
+                 * @param player1Matrix The matrix representing the choices of player 1.
+                 * @param player2Matrix The matrix representing the choices of player 2.
+                 * @param stateLabeling The labeling of the states.
+                 * @param optionalStateRewardVector The reward values associated with the states.
+                 * @param optionalPlayer1ChoiceLabeling A vector that represents the labels associated with the choices of each player 1 state.
+                 * @param optionalPlayer2ChoiceLabeling A vector that represents the labels associated with the choices of each player 2 state.
+                 */
+                StochasticTwoPlayerGame(storm::storage::SparseMatrix<storm::storage::sparse::state_type> const& player1Matrix,
+                                        storm::storage::SparseMatrix<ValueType> const& player2Matrix,
+                                        storm::models::sparse::StateLabeling const& stateLabeling,
+                                        boost::optional<std::vector<ValueType>> const& optionalStateRewardVector = boost::optional<std::vector<ValueType>>(),
+                                        boost::optional<std::vector<LabelSet>> const& optionalPlayer1ChoiceLabeling = boost::optional<std::vector<LabelSet>>(),
+                                        boost::optional<std::vector<LabelSet>> const& optionalPlayer2ChoiceLabeling = boost::optional<std::vector<LabelSet>>());
+                
+                /*!
+                 * Constructs a model by moving the given data.
+                 *
+                 * @param player1Matrix The matrix representing the choices of player 1.
+                 * @param player2Matrix The matrix representing the choices of player 2.
+                 * @param stateLabeling The labeling of the states.
+                 * @param optionalStateRewardVector The reward values associated with the states.
+                 * @param optionalPlayer1ChoiceLabeling A vector that represents the labels associated with the choices of each player 1 state.
+                 * @param optionalPlayer2ChoiceLabeling A vector that represents the labels associated with the choices of each player 2 state.
+                 */
+                StochasticTwoPlayerGame(storm::storage::SparseMatrix<storm::storage::sparse::state_type>&& player1Matrix,
+                                        storm::storage::SparseMatrix<ValueType>&& player2Matrix,
+                                        storm::models::sparse::StateLabeling&& stateLabeling,
+                                        boost::optional<std::vector<ValueType>>&& optionalStateRewardVector = boost::optional<std::vector<ValueType>>(),
+                                        boost::optional<std::vector<LabelSet>>&& optionalPlayer1ChoiceLabeling = boost::optional<std::vector<LabelSet>>(),
+                                        boost::optional<std::vector<LabelSet>>&& optionalPlayer2ChoiceLabeling = boost::optional<std::vector<LabelSet>>());
+                
+                StochasticTwoPlayerGame(StochasticTwoPlayerGame const& other) = default;
+                StochasticTwoPlayerGame& operator=(StochasticTwoPlayerGame const& other) = default;
+                
+#ifndef WINDOWS
+                StochasticTwoPlayerGame(StochasticTwoPlayerGame&& other) = default;
+                StochasticTwoPlayerGame& operator=(StochasticTwoPlayerGame&& other) = default;
+#endif
+                
+            private:
+                // A matrix that stores the player 1 choices. This matrix contains a row group for each player 1 node. Every
+                // row group contains a row for each choice in that player 1 node. Each such row contains exactly one
+                // (non-zero) entry at a column that indicates the player 2 node this choice leads to (which is essentially
+                // the index of a row group in the matrix for player 2).
+                storm::storage::SparseMatrix<storm::storage::sparse::state_type> player1Matrix;
+                
+                // An (optional) vector of labels attached to the choices of player 1. Each row of the matrix can be equipped
+                // with a set of labels to tag certain choices.
+                boost::optional<std::vector<LabelSet>> player1Labels;
+                
+                // The matrix and labels for player 2 are stored in the superclass.
+            };
+            
+        } // namespace sparse
+    } // namespace models
+} // namespace storm
+
+#endif /* STORM_MODELS_SPARSE_STOCHASTICTWOPLAYERGAME_H_ */
diff --git a/src/models/symbolic/StochasticTwoPlayerGame.cpp b/src/models/symbolic/StochasticTwoPlayerGame.cpp
index e69de29bb..0424f100c 100644
--- a/src/models/symbolic/StochasticTwoPlayerGame.cpp
+++ b/src/models/symbolic/StochasticTwoPlayerGame.cpp
@@ -0,0 +1,42 @@
+#include "src/models/symbolic/StochasticTwoPlayerGame.h"
+
+namespace storm {
+    namespace models {
+        namespace symbolic {
+            
+            template<storm::dd::DdType Type>
+            StochasticTwoPlayerGame<Type>::StochasticTwoPlayerGame(std::shared_ptr<storm::dd::DdManager<Type>> manager,
+                                                                   storm::dd::Bdd<Type> reachableStates,
+                                                                   storm::dd::Bdd<Type> initialStates,
+                                                                   storm::dd::Add<Type> transitionMatrix,
+                                                                   std::set<storm::expressions::Variable> const& rowVariables,
+                                                                   std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>> rowExpressionAdapter,
+                                                                   std::set<storm::expressions::Variable> const& columnVariables,
+                                                                   std::shared_ptr<storm::adapters::AddExpressionAdapter<Type>> columnExpressionAdapter,
+                                                                   std::vector<std::pair<storm::expressions::Variable, storm::expressions::Variable>> const& rowColumnMetaVariablePairs,
+                                                                   std::set<storm::expressions::Variable> const& player1Variables,
+                                                                   std::set<storm::expressions::Variable> const& player2Variables,
+                                                                   std::set<storm::expressions::Variable> const& nondeterminismVariables,
+                                                                   std::map<std::string, storm::expressions::Expression> labelToExpressionMap,
+                                                                   boost::optional<storm::dd::Add<Type>> const& optionalStateRewardVector,
+                                                                   boost::optional<storm::dd::Add<Type>> const& optionalTransitionRewardMatrix)
+                : NondeterministicModel<Type>(storm::models::ModelType::S2pg, manager, reachableStates, initialStates, transitionMatrix, rowVariables, rowExpressionAdapter, columnVariables, columnExpressionAdapter, rowColumnMetaVariablePairs, nondeterminismVariables, labelToExpressionMap, optionalStateRewardVector, optionalTransitionRewardMatrix), player1Variables(player1Variables), player2Variables(player2Variables) {
+                // Intentionally left empty.
+            }
+            
+            template<storm::dd::DdType Type>
+            std::set<storm::expressions::Variable> const& StochasticTwoPlayerGame<Type>::getPlayer1Variables() const {
+                return player1Variables;
+            }
+            
+            template<storm::dd::DdType Type>
+            std::set<storm::expressions::Variable> const& StochasticTwoPlayerGame<Type>::getPlayer2Variables() const {
+                return player2Variables;
+            }
+            
+            // Explicitly instantiate the template class.
+            template class StochasticTwoPlayerGame<storm::dd::DdType::CUDD>;
+            
+        } // namespace symbolic
+    } // namespace models
+} // namespace storm
\ No newline at end of file
diff --git a/src/models/symbolic/StochasticTwoPlayerGame.h b/src/models/symbolic/StochasticTwoPlayerGame.h
index 45d1e378a..841cce5c4 100644
--- a/src/models/symbolic/StochasticTwoPlayerGame.h
+++ b/src/models/symbolic/StochasticTwoPlayerGame.h
@@ -9,12 +9,12 @@ namespace storm {
         namespace symbolic {
             
             /*!
-             * This class represents a discrete-time Markov decision process.
+             * This class represents a discrete-time stochastic two-player game.
              */
             template<storm::dd::DdType Type>
             class StochasticTwoPlayerGame : public NondeterministicModel<Type> {
             public:
-                StochasticTwoPlayerGame(Mdp<Type> const& other) = default;
+                StochasticTwoPlayerGame(StochasticTwoPlayerGame<Type> const& other) = default;
                 StochasticTwoPlayerGame& operator=(StochasticTwoPlayerGame<Type> const& other) = default;
                 
 #ifndef WINDOWS
@@ -25,7 +25,6 @@ namespace storm {
                 /*!
                  * Constructs a model from the given data.
                  *
-                 * @param modelType The type of the model.
                  * @param manager The manager responsible for the decision diagrams.
                  * @param reachableStates A DD representing the reachable states.
                  * @param initialStates A DD representing the initial states of the model.
@@ -59,7 +58,27 @@ namespace storm {
                                         std::map<std::string, storm::expressions::Expression> labelToExpressionMap = std::map<std::string, storm::expressions::Expression>(),
                                         boost::optional<storm::dd::Add<Type>> const& optionalStateRewardVector = boost::optional<storm::dd::Dd<Type>>(),
                                         boost::optional<storm::dd::Add<Type>> const& optionalTransitionRewardMatrix = boost::optional<storm::dd::Dd<Type>>());
+
+                /*!
+                 * Retrieeves the set of meta variables used to encode the nondeterministic choices of player 1.
+                 *
+                 * @return The set of meta variables used to encode the nondeterministic choices of player 1.
+                 */
+                std::set<storm::expressions::Variable> const& getPlayer1Variables() const;
+                
+                /*!
+                 * Retrieeves the set of meta variables used to encode the nondeterministic choices of player 2.
+                 *
+                 * @return The set of meta variables used to encode the nondeterministic choices of player 2.
+                 */
+                std::set<storm::expressions::Variable> const& getPlayer2Variables() const;
+                
+            private:
+                // The meta variables used to encode the nondeterministic choices of player 1.
+                std::set<storm::expressions::Variable> player1Variables;
                 
+                // The meta variables used to encode the nondeterministic choices of player 2.
+                std::set<storm::expressions::Variable> player2Variables;
             };
             
         } // namespace symbolic