diff --git a/SparseLearningModelChecker.cpp b/SparseLearningModelChecker.cpp
new file mode 100644
index 000000000..e69de29bb
diff --git a/src/CMakeLists.txt b/src/CMakeLists.txt
index 60258b436..fe251d665 100644
--- a/src/CMakeLists.txt
+++ b/src/CMakeLists.txt
@@ -21,6 +21,7 @@ file(GLOB_RECURSE STORM_MODELCHECKER_PRCTL_HELPER_FILES ${PROJECT_SOURCE_DIR}/sr
 file(GLOB STORM_MODELCHECKER_CSL_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/csl/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/csl/*.cpp)
 file(GLOB_RECURSE STORM_MODELCHECKER_CSL_HELPER_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/csl/helper/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/csl/helper/*.cpp)
 file(GLOB_RECURSE STORM_MODELCHECKER_REACHABILITY_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/reachability/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/reachability/*.cpp)
+file(GLOB_RECURSE STORM_MODELCHECKER_EXPLORATION_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/exploration/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/exploration/*.cpp)
 file(GLOB_RECURSE STORM_MODELCHECKER_PROPOSITIONAL_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/propositional/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/propositional/*.cpp)
 file(GLOB_RECURSE STORM_MODELCHECKER_ABSTRACTION_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/abstraction/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/abstraction/*.cpp)
 file(GLOB_RECURSE STORM_MODELCHECKER_RESULTS_FILES ${PROJECT_SOURCE_DIR}/src/modelchecker/results/*.h ${PROJECT_SOURCE_DIR}/src/modelchecker/results/*.cpp)
@@ -70,6 +71,7 @@ source_group(modelchecker\\prctl FILES ${STORM_MODELCHECKER_PRCTL_FILES})
 source_group(modelchecker\\prctl\\helper FILES ${STORM_MODELCHECKER_PRCTL_HELPER_FILES})
 source_group(modelchecker\\csl FILES ${STORM_MODELCHECKER_CSL_FILES})
 source_group(modelchecker\\csl\\helper FILES ${STORM_MODELCHECKER_CSL_HELPER_FILES})
+source_group(modelchecker\\exploration FILES ${STORM_MODELCHECKER_EXPLORATION_FILES})
 source_group(modelchecker\\reachability FILES ${STORM_MODELCHECKER_REACHABILITY_FILES})
 source_group(modelchecker\\propositional FILES ${STORM_MODELCHECKER_PROPOSITIONAL_FILES})
 source_group(modelchecker\\abstraction FILES ${STORM_MODELCHECKER_ABSTRACTION_FILES})
diff --git a/src/builder/ExplicitPrismModelBuilder.cpp b/src/builder/ExplicitPrismModelBuilder.cpp
index 374ffada9..36bc474e7 100644
--- a/src/builder/ExplicitPrismModelBuilder.cpp
+++ b/src/builder/ExplicitPrismModelBuilder.cpp
@@ -62,40 +62,25 @@ namespace storm {
             // The state-action reward vector.
             std::vector<ValueType> stateActionRewardVector;
         };
-        
-        template <typename ValueType, typename RewardModelType, typename StateType>
-        ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::StateInformation::StateInformation(uint_fast64_t numberOfStates) : valuations(numberOfStates) {
-            // Intentionally left empty.
-        }
-        
-        template <typename ValueType, typename RewardModelType, typename StateType>
-        ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::InternalStateInformation::InternalStateInformation() : stateStorage(64, 10), initialStateIndices(), bitsPerState(64), numberOfStates() {
-            // Intentionally left empty.
-        }
-        
-        template <typename ValueType, typename RewardModelType, typename StateType>
-        ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::InternalStateInformation::InternalStateInformation(uint64_t bitsPerState) : stateStorage(bitsPerState, 10000000), initialStateIndices(), bitsPerState(bitsPerState), numberOfStates() {
-            // Intentionally left empty.
-        }
-        
+                        
         template <typename ValueType, typename RewardModelType, typename StateType>
         ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::ModelComponents::ModelComponents() : transitionMatrix(), stateLabeling(), rewardModels(), choiceLabeling() {
             // Intentionally left empty.
         }
         
         template <typename ValueType, typename RewardModelType, typename StateType>
-        ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::Options::Options() : explorationOrder(storm::settings::generalSettings().getExplorationOrder()), buildCommandLabels(false), buildAllRewardModels(true), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
+        ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::Options::Options() : explorationOrder(storm::settings::generalSettings().getExplorationOrder()), buildCommandLabels(false), buildAllRewardModels(true), buildStateValuations(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(true), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
             // Intentionally left empty.
         }
         
         template <typename ValueType, typename RewardModelType, typename StateType>
-        ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::Options::Options(storm::logic::Formula const& formula) : explorationOrder(storm::settings::generalSettings().getExplorationOrder()), buildCommandLabels(false), buildAllRewardModels(false), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()), terminalStates(), negatedTerminalStates() {
+        ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::Options::Options(storm::logic::Formula const& formula) : explorationOrder(storm::settings::generalSettings().getExplorationOrder()), buildCommandLabels(false), buildAllRewardModels(false), buildStateValuations(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(std::set<std::string>()), expressionLabels(std::vector<storm::expressions::Expression>()), terminalStates(), negatedTerminalStates() {
             this->preserveFormula(formula);
             this->setTerminalStatesFromFormula(formula);
         }
         
         template <typename ValueType, typename RewardModelType, typename StateType>
-        ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::Options::Options(std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) : explorationOrder(storm::settings::generalSettings().getExplorationOrder()), buildCommandLabels(false), buildAllRewardModels(false), buildStateInformation(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
+        ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::Options::Options(std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas) : explorationOrder(storm::settings::generalSettings().getExplorationOrder()), buildCommandLabels(false), buildAllRewardModels(false), buildStateValuations(false), rewardModelsToBuild(), constantDefinitions(), buildAllLabels(false), labelsToBuild(), expressionLabels(), terminalStates(), negatedTerminalStates() {
             if (formulas.empty()) {
                 this->buildAllRewardModels = true;
                 this->buildAllLabels = true;
@@ -187,69 +172,14 @@ namespace storm {
         }
         
         template <typename ValueType, typename RewardModelType, typename StateType>
-        ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::ExplicitPrismModelBuilder(storm::prism::Program const& program, Options const& options) : program(program), options(options) {
-            // Start by defining the undefined constants in the model.
-            if (options.constantDefinitions) {
-                this->program = program.defineUndefinedConstants(options.constantDefinitions.get());
-            } else {
-                this->program = program;
-            }
-            
-            // If the program still contains undefined constants and we are not in a parametric setting, assemble an appropriate error message.
-            if (!std::is_same<ValueType, storm::RationalFunction>::value && this->program.hasUndefinedConstants()) {
-                std::vector<std::reference_wrapper<storm::prism::Constant const>> undefinedConstants = this->program.getUndefinedConstants();
-                std::stringstream stream;
-                bool printComma = false;
-                for (auto const& constant : undefinedConstants) {
-                    if (printComma) {
-                        stream << ", ";
-                    } else {
-                        printComma = true;
-                    }
-                    stream << constant.get().getName() << " (" << constant.get().getType() << ")";
-                }
-                stream << ".";
-                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str());
-            } else if (std::is_same<ValueType, storm::RationalFunction>::value && !this->program.hasUndefinedConstantsOnlyInUpdateProbabilitiesAndRewards()) {
-                STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The program contains undefined constants that appear in some places other than update probabilities and reward value expressions, which is not admitted.");
-            }
-            
-            // If the set of labels we are supposed to built is restricted, we need to remove the other labels from the program.
-            if (options.labelsToBuild) {
-                if (!options.buildAllLabels) {
-                    this->program.filterLabels(options.labelsToBuild.get());
-                }
-            }
-            
-            // If we need to build labels for expressions that may appear in some formula, we need to add appropriate
-            // labels to the program.
-            if (options.expressionLabels) {
-                std::map<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution = this->program.getConstantsSubstitution();
-                
-                for (auto const& expression : options.expressionLabels.get()) {
-                    std::stringstream stream;
-                    stream << expression.substitute(constantsSubstitution);
-                    std::string name = stream.str();
-                    if (!this->program.hasLabel(name)) {
-                        this->program.addLabel(name, expression);
-                    }
-                }
-            }
-            
-            // Now that the program is fixed, we we need to substitute all constants with their concrete value.
-            this->program = this->program.substituteConstants();
-
-            // Create the variable information for the transformed program.
-            this->variableInformation = VariableInformation(this->program);
-            
-            // Create the internal state storage.
-            this->internalStateInformation = InternalStateInformation(variableInformation.getTotalBitOffset(true));
+        ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::ExplicitPrismModelBuilder(storm::prism::Program const& program, Options const& options) : program(storm::utility::prism::preprocessProgram<ValueType>(program, options.constantDefinitions, !options.buildAllLabels ? options.labelsToBuild : boost::none, options.expressionLabels)), options(options), variableInformation(this->program), stateStorage(variableInformation.getTotalBitOffset(true)) {
+            // Intentionally left empty.
         }
         
         template <typename ValueType, typename RewardModelType, typename StateType>
-        typename ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::StateInformation const& ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::getStateInformation() const {
-            STORM_LOG_THROW(static_cast<bool>(stateInformation), storm::exceptions::InvalidOperationException, "The state information was not properly build.");
-            return stateInformation.get();
+        storm::storage::sparse::StateValuations const& ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::getStateValuations() const {
+            STORM_LOG_THROW(static_cast<bool>(stateValuations), storm::exceptions::InvalidOperationException, "The state information was not properly build.");
+            return stateValuations.get();
         }
         
         template <typename ValueType, typename RewardModelType, typename StateType>
@@ -302,24 +232,12 @@ namespace storm {
             return result;
         }
         
-        template <typename ValueType, typename RewardModelType, typename StateType>
-        storm::expressions::SimpleValuation ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::unpackStateIntoValuation(storm::storage::BitVector const& currentState) {
-            storm::expressions::SimpleValuation result(program.getManager().getSharedPointer());
-            for (auto const& booleanVariable : variableInformation.booleanVariables) {
-                result.setBooleanValue(booleanVariable.variable, currentState.get(booleanVariable.bitOffset));
-            }
-            for (auto const& integerVariable : variableInformation.integerVariables) {
-                result.setIntegerValue(integerVariable.variable, currentState.getAsInt(integerVariable.bitOffset, integerVariable.bitWidth) + integerVariable.lowerBound);
-            }
-            return result;
-        }
-        
         template <typename ValueType, typename RewardModelType, typename StateType>
         StateType ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::getOrAddStateIndex(CompressedState const& state) {
-            uint32_t newIndex = internalStateInformation.numberOfStates;
+            StateType newIndex = static_cast<StateType>(stateStorage.getNumberOfStates());
             
             // Check, if the state was already registered.
-            std::pair<uint32_t, std::size_t> actualIndexBucketPair = internalStateInformation.stateStorage.findOrAddAndGetBucket(state, newIndex);
+            std::pair<StateType, std::size_t> actualIndexBucketPair = stateStorage.stateToId.findOrAddAndGetBucket(state, newIndex);
             
             if (actualIndexBucketPair.first == newIndex) {
                 if (options.explorationOrder == ExplorationOrder::Dfs) {
@@ -332,7 +250,6 @@ namespace storm {
                 } else {
                     STORM_LOG_ASSERT(false, "Invalid exploration order.");
                 }
-                ++internalStateInformation.numberOfStates;
             }
             
             return actualIndexBucketPair.first;
@@ -366,7 +283,7 @@ namespace storm {
             }
             
             // Let the generator create all initial states.
-            this->internalStateInformation.initialStateIndices = generator.getInitialStates(stateToIdCallback);
+            this->stateStorage.initialStateIndices = generator.getInitialStates(stateToIdCallback);
             
             // Now explore the current state until there is no more reachable state.
             uint_fast64_t currentRowGroup = 0;
@@ -376,7 +293,7 @@ namespace storm {
             while (!statesToExplore.empty()) {
                 // Get the first state in the queue.
                 CompressedState currentState = statesToExplore.front();
-                StateType currentIndex = internalStateInformation.stateStorage.getValue(currentState);
+                StateType currentIndex = stateStorage.stateToId.getValue(currentState);
                 statesToExplore.pop_front();
                 
                 // If the exploration order differs from breadth-first, we remember that this row group was actually
@@ -387,7 +304,8 @@ namespace storm {
                 
                 STORM_LOG_TRACE("Exploring state with id " << currentIndex << ".");
                 
-                storm::generator::StateBehavior<ValueType, StateType> behavior = generator.expand(currentState, stateToIdCallback);
+                generator.load(currentState);
+                storm::generator::StateBehavior<ValueType, StateType> behavior = generator.expand(stateToIdCallback);
                 
                 // If there is no behavior, we might have to introduce a self-loop.
                 if (behavior.empty()) {
@@ -417,7 +335,7 @@ namespace storm {
                         ++currentRow;
                         ++currentRowGroup;
                     } else {
-                        std::cout << unpackStateIntoValuation(currentState).toString(true) << std::endl;
+                        std::cout << storm::generator::unpackStateIntoValuation(currentState, variableInformation, program.getManager()).toString(true) << std::endl;
                         STORM_LOG_THROW(false, storm::exceptions::WrongFormatException,
                                         "Error while creating sparse matrix from probabilistic program: found deadlock state. For fixing these, please provide the appropriate option.");
                     }
@@ -481,13 +399,13 @@ namespace storm {
                 transitionMatrixBuilder.replaceColumns(remapping, 0);
 
                 // Fix (b).
-                std::vector<StateType> newInitialStateIndices(this->internalStateInformation.initialStateIndices.size());
-                std::transform(this->internalStateInformation.initialStateIndices.begin(), this->internalStateInformation.initialStateIndices.end(), newInitialStateIndices.begin(), [&remapping] (StateType const& state) { return remapping[state]; } );
+                std::vector<StateType> newInitialStateIndices(this->stateStorage.initialStateIndices.size());
+                std::transform(this->stateStorage.initialStateIndices.begin(), this->stateStorage.initialStateIndices.end(), newInitialStateIndices.begin(), [&remapping] (StateType const& state) { return remapping[state]; } );
                 std::sort(newInitialStateIndices.begin(), newInitialStateIndices.end());
-                this->internalStateInformation.initialStateIndices = std::move(newInitialStateIndices);
+                this->stateStorage.initialStateIndices = std::move(newInitialStateIndices);
                 
                 // Fix (c).
-                this->internalStateInformation.stateStorage.remap([&remapping] (StateType const& state) { return remapping[state]; } );
+                this->stateStorage.stateToId.remap([&remapping] (StateType const& state) { return remapping[state]; } );
             }
             
             return choiceLabels;
@@ -552,10 +470,10 @@ namespace storm {
             modelComponents.stateLabeling = buildStateLabeling();
             
             // Finally -- if requested -- build the state information that can be retrieved from the outside.
-            if (options.buildStateInformation) {
-                stateInformation = StateInformation(internalStateInformation.numberOfStates);
-                for (auto const& bitVectorIndexPair : internalStateInformation.stateStorage) {
-                    stateInformation.get().valuations[bitVectorIndexPair.second] = unpackStateIntoValuation(bitVectorIndexPair.first);
+            if (options.buildStateValuations) {
+                stateValuations = storm::storage::sparse::StateValuations(stateStorage.getNumberOfStates());
+                for (auto const& bitVectorIndexPair : stateStorage.stateToId) {
+                    stateValuations.get().valuations[bitVectorIndexPair.second] = unpackStateIntoValuation(bitVectorIndexPair.first, variableInformation, program.getManager());
                 }
             }
             
@@ -565,7 +483,7 @@ namespace storm {
         template <typename ValueType, typename RewardModelType, typename StateType>
         storm::models::sparse::StateLabeling ExplicitPrismModelBuilder<ValueType, RewardModelType, StateType>::buildStateLabeling() {
             storm::generator::PrismStateLabelingGenerator<ValueType, StateType> generator(program, variableInformation);
-            return generator.generate(internalStateInformation.stateStorage, internalStateInformation.initialStateIndices);
+            return generator.generate(stateStorage.stateToId, stateStorage.initialStateIndices);
         }
         
         // Explicitly instantiate the class.
diff --git a/src/builder/ExplicitPrismModelBuilder.h b/src/builder/ExplicitPrismModelBuilder.h
index ab2eb9815..d790f0bb1 100644
--- a/src/builder/ExplicitPrismModelBuilder.h
+++ b/src/builder/ExplicitPrismModelBuilder.h
@@ -20,6 +20,8 @@
 #include "src/models/sparse/Model.h"
 #include "src/models/sparse/StateLabeling.h"
 #include "src/storage/SparseMatrix.h"
+#include "src/storage/sparse/StateValuations.h"
+#include "src/storage/sparse/StateStorage.h"
 #include "src/settings/SettingsManager.h"
 
 #include "src/utility/prism.h"
@@ -45,42 +47,6 @@ namespace storm {
         template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>, typename StateType = uint32_t>
         class ExplicitPrismModelBuilder {
         public:
-            // A structure holding information about the reachable state space while building it.
-            struct InternalStateInformation {
-                // Builds an empty state information.
-                InternalStateInformation();
-                
-                // Creates a state information structure for storing states of the given bit width.
-                InternalStateInformation(uint64_t bitsPerState);
-
-                // This member stores all the states and maps them to their unique indices.
-                storm::storage::BitVectorHashMap<StateType> stateStorage;
-                
-                // A list of initial states in terms of their global indices.
-                std::vector<StateType> initialStateIndices;
-
-                // The number of bits of each state.
-                uint64_t bitsPerState;
-                
-                // The number of states that were found in the exploration so far.
-                uint_fast64_t numberOfStates;
-            };
-            
-            // A structure holding information about the reachable state space that can be retrieved from the outside.
-            struct StateInformation : public storm::models::sparse::StateAnnotation {
-                /*!
-                 * Constructs a state information object for the given number of states.
-                 */
-                StateInformation(uint_fast64_t numberOfStates);
-                
-                // A mapping from state indices to their variable valuations.
-                std::vector<storm::expressions::SimpleValuation> valuations;
-
-                std::string stateInfo(uint_fast64_t state) const override {
-                    return valuations[state].toString();
-                }
-            };
-            
             // A structure holding the individual components of a model.
             struct ModelComponents {
                 ModelComponents();
@@ -163,7 +129,7 @@ namespace storm {
                 // A flag that indicates whether or not to store the state information after successfully building the
                 // model. If it is to be preserved, it can be retrieved via the appropriate methods after a successful
                 // call to <code>translateProgram</code>.
-                bool buildStateInformation;
+                bool buildStateValuations;
                 
                 // A list of reward models to be build in case not all reward models are to be build.
                 std::set<std::string> rewardModelsToBuild;
@@ -214,7 +180,7 @@ namespace storm {
              *
              * @return A structure that stores information about all reachable states.
              */
-            StateInformation const& getStateInformation() const;
+            storm::storage::sparse::StateValuations const& getStateValuations() const;
             
             /*!
              * Retrieves the program that was actually translated (i.e. including constant substitutions etc.).
@@ -224,8 +190,6 @@ namespace storm {
             storm::prism::Program const& getTranslatedProgram() const;
             
         private:
-            storm::expressions::SimpleValuation unpackStateIntoValuation(storm::storage::BitVector const& currentState);
-            
             /*!
              * Retrieves the state id of the given state. If the state has not been encountered yet, it will be added to
              * the lists of all states with a new id. If the state was already known, the object that is pointed to by
@@ -233,7 +197,6 @@ namespace storm {
              * used after invoking this method.
              *
              * @param state A pointer to a state for which to retrieve the index. This must not be used after the call.
-             * @param internalStateInformation The information about the already explored part of the reachable state space.
              * @return A pair indicating whether the state was already discovered before and the state id of the state.
              */
             StateType getOrAddStateIndex(CompressedState const& state);
@@ -245,7 +208,6 @@ namespace storm {
              * @param variableInformation A structure containing information about the variables in the program.
              * @param transitionRewards A list of transition rewards that are to be considered in the transition reward
              * matrix.
-             * @param internalStateInformation A structure containing information about the states of the program.
              * @param deterministicModel A flag indicating whether the model is supposed to be deterministic or not.
              * @param transitionMatrix A reference to an initialized matrix which is filled with all transitions by this
              * function.
@@ -270,9 +232,6 @@ namespace storm {
             /*!
              * Builds the state labeling for the given program.
              *
-             * @param program The program for which to build the state labeling.
-             * @param variableInformation Information about the variables in the program.
-             * @param internalStateInformation Information about the state space of the program.
              * @return The state labeling of the given program.
              */
             storm::models::sparse::StateLabeling buildStateLabeling();
@@ -287,11 +246,11 @@ namespace storm {
             VariableInformation variableInformation;
             
             // Internal information about the states that were explored.
-            InternalStateInformation internalStateInformation;
+            storm::storage::sparse::StateStorage<StateType> stateStorage;
             
             // This member holds information about reachable states that can be retrieved from the outside after a
             // successful build.
-            boost::optional<StateInformation> stateInformation;
+            boost::optional<storm::storage::sparse::StateValuations> stateValuations;
             
             // A set of states that still need to be explored.
             std::deque<CompressedState> statesToExplore;
diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h
index 36db3dcf4..114abb445 100644
--- a/src/cli/entrypoints.h
+++ b/src/cli/entrypoints.h
@@ -61,6 +61,37 @@ namespace storm {
                 }
             }
         }
+        
+        template<typename ValueType>
+        void verifySymbolicModelWithExplorationEngine(storm::prism::Program const& program, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas, bool onlyInitialStatesRelevant = false) {
+            
+            for (auto const& formula : formulas) {
+                STORM_LOG_THROW(program.getModelType() == storm::prism::Program::ModelType::DTMC || program.getModelType() == storm::prism::Program::ModelType::MDP, storm::exceptions::InvalidSettingsException, "Currently exploration-based verification is only available for DTMCs and MDPs.");
+                std::cout << std::endl << "Model checking property: " << *formula << " ...";
+                storm::modelchecker::CheckTask<storm::logic::Formula> task(*formula, onlyInitialStatesRelevant);
+                storm::modelchecker::SparseExplorationModelChecker<ValueType> checker(program, storm::utility::prism::parseConstantDefinitionString(program, storm::settings::generalSettings().getConstantDefinitionString()));
+                std::unique_ptr<storm::modelchecker::CheckResult> result;
+                if (checker.canHandle(task)) {
+                    result = checker.check(task);
+                    if (result) {
+                        std::cout << " done." << std::endl;
+                        std::cout << "Result (initial states): ";
+                        std::cout << *result << std::endl;
+                    } else {
+                        std::cout << " skipped, because the modelling formalism is currently unsupported." << std::endl;
+                    }
+                } else {
+                    std::cout << " skipped, because the formula cannot be handled by the selected engine/method." << std::endl;
+                }
+            }
+        }
+        
+#ifdef STORM_HAVE_CARL
+        template<>
+        void verifySymbolicModelWithExplorationEngine<storm::RationalFunction>(storm::prism::Program const& program, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas, bool onlyInitialStatesRelevant) {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidSettingsException, "Exploration-based verification does currently not support parametric models.");
+        }
+#endif
 
         template<storm::dd::DdType DdType>
         void verifySymbolicModelWithHybridEngine(std::shared_ptr<storm::models::symbolic::Model<DdType>> model, std::vector<std::shared_ptr<const storm::logic::Formula>> const& formulas, bool onlyInitialStatesRelevant = false) {
@@ -128,6 +159,8 @@ namespace storm {
 
             if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::AbstractionRefinement) {
                 verifySymbolicModelWithAbstractionRefinementEngine<ValueType, LibraryType>(program, formulas, onlyInitialStatesRelevant);
+            } else if (settings.getEngine() == storm::settings::modules::GeneralSettings::Engine::Exploration) {
+                verifySymbolicModelWithExplorationEngine<ValueType>(program, formulas, onlyInitialStatesRelevant);
             } else {
                 storm::storage::ModelFormulasPair modelFormulasPair = buildSymbolicModel<ValueType, LibraryType>(program, formulas);
                 STORM_LOG_THROW(modelFormulasPair.model != nullptr, storm::exceptions::InvalidStateException,
@@ -144,7 +177,7 @@ namespace storm {
                     if (modelFormulasPair.model->isSparseModel()) {
                         if (storm::settings::generalSettings().isCounterexampleSet()) {
                             // If we were requested to generate a counterexample, we now do so for each formula.
-                            for (auto const &formula : modelFormulasPair.formulas) {
+                            for (auto const& formula : modelFormulasPair.formulas) {
                                 generateCounterexample<ValueType>(program, modelFormulasPair.model->as<storm::models::sparse::Model<ValueType>>(), formula);
                             }
                         } else {
diff --git a/src/generator/CompressedState.cpp b/src/generator/CompressedState.cpp
index c63504ebb..03ba3d4c7 100644
--- a/src/generator/CompressedState.cpp
+++ b/src/generator/CompressedState.cpp
@@ -1,6 +1,8 @@
 #include "src/generator/CompressedState.h"
 
 #include "src/generator/VariableInformation.h"
+#include "src/storage/expressions/ExpressionManager.h"
+#include "src/storage/expressions/SimpleValuation.h"
 #include "src/storage/expressions/ExpressionEvaluator.h"
 
 namespace storm {
@@ -14,10 +16,21 @@ namespace storm {
             for (auto const& integerVariable : variableInformation.integerVariables) {
                 evaluator.setIntegerValue(integerVariable.variable, state.getAsInt(integerVariable.bitOffset, integerVariable.bitWidth) + integerVariable.lowerBound);
             }
-
+        }
+        
+        storm::expressions::SimpleValuation unpackStateIntoValuation(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionManager const& manager) {
+            storm::expressions::SimpleValuation result(manager.getSharedPointer());
+            for (auto const& booleanVariable : variableInformation.booleanVariables) {
+                result.setBooleanValue(booleanVariable.variable, state.get(booleanVariable.bitOffset));
+            }
+            for (auto const& integerVariable : variableInformation.integerVariables) {
+                result.setIntegerValue(integerVariable.variable, state.getAsInt(integerVariable.bitOffset, integerVariable.bitWidth) + integerVariable.lowerBound);
+            }
+            return result;
         }
 
         template void unpackStateIntoEvaluator<double>(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<double>& evaluator);
         template void unpackStateIntoEvaluator<storm::RationalFunction>(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<storm::RationalFunction>& evaluator);
+        storm::expressions::SimpleValuation unpackStateIntoValuation(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionManager const& manager);
     }
 }
\ No newline at end of file
diff --git a/src/generator/CompressedState.h b/src/generator/CompressedState.h
index 52f0b4a62..a1b6212bb 100644
--- a/src/generator/CompressedState.h
+++ b/src/generator/CompressedState.h
@@ -6,6 +6,9 @@
 namespace storm {
     namespace expressions {
         template<typename ValueType> class ExpressionEvaluator;
+        
+        class ExpressionManager;
+        class SimpleValuation;
     }
     
     namespace generator {
@@ -18,11 +21,21 @@ namespace storm {
          * Unpacks the compressed state into the evaluator.
          *
          * @param state The state to unpack.
-         * @param variableInformation The information about how the variables are packed with the state.
+         * @param variableInformation The information about how the variables are packed within the state.
          * @param evaluator The evaluator into which to load the state.
          */
         template<typename ValueType>
         void unpackStateIntoEvaluator(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionEvaluator<ValueType>& evaluator);
+
+        /*!
+         * Converts the compressed state into an explicit representation in the form of a valuation.
+         *
+         * @param state The state to unpack.
+         * @param variableInformation The information about how the variables are packed within the state.
+         * @param manager The manager responsible for the variables.
+         * @return A valuation that corresponds to the compressed state.
+         */
+        storm::expressions::SimpleValuation unpackStateIntoValuation(CompressedState const& state, VariableInformation const& variableInformation, storm::expressions::ExpressionManager const& manager);
     }
 }
 
diff --git a/src/generator/NextStateGenerator.h b/src/generator/NextStateGenerator.h
index 779a49ef3..7dab9f470 100644
--- a/src/generator/NextStateGenerator.h
+++ b/src/generator/NextStateGenerator.h
@@ -4,6 +4,8 @@
 #include <vector>
 #include <cstdint>
 
+#include "src/storage/expressions/Expression.h"
+
 #include "src/generator/CompressedState.h"
 #include "src/generator/StateBehavior.h"
 
@@ -16,7 +18,10 @@ namespace storm {
 
             virtual bool isDeterministicModel() const = 0;
             virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) = 0;
-            virtual StateBehavior<ValueType, StateType> expand(CompressedState const& state, StateToIdCallback const& stateToIdCallback) = 0;
+            
+            virtual void load(CompressedState const& state) = 0;
+            virtual StateBehavior<ValueType, StateType> expand(StateToIdCallback const& stateToIdCallback) = 0;
+            virtual bool satisfies(storm::expressions::Expression const& expression) const = 0;
         };
     }
 }
diff --git a/src/generator/PrismNextStateGenerator.cpp b/src/generator/PrismNextStateGenerator.cpp
index fac3be0f5..3ba8b89f7 100644
--- a/src/generator/PrismNextStateGenerator.cpp
+++ b/src/generator/PrismNextStateGenerator.cpp
@@ -10,10 +10,10 @@ namespace storm {
     namespace generator {
         
         template<typename ValueType, typename StateType>
-        PrismNextStateGenerator<ValueType, StateType>::PrismNextStateGenerator(storm::prism::Program const& program, VariableInformation const& variableInformation, bool buildChoiceLabeling) : program(program), selectedRewardModels(), buildChoiceLabeling(buildChoiceLabeling), variableInformation(variableInformation), evaluator(program.getManager()), comparator() {
+        PrismNextStateGenerator<ValueType, StateType>::PrismNextStateGenerator(storm::prism::Program const& program, VariableInformation const& variableInformation, bool buildChoiceLabeling) : program(program), selectedRewardModels(), buildChoiceLabeling(buildChoiceLabeling), variableInformation(variableInformation), evaluator(program.getManager()), state(nullptr), comparator() {
             // Intentionally left empty.
         }
-        
+                
         template<typename ValueType, typename StateType>
         void PrismNextStateGenerator<ValueType, StateType>::addRewardModel(storm::prism::RewardModel const& rewardModel) {
             selectedRewardModels.push_back(rewardModel);
@@ -49,10 +49,24 @@ namespace storm {
         }
         
         template<typename ValueType, typename StateType>
-        StateBehavior<ValueType, StateType> PrismNextStateGenerator<ValueType, StateType>::expand(CompressedState const& state, StateToIdCallback const& stateToIdCallback) {
+        void PrismNextStateGenerator<ValueType, StateType>::load(CompressedState const& state) {
             // Since almost all subsequent operations are based on the evaluator, we load the state into it now.
             unpackStateIntoEvaluator(state, variableInformation, evaluator);
-
+            
+            // Also, we need to store a pointer to the state itself, because we need to be able to access it when expanding it.
+            this->state = &state;
+        }
+        
+        template<typename ValueType, typename StateType>
+        bool PrismNextStateGenerator<ValueType, StateType>::satisfies(storm::expressions::Expression const& expression) const {
+            if (expression.isTrue()) {
+                return true;
+            }
+            return evaluator.asBool(expression);
+        }
+        
+        template<typename ValueType, typename StateType>
+        StateBehavior<ValueType, StateType> PrismNextStateGenerator<ValueType, StateType>::expand(StateToIdCallback const& stateToIdCallback) {
             // Prepare the result, in case we return early.
             StateBehavior<ValueType, StateType> result;
             
@@ -76,8 +90,8 @@ namespace storm {
             }
             
             // Get all choices for the state.
-            std::vector<Choice<ValueType>> allChoices = getUnlabeledChoices(state, stateToIdCallback);
-            std::vector<Choice<ValueType>> allLabeledChoices = getLabeledChoices(state, stateToIdCallback);
+            std::vector<Choice<ValueType>> allChoices = getUnlabeledChoices(*this->state, stateToIdCallback);
+            std::vector<Choice<ValueType>> allLabeledChoices = getLabeledChoices(*this->state, stateToIdCallback);
             for (auto& choice : allLabeledChoices) {
                 allChoices.push_back(std::move(choice));
             }
diff --git a/src/generator/PrismNextStateGenerator.h b/src/generator/PrismNextStateGenerator.h
index d8eddc0ac..fe997d73a 100644
--- a/src/generator/PrismNextStateGenerator.h
+++ b/src/generator/PrismNextStateGenerator.h
@@ -18,7 +18,7 @@ namespace storm {
             typedef typename NextStateGenerator<ValueType, StateType>::StateToIdCallback StateToIdCallback;
             
             PrismNextStateGenerator(storm::prism::Program const& program, VariableInformation const& variableInformation, bool buildChoiceLabeling);
-            
+                        
             /*!
              * Adds a reward model to the list of selected reward models ()
              */
@@ -31,7 +31,10 @@ namespace storm {
             
             virtual bool isDeterministicModel() const override;
             virtual std::vector<StateType> getInitialStates(StateToIdCallback const& stateToIdCallback) override;
-            virtual StateBehavior<ValueType, StateType> expand(CompressedState const& state, StateToIdCallback const& stateToIdCallback) override;
+
+            virtual void load(CompressedState const& state) override;
+            virtual StateBehavior<ValueType, StateType> expand(StateToIdCallback const& stateToIdCallback) override;
+            virtual bool satisfies(storm::expressions::Expression const& expression) const override;
 
         private:
             /*!
@@ -98,6 +101,8 @@ namespace storm {
             // An evaluator used to evaluate expressions.
             storm::expressions::ExpressionEvaluator<ValueType> evaluator;
             
+            CompressedState const* state;
+            
             // A comparator used to compare constants.
             storm::utility::ConstantsComparator<ValueType> comparator;
         };
diff --git a/src/generator/StateBehavior.cpp b/src/generator/StateBehavior.cpp
index e14417779..6ae1f6de0 100644
--- a/src/generator/StateBehavior.cpp
+++ b/src/generator/StateBehavior.cpp
@@ -50,6 +50,11 @@ namespace storm {
             return stateRewards;
         }
         
+        template<typename ValueType, typename StateType>
+        std::size_t StateBehavior<ValueType, StateType>::getNumberOfChoices() const {
+            return choices.size();
+        }
+        
         template class StateBehavior<double>;
         template class StateBehavior<storm::RationalFunction>;
 
diff --git a/src/generator/StateBehavior.h b/src/generator/StateBehavior.h
index 393c3280c..8f81c8b30 100644
--- a/src/generator/StateBehavior.h
+++ b/src/generator/StateBehavior.h
@@ -56,6 +56,11 @@ namespace storm {
              */
             std::vector<ValueType> const& getStateRewards() const;
             
+            /*!
+             * Retrieves the number of choices in the behavior.
+             */
+            std::size_t getNumberOfChoices() const;
+            
         private:
             // The choices available in the state.
             std::vector<Choice<ValueType, StateType>> choices;
diff --git a/src/logic/AtomicExpressionFormula.cpp b/src/logic/AtomicExpressionFormula.cpp
index 5f8f0f509..b782fd368 100644
--- a/src/logic/AtomicExpressionFormula.cpp
+++ b/src/logic/AtomicExpressionFormula.cpp
@@ -24,10 +24,6 @@ namespace storm {
             atomicExpressionFormulas.push_back(std::dynamic_pointer_cast<AtomicExpressionFormula const>(this->shared_from_this()));
         }
         
-        std::shared_ptr<Formula> AtomicExpressionFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return std::make_shared<AtomicExpressionFormula>(this->expression.substitute(substitution));
-        }
-        
         std::ostream& AtomicExpressionFormula::writeToStream(std::ostream& out) const {
             out << expression;
             return out;
diff --git a/src/logic/AtomicExpressionFormula.h b/src/logic/AtomicExpressionFormula.h
index 12636475d..2299b5eac 100644
--- a/src/logic/AtomicExpressionFormula.h
+++ b/src/logic/AtomicExpressionFormula.h
@@ -23,8 +23,6 @@ namespace storm {
             
             virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;
             
-            virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
-
         private:
             // The atomic expression represented by this node in the formula tree.
             storm::expressions::Expression expression;
diff --git a/src/logic/AtomicLabelFormula.cpp b/src/logic/AtomicLabelFormula.cpp
index 19a5f673f..b0406d62c 100644
--- a/src/logic/AtomicLabelFormula.cpp
+++ b/src/logic/AtomicLabelFormula.cpp
@@ -1,5 +1,6 @@
 #include "src/logic/AtomicLabelFormula.h"
 
+#include "src/logic/AtomicExpressionFormula.h"
 #include "src/logic/FormulaVisitor.h"
 
 namespace storm {
@@ -24,10 +25,6 @@ namespace storm {
             atomicExpressionFormulas.push_back(std::dynamic_pointer_cast<AtomicLabelFormula const>(this->shared_from_this()));
         }
         
-        std::shared_ptr<Formula> AtomicLabelFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return std::make_shared<AtomicLabelFormula>(*this);
-        }
-        
         std::ostream& AtomicLabelFormula::writeToStream(std::ostream& out) const {
             out << "\"" << label << "\"";
             return out;
diff --git a/src/logic/AtomicLabelFormula.h b/src/logic/AtomicLabelFormula.h
index 795704305..a7a627f74 100644
--- a/src/logic/AtomicLabelFormula.h
+++ b/src/logic/AtomicLabelFormula.h
@@ -22,9 +22,7 @@ namespace storm {
             std::string const& getLabel() const;
             
             virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
-            
-            virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
-            
+                        
             virtual std::ostream& writeToStream(std::ostream& out) const override;
                         
         private:
diff --git a/src/logic/BinaryBooleanStateFormula.cpp b/src/logic/BinaryBooleanStateFormula.cpp
index d6757e508..a697b151c 100644
--- a/src/logic/BinaryBooleanStateFormula.cpp
+++ b/src/logic/BinaryBooleanStateFormula.cpp
@@ -30,11 +30,7 @@ namespace storm {
         bool BinaryBooleanStateFormula::isOr() const {
             return this->getOperator() == OperatorType::Or;
         }
-        
-        std::shared_ptr<Formula> BinaryBooleanStateFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return std::make_shared<BinaryBooleanStateFormula>(this->operatorType, this->getLeftSubformula().substitute(substitution), this->getRightSubformula().substitute(substitution));
-        }
-        
+                
         std::ostream& BinaryBooleanStateFormula::writeToStream(std::ostream& out) const {
             out << "(";
             this->getLeftSubformula().writeToStream(out);
diff --git a/src/logic/BinaryBooleanStateFormula.h b/src/logic/BinaryBooleanStateFormula.h
index 892d28bc9..d94260caa 100644
--- a/src/logic/BinaryBooleanStateFormula.h
+++ b/src/logic/BinaryBooleanStateFormula.h
@@ -28,8 +28,6 @@ namespace storm {
                         
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             
-            virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
-            
         private:
             OperatorType operatorType;
         };
diff --git a/src/logic/BooleanLiteralFormula.cpp b/src/logic/BooleanLiteralFormula.cpp
index 897fbf377..2cc139cf3 100644
--- a/src/logic/BooleanLiteralFormula.cpp
+++ b/src/logic/BooleanLiteralFormula.cpp
@@ -24,10 +24,6 @@ namespace storm {
             return visitor.visit(*this, data);
         }
         
-        std::shared_ptr<Formula> BooleanLiteralFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return std::make_shared<BooleanLiteralFormula>(*this);
-        }
-        
         std::ostream& BooleanLiteralFormula::writeToStream(std::ostream& out) const {
             if (value) {
                 out << "true";
diff --git a/src/logic/BooleanLiteralFormula.h b/src/logic/BooleanLiteralFormula.h
index 405044600..0946852fc 100644
--- a/src/logic/BooleanLiteralFormula.h
+++ b/src/logic/BooleanLiteralFormula.h
@@ -19,8 +19,6 @@ namespace storm {
             
             virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
             
-            virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
-            
             virtual std::ostream& writeToStream(std::ostream& out) const override;
                         
         private:
diff --git a/src/logic/BoundedUntilFormula.cpp b/src/logic/BoundedUntilFormula.cpp
index 8f3e73286..dd9f965f7 100644
--- a/src/logic/BoundedUntilFormula.cpp
+++ b/src/logic/BoundedUntilFormula.cpp
@@ -44,10 +44,6 @@ namespace storm {
             return boost::get<uint_fast64_t>(bounds);
         }
         
-        std::shared_ptr<Formula> BoundedUntilFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return std::make_shared<BoundedUntilFormula>(this->getLeftSubformula().substitute(substitution), this->getRightSubformula().substitute(substitution), bounds);
-        }
-        
         std::ostream& BoundedUntilFormula::writeToStream(std::ostream& out) const {
             this->getLeftSubformula().writeToStream(out);
             
diff --git a/src/logic/BoundedUntilFormula.h b/src/logic/BoundedUntilFormula.h
index 222bab142..13ee7cefc 100644
--- a/src/logic/BoundedUntilFormula.h
+++ b/src/logic/BoundedUntilFormula.h
@@ -26,8 +26,6 @@ namespace storm {
 
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             
-            virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
-            
         private:
             boost::variant<uint_fast64_t, std::pair<double, double>> bounds;
         };
diff --git a/src/logic/CloneVisitor.cpp b/src/logic/CloneVisitor.cpp
new file mode 100644
index 000000000..fe7182bf7
--- /dev/null
+++ b/src/logic/CloneVisitor.cpp
@@ -0,0 +1,106 @@
+#include "src/logic/CloneVisitor.h"
+
+#include "src/logic/Formulas.h"
+
+namespace storm {
+    namespace logic {
+        
+        std::shared_ptr<Formula> CloneVisitor::clone(Formula const& f) const {
+            boost::any result = f.accept(*this, boost::any());
+            return boost::any_cast<std::shared_ptr<Formula>>(result);
+        }
+        
+        boost::any CloneVisitor::visit(AtomicExpressionFormula const& f, boost::any const& data) const {
+            return std::static_pointer_cast<Formula>(std::make_shared<AtomicExpressionFormula>(f));
+        }
+        
+        boost::any CloneVisitor::visit(AtomicLabelFormula const& f, boost::any const& data) const {
+            return std::static_pointer_cast<Formula>(std::make_shared<AtomicLabelFormula>(f));
+        }
+        
+        boost::any CloneVisitor::visit(BinaryBooleanStateFormula const& f, boost::any const& data) const {
+            std::shared_ptr<Formula> left = boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula().accept(*this, data));
+            std::shared_ptr<Formula> right = boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula().accept(*this, data));
+            return std::static_pointer_cast<Formula>(std::make_shared<BinaryBooleanStateFormula>(f.getOperator(), left, right));
+        }
+        
+        boost::any CloneVisitor::visit(BooleanLiteralFormula const& f, boost::any const& data) const {
+            return std::static_pointer_cast<Formula>(std::make_shared<BooleanLiteralFormula>(f));
+        }
+        
+        boost::any CloneVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const {
+            std::shared_ptr<Formula> left = boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula().accept(*this, data));
+            std::shared_ptr<Formula> right = boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula().accept(*this, data));
+            if (f.hasDiscreteTimeBound()) {
+                return std::static_pointer_cast<Formula>(std::make_shared<BoundedUntilFormula>(left, right, f.getDiscreteTimeBound()));
+            } else {
+                return std::static_pointer_cast<Formula>(std::make_shared<BoundedUntilFormula>(left, right, f.getIntervalBounds()));
+            }
+        }
+        
+        boost::any CloneVisitor::visit(ConditionalFormula const& f, boost::any const& data) const {
+            std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
+            std::shared_ptr<Formula> conditionFormula = boost::any_cast<std::shared_ptr<Formula>>(f.getConditionFormula().accept(*this, data));
+            return std::static_pointer_cast<Formula>(std::make_shared<ConditionalFormula>(subformula, conditionFormula, f.getContext()));
+        }
+        
+        boost::any CloneVisitor::visit(CumulativeRewardFormula const& f, boost::any const& data) const {
+            return std::static_pointer_cast<Formula>(std::make_shared<CumulativeRewardFormula>(f));
+        }
+        
+        boost::any CloneVisitor::visit(EventuallyFormula const& f, boost::any const& data) const {
+            std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
+            return std::static_pointer_cast<Formula>(std::make_shared<EventuallyFormula>(subformula, f.getContext()));
+        }
+        
+        boost::any CloneVisitor::visit(TimeOperatorFormula const& f, boost::any const& data) const {
+            std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
+            return std::static_pointer_cast<Formula>(std::make_shared<TimeOperatorFormula>(subformula, f.getOperatorInformation()));
+        }
+        
+        boost::any CloneVisitor::visit(GloballyFormula const& f, boost::any const& data) const {
+            std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
+            return std::static_pointer_cast<Formula>(std::make_shared<GloballyFormula>(subformula));
+        }
+        
+        boost::any CloneVisitor::visit(InstantaneousRewardFormula const& f, boost::any const& data) const {
+            return std::static_pointer_cast<Formula>(std::make_shared<InstantaneousRewardFormula>(f));
+        }
+        
+        boost::any CloneVisitor::visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const {
+            std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
+            return std::static_pointer_cast<Formula>(std::make_shared<LongRunAverageOperatorFormula>(subformula, f.getOperatorInformation()));
+        }
+        
+        boost::any CloneVisitor::visit(LongRunAverageRewardFormula const& f, boost::any const& data) const {
+            return std::static_pointer_cast<Formula>(std::make_shared<LongRunAverageRewardFormula>(f));
+        }
+        
+        boost::any CloneVisitor::visit(NextFormula const& f, boost::any const& data) const {
+            std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
+            return std::static_pointer_cast<Formula>(std::make_shared<NextFormula>(subformula));
+        }
+        
+        boost::any CloneVisitor::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const {
+            std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
+            return std::static_pointer_cast<Formula>(std::make_shared<ProbabilityOperatorFormula>(subformula, f.getOperatorInformation()));
+        }
+        
+        boost::any CloneVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const {
+            std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
+            return std::static_pointer_cast<Formula>(std::make_shared<RewardOperatorFormula>(subformula, f.getOptionalRewardModelName(), f.getOperatorInformation()));
+        }
+        
+        boost::any CloneVisitor::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const {
+            std::shared_ptr<Formula> subformula = boost::any_cast<std::shared_ptr<Formula>>(f.getSubformula().accept(*this, data));
+            return std::static_pointer_cast<Formula>(std::make_shared<UnaryBooleanStateFormula>(f.getOperator(), subformula));
+        }
+        
+        boost::any CloneVisitor::visit(UntilFormula const& f, boost::any const& data) const {
+            std::shared_ptr<Formula> left = boost::any_cast<std::shared_ptr<Formula>>(f.getLeftSubformula().accept(*this, data));
+            std::shared_ptr<Formula> right = boost::any_cast<std::shared_ptr<Formula>>(f.getRightSubformula().accept(*this, data));
+            return std::static_pointer_cast<Formula>(std::make_shared<UntilFormula>(left, right));
+        }
+        
+    }
+}
diff --git a/src/logic/CloneVisitor.h b/src/logic/CloneVisitor.h
new file mode 100644
index 000000000..a23ee4a8b
--- /dev/null
+++ b/src/logic/CloneVisitor.h
@@ -0,0 +1,37 @@
+#ifndef STORM_LOGIC_CLONEVISITOR_H_
+#define STORM_LOGIC_CLONEVISITOR_H_
+
+#include "src/logic/FormulaVisitor.h"
+
+namespace storm {
+    namespace logic {
+        
+        class CloneVisitor : public FormulaVisitor {
+        public:
+            std::shared_ptr<Formula> clone(Formula const& f) const;
+            
+            virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(BooleanLiteralFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(ConditionalFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(TimeOperatorFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(GloballyFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(NextFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(ProbabilityOperatorFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(UntilFormula const& f, boost::any const& data) const override;
+        };
+        
+    }
+}
+
+
+#endif /* STORM_LOGIC_CLONEVISITOR_H_ */
\ No newline at end of file
diff --git a/src/logic/ConditionalFormula.cpp b/src/logic/ConditionalFormula.cpp
index b12b831be..fd1b1b442 100644
--- a/src/logic/ConditionalFormula.cpp
+++ b/src/logic/ConditionalFormula.cpp
@@ -18,6 +18,10 @@ namespace storm {
             return *conditionFormula;
         }
         
+        FormulaContext const& ConditionalFormula::getContext() const {
+            return context;
+        }
+        
         bool ConditionalFormula::isConditionalProbabilityFormula() const {
             return context == FormulaContext::Probability;
         }
@@ -29,11 +33,7 @@ namespace storm {
         boost::any ConditionalFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
             return visitor.visit(*this, data);
         }
-        
-        std::shared_ptr<Formula> ConditionalFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return std::make_shared<ConditionalFormula>(this->getSubformula().substitute(substitution), this->getConditionFormula().substitute(substitution), context);
-        }
-        
+                
         void ConditionalFormula::gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const {
             this->getSubformula().gatherAtomicExpressionFormulas(atomicExpressionFormulas);
             this->getConditionFormula().gatherAtomicExpressionFormulas(atomicExpressionFormulas);
diff --git a/src/logic/ConditionalFormula.h b/src/logic/ConditionalFormula.h
index 66d71ebba..6bb4317b6 100644
--- a/src/logic/ConditionalFormula.h
+++ b/src/logic/ConditionalFormula.h
@@ -7,9 +7,7 @@
 namespace storm {
     namespace logic {
         class ConditionalFormula : public Formula {
-        public:
-            enum class Context { Probability, Reward };
-            
+        public:            
             ConditionalFormula(std::shared_ptr<Formula const> const& subformula, std::shared_ptr<Formula const> const& conditionFormula, FormulaContext context = FormulaContext::Probability);
             
             virtual ~ConditionalFormula() {
@@ -18,6 +16,7 @@ namespace storm {
             
             Formula const& getSubformula() const;
             Formula const& getConditionFormula() const;
+            FormulaContext const& getContext() const;
 
             virtual bool isConditionalProbabilityFormula() const override;
             virtual bool isConditionalRewardFormula() const override;
@@ -26,8 +25,6 @@ namespace storm {
 
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             
-            virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
-            
             virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const override;
             virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const override;
             virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const override;
diff --git a/src/logic/CumulativeRewardFormula.cpp b/src/logic/CumulativeRewardFormula.cpp
index d8318164d..f32d476e5 100644
--- a/src/logic/CumulativeRewardFormula.cpp
+++ b/src/logic/CumulativeRewardFormula.cpp
@@ -44,10 +44,6 @@ namespace storm {
             }
         }
         
-        std::shared_ptr<Formula> CumulativeRewardFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return std::make_shared<CumulativeRewardFormula>(*this);
-        }
-        
         std::ostream& CumulativeRewardFormula::writeToStream(std::ostream& out) const {
             if (this->hasDiscreteTimeBound()) {
                 out << "C<=" << this->getDiscreteTimeBound();
diff --git a/src/logic/CumulativeRewardFormula.h b/src/logic/CumulativeRewardFormula.h
index 6a5e8c035..422bc09ff 100644
--- a/src/logic/CumulativeRewardFormula.h
+++ b/src/logic/CumulativeRewardFormula.h
@@ -32,8 +32,6 @@ namespace storm {
             
             double getContinuousTimeBound() const;
             
-            virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
-            
         private:
             boost::variant<uint_fast64_t, double> timeBound;
         };
diff --git a/src/logic/EventuallyFormula.cpp b/src/logic/EventuallyFormula.cpp
index 56c9decff..e83609e1b 100644
--- a/src/logic/EventuallyFormula.cpp
+++ b/src/logic/EventuallyFormula.cpp
@@ -10,6 +10,10 @@ namespace storm {
             STORM_LOG_THROW(context == FormulaContext::Probability || context == FormulaContext::Reward || context == FormulaContext::Time, storm::exceptions::InvalidPropertyException, "Invalid context for formula.");
         }
         
+        FormulaContext const& EventuallyFormula::getContext() const {
+            return context;
+        }
+        
         bool EventuallyFormula::isEventuallyFormula() const {
             return true;
         }
@@ -41,11 +45,7 @@ namespace storm {
         boost::any EventuallyFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
             return visitor.visit(*this, data);
         }
-        
-        std::shared_ptr<Formula> EventuallyFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return std::make_shared<EventuallyFormula>(this->getSubformula().substitute(substitution), context);
-        }
-        
+                
         std::ostream& EventuallyFormula::writeToStream(std::ostream& out) const {
             out << "F ";
             this->getSubformula().writeToStream(out);
diff --git a/src/logic/EventuallyFormula.h b/src/logic/EventuallyFormula.h
index f3716fee9..779b36f81 100644
--- a/src/logic/EventuallyFormula.h
+++ b/src/logic/EventuallyFormula.h
@@ -14,6 +14,8 @@ namespace storm {
                 // Intentionally left empty.
             }
             
+            FormulaContext const& getContext() const;
+            
             virtual bool isEventuallyFormula() const override;
             virtual bool isReachabilityProbabilityFormula() const override;
             virtual bool isReachabilityRewardFormula() const override;
@@ -26,8 +28,6 @@ namespace storm {
 
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             
-            virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
-
         private:
             FormulaContext context;
         };
diff --git a/src/logic/Formula.cpp b/src/logic/Formula.cpp
index c48548f10..de915eaa1 100644
--- a/src/logic/Formula.cpp
+++ b/src/logic/Formula.cpp
@@ -3,6 +3,9 @@
 
 #include "src/logic/FragmentChecker.h"
 #include "src/logic/FormulaInformationVisitor.h"
+#include "src/logic/VariableSubstitutionVisitor.h"
+#include "src/logic/LabelSubstitutionVisitor.h"
+#include "src/logic/ToExpressionVisitor.h"
 
 namespace storm {
     namespace logic {
@@ -406,6 +409,25 @@ namespace storm {
             return referencedRewardModels;
         }
         
+        std::shared_ptr<Formula> Formula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
+            VariableSubstitutionVisitor visitor(substitution);
+            return visitor.substitute(*this);
+        }
+        
+        std::shared_ptr<Formula> Formula::substitute(std::map<std::string, storm::expressions::Expression> const& labelSubstitution) const {
+            LabelSubstitutionVisitor visitor(labelSubstitution);
+            return visitor.substitute(*this);
+        }
+        
+        storm::expressions::Expression Formula::toExpression(storm::expressions::ExpressionManager const& manager, std::map<std::string, storm::expressions::Expression> const& labelToExpressionMapping) const {
+            ToExpressionVisitor visitor;
+            if (labelToExpressionMapping.empty()) {
+                return visitor.toExpression(*this, manager);
+            } else {
+                return visitor.toExpression(*this->substitute(labelToExpressionMapping), manager);
+            }
+        }
+        
         std::shared_ptr<Formula const> Formula::asSharedPointer() {
             return this->shared_from_this();
         }
diff --git a/src/logic/Formula.h b/src/logic/Formula.h
index b77ecfb20..d5625a296 100644
--- a/src/logic/Formula.h
+++ b/src/logic/Formula.h
@@ -186,7 +186,19 @@ namespace storm {
             std::shared_ptr<Formula const> asSharedPointer();
             std::shared_ptr<Formula const> asSharedPointer() const;
             
-            virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const = 0;
+            std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
+            std::shared_ptr<Formula> substitute(std::map<std::string, storm::expressions::Expression> const& labelSubstitution) const;
+
+            /*!
+             * Takes the formula and converts it to an equivalent expression. The formula may contain atomic labels, but
+             * then the given mapping must provide a corresponding expression. Other than that, only atomic expression
+             * formulas and boolean connectives may appear in the formula.
+             *
+             * @param manager The manager responsible for the expressions in the formula and the resulting expression.
+             * @param A mapping from labels to the expressions that define them.
+             * @return An equivalent expression.
+             */
+            storm::expressions::Expression toExpression(storm::expressions::ExpressionManager const& manager, std::map<std::string, storm::expressions::Expression> const& labelToExpressionMapping = {}) const;
             
             std::string toString() const;
             virtual std::ostream& writeToStream(std::ostream& out) const = 0;
diff --git a/src/logic/FragmentChecker.cpp b/src/logic/FragmentChecker.cpp
index 09bfc31dd..b86a96693 100644
--- a/src/logic/FragmentChecker.cpp
+++ b/src/logic/FragmentChecker.cpp
@@ -19,8 +19,13 @@ namespace storm {
         };
         
         bool FragmentChecker::conformsToSpecification(Formula const& f, FragmentSpecification const& specification) const {
-            boost::any result = f.accept(*this, InheritedInformation(specification));
-            return boost::any_cast<bool>(result);
+            bool result = boost::any_cast<bool>(f.accept(*this, InheritedInformation(specification)));
+            
+            if (specification.isOperatorAtTopLevelRequired()) {
+                result &= f.isOperatorFormula();
+            }
+            
+            return result;
         }
         
         boost::any FragmentChecker::visit(AtomicExpressionFormula const& f, boost::any const& data) const {
diff --git a/src/logic/FragmentSpecification.cpp b/src/logic/FragmentSpecification.cpp
index 31f2eeee2..3dd2bf12b 100644
--- a/src/logic/FragmentSpecification.cpp
+++ b/src/logic/FragmentSpecification.cpp
@@ -17,6 +17,18 @@ namespace storm {
             return propositional;
         }
         
+        FragmentSpecification reachability() {
+            FragmentSpecification reachability = propositional();
+            
+            reachability.setProbabilityOperatorsAllowed(true);
+            reachability.setUntilFormulasAllowed(true);
+            reachability.setReachabilityProbabilityFormulasAllowed(true);
+            reachability.setOperatorAtTopLevelRequired(true);
+            reachability.setNestedOperatorsAllowed(false);
+            
+            return reachability;
+        }
+        
         FragmentSpecification pctl() {
             FragmentSpecification pctl = propositional();
             
@@ -31,6 +43,14 @@ namespace storm {
             return pctl;
         }
         
+        FragmentSpecification flatPctl() {
+            FragmentSpecification flatPctl = pctl();
+            
+            flatPctl.setNestedOperatorsAllowed(false);
+            
+            return flatPctl;
+        }
+        
         FragmentSpecification prctl() {
             FragmentSpecification prctl = pctl();
             
@@ -100,6 +120,8 @@ namespace storm {
             
             qualitativeOperatorResults = true;
             quantitativeOperatorResults = true;
+            
+            operatorAtTopLevelRequired = false;
         }
         
         FragmentSpecification FragmentSpecification::copy() const {
@@ -386,6 +408,14 @@ namespace storm {
             return *this;
         }
 
+        bool FragmentSpecification::isOperatorAtTopLevelRequired() const {
+            return operatorAtTopLevelRequired;
+        }
+        
+        FragmentSpecification& FragmentSpecification::setOperatorAtTopLevelRequired(bool newValue) {
+            operatorAtTopLevelRequired = newValue;
+            return *this;
+        }
         
     }
 }
\ No newline at end of file
diff --git a/src/logic/FragmentSpecification.h b/src/logic/FragmentSpecification.h
index 5074187b8..6637d0750 100644
--- a/src/logic/FragmentSpecification.h
+++ b/src/logic/FragmentSpecification.h
@@ -100,6 +100,9 @@ namespace storm {
             bool areQualitativeOperatorResultsAllowed() const;
             FragmentSpecification& setQualitativeOperatorResultsAllowed(bool newValue);
             
+            bool isOperatorAtTopLevelRequired() const;
+            FragmentSpecification& setOperatorAtTopLevelRequired(bool newValue);
+            
             FragmentSpecification& setOperatorsAllowed(bool newValue);
             FragmentSpecification& setTimeAllowed(bool newValue);
             FragmentSpecification& setLongRunAverageProbabilitiesAllowed(bool newValue);
@@ -142,13 +145,20 @@ namespace storm {
             bool varianceAsMeasureType;
             bool quantitativeOperatorResults;
             bool qualitativeOperatorResults;
+            bool operatorAtTopLevelRequired;
         };
         
         // Propositional.
         FragmentSpecification propositional();
         
+        // Just reachability properties.
+        FragmentSpecification reachability();
+        
         // Regular PCTL.
         FragmentSpecification pctl();
+
+        // Flat PCTL.
+        FragmentSpecification flatPctl();
         
         // PCTL + cumulative, instantaneous, reachability and long-run rewards.
         FragmentSpecification prctl();
diff --git a/src/logic/GloballyFormula.cpp b/src/logic/GloballyFormula.cpp
index df33f0b52..ae6f5b508 100644
--- a/src/logic/GloballyFormula.cpp
+++ b/src/logic/GloballyFormula.cpp
@@ -19,10 +19,6 @@ namespace storm {
         boost::any GloballyFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
             return visitor.visit(*this, data);
         }
-
-        std::shared_ptr<Formula> GloballyFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return std::make_shared<GloballyFormula>(this->getSubformula().substitute(substitution));
-        }
         
         std::ostream& GloballyFormula::writeToStream(std::ostream& out) const {
             out << "G ";
diff --git a/src/logic/GloballyFormula.h b/src/logic/GloballyFormula.h
index 011c61de9..e17347e11 100644
--- a/src/logic/GloballyFormula.h
+++ b/src/logic/GloballyFormula.h
@@ -17,8 +17,6 @@ namespace storm {
             virtual bool isProbabilityPathFormula() const override;
 
             virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
-
-            virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
             
             virtual std::ostream& writeToStream(std::ostream& out) const override;
         };
diff --git a/src/logic/InstantaneousRewardFormula.cpp b/src/logic/InstantaneousRewardFormula.cpp
index 4f1f65429..bf39cd763 100644
--- a/src/logic/InstantaneousRewardFormula.cpp
+++ b/src/logic/InstantaneousRewardFormula.cpp
@@ -43,11 +43,7 @@ namespace storm {
                 return boost::get<double>(timeBound);
             }
         }
-        
-        std::shared_ptr<Formula> InstantaneousRewardFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return std::make_shared<InstantaneousRewardFormula>(*this);
-        }
-        
+                
         std::ostream& InstantaneousRewardFormula::writeToStream(std::ostream& out) const {
             if (this->hasDiscreteTimeBound()) {
                 out << "I=" << this->getDiscreteTimeBound();
diff --git a/src/logic/InstantaneousRewardFormula.h b/src/logic/InstantaneousRewardFormula.h
index 069bf21bd..85d27c450 100644
--- a/src/logic/InstantaneousRewardFormula.h
+++ b/src/logic/InstantaneousRewardFormula.h
@@ -32,9 +32,7 @@ namespace storm {
             bool hasContinuousTimeBound() const;
             
             double getContinuousTimeBound() const;
-            
-            virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
-            
+                        
         private:
             boost::variant<uint_fast64_t, double> timeBound;
         };
diff --git a/src/logic/LabelSubstitutionVisitor.cpp b/src/logic/LabelSubstitutionVisitor.cpp
new file mode 100644
index 000000000..ffb28dbed
--- /dev/null
+++ b/src/logic/LabelSubstitutionVisitor.cpp
@@ -0,0 +1,26 @@
+#include "src/logic/LabelSubstitutionVisitor.h"
+
+#include "src/logic/Formulas.h"
+
+namespace storm {
+    namespace logic {
+        
+        LabelSubstitutionVisitor::LabelSubstitutionVisitor(std::map<std::string, storm::expressions::Expression> const& labelToExpressionMapping) : labelToExpressionMapping(labelToExpressionMapping) {
+            // Intentionally left empty.
+        }
+
+        std::shared_ptr<Formula> LabelSubstitutionVisitor::substitute(Formula const& f) const {
+            boost::any result = f.accept(*this, boost::any());
+            return boost::any_cast<std::shared_ptr<Formula>>(result);
+        }
+        
+        boost::any LabelSubstitutionVisitor::visit(AtomicLabelFormula const& f, boost::any const& data) const {
+            auto it = labelToExpressionMapping.find(f.getLabel());
+            if (it != labelToExpressionMapping.end()) {
+                return std::static_pointer_cast<Formula>(std::make_shared<AtomicExpressionFormula>(it->second));
+            } else {
+                return std::static_pointer_cast<Formula>(std::make_shared<AtomicLabelFormula>(f));
+            }
+        }        
+    }
+}
diff --git a/src/logic/LabelSubstitutionVisitor.h b/src/logic/LabelSubstitutionVisitor.h
new file mode 100644
index 000000000..dec06231e
--- /dev/null
+++ b/src/logic/LabelSubstitutionVisitor.h
@@ -0,0 +1,29 @@
+#ifndef STORM_LOGIC_LABELSUBSTITUTIONVISITOR_H_
+#define STORM_LOGIC_LABELSUBSTITUTIONVISITOR_H_
+
+#include <map>
+
+#include "src/logic/CloneVisitor.h"
+
+#include "src/storage/expressions/Expression.h"
+
+namespace storm {
+    namespace logic {
+        
+        class LabelSubstitutionVisitor : public CloneVisitor {
+        public:
+            LabelSubstitutionVisitor(std::map<std::string, storm::expressions::Expression> const& labelToExpressionMapping);
+            
+            std::shared_ptr<Formula> substitute(Formula const& f) const;
+            
+            virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const override;
+            
+        private:
+            std::map<std::string, storm::expressions::Expression> const& labelToExpressionMapping;
+        };
+        
+    }
+}
+
+
+#endif /* STORM_LOGIC_FORMULAINFORMATIONVISITOR_H_ */
\ No newline at end of file
diff --git a/src/logic/LongRunAverageOperatorFormula.cpp b/src/logic/LongRunAverageOperatorFormula.cpp
index f2e253ead..bf6b250ea 100644
--- a/src/logic/LongRunAverageOperatorFormula.cpp
+++ b/src/logic/LongRunAverageOperatorFormula.cpp
@@ -18,11 +18,7 @@ namespace storm {
         boost::any LongRunAverageOperatorFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
             return visitor.visit(*this, data);
         }
-        
-        std::shared_ptr<Formula> LongRunAverageOperatorFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return std::make_shared<LongRunAverageOperatorFormula>(this->getSubformula().substitute(substitution), this->operatorInformation);
-        }
-        
+                
         std::ostream& LongRunAverageOperatorFormula::writeToStream(std::ostream& out) const {
             out << "LRA";
             OperatorFormula::writeToStream(out);
diff --git a/src/logic/LongRunAverageOperatorFormula.h b/src/logic/LongRunAverageOperatorFormula.h
index 394188b67..3590ac5b2 100644
--- a/src/logic/LongRunAverageOperatorFormula.h
+++ b/src/logic/LongRunAverageOperatorFormula.h
@@ -17,8 +17,6 @@ namespace storm {
             
             virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
             
-            virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
-
             virtual std::ostream& writeToStream(std::ostream& out) const override;
         };
     }
diff --git a/src/logic/LongRunAverageRewardFormula.cpp b/src/logic/LongRunAverageRewardFormula.cpp
index 30bfd7ba9..3207b9bf2 100644
--- a/src/logic/LongRunAverageRewardFormula.cpp
+++ b/src/logic/LongRunAverageRewardFormula.cpp
@@ -20,10 +20,6 @@ namespace storm {
             return visitor.visit(*this, data);
         }
         
-        std::shared_ptr<Formula> LongRunAverageRewardFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return std::shared_ptr<Formula>(new LongRunAverageRewardFormula());
-        }
-        
         std::ostream& LongRunAverageRewardFormula::writeToStream(std::ostream& out) const {
             return out << "LRA";
         }
diff --git a/src/logic/LongRunAverageRewardFormula.h b/src/logic/LongRunAverageRewardFormula.h
index 3dfea465e..d65e55314 100644
--- a/src/logic/LongRunAverageRewardFormula.h
+++ b/src/logic/LongRunAverageRewardFormula.h
@@ -17,8 +17,6 @@ namespace storm {
             virtual bool isRewardPathFormula() const override;
 
             virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
-
-            virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
             
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             
diff --git a/src/logic/NextFormula.cpp b/src/logic/NextFormula.cpp
index e73171a95..a0916e14f 100644
--- a/src/logic/NextFormula.cpp
+++ b/src/logic/NextFormula.cpp
@@ -19,11 +19,7 @@ namespace storm {
         boost::any NextFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
             return visitor.visit(*this, data);
         }
-        
-        std::shared_ptr<Formula> NextFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return std::make_shared<NextFormula>(this->getSubformula().substitute(substitution));
-        }
-        
+                
         std::ostream& NextFormula::writeToStream(std::ostream& out) const {
             out << "X ";
             this->getSubformula().writeToStream(out);
diff --git a/src/logic/NextFormula.h b/src/logic/NextFormula.h
index bade60456..4d895a48e 100644
--- a/src/logic/NextFormula.h
+++ b/src/logic/NextFormula.h
@@ -17,9 +17,7 @@ namespace storm {
             virtual bool isProbabilityPathFormula() const override;
 
             virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
-            
-            virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
-            
+                        
             virtual std::ostream& writeToStream(std::ostream& out) const override;
         };
     }
diff --git a/src/logic/OperatorFormula.cpp b/src/logic/OperatorFormula.cpp
index 4a8e2e215..474a9608b 100644
--- a/src/logic/OperatorFormula.cpp
+++ b/src/logic/OperatorFormula.cpp
@@ -50,6 +50,10 @@ namespace storm {
             return true;
         }
         
+        OperatorInformation const& OperatorFormula::getOperatorInformation() const {
+            return operatorInformation;
+        }
+        
         bool OperatorFormula::hasQualitativeResult() const {
             return this->hasBound();
         }
diff --git a/src/logic/OperatorFormula.h b/src/logic/OperatorFormula.h
index 447647b99..ee7f7a87a 100644
--- a/src/logic/OperatorFormula.h
+++ b/src/logic/OperatorFormula.h
@@ -37,7 +37,9 @@ namespace storm {
             bool hasOptimalityType() const;
             storm::solver::OptimizationDirection const& getOptimalityType() const;
             virtual bool isOperatorFormula() const override;
-                        
+            
+            OperatorInformation const& getOperatorInformation() const;
+            
             virtual bool hasQualitativeResult() const override;
             virtual bool hasQuantitativeResult() const override;
             
diff --git a/src/logic/ProbabilityOperatorFormula.cpp b/src/logic/ProbabilityOperatorFormula.cpp
index 84d6c55d8..e630e45da 100644
--- a/src/logic/ProbabilityOperatorFormula.cpp
+++ b/src/logic/ProbabilityOperatorFormula.cpp
@@ -18,11 +18,7 @@ namespace storm {
         boost::any ProbabilityOperatorFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
             return visitor.visit(*this, data);
         }
-        
-        std::shared_ptr<Formula> ProbabilityOperatorFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return std::make_shared<ProbabilityOperatorFormula>(this->getSubformula().substitute(substitution), this->operatorInformation);
-        }
-        
+                
         std::ostream& ProbabilityOperatorFormula::writeToStream(std::ostream& out) const {
             out << "P";
             OperatorFormula::writeToStream(out);
diff --git a/src/logic/ProbabilityOperatorFormula.h b/src/logic/ProbabilityOperatorFormula.h
index 786d58b44..b1259262c 100644
--- a/src/logic/ProbabilityOperatorFormula.h
+++ b/src/logic/ProbabilityOperatorFormula.h
@@ -16,9 +16,7 @@ namespace storm {
             virtual bool isProbabilityOperatorFormula() const override;
 
             virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
-            
-            virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
-            
+                        
             virtual std::ostream& writeToStream(std::ostream& out) const override;
         };
     }
diff --git a/src/logic/RewardOperatorFormula.cpp b/src/logic/RewardOperatorFormula.cpp
index 5daea4b59..aba2ec92a 100644
--- a/src/logic/RewardOperatorFormula.cpp
+++ b/src/logic/RewardOperatorFormula.cpp
@@ -40,10 +40,6 @@ namespace storm {
             this->getSubformula().gatherReferencedRewardModels(referencedRewardModels);
         }
         
-        std::shared_ptr<Formula> RewardOperatorFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return std::make_shared<RewardOperatorFormula>(this->getSubformula().substitute(substitution), this->rewardModelName, this->operatorInformation, this->rewardMeasureType);
-        }
-        
         RewardMeasureType RewardOperatorFormula::getMeasureType() const {
             return rewardMeasureType;
         }
diff --git a/src/logic/RewardOperatorFormula.h b/src/logic/RewardOperatorFormula.h
index 300a82e37..99ca17233 100644
--- a/src/logic/RewardOperatorFormula.h
+++ b/src/logic/RewardOperatorFormula.h
@@ -50,9 +50,7 @@ namespace storm {
              * @return The measure type.
              */
             RewardMeasureType getMeasureType() const;
-            
-            virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
-            
+                        
         private:
             // The (optional) name of the reward model this property refers to.
             boost::optional<std::string> rewardModelName;
diff --git a/src/logic/TimeOperatorFormula.cpp b/src/logic/TimeOperatorFormula.cpp
index 6a421a1a5..e7f711729 100644
--- a/src/logic/TimeOperatorFormula.cpp
+++ b/src/logic/TimeOperatorFormula.cpp
@@ -18,11 +18,7 @@ namespace storm {
         boost::any TimeOperatorFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
             return visitor.visit(*this, data);
         }
-        
-        std::shared_ptr<Formula> TimeOperatorFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return std::make_shared<TimeOperatorFormula>(this->getSubformula().substitute(substitution), this->operatorInformation, this->rewardMeasureType);
-        }
-        
+                
         RewardMeasureType TimeOperatorFormula::getMeasureType() const {
             return rewardMeasureType;
         }
diff --git a/src/logic/TimeOperatorFormula.h b/src/logic/TimeOperatorFormula.h
index b9f243a4c..24906bb6e 100644
--- a/src/logic/TimeOperatorFormula.h
+++ b/src/logic/TimeOperatorFormula.h
@@ -18,9 +18,7 @@ namespace storm {
             virtual bool isTimeOperatorFormula() const override;
 
             virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
-            
-            virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
-            
+                        
             virtual std::ostream& writeToStream(std::ostream& out) const override;
             
             /*!
diff --git a/src/logic/ToExpressionVisitor.cpp b/src/logic/ToExpressionVisitor.cpp
new file mode 100644
index 000000000..53dfedeca
--- /dev/null
+++ b/src/logic/ToExpressionVisitor.cpp
@@ -0,0 +1,111 @@
+#include "src/logic/ToExpressionVisitor.h"
+
+#include "src/logic/Formulas.h"
+
+#include "src/storage/expressions/ExpressionManager.h"
+
+#include "src/utility/macros.h"
+#include "src/exceptions/InvalidOperationException.h"
+
+namespace storm {
+    namespace logic {
+        
+        storm::expressions::Expression ToExpressionVisitor::toExpression(Formula const& f, storm::expressions::ExpressionManager const& manager) const {
+            boost::any result = f.accept(*this, std::ref(manager));
+            return boost::any_cast<storm::expressions::Expression>(result);
+        }
+        
+        boost::any ToExpressionVisitor::visit(AtomicExpressionFormula const& f, boost::any const& data) const {
+            return f.getExpression();
+        }
+        
+        boost::any ToExpressionVisitor::visit(AtomicLabelFormula const& f, boost::any const& data) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression, because the undefined atomic label '" << f.getLabel() << "' appears in the formula.");
+        }
+        
+        boost::any ToExpressionVisitor::visit(BinaryBooleanStateFormula const& f, boost::any const& data) const {
+            storm::expressions::Expression left = boost::any_cast<storm::expressions::Expression>(f.getLeftSubformula().accept(*this, data));
+            storm::expressions::Expression right = boost::any_cast<storm::expressions::Expression>(f.getRightSubformula().accept(*this, data));
+            switch (f.getOperator()) {
+                case BinaryBooleanStateFormula::OperatorType::And:
+                    return left && right;
+                    break;
+                case BinaryBooleanStateFormula::OperatorType::Or:
+                    return left || right;
+                    break;
+            }
+        }
+        
+        boost::any ToExpressionVisitor::visit(BooleanLiteralFormula const& f, boost::any const& data) const {
+            storm::expressions::Expression result;
+            if (f.isTrueFormula()) {
+                result = boost::any_cast<std::reference_wrapper<storm::expressions::ExpressionManager const>>(data).get().boolean(true);
+            } else {
+                result = boost::any_cast<std::reference_wrapper<storm::expressions::ExpressionManager const>>(data).get().boolean(false);
+            }
+            return result;
+        }
+        
+        boost::any ToExpressionVisitor::visit(BoundedUntilFormula const& f, boost::any const& data) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
+        }
+        
+        boost::any ToExpressionVisitor::visit(ConditionalFormula const& f, boost::any const& data) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
+        }
+        
+        boost::any ToExpressionVisitor::visit(CumulativeRewardFormula const& f, boost::any const& data) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
+        }
+        
+        boost::any ToExpressionVisitor::visit(EventuallyFormula const& f, boost::any const& data) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
+        }
+        
+        boost::any ToExpressionVisitor::visit(TimeOperatorFormula const& f, boost::any const& data) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
+        }
+        
+        boost::any ToExpressionVisitor::visit(GloballyFormula const& f, boost::any const& data) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
+        }
+        
+        boost::any ToExpressionVisitor::visit(InstantaneousRewardFormula const& f, boost::any const& data) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
+        }
+        
+        boost::any ToExpressionVisitor::visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
+        }
+        
+        boost::any ToExpressionVisitor::visit(LongRunAverageRewardFormula const& f, boost::any const& data) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
+        }
+        
+        boost::any ToExpressionVisitor::visit(NextFormula const& f, boost::any const& data) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
+        }
+        
+        boost::any ToExpressionVisitor::visit(ProbabilityOperatorFormula const& f, boost::any const& data) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
+        }
+        
+        boost::any ToExpressionVisitor::visit(RewardOperatorFormula const& f, boost::any const& data) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
+        }
+        
+        boost::any ToExpressionVisitor::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const {
+            storm::expressions::Expression subexpression = boost::any_cast<storm::expressions::Expression>(f.getSubformula().accept(*this, data));
+            switch (f.getOperator()) {
+                case UnaryBooleanStateFormula::OperatorType::Not:
+                    return !subexpression;
+                    break;
+            }
+        }
+        
+        boost::any ToExpressionVisitor::visit(UntilFormula const& f, boost::any const& data) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
+        }
+        
+    }
+}
diff --git a/src/logic/ToExpressionVisitor.h b/src/logic/ToExpressionVisitor.h
new file mode 100644
index 000000000..ee4a81d8f
--- /dev/null
+++ b/src/logic/ToExpressionVisitor.h
@@ -0,0 +1,39 @@
+#ifndef STORM_LOGIC_TOEXPRESSIONVISITOR_H_
+#define STORM_LOGIC_TOEXPRESSIONVISITOR_H_
+
+#include "src/logic/FormulaVisitor.h"
+
+#include "src/storage/expressions/Expression.h"
+
+namespace storm {
+    namespace logic {
+        
+        class ToExpressionVisitor : public FormulaVisitor {
+        public:
+            storm::expressions::Expression toExpression(Formula const& f, storm::expressions::ExpressionManager const& manager) const;
+            
+            virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(BooleanLiteralFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(ConditionalFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(TimeOperatorFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(GloballyFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(NextFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(ProbabilityOperatorFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(UntilFormula const& f, boost::any const& data) const override;
+        };
+        
+    }
+}
+
+
+#endif /* STORM_LOGIC_TOEXPRESSIONVISITOR_H_ */
\ No newline at end of file
diff --git a/src/logic/UnaryBooleanStateFormula.cpp b/src/logic/UnaryBooleanStateFormula.cpp
index 3983e5b27..83feb7fd4 100644
--- a/src/logic/UnaryBooleanStateFormula.cpp
+++ b/src/logic/UnaryBooleanStateFormula.cpp
@@ -26,11 +26,7 @@ namespace storm {
         bool UnaryBooleanStateFormula::isNot() const {
             return this->getOperator() == OperatorType::Not;
         }
-        
-        std::shared_ptr<Formula> UnaryBooleanStateFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return std::make_shared<UnaryBooleanStateFormula>(this->operatorType, this->getSubformula().substitute(substitution));
-        }
-        
+                
         std::ostream& UnaryBooleanStateFormula::writeToStream(std::ostream& out) const {
             switch (operatorType) {
                 case OperatorType::Not: out << "!("; break;
diff --git a/src/logic/UnaryBooleanStateFormula.h b/src/logic/UnaryBooleanStateFormula.h
index 93d45f862..a30886a60 100644
--- a/src/logic/UnaryBooleanStateFormula.h
+++ b/src/logic/UnaryBooleanStateFormula.h
@@ -22,8 +22,6 @@ namespace storm {
             OperatorType getOperator() const;
             
             virtual bool isNot() const;
-
-            virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
             
             virtual std::ostream& writeToStream(std::ostream& out) const override;
 
diff --git a/src/logic/UntilFormula.cpp b/src/logic/UntilFormula.cpp
index a00eae77d..3aaf93da1 100644
--- a/src/logic/UntilFormula.cpp
+++ b/src/logic/UntilFormula.cpp
@@ -20,10 +20,6 @@ namespace storm {
             return visitor.visit(*this, data);
         }
         
-        std::shared_ptr<Formula> UntilFormula::substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const {
-            return std::make_shared<UntilFormula>(this->getLeftSubformula().substitute(substitution), this->getRightSubformula().substitute(substitution));
-        }
-        
         std::ostream& UntilFormula::writeToStream(std::ostream& out) const {
             this->getLeftSubformula().writeToStream(out);
             out << " U ";
diff --git a/src/logic/UntilFormula.h b/src/logic/UntilFormula.h
index 887d39b45..e03d32047 100644
--- a/src/logic/UntilFormula.h
+++ b/src/logic/UntilFormula.h
@@ -17,9 +17,7 @@ namespace storm {
             virtual bool isProbabilityPathFormula() const override;
 
             virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
-            
-            virtual std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const override;
-            
+                        
             virtual std::ostream& writeToStream(std::ostream& out) const override;
         };
     }
diff --git a/src/logic/VariableSubstitutionVisitor.cpp b/src/logic/VariableSubstitutionVisitor.cpp
new file mode 100644
index 000000000..9a5ba5b8a
--- /dev/null
+++ b/src/logic/VariableSubstitutionVisitor.cpp
@@ -0,0 +1,21 @@
+#include "src/logic/VariableSubstitutionVisitor.h"
+
+#include "src/logic/Formulas.h"
+
+namespace storm {
+    namespace logic {
+        
+        VariableSubstitutionVisitor::VariableSubstitutionVisitor(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) : substitution(substitution) {
+            // Intentionally left empty.
+        }
+        
+        std::shared_ptr<Formula> VariableSubstitutionVisitor::substitute(Formula const& f) const {
+            boost::any result = f.accept(*this, boost::any());
+            return boost::any_cast<std::shared_ptr<Formula>>(result);
+        }
+        
+        boost::any VariableSubstitutionVisitor::visit(AtomicExpressionFormula const& f, boost::any const& data) const {
+            return std::static_pointer_cast<Formula>(std::make_shared<AtomicExpressionFormula>(f.getExpression().substitute(substitution)));
+        }
+    }
+}
diff --git a/src/logic/VariableSubstitutionVisitor.h b/src/logic/VariableSubstitutionVisitor.h
new file mode 100644
index 000000000..11876ba59
--- /dev/null
+++ b/src/logic/VariableSubstitutionVisitor.h
@@ -0,0 +1,29 @@
+#ifndef STORM_LOGIC_VARIABLESUBSTITUTIONVISITOR_H_
+#define STORM_LOGIC_VARIABLESUBSTITUTIONVISITOR_H_
+
+#include <map>
+
+#include "src/logic/CloneVisitor.h"
+
+#include "src/storage/expressions/Expression.h"
+
+namespace storm {
+    namespace logic {
+        
+        class VariableSubstitutionVisitor : public CloneVisitor {
+        public:
+            VariableSubstitutionVisitor(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution);
+            
+            std::shared_ptr<Formula> substitute(Formula const& f) const;
+            
+            virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const override;
+            
+        private:
+            std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution;
+        };
+        
+    }
+}
+
+
+#endif /* STORM_LOGIC_VARIABLESUBSTITUTIONVISITOR_H_ */
\ No newline at end of file
diff --git a/src/modelchecker/AbstractModelChecker.cpp b/src/modelchecker/AbstractModelChecker.cpp
index 0ad70fd4b..850cae65d 100644
--- a/src/modelchecker/AbstractModelChecker.cpp
+++ b/src/modelchecker/AbstractModelChecker.cpp
@@ -13,7 +13,7 @@ namespace storm {
     namespace modelchecker {
         std::unique_ptr<CheckResult> AbstractModelChecker::check(CheckTask<storm::logic::Formula> const& checkTask) {
             storm::logic::Formula const& formula = checkTask.getFormula();
-            STORM_LOG_THROW(this->canHandle(formula), storm::exceptions::InvalidArgumentException, "The model checker is not able to check the formula '" << formula << "'.");
+            STORM_LOG_THROW(this->canHandle(checkTask), storm::exceptions::InvalidArgumentException, "The model checker is not able to check the formula '" << formula << "'.");
             if (formula.isStateFormula()) {
                 return this->checkStateFormula(checkTask.substituteFormula(formula.asStateFormula()));
             }
diff --git a/src/modelchecker/CheckTask.h b/src/modelchecker/CheckTask.h
index 8693f09f2..3d45dd5d4 100644
--- a/src/modelchecker/CheckTask.h
+++ b/src/modelchecker/CheckTask.h
@@ -23,7 +23,7 @@ namespace storm {
         /*
          * This class is used to customize the checking process of a formula.
          */
-        template<typename FormulaType, typename ValueType = double>
+        template<typename FormulaType = storm::logic::Formula, typename ValueType = double>
         class CheckTask {
         public:
             template<typename OtherFormulaType, typename OtherValueType>
diff --git a/src/modelchecker/exploration/Bounds.cpp b/src/modelchecker/exploration/Bounds.cpp
new file mode 100644
index 000000000..db36d0f16
--- /dev/null
+++ b/src/modelchecker/exploration/Bounds.cpp
@@ -0,0 +1,149 @@
+#include "src/modelchecker/exploration/Bounds.h"
+
+#include "src/modelchecker/exploration/ExplorationInformation.h"
+
+namespace storm {
+    namespace modelchecker {
+        namespace exploration_detail {
+            
+            template<typename StateType, typename ValueType>
+            std::pair<ValueType, ValueType> Bounds<StateType, ValueType>::getBoundsForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation) const {
+                ActionType index = explorationInformation.getRowGroup(state);
+                if (index == explorationInformation.getUnexploredMarker()) {
+                    return std::make_pair(storm::utility::zero<ValueType>(), storm::utility::one<ValueType>());
+                } else {
+                    return boundsPerState[index];
+                }
+            }
+                        
+            template<typename StateType, typename ValueType>
+            ValueType Bounds<StateType, ValueType>::getLowerBoundForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation) const {
+                ActionType index = explorationInformation.getRowGroup(state);
+                if (index == explorationInformation.getUnexploredMarker()) {
+                    return storm::utility::zero<ValueType>();
+                } else {
+                    return getLowerBoundForRowGroup(index);
+                }
+            }
+            
+            template<typename StateType, typename ValueType>
+            ValueType const& Bounds<StateType, ValueType>::getLowerBoundForRowGroup(StateType const& rowGroup) const {
+                return boundsPerState[rowGroup].first;
+            }
+            
+            template<typename StateType, typename ValueType>
+            ValueType Bounds<StateType, ValueType>::getUpperBoundForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation) const {
+                ActionType index = explorationInformation.getRowGroup(state);
+                if (index == explorationInformation.getUnexploredMarker()) {
+                    return storm::utility::one<ValueType>();
+                } else {
+                    return getUpperBoundForRowGroup(index);
+                }
+            }
+            
+            template<typename StateType, typename ValueType>
+            ValueType const& Bounds<StateType, ValueType>::getUpperBoundForRowGroup(StateType const& rowGroup) const {
+                return boundsPerState[rowGroup].second;
+            }
+            
+            template<typename StateType, typename ValueType>
+            std::pair<ValueType, ValueType> const& Bounds<StateType, ValueType>::getBoundsForAction(ActionType const& action) const {
+                return boundsPerAction[action];
+            }
+            
+            template<typename StateType, typename ValueType>
+            ValueType const& Bounds<StateType, ValueType>::getLowerBoundForAction(ActionType const& action) const {
+                return boundsPerAction[action].first;
+            }
+            
+            template<typename StateType, typename ValueType>
+            ValueType const& Bounds<StateType, ValueType>::getUpperBoundForAction(ActionType const& action) const {
+                return boundsPerAction[action].second;
+            }
+            
+            template<typename StateType, typename ValueType>
+            ValueType const& Bounds<StateType, ValueType>::getBoundForAction(storm::OptimizationDirection const& direction, ActionType const& action) const {
+                if (direction == storm::OptimizationDirection::Maximize) {
+                    return getUpperBoundForAction(action);
+                } else {
+                    return getLowerBoundForAction(action);
+                }
+            }
+            
+            template<typename StateType, typename ValueType>
+            ValueType Bounds<StateType, ValueType>::getDifferenceOfStateBounds(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation) const {
+                std::pair<ValueType, ValueType> bounds = getBoundsForState(state, explorationInformation);
+                return bounds.second - bounds.first;
+            }
+            
+            template<typename StateType, typename ValueType>
+            void Bounds<StateType, ValueType>::initializeBoundsForNextState(std::pair<ValueType, ValueType> const& vals) {
+                boundsPerState.push_back(vals);
+            }
+            
+            template<typename StateType, typename ValueType>
+            void Bounds<StateType, ValueType>::initializeBoundsForNextAction(std::pair<ValueType, ValueType> const& vals) {
+                boundsPerAction.push_back(vals);
+            }
+            
+            template<typename StateType, typename ValueType>
+            void Bounds<StateType, ValueType>::setLowerBoundForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation, ValueType const& value) {
+                setLowerBoundForRowGroup(explorationInformation.getRowGroup(state), value);
+            }
+            
+            template<typename StateType, typename ValueType>
+            void Bounds<StateType, ValueType>::setLowerBoundForRowGroup(StateType const& group, ValueType const& value) {
+                boundsPerState[group].first = value;
+            }
+            
+            template<typename StateType, typename ValueType>
+            void Bounds<StateType, ValueType>::setUpperBoundForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation, ValueType const& value) {
+                setUpperBoundForRowGroup(explorationInformation.getRowGroup(state), value);
+            }
+            
+            template<typename StateType, typename ValueType>
+            void Bounds<StateType, ValueType>::setUpperBoundForRowGroup(StateType const& group, ValueType const& value) {
+                boundsPerState[group].second = value;
+            }
+            
+            template<typename StateType, typename ValueType>
+            void Bounds<StateType, ValueType>::setBoundsForAction(ActionType const& action, std::pair<ValueType, ValueType> const& values) {
+                boundsPerAction[action] = values;
+            }
+            
+            template<typename StateType, typename ValueType>
+            void Bounds<StateType, ValueType>::setBoundsForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation, std::pair<ValueType, ValueType> const& values) {
+                StateType const& rowGroup = explorationInformation.getRowGroup(state);
+                setBoundsForRowGroup(rowGroup, values);
+            }
+            
+            template<typename StateType, typename ValueType>
+            void Bounds<StateType, ValueType>::setBoundsForRowGroup(StateType const& rowGroup, std::pair<ValueType, ValueType> const& values) {
+                boundsPerState[rowGroup] = values;
+            }
+            
+            template<typename StateType, typename ValueType>
+            bool Bounds<StateType, ValueType>::setLowerBoundOfStateIfGreaterThanOld(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation, ValueType const& newLowerValue) {
+                StateType const& rowGroup = explorationInformation.getRowGroup(state);
+                if (boundsPerState[rowGroup].first < newLowerValue) {
+                    boundsPerState[rowGroup].first = newLowerValue;
+                    return true;
+                }
+                return false;
+            }
+            
+            template<typename StateType, typename ValueType>
+            bool Bounds<StateType, ValueType>::setUpperBoundOfStateIfLessThanOld(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation, ValueType const& newUpperValue) {
+                StateType const& rowGroup = explorationInformation.getRowGroup(state);
+                if (newUpperValue < boundsPerState[rowGroup].second) {
+                    boundsPerState[rowGroup].second = newUpperValue;
+                    return true;
+                }
+                return false;
+            }
+            
+            template class Bounds<uint32_t, double>;
+            
+        }
+    }
+}
diff --git a/src/modelchecker/exploration/Bounds.h b/src/modelchecker/exploration/Bounds.h
new file mode 100644
index 000000000..816e8c923
--- /dev/null
+++ b/src/modelchecker/exploration/Bounds.h
@@ -0,0 +1,74 @@
+#ifndef STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_BOUNDS_H_
+#define STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_BOUNDS_H_
+
+#include <vector>
+#include <utility>
+
+#include "src/solver/OptimizationDirection.h"
+
+#include "src/utility/constants.h"
+
+namespace storm {
+    namespace modelchecker {
+        namespace exploration_detail {
+         
+            template<typename StateType, typename ValueType>
+            class ExplorationInformation;
+            
+            template<typename StateType, typename ValueType>
+            class Bounds {
+            public:
+                typedef StateType ActionType;
+                
+                std::pair<ValueType, ValueType> getBoundsForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation) const;
+                
+                ValueType getLowerBoundForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation) const;
+                
+                ValueType const& getLowerBoundForRowGroup(StateType const& rowGroup) const;
+                
+                ValueType getUpperBoundForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation) const;
+                
+                ValueType const& getUpperBoundForRowGroup(StateType const& rowGroup) const;
+                
+                std::pair<ValueType, ValueType> const& getBoundsForAction(ActionType const& action) const;
+                
+                ValueType const& getLowerBoundForAction(ActionType const& action) const;
+                
+                ValueType const& getUpperBoundForAction(ActionType const& action) const;
+                
+                ValueType const& getBoundForAction(storm::OptimizationDirection const& direction, ActionType const& action) const;
+                
+                ValueType getDifferenceOfStateBounds(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation) const;
+                
+                void initializeBoundsForNextState(std::pair<ValueType, ValueType> const& vals = std::pair<ValueType, ValueType>(storm::utility::zero<ValueType>(), storm::utility::one<ValueType>()));
+                
+                void initializeBoundsForNextAction(std::pair<ValueType, ValueType> const& vals = std::pair<ValueType, ValueType>(storm::utility::zero<ValueType>(), storm::utility::one<ValueType>()));
+                
+                void setLowerBoundForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation, ValueType const& value);
+                
+                void setLowerBoundForRowGroup(StateType const& group, ValueType const& value);
+                
+                void setUpperBoundForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation, ValueType const& value);
+                
+                void setUpperBoundForRowGroup(StateType const& group, ValueType const& value);
+                
+                void setBoundsForAction(ActionType const& action, std::pair<ValueType, ValueType> const& values);
+                
+                void setBoundsForState(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation, std::pair<ValueType, ValueType> const& values);
+                
+                void setBoundsForRowGroup(StateType const& rowGroup, std::pair<ValueType, ValueType> const& values);
+                
+                bool setLowerBoundOfStateIfGreaterThanOld(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation, ValueType const& newLowerValue);
+                
+                bool setUpperBoundOfStateIfLessThanOld(StateType const& state, ExplorationInformation<StateType, ValueType> const& explorationInformation, ValueType const& newUpperValue);
+                
+            private:
+                std::vector<std::pair<ValueType, ValueType>> boundsPerState;
+                std::vector<std::pair<ValueType, ValueType>> boundsPerAction;
+            };
+            
+        }
+    }
+}
+
+#endif /* STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_BOUNDS_H_ */
\ No newline at end of file
diff --git a/src/modelchecker/exploration/ExplorationInformation.cpp b/src/modelchecker/exploration/ExplorationInformation.cpp
new file mode 100644
index 000000000..756fd57d9
--- /dev/null
+++ b/src/modelchecker/exploration/ExplorationInformation.cpp
@@ -0,0 +1,227 @@
+#include "src/modelchecker/exploration/ExplorationInformation.h"
+
+#include "src/settings/SettingsManager.h"
+#include "src/settings/modules/ExplorationSettings.h"
+
+#include "src/utility/macros.h"
+
+namespace storm {
+    namespace modelchecker {
+        namespace exploration_detail {
+            
+            template<typename StateType, typename ValueType>
+            ExplorationInformation<StateType, ValueType>::ExplorationInformation(storm::OptimizationDirection const& direction, ActionType const& unexploredMarker) : unexploredMarker(unexploredMarker), optimizationDirection(direction), localPrecomputation(false), numberOfExplorationStepsUntilPrecomputation(100000), numberOfSampledPathsUntilPrecomputation(), nextStateHeuristic(storm::settings::modules::ExplorationSettings::NextStateHeuristic::DifferenceProbabilitySum) {
+                
+                storm::settings::modules::ExplorationSettings const& settings = storm::settings::explorationSettings();
+                localPrecomputation = settings.isLocalPrecomputationSet();
+                numberOfExplorationStepsUntilPrecomputation = settings.getNumberOfExplorationStepsUntilPrecomputation();
+                if (settings.isNumberOfSampledPathsUntilPrecomputationSet()) {
+                    numberOfSampledPathsUntilPrecomputation = settings.getNumberOfSampledPathsUntilPrecomputation();
+                }
+                
+                nextStateHeuristic = settings.getNextStateHeuristic();
+            }
+            
+            template<typename StateType, typename ValueType>
+            typename ExplorationInformation<StateType, ValueType>::const_iterator ExplorationInformation<StateType, ValueType>::findUnexploredState(StateType const& state) const {
+                return unexploredStates.find(state);
+            }
+            
+            template<typename StateType, typename ValueType>
+            typename ExplorationInformation<StateType, ValueType>::const_iterator ExplorationInformation<StateType, ValueType>::unexploredStatesEnd() const {
+                return unexploredStates.end();
+            }
+            
+            template<typename StateType, typename ValueType>
+            void ExplorationInformation<StateType, ValueType>::removeUnexploredState(const_iterator it) {
+                unexploredStates.erase(it);
+            }
+            
+            template<typename StateType, typename ValueType>
+            void ExplorationInformation<StateType, ValueType>::addUnexploredState(StateType const& stateId, storm::generator::CompressedState const& compressedState) {
+                stateToRowGroupMapping.push_back(unexploredMarker);
+                unexploredStates[stateId] = compressedState;
+            }
+            
+            template<typename StateType, typename ValueType>
+            void ExplorationInformation<StateType, ValueType>::assignStateToRowGroup(StateType const& state, ActionType const& rowGroup) {
+                stateToRowGroupMapping[state] = rowGroup;
+            }
+            
+            template<typename StateType, typename ValueType>
+            StateType ExplorationInformation<StateType, ValueType>::assignStateToNextRowGroup(StateType const& state) {
+                stateToRowGroupMapping[state] = rowGroupIndices.size() - 1;
+                return stateToRowGroupMapping[state];
+            }
+            
+            template<typename StateType, typename ValueType>
+            StateType ExplorationInformation<StateType, ValueType>::getNextRowGroup() const {
+                return rowGroupIndices.size() - 1;
+            }
+            
+            template<typename StateType, typename ValueType>
+            void ExplorationInformation<StateType, ValueType>::newRowGroup(ActionType const& action) {
+                rowGroupIndices.push_back(action);
+            }
+            
+            template<typename StateType, typename ValueType>
+            void ExplorationInformation<StateType, ValueType>::newRowGroup() {
+                newRowGroup(matrix.size());
+            }
+            
+            template<typename StateType, typename ValueType>
+            void ExplorationInformation<StateType, ValueType>::terminateCurrentRowGroup() {
+                rowGroupIndices.push_back(matrix.size());
+            }
+            
+            template<typename StateType, typename ValueType>
+            void ExplorationInformation<StateType, ValueType>::moveActionToBackOfMatrix(ActionType const& action) {
+                matrix.emplace_back(std::move(matrix[action]));
+            }
+            
+            template<typename StateType, typename ValueType>
+            StateType ExplorationInformation<StateType, ValueType>::getActionCount() const {
+                return matrix.size();
+            }
+            
+            template<typename StateType, typename ValueType>
+            std::size_t ExplorationInformation<StateType, ValueType>::getNumberOfUnexploredStates() const {
+                return unexploredStates.size();
+            }
+            
+            template<typename StateType, typename ValueType>
+            std::size_t ExplorationInformation<StateType, ValueType>::getNumberOfDiscoveredStates() const {
+                return stateToRowGroupMapping.size();
+            }
+            
+            template<typename StateType, typename ValueType>
+            StateType const& ExplorationInformation<StateType, ValueType>::getRowGroup(StateType const& state) const {
+                return stateToRowGroupMapping[state];
+            }
+            
+            template<typename StateType, typename ValueType>
+            StateType const& ExplorationInformation<StateType, ValueType>::getUnexploredMarker() const {
+                return unexploredMarker;
+            }
+            
+            template<typename StateType, typename ValueType>
+            bool ExplorationInformation<StateType, ValueType>::isUnexplored(StateType const& state) const {
+                return stateToRowGroupMapping[state] == unexploredMarker;
+            }
+            
+            template<typename StateType, typename ValueType>
+            bool ExplorationInformation<StateType, ValueType>::isTerminal(StateType const& state) const {
+                return terminalStates.find(state) != terminalStates.end();
+            }
+            
+            template<typename StateType, typename ValueType>
+            typename ExplorationInformation<StateType, ValueType>::ActionType const& ExplorationInformation<StateType, ValueType>::getStartRowOfGroup(StateType const& group) const {
+                return rowGroupIndices[group];
+            }
+            
+            template<typename StateType, typename ValueType>
+            std::size_t ExplorationInformation<StateType, ValueType>::getRowGroupSize(StateType const& group) const {
+                return rowGroupIndices[group + 1] - rowGroupIndices[group];
+            }
+            
+            template<typename StateType, typename ValueType>
+            bool ExplorationInformation<StateType, ValueType>::onlyOneActionAvailable(StateType const& group) const {
+                return getRowGroupSize(group) == 1;
+            }
+            
+            template<typename StateType, typename ValueType>
+            void ExplorationInformation<StateType, ValueType>::addTerminalState(StateType const& state) {
+                terminalStates.insert(state);
+            }
+            
+            template<typename StateType, typename ValueType>
+            std::vector<storm::storage::MatrixEntry<StateType, ValueType>>& ExplorationInformation<StateType, ValueType>::getRowOfMatrix(ActionType const& row) {
+                return matrix[row];
+            }
+            
+            template<typename StateType, typename ValueType>
+            std::vector<storm::storage::MatrixEntry<StateType, ValueType>> const& ExplorationInformation<StateType, ValueType>::getRowOfMatrix(ActionType const& row) const {
+                return matrix[row];
+            }
+            
+            template<typename StateType, typename ValueType>
+            void ExplorationInformation<StateType, ValueType>::addActionsToMatrix(std::size_t const& count) {
+                matrix.resize(matrix.size() + count);
+            }
+            
+            template<typename StateType, typename ValueType>
+            bool ExplorationInformation<StateType, ValueType>::maximize() const {
+                return optimizationDirection == storm::OptimizationDirection::Maximize;
+            }
+            
+            template<typename StateType, typename ValueType>
+            bool ExplorationInformation<StateType, ValueType>::minimize() const {
+                return !maximize();
+            }
+            
+            template<typename StateType, typename ValueType>
+            bool ExplorationInformation<StateType, ValueType>::performPrecomputationExcessiveExplorationSteps(std::size_t& numberExplorationStepsSinceLastPrecomputation) const {
+                bool result = numberExplorationStepsSinceLastPrecomputation > numberOfExplorationStepsUntilPrecomputation;
+                if (result) {
+                    numberExplorationStepsSinceLastPrecomputation = 0;
+                }
+                return result;
+            }
+            
+            template<typename StateType, typename ValueType>
+            bool ExplorationInformation<StateType, ValueType>::performPrecomputationExcessiveSampledPaths(std::size_t& numberOfSampledPathsSinceLastPrecomputation) const {
+                if (!numberOfSampledPathsUntilPrecomputation) {
+                    return false;
+                } else {
+                    bool result = numberOfSampledPathsSinceLastPrecomputation > numberOfSampledPathsUntilPrecomputation.get();
+                    if (result) {
+                        numberOfSampledPathsSinceLastPrecomputation = 0;
+                    }
+                    return result;
+                }
+            }
+            
+            template<typename StateType, typename ValueType>
+            bool ExplorationInformation<StateType, ValueType>::useLocalPrecomputation() const {
+                return localPrecomputation;
+            }
+            
+            template<typename StateType, typename ValueType>
+            bool ExplorationInformation<StateType, ValueType>::useGlobalPrecomputation() const {
+                return !useLocalPrecomputation();
+            }
+            
+            template<typename StateType, typename ValueType>
+            storm::settings::modules::ExplorationSettings::NextStateHeuristic const& ExplorationInformation<StateType, ValueType>::getNextStateHeuristic() const {
+                return nextStateHeuristic;
+            }
+            
+            template<typename StateType, typename ValueType>
+            bool ExplorationInformation<StateType, ValueType>::useDifferenceProbabilitySumHeuristic() const {
+                return nextStateHeuristic == storm::settings::modules::ExplorationSettings::NextStateHeuristic::DifferenceProbabilitySum;
+            }
+            
+            template<typename StateType, typename ValueType>
+            bool ExplorationInformation<StateType, ValueType>::useProbabilityHeuristic() const {
+                return nextStateHeuristic == storm::settings::modules::ExplorationSettings::NextStateHeuristic::Probability;
+            }
+
+            template<typename StateType, typename ValueType>
+            bool ExplorationInformation<StateType, ValueType>::useUniformHeuristic() const {
+                return nextStateHeuristic == storm::settings::modules::ExplorationSettings::NextStateHeuristic::Uniform;
+            }
+            
+            template<typename StateType, typename ValueType>
+            storm::OptimizationDirection const& ExplorationInformation<StateType, ValueType>::getOptimizationDirection() const {
+                return optimizationDirection;
+            }
+            
+            template<typename StateType, typename ValueType>
+            void ExplorationInformation<StateType, ValueType>::setOptimizationDirection(storm::OptimizationDirection const& direction) {
+                optimizationDirection = direction;
+            }
+            
+            template class ExplorationInformation<uint32_t, double>;
+        }
+    }
+}
\ No newline at end of file
diff --git a/src/modelchecker/exploration/ExplorationInformation.h b/src/modelchecker/exploration/ExplorationInformation.h
new file mode 100644
index 000000000..4716bfc96
--- /dev/null
+++ b/src/modelchecker/exploration/ExplorationInformation.h
@@ -0,0 +1,128 @@
+#ifndef STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_EXPLORATIONINFORMATION_H_
+#define STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_EXPLORATIONINFORMATION_H_
+
+#include <vector>
+#include <limits>
+#include <unordered_map>
+
+#include <boost/optional.hpp>
+#include <boost/container/flat_set.hpp>
+
+#include "src/solver/OptimizationDirection.h"
+
+#include "src/generator/CompressedState.h"
+
+#include "src/storage/SparseMatrix.h"
+
+#include "src/settings/modules/ExplorationSettings.h"
+
+namespace storm {    
+    namespace modelchecker {
+        namespace exploration_detail {
+            template<typename StateType, typename ValueType>
+            class ExplorationInformation {
+            public:
+                typedef StateType ActionType;
+                typedef boost::container::flat_set<StateType> StateSet;
+                typedef std::unordered_map<StateType, storm::generator::CompressedState> IdToStateMap;
+                typedef typename IdToStateMap::const_iterator const_iterator;
+                typedef std::vector<std::vector<storm::storage::MatrixEntry<StateType, ValueType>>> MatrixType;
+                
+                ExplorationInformation(storm::OptimizationDirection const& direction, ActionType const& unexploredMarker = std::numeric_limits<ActionType>::max());
+                
+                const_iterator findUnexploredState(StateType const& state) const;
+                
+                const_iterator unexploredStatesEnd() const;
+                
+                void removeUnexploredState(const_iterator it);
+                
+                void addUnexploredState(StateType const& stateId, storm::generator::CompressedState const& compressedState);
+                
+                void assignStateToRowGroup(StateType const& state, ActionType const& rowGroup);
+                
+                StateType assignStateToNextRowGroup(StateType const& state);
+                
+                StateType getNextRowGroup() const;
+                
+                void newRowGroup(ActionType const& action);
+                
+                void newRowGroup();
+                
+                void terminateCurrentRowGroup();
+                
+                void moveActionToBackOfMatrix(ActionType const& action);
+                
+                StateType getActionCount() const;
+                
+                std::size_t getNumberOfUnexploredStates() const;
+                
+                std::size_t getNumberOfDiscoveredStates() const;
+                
+                StateType const& getRowGroup(StateType const& state) const;
+                
+                StateType const& getUnexploredMarker() const;
+                
+                bool isUnexplored(StateType const& state) const;
+                
+                bool isTerminal(StateType const& state) const;
+                
+                ActionType const& getStartRowOfGroup(StateType const& group) const;
+                
+                std::size_t getRowGroupSize(StateType const& group) const;
+                
+                bool onlyOneActionAvailable(StateType const& group) const;
+                
+                void addTerminalState(StateType const& state);
+                
+                std::vector<storm::storage::MatrixEntry<StateType, ValueType>>& getRowOfMatrix(ActionType const& row);
+                
+                std::vector<storm::storage::MatrixEntry<StateType, ValueType>> const& getRowOfMatrix(ActionType const& row) const;
+                
+                void addActionsToMatrix(std::size_t const& count);
+                
+                bool maximize() const;
+                
+                bool minimize() const;
+                
+                bool performPrecomputationExcessiveExplorationSteps(std::size_t& numberExplorationStepsSinceLastPrecomputation) const;
+                
+                bool performPrecomputationExcessiveSampledPaths(std::size_t& numberOfSampledPathsSinceLastPrecomputation) const;
+                
+                bool useLocalPrecomputation() const;
+                
+                bool useGlobalPrecomputation() const;
+                
+                storm::settings::modules::ExplorationSettings::NextStateHeuristic const& getNextStateHeuristic() const;
+                
+                bool useDifferenceProbabilitySumHeuristic() const;
+                
+                bool useProbabilityHeuristic() const;
+                
+                bool useUniformHeuristic() const;
+                
+                storm::OptimizationDirection const& getOptimizationDirection() const;
+                
+                void setOptimizationDirection(storm::OptimizationDirection const& direction);
+                
+            private:
+                MatrixType matrix;
+                std::vector<StateType> rowGroupIndices;
+                
+                std::vector<StateType> stateToRowGroupMapping;
+                StateType unexploredMarker;
+                IdToStateMap unexploredStates;
+                
+                storm::OptimizationDirection optimizationDirection;
+                StateSet terminalStates;
+                
+                bool localPrecomputation;
+                std::size_t numberOfExplorationStepsUntilPrecomputation;
+                boost::optional<std::size_t> numberOfSampledPathsUntilPrecomputation;
+                
+                storm::settings::modules::ExplorationSettings::NextStateHeuristic nextStateHeuristic;
+            };
+        }
+    }
+}
+
+#endif /* STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_EXPLORATIONINFORMATION_H_ */
\ No newline at end of file
diff --git a/src/modelchecker/exploration/SparseExplorationModelChecker.cpp b/src/modelchecker/exploration/SparseExplorationModelChecker.cpp
new file mode 100644
index 000000000..322af7999
--- /dev/null
+++ b/src/modelchecker/exploration/SparseExplorationModelChecker.cpp
@@ -0,0 +1,687 @@
+#include "src/modelchecker/exploration/SparseExplorationModelChecker.h"
+
+#include "src/modelchecker/exploration/ExplorationInformation.h"
+#include "src/modelchecker/exploration/StateGeneration.h"
+#include "src/modelchecker/exploration/Bounds.h"
+#include "src/modelchecker/exploration/Statistics.h"
+
+#include "src/generator/CompressedState.h"
+
+#include "src/storage/SparseMatrix.h"
+#include "src/storage/MaximalEndComponentDecomposition.h"
+
+#include "src/storage/prism/Program.h"
+
+#include "src/logic/FragmentSpecification.h"
+
+#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+
+#include "src/models/sparse/StandardRewardModel.h"
+
+#include "src/settings/SettingsManager.h"
+#include "src/settings/modules/GeneralSettings.h"
+
+#include "src/utility/macros.h"
+#include "src/utility/constants.h"
+#include "src/utility/graph.h"
+#include "src/utility/prism.h"
+
+#include "src/exceptions/InvalidOperationException.h"
+#include "src/exceptions/InvalidPropertyException.h"
+#include "src/exceptions/NotSupportedException.h"
+
+namespace storm {
+    namespace modelchecker {
+        
+        template<typename ValueType, typename StateType>
+        SparseExplorationModelChecker<ValueType, StateType>::SparseExplorationModelChecker(storm::prism::Program const& program, boost::optional<std::map<storm::expressions::Variable, storm::expressions::Expression>> const& constantDefinitions) : program(storm::utility::prism::preprocessProgram<ValueType>(program, constantDefinitions)), variableInformation(this->program), randomGenerator(std::chrono::system_clock::now().time_since_epoch().count()), comparator(storm::settings::explorationSettings().getPrecision()) {
+            // Intentionally left empty.
+        }
+        
+        template<typename ValueType, typename StateType>
+        bool SparseExplorationModelChecker<ValueType, StateType>::canHandle(CheckTask<storm::logic::Formula> const& checkTask) const {
+            storm::logic::Formula const& formula = checkTask.getFormula();
+            storm::logic::FragmentSpecification fragment = storm::logic::reachability();
+            return formula.isInFragment(fragment) && checkTask.isOnlyInitialStatesRelevantSet();
+        }
+        
+        template<typename ValueType, typename StateType>
+        std::unique_ptr<CheckResult> SparseExplorationModelChecker<ValueType, StateType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) {
+            storm::logic::UntilFormula const& untilFormula = checkTask.getFormula();
+            storm::logic::Formula const& conditionFormula = untilFormula.getLeftSubformula();
+            storm::logic::Formula const& targetFormula = untilFormula.getRightSubformula();
+            STORM_LOG_THROW(program.isDeterministicModel() || checkTask.isOptimizationDirectionSet(), storm::exceptions::InvalidPropertyException, "For nondeterministic systems, an optimization direction (min/max) must be given in the property.");
+            
+            ExplorationInformation<StateType, ValueType> explorationInformation(checkTask.isOptimizationDirectionSet() ? checkTask.getOptimizationDirection() : storm::OptimizationDirection::Maximize);
+            
+            // The first row group starts at action 0.
+            explorationInformation.newRowGroup(0);
+            
+            std::map<std::string, storm::expressions::Expression> labelToExpressionMapping = program.getLabelToExpressionMapping();
+            StateGeneration<StateType, ValueType> stateGeneration(program, variableInformation, explorationInformation, conditionFormula.toExpression(program.getManager(), labelToExpressionMapping), targetFormula.toExpression(program.getManager(), labelToExpressionMapping));
+            
+            
+            // Compute and return result.
+            std::tuple<StateType, ValueType, ValueType> boundsForInitialState = performExploration(stateGeneration, explorationInformation);
+            return std::make_unique<ExplicitQuantitativeCheckResult<ValueType>>(std::get<0>(boundsForInitialState), std::get<1>(boundsForInitialState));
+        }
+        
+        template<typename ValueType, typename StateType>
+        std::tuple<StateType, ValueType, ValueType> SparseExplorationModelChecker<ValueType, StateType>::performExploration(StateGeneration<StateType, ValueType>& stateGeneration, ExplorationInformation<StateType, ValueType>& explorationInformation) const {
+            // Generate the initial state so we know where to start the simulation.
+            stateGeneration.computeInitialStates();
+            STORM_LOG_THROW(stateGeneration.getNumberOfInitialStates() == 1, storm::exceptions::NotSupportedException, "Currently only models with one initial state are supported by the exploration engine.");
+            StateType initialStateIndex = stateGeneration.getFirstInitialState();
+            
+            // Create a structure that holds the bounds for the states and actions.
+            Bounds<StateType, ValueType> bounds;
+            
+            // Create a stack that is used to track the path we sampled.
+            StateActionStack stack;
+            
+            // Now perform the actual sampling.
+            Statistics<StateType, ValueType> stats;
+            bool convergenceCriterionMet = false;
+            while (!convergenceCriterionMet) {
+                bool result = samplePathFromInitialState(stateGeneration, explorationInformation, stack, bounds, stats);
+                
+                stats.sampledPath();
+                stats.updateMaxPathLength(stack.size());
+                
+                // If a terminal state was found, we update the probabilities along the path contained in the stack.
+                if (result) {
+                    // Update the bounds along the path to the terminal state.
+                    STORM_LOG_TRACE("Found terminal state, updating probabilities along path.");
+                    updateProbabilityBoundsAlongSampledPath(stack, explorationInformation, bounds);
+                } else {
+                    // If not terminal state was found, the search aborted, possibly because of an EC-detection. In this
+                    // case, we cannot update the probabilities.
+                    STORM_LOG_TRACE("Did not find terminal state.");
+                }
+                
+                STORM_LOG_DEBUG("Discovered states: " << explorationInformation.getNumberOfDiscoveredStates() << " (" << stats.numberOfExploredStates << " explored, " << explorationInformation.getNumberOfUnexploredStates() << " unexplored).");
+                STORM_LOG_DEBUG("Value of initial state is in [" << bounds.getLowerBoundForState(initialStateIndex, explorationInformation) << ", " << bounds.getUpperBoundForState(initialStateIndex, explorationInformation) << "].");
+                ValueType difference = bounds.getDifferenceOfStateBounds(initialStateIndex, explorationInformation);
+                STORM_LOG_DEBUG("Difference after iteration " << stats.pathsSampled << " is " << difference << ".");
+                convergenceCriterionMet = comparator.isZero(difference);
+                
+                // If the number of sampled paths exceeds a certain threshold, do a precomputation.
+                if (!convergenceCriterionMet && explorationInformation.performPrecomputationExcessiveSampledPaths(stats.pathsSampledSinceLastPrecomputation)) {
+                    performPrecomputation(stack, explorationInformation, bounds, stats);
+                }
+            }
+            
+            // Show statistics if required.
+            if (storm::settings::generalSettings().isShowStatisticsSet()) {
+                stats.printToStream(std::cout, explorationInformation);
+            }
+            
+            return std::make_tuple(initialStateIndex, bounds.getLowerBoundForState(initialStateIndex, explorationInformation), bounds.getUpperBoundForState(initialStateIndex, explorationInformation));
+        }
+        
+        template<typename ValueType, typename StateType>
+        bool SparseExplorationModelChecker<ValueType, StateType>::samplePathFromInitialState(StateGeneration<StateType, ValueType>& stateGeneration, ExplorationInformation<StateType, ValueType>& explorationInformation, StateActionStack& stack, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const {
+            // Start the search from the initial state.
+            stack.push_back(std::make_pair(stateGeneration.getFirstInitialState(), 0));
+            
+            // As long as we didn't find a terminal (accepting or rejecting) state in the search, sample a new successor.
+            bool foundTerminalState = false;
+            while (!foundTerminalState) {
+                StateType const& currentStateId = stack.back().first;
+                STORM_LOG_TRACE("State on top of stack is: " << currentStateId << ".");
+                
+                // If the state is not yet explored, we need to retrieve its behaviors.
+                auto unexploredIt = explorationInformation.findUnexploredState(currentStateId);
+                if (unexploredIt != explorationInformation.unexploredStatesEnd()) {
+                    STORM_LOG_TRACE("State was not yet explored.");
+                    
+                    // Explore the previously unexplored state.
+                    storm::generator::CompressedState const& compressedState = unexploredIt->second;
+                    foundTerminalState = exploreState(stateGeneration, currentStateId, compressedState, explorationInformation, bounds, stats);
+                    if (foundTerminalState) {
+                        STORM_LOG_TRACE("Aborting sampling of path, because a terminal state was reached.");
+                    }
+                    explorationInformation.removeUnexploredState(unexploredIt);
+                } else {
+                    // If the state was already explored, we check whether it is a terminal state or not.
+                    if (explorationInformation.isTerminal(currentStateId)) {
+                        STORM_LOG_TRACE("Found already explored terminal state: " << currentStateId << ".");
+                        foundTerminalState = true;
+                    }
+                }
+                
+                // Notify the stats about the performed exploration step.
+                stats.explorationStep();
+                
+                // If the state was not a terminal state, we continue the path search and sample the next state.
+                if (!foundTerminalState) {
+                    // At this point, we can be sure that the state was expanded and that we can sample according to the
+                    // probabilities in the matrix.
+                    uint32_t chosenAction = sampleActionOfState(currentStateId, explorationInformation, bounds);
+                    stack.back().second = chosenAction;
+                    STORM_LOG_TRACE("Sampled action " << chosenAction << " in state " << currentStateId << ".");
+                    
+                    StateType successor = sampleSuccessorFromAction(chosenAction, explorationInformation, bounds);
+                    STORM_LOG_TRACE("Sampled successor " << successor << " according to action " << chosenAction << " of state " << currentStateId << ".");
+                    
+                    // Put the successor state and a dummy action on top of the stack.
+                    stack.emplace_back(successor, 0);
+                    
+                    // If the number of exploration steps exceeds a certain threshold, do a precomputation.
+                    if (explorationInformation.performPrecomputationExcessiveExplorationSteps(stats.explorationStepsSinceLastPrecomputation)) {
+                        performPrecomputation(stack, explorationInformation, bounds, stats);
+                        
+                        STORM_LOG_TRACE("Aborting the search after precomputation.");
+                        stack.clear();
+                        break;
+                    }
+                }
+            }
+            
+            return foundTerminalState;
+        }
+        
+        template<typename ValueType, typename StateType>
+        bool SparseExplorationModelChecker<ValueType, StateType>::exploreState(StateGeneration<StateType, ValueType>& stateGeneration, StateType const& currentStateId, storm::generator::CompressedState const& currentState, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const {
+            bool isTerminalState = false;
+            bool isTargetState = false;
+            
+            ++stats.numberOfExploredStates;
+            
+            // Finally, map the unexplored state to the row group.
+            explorationInformation.assignStateToNextRowGroup(currentStateId);
+            STORM_LOG_TRACE("Assigning row group " << explorationInformation.getRowGroup(currentStateId) << " to state " << currentStateId << ".");
+            
+            // Initialize the bounds, because some of the following computations depend on the values to be available for
+            // all states that have been assigned to a row-group.
+            bounds.initializeBoundsForNextState();
+            
+            // Before generating the behavior of the state, we need to determine whether it's a target state that
+            // does not need to be expanded.
+            stateGeneration.load(currentState);
+            if (stateGeneration.isTargetState()) {
+                ++stats.numberOfTargetStates;
+                isTargetState = true;
+                isTerminalState = true;
+            } else if (stateGeneration.isConditionState()) {
+                STORM_LOG_TRACE("Exploring state.");
+                
+                // If it needs to be expanded, we use the generator to retrieve the behavior of the new state.
+                storm::generator::StateBehavior<ValueType, StateType> behavior = stateGeneration.expand();
+                STORM_LOG_TRACE("State has " << behavior.getNumberOfChoices() << " choices.");
+                
+                // Clumsily check whether we have found a state that forms a trivial BMEC.
+                bool otherSuccessor = false;
+                for (auto const& choice : behavior) {
+                    for (auto const& entry : choice) {
+                        if (entry.first != currentStateId) {
+                            otherSuccessor = true;
+                            break;
+                        }
+                    }
+                }
+                isTerminalState = !otherSuccessor;
+                
+                // If the state was neither a trivial (non-accepting) terminal state nor a target state, we
+                // need to store its behavior.
+                if (!isTerminalState) {
+                    // Next, we insert the behavior into our matrix structure.
+                    StateType startAction = explorationInformation.getActionCount();
+                    explorationInformation.addActionsToMatrix(behavior.getNumberOfChoices());
+                    
+                    ActionType localAction = 0;
+                    
+                    // Retrieve the lowest state bounds (wrt. to the current optimization direction).
+                    std::pair<ValueType, ValueType> stateBounds = getLowestBounds(explorationInformation.getOptimizationDirection());
+                    
+                    for (auto const& choice : behavior) {
+                        for (auto const& entry : choice) {
+                            explorationInformation.getRowOfMatrix(startAction + localAction).emplace_back(entry.first, entry.second);
+                            STORM_LOG_TRACE("Found transition " << currentStateId << "-[" << (startAction + localAction) << ", " << entry.second << "]-> " << entry.first << ".");
+                        }
+                        
+                        std::pair<ValueType, ValueType> actionBounds = computeBoundsOfAction(startAction + localAction, explorationInformation, bounds);
+                        bounds.initializeBoundsForNextAction(actionBounds);
+                        stateBounds = combineBounds(explorationInformation.getOptimizationDirection(), stateBounds, actionBounds);
+                        
+                        STORM_LOG_TRACE("Initializing bounds of action " << (startAction + localAction) << " to " << bounds.getLowerBoundForAction(startAction + localAction) << " and " << bounds.getUpperBoundForAction(startAction + localAction) << ".");
+                        
+                        ++localAction;
+                    }
+                    
+                    // Terminate the row group.
+                    explorationInformation.terminateCurrentRowGroup();
+                    
+                    bounds.setBoundsForState(currentStateId, explorationInformation, stateBounds);
+                    STORM_LOG_TRACE("Initializing bounds of state " << currentStateId << " to " << bounds.getLowerBoundForState(currentStateId, explorationInformation) << " and " << bounds.getUpperBoundForState(currentStateId, explorationInformation) << ".");
+                }
+            } else {
+                // In this case, the state is neither a target state nor a condition state and therefore a rejecting
+                // terminal state.
+                isTerminalState = true;
+            }
+            
+            if (isTerminalState) {
+                STORM_LOG_TRACE("State does not need to be explored, because it is " << (isTargetState ? "a target state" : "a rejecting terminal state") << ".");
+                explorationInformation.addTerminalState(currentStateId);
+                
+                if (isTargetState) {
+                    bounds.setBoundsForState(currentStateId, explorationInformation, std::make_pair(storm::utility::one<ValueType>(), storm::utility::one<ValueType>()));
+                    bounds.initializeBoundsForNextAction(std::make_pair(storm::utility::one<ValueType>(), storm::utility::one<ValueType>()));
+                } else {
+                    bounds.setBoundsForState(currentStateId, explorationInformation, std::make_pair(storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>()));
+                    bounds.initializeBoundsForNextAction(std::make_pair(storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>()));
+                }
+                
+                // Increase the size of the matrix, but leave the row empty.
+                explorationInformation.addActionsToMatrix(1);
+                
+                // Terminate the row group.
+                explorationInformation.newRowGroup();
+            }
+            
+            return isTerminalState;
+        }
+        
+        template<typename ValueType, typename StateType>
+        typename SparseExplorationModelChecker<ValueType, StateType>::ActionType SparseExplorationModelChecker<ValueType, StateType>::sampleActionOfState(StateType const& currentStateId, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const {
+            // Determine the values of all available actions.
+            std::vector<std::pair<ActionType, ValueType>> actionValues;
+            StateType rowGroup = explorationInformation.getRowGroup(currentStateId);
+            
+            // Check for cases in which we do not need to perform more work.
+            if (explorationInformation.onlyOneActionAvailable(rowGroup)) {
+                return explorationInformation.getStartRowOfGroup(rowGroup);
+            }
+            
+            // If there are more choices to consider, start by gathering the values of relevant actions.
+            STORM_LOG_TRACE("Sampling from actions leaving the state.");
+            
+            for (uint32_t row = explorationInformation.getStartRowOfGroup(rowGroup); row < explorationInformation.getStartRowOfGroup(rowGroup + 1); ++row) {
+                actionValues.push_back(std::make_pair(row, bounds.getBoundForAction(explorationInformation.getOptimizationDirection(), row)));
+            }
+            
+            STORM_LOG_ASSERT(!actionValues.empty(), "Values for actions must not be empty.");
+            
+            // Sort the actions wrt. to the optimization direction.
+            if (explorationInformation.maximize()) {
+                std::sort(actionValues.begin(), actionValues.end(), [] (std::pair<ActionType, ValueType> const& a, std::pair<ActionType, ValueType> const& b) { return a.second > b.second; } );
+            } else {
+                std::sort(actionValues.begin(), actionValues.end(), [] (std::pair<ActionType, ValueType> const& a, std::pair<ActionType, ValueType> const& b) { return a.second < b.second; } );
+            }
+            
+            // Determine the first elements of the sorted range that agree on their value.
+            auto end = ++actionValues.begin();
+            while (end != actionValues.end() && comparator.isEqual(actionValues.begin()->second, end->second)) {
+                ++end;
+            }
+            
+            // Now sample from all maximizing actions.
+            std::uniform_int_distribution<ActionType> distribution(0, std::distance(actionValues.begin(), end) - 1);
+            return actionValues[distribution(randomGenerator)].first;
+        }
+        
+        template<typename ValueType, typename StateType>
+        StateType SparseExplorationModelChecker<ValueType, StateType>::sampleSuccessorFromAction(ActionType const& chosenAction, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
+            std::vector<storm::storage::MatrixEntry<StateType, ValueType>> const& row = explorationInformation.getRowOfMatrix(chosenAction);
+            if (row.size() == 1) {
+                return row.front().getColumn();
+            }
+            
+            // Depending on the selected next-state heuristic, we give the states other likelihoods of getting chosen.
+            if (explorationInformation.useDifferenceProbabilitySumHeuristic() || explorationInformation.useProbabilityHeuristic()) {
+                std::vector<ValueType> probabilities(row.size());
+                if (explorationInformation.useDifferenceProbabilitySumHeuristic()) {
+                std::transform(row.begin(), row.end(), probabilities.begin(),
+                               [&bounds, &explorationInformation] (storm::storage::MatrixEntry<StateType, ValueType> const& entry) {
+                                   return entry.getValue() + bounds.getDifferenceOfStateBounds(entry.getColumn(), explorationInformation);
+                               });
+                } else if (explorationInformation.useProbabilityHeuristic()) {
+                    std::transform(row.begin(), row.end(), probabilities.begin(),
+                                   [&bounds, &explorationInformation] (storm::storage::MatrixEntry<StateType, ValueType> const& entry) {
+                                       return entry.getValue();
+                                   });
+                }
+                
+                // Now sample according to the probabilities.
+                std::discrete_distribution<StateType> distribution(probabilities.begin(), probabilities.end());
+                return row[distribution(randomGenerator)].getColumn();
+            } else {
+                STORM_LOG_ASSERT(explorationInformation.useUniformHeuristic(), "Illegal next-state heuristic.");
+                std::uniform_int_distribution<ActionType> distribution(0, row.size() - 1);
+                return row[distribution(randomGenerator)].getColumn();
+            }
+        }
+        
+        template<typename ValueType, typename StateType>
+        bool SparseExplorationModelChecker<ValueType, StateType>::performPrecomputation(StateActionStack const& stack, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const {
+            ++stats.numberOfPrecomputations;
+            
+            // Outline:
+            // 1. construct a sparse transition matrix of the relevant part of the state space.
+            // 2. use this matrix to compute states with probability 0/1 and an MEC decomposition (in the max case).
+            // 3. use MEC decomposition to collapse MECs.
+            STORM_LOG_TRACE("Starting " << (explorationInformation.useLocalPrecomputation() ? "local" : "global") << " precomputation.");
+            
+            // Construct the matrix that represents the fragment of the system contained in the currently sampled path.
+            storm::storage::SparseMatrixBuilder<ValueType> builder(0, 0, 0, false, true, 0);
+            
+            // Determine the set of states that was expanded.
+            std::vector<StateType> relevantStates;
+            if (explorationInformation.useLocalPrecomputation()) {
+                for (auto const& stateActionPair : stack) {
+                    if (explorationInformation.maximize() || !storm::utility::isOne(bounds.getLowerBoundForState(stateActionPair.first, explorationInformation))) {
+                        relevantStates.push_back(stateActionPair.first);
+                    }
+                }
+                std::sort(relevantStates.begin(), relevantStates.end());
+                auto newEnd = std::unique(relevantStates.begin(), relevantStates.end());
+                relevantStates.resize(std::distance(relevantStates.begin(), newEnd));
+            } else {
+                for (StateType state = 0; state < explorationInformation.getNumberOfDiscoveredStates(); ++state) {
+                    // Add the state to the relevant states if they are not unexplored.
+                    if (!explorationInformation.isUnexplored(state)) {
+                        relevantStates.push_back(state);
+                    }
+                }
+            }
+            StateType sink = relevantStates.size();
+            
+            // Create a mapping for faster look-up during the translation of flexible matrix to the real sparse matrix.
+            // While doing so, record all target states.
+            std::unordered_map<StateType, StateType> relevantStateToNewRowGroupMapping;
+            storm::storage::BitVector targetStates(sink + 1);
+            for (StateType index = 0; index < relevantStates.size(); ++index) {
+                relevantStateToNewRowGroupMapping.emplace(relevantStates[index], index);
+                if (storm::utility::isOne(bounds.getLowerBoundForState(relevantStates[index], explorationInformation))) {
+                    targetStates.set(index);
+                }
+            }
+            
+            // Do the actual translation.
+            StateType currentRow = 0;
+            for (auto const& state : relevantStates) {
+                builder.newRowGroup(currentRow);
+                StateType rowGroup = explorationInformation.getRowGroup(state);
+                for (auto row = explorationInformation.getStartRowOfGroup(rowGroup); row < explorationInformation.getStartRowOfGroup(rowGroup + 1); ++row) {
+                    ValueType unexpandedProbability = storm::utility::zero<ValueType>();
+                    for (auto const& entry : explorationInformation.getRowOfMatrix(row)) {
+                        auto it = relevantStateToNewRowGroupMapping.find(entry.getColumn());
+                        if (it != relevantStateToNewRowGroupMapping.end()) {
+                            // If the entry is a relevant state, we copy it over (and compensate for the offset change).
+                            builder.addNextValue(currentRow, it->second, entry.getValue());
+                        } else {
+                            // If the entry is an unexpanded state, we gather the probability to later redirect it to an unexpanded sink.
+                            unexpandedProbability += entry.getValue();
+                        }
+                    }
+                    if (unexpandedProbability != storm::utility::zero<ValueType>()) {
+                        builder.addNextValue(currentRow, sink, unexpandedProbability);
+                    }
+                    ++currentRow;
+                }
+            }
+            // Then, make the unexpanded state absorbing.
+            builder.newRowGroup(currentRow);
+            builder.addNextValue(currentRow, sink, storm::utility::one<ValueType>());
+            storm::storage::SparseMatrix<ValueType> relevantStatesMatrix = builder.build();
+            storm::storage::SparseMatrix<ValueType> transposedMatrix = relevantStatesMatrix.transpose(true);
+            STORM_LOG_TRACE("Successfully built matrix for precomputation.");
+            
+            storm::storage::BitVector allStates(sink + 1, true);
+            storm::storage::BitVector statesWithProbability0;
+            storm::storage::BitVector statesWithProbability1;
+            if (explorationInformation.maximize()) {
+                // If we are computing maximal probabilities, we first perform a detection of states that have
+                // probability 01 and then additionally perform an MEC decomposition. The reason for this somewhat
+                // duplicate work is the following. Optimally, we would only do the MEC decomposition, because we need
+                // it anyway. However, when only detecting (accepting) MECs, we do not infer which of the other states
+                // (not contained in MECs) also have probability 0/1.
+                statesWithProbability0 = storm::utility::graph::performProb0A(relevantStatesMatrix, relevantStatesMatrix.getRowGroupIndices(), transposedMatrix, allStates, targetStates);
+                targetStates.set(sink, true);
+                statesWithProbability1 = storm::utility::graph::performProb1E(relevantStatesMatrix, relevantStatesMatrix.getRowGroupIndices(), transposedMatrix, allStates, targetStates);
+                
+                storm::storage::MaximalEndComponentDecomposition<ValueType> mecDecomposition(relevantStatesMatrix, relevantStatesMatrix.transpose(true));
+                ++stats.ecDetections;
+                STORM_LOG_TRACE("Successfully computed MEC decomposition. Found " << (mecDecomposition.size() > 1 ? (mecDecomposition.size() - 1) : 0) << " MEC(s).");
+                
+                // If the decomposition contains only the MEC consisting of the sink state, we count it as 'failed'.
+                if (mecDecomposition.size() > 1) {
+                    ++stats.failedEcDetections;
+                } else {
+                    stats.totalNumberOfEcDetected += mecDecomposition.size() - 1;
+                    
+                    // 3. Analyze the MEC decomposition.
+                    for (auto const& mec : mecDecomposition) {
+                        // Ignore the (expected) MEC of the sink state.
+                        if (mec.containsState(sink)) {
+                            continue;
+                        }
+                        
+                        collapseMec(mec, relevantStates, relevantStatesMatrix, explorationInformation, bounds);
+                    }
+                }
+            } else {
+                // If we are computing minimal probabilities, we do not need to perform an EC-detection. We rather
+                // compute all states (of the considered fragment) that have probability 0/1. For states with
+                // probability 0, we have to mark the sink as being a target. For states with probability 1, however,
+                // we must treat the sink as being rejecting.
+                targetStates.set(sink, true);
+                statesWithProbability0 = storm::utility::graph::performProb0E(relevantStatesMatrix, relevantStatesMatrix.getRowGroupIndices(), transposedMatrix, allStates, targetStates);
+                targetStates.set(sink, false);
+                statesWithProbability1 = storm::utility::graph::performProb1A(relevantStatesMatrix, relevantStatesMatrix.getRowGroupIndices(), transposedMatrix, allStates, targetStates);
+            }
+            
+            // Set the bounds of the identified states.
+            for (auto state : statesWithProbability0) {
+                StateType originalState = relevantStates[state];
+                bounds.setUpperBoundForState(originalState, explorationInformation, storm::utility::zero<ValueType>());
+                explorationInformation.addTerminalState(originalState);
+            }
+            for (auto state : statesWithProbability1) {
+                StateType originalState = relevantStates[state];
+                bounds.setLowerBoundForState(originalState, explorationInformation, storm::utility::one<ValueType>());
+                explorationInformation.addTerminalState(originalState);
+            }
+            return true;
+        }
+        
+        template<typename ValueType, typename StateType>
+        void SparseExplorationModelChecker<ValueType, StateType>::collapseMec(storm::storage::MaximalEndComponent const& mec, std::vector<StateType> const& relevantStates, storm::storage::SparseMatrix<ValueType> const& relevantStatesMatrix, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds) const {
+            bool containsTargetState = false;
+            
+            // Now we record all actions leaving the EC.
+            std::vector<ActionType> leavingActions;
+            for (auto const& stateAndChoices : mec) {
+                // Compute the state of the original model that corresponds to the current state.
+                StateType originalState = relevantStates[stateAndChoices.first];
+                StateType originalRowGroup = explorationInformation.getRowGroup(originalState);
+                
+                // Check whether a target state is contained in the MEC.
+                if (!containsTargetState && storm::utility::isOne(bounds.getLowerBoundForRowGroup(originalRowGroup))) {
+                    containsTargetState = true;
+                }
+                
+                // For each state, compute the actions that leave the MEC.
+                auto includedChoicesIt = stateAndChoices.second.begin();
+                auto includedChoicesIte = stateAndChoices.second.end();
+                for (auto action = explorationInformation.getStartRowOfGroup(originalRowGroup); action < explorationInformation.getStartRowOfGroup(originalRowGroup + 1); ++action) {
+                    if (includedChoicesIt != includedChoicesIte) {
+                        STORM_LOG_TRACE("Next (local) choice contained in MEC is " << (*includedChoicesIt - relevantStatesMatrix.getRowGroupIndices()[stateAndChoices.first]));
+                        STORM_LOG_TRACE("Current (local) choice iterated is " << (action - explorationInformation.getStartRowOfGroup(originalRowGroup)));
+                        if (action - explorationInformation.getStartRowOfGroup(originalRowGroup) != *includedChoicesIt - relevantStatesMatrix.getRowGroupIndices()[stateAndChoices.first]) {
+                            STORM_LOG_TRACE("Choice leaves the EC.");
+                            leavingActions.push_back(action);
+                        } else {
+                            STORM_LOG_TRACE("Choice stays in the EC.");
+                            ++includedChoicesIt;
+                        }
+                    } else {
+                        STORM_LOG_TRACE("Choice leaves the EC, because there is no more choice staying in the EC.");
+                        leavingActions.push_back(action);
+                    }
+                }
+            }
+            
+            // Now, we need to collapse the EC only if it does not contain a target state and the leaving actions are
+            // non-empty, because only then have the states a (potentially) non-zero, non-one probability.
+            if (!containsTargetState && !leavingActions.empty()) {
+                // In this case, no target state is contained in the MEC, but there are actions leaving the MEC. To
+                // prevent the simulation getting stuck in this MEC again, we replace all states in the MEC by a new
+                // state whose outgoing actions are the ones leaving the MEC. We do this, by assigning all states in the
+                // MEC to a new row group, which will then hold all the outgoing choices.
+                
+                // Remap all contained states to the new row group.
+                StateType nextRowGroup = explorationInformation.getNextRowGroup();
+                for (auto const& stateAndChoices : mec) {
+                    explorationInformation.assignStateToRowGroup(stateAndChoices.first, nextRowGroup);
+                }
+                
+                bounds.initializeBoundsForNextState();
+                
+                // Add to the new row group all leaving actions of contained states and set the appropriate bounds for
+                // the actions and the new state.
+                std::pair<ValueType, ValueType> stateBounds = getLowestBounds(explorationInformation.getOptimizationDirection());
+                for (auto const& action : leavingActions) {
+                    explorationInformation.moveActionToBackOfMatrix(action);
+                    std::pair<ValueType, ValueType> const& actionBounds = bounds.getBoundsForAction(action);
+                    bounds.initializeBoundsForNextAction(actionBounds);
+                    stateBounds = combineBounds(explorationInformation.getOptimizationDirection(), stateBounds, actionBounds);
+                }
+                bounds.setBoundsForRowGroup(nextRowGroup, stateBounds);
+                
+                // Terminate the row group of the newly introduced state.
+                explorationInformation.terminateCurrentRowGroup();
+            }
+        }
+        
+        template<typename ValueType, typename StateType>
+        ValueType SparseExplorationModelChecker<ValueType, StateType>::computeLowerBoundOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
+            ValueType result = storm::utility::zero<ValueType>();
+            for (auto const& element : explorationInformation.getRowOfMatrix(action)) {
+                result += element.getValue() * bounds.getLowerBoundForState(element.getColumn(), explorationInformation);
+            }
+            return result;
+        }
+        
+        template<typename ValueType, typename StateType>
+        ValueType SparseExplorationModelChecker<ValueType, StateType>::computeUpperBoundOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
+            ValueType result = storm::utility::zero<ValueType>();
+            for (auto const& element : explorationInformation.getRowOfMatrix(action)) {
+                result += element.getValue() * bounds.getUpperBoundForState(element.getColumn(), explorationInformation);
+            }
+            return result;
+        }
+        
+        template<typename ValueType, typename StateType>
+        std::pair<ValueType, ValueType> SparseExplorationModelChecker<ValueType, StateType>::computeBoundsOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
+            // TODO: take into account self-loops?
+            std::pair<ValueType, ValueType> result = std::make_pair(storm::utility::zero<ValueType>(), storm::utility::zero<ValueType>());
+            for (auto const& element : explorationInformation.getRowOfMatrix(action)) {
+                result.first += element.getValue() * bounds.getLowerBoundForState(element.getColumn(), explorationInformation);
+                result.second += element.getValue() * bounds.getUpperBoundForState(element.getColumn(), explorationInformation);
+            }
+            return result;
+        }
+        
+        template<typename ValueType, typename StateType>
+        std::pair<ValueType, ValueType> SparseExplorationModelChecker<ValueType, StateType>::computeBoundsOfState(StateType const& currentStateId, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
+            StateType group = explorationInformation.getRowGroup(currentStateId);
+            std::pair<ValueType, ValueType> result = getLowestBounds(explorationInformation.getOptimizationDirection());
+            for (ActionType action = explorationInformation.getStartRowOfGroup(group); action < explorationInformation.getStartRowOfGroup(group + 1); ++action) {
+                std::pair<ValueType, ValueType> actionValues = computeBoundsOfAction(action, explorationInformation, bounds);
+                result = combineBounds(explorationInformation.getOptimizationDirection(), result, actionValues);
+            }
+            return result;
+        }
+        
+        template<typename ValueType, typename StateType>
+        void SparseExplorationModelChecker<ValueType, StateType>::updateProbabilityBoundsAlongSampledPath(StateActionStack& stack, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const {
+            stack.pop_back();
+            while (!stack.empty()) {
+                updateProbabilityOfAction(stack.back().first, stack.back().second, explorationInformation, bounds);
+                stack.pop_back();
+            }
+        }
+        
+        template<typename ValueType, typename StateType>
+        void SparseExplorationModelChecker<ValueType, StateType>::updateProbabilityOfAction(StateType const& state, ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const {
+            // Compute the new lower/upper values of the action.
+            std::pair<ValueType, ValueType> newBoundsForAction = computeBoundsOfAction(action, explorationInformation, bounds);
+            
+            // And set them as the current value.
+            bounds.setBoundsForAction(action, newBoundsForAction);
+            
+            // Check if we need to update the values for the states.
+            if (explorationInformation.maximize()) {
+                bounds.setLowerBoundOfStateIfGreaterThanOld(state, explorationInformation, newBoundsForAction.first);
+                
+                StateType rowGroup = explorationInformation.getRowGroup(state);
+                if (newBoundsForAction.second < bounds.getUpperBoundForRowGroup(rowGroup)) {
+                    if (explorationInformation.getRowGroupSize(rowGroup) > 1) {
+                        newBoundsForAction.second = std::max(newBoundsForAction.second, computeBoundOverAllOtherActions(storm::OptimizationDirection::Maximize, state, action, explorationInformation, bounds));
+                    }
+                    
+                    bounds.setUpperBoundForRowGroup(rowGroup, newBoundsForAction.second);
+                }
+            } else {
+                bounds.setUpperBoundOfStateIfLessThanOld(state, explorationInformation, newBoundsForAction.second);
+                
+                StateType rowGroup = explorationInformation.getRowGroup(state);
+                if (bounds.getLowerBoundForRowGroup(rowGroup) < newBoundsForAction.first) {
+                    if (explorationInformation.getRowGroupSize(rowGroup) > 1) {
+                        ValueType min = computeBoundOverAllOtherActions(storm::OptimizationDirection::Minimize, state, action, explorationInformation, bounds);
+                        newBoundsForAction.first = std::min(newBoundsForAction.first, min);
+                    }
+                    
+                    bounds.setLowerBoundForRowGroup(rowGroup, newBoundsForAction.first);
+                }
+            }
+        }
+        
+        template<typename ValueType, typename StateType>
+        ValueType SparseExplorationModelChecker<ValueType, StateType>::computeBoundOverAllOtherActions(storm::OptimizationDirection const& direction, StateType const& state, ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
+            ValueType bound = getLowestBound(explorationInformation.getOptimizationDirection());
+            
+            ActionType group = explorationInformation.getRowGroup(state);
+            for (auto currentAction = explorationInformation.getStartRowOfGroup(group); currentAction < explorationInformation.getStartRowOfGroup(group + 1); ++currentAction) {
+                if (currentAction == action) {
+                    continue;
+                }
+                
+                if (direction == storm::OptimizationDirection::Maximize) {
+                    bound = std::max(bound, computeUpperBoundOfAction(currentAction, explorationInformation, bounds));
+                } else {
+                    bound = std::min(bound, computeLowerBoundOfAction(currentAction, explorationInformation, bounds));
+                }
+            }
+            return bound;
+        }
+        
+        template<typename ValueType, typename StateType>
+        std::pair<ValueType, ValueType> SparseExplorationModelChecker<ValueType, StateType>::getLowestBounds(storm::OptimizationDirection const& direction) const {
+            ValueType val = getLowestBound(direction);
+            return std::make_pair(val, val);
+        }
+        
+        template<typename ValueType, typename StateType>
+        ValueType SparseExplorationModelChecker<ValueType, StateType>::getLowestBound(storm::OptimizationDirection const& direction) const {
+            if (direction == storm::OptimizationDirection::Maximize) {
+                return storm::utility::zero<ValueType>();
+            } else {
+                return storm::utility::one<ValueType>();
+            }
+        }
+        
+        template<typename ValueType, typename StateType>
+        std::pair<ValueType, ValueType> SparseExplorationModelChecker<ValueType, StateType>::combineBounds(storm::OptimizationDirection const& direction, std::pair<ValueType, ValueType> const& bounds1, std::pair<ValueType, ValueType> const& bounds2) const {
+            if (direction == storm::OptimizationDirection::Maximize) {
+                return std::make_pair(std::max(bounds1.first, bounds2.first), std::max(bounds1.second, bounds2.second));
+            } else {
+                return std::make_pair(std::min(bounds1.first, bounds2.first), std::min(bounds1.second, bounds2.second));
+            }
+        }
+        
+        template class SparseExplorationModelChecker<double, uint32_t>;
+    }
+}
\ No newline at end of file
diff --git a/src/modelchecker/exploration/SparseExplorationModelChecker.h b/src/modelchecker/exploration/SparseExplorationModelChecker.h
new file mode 100644
index 000000000..aa13f379a
--- /dev/null
+++ b/src/modelchecker/exploration/SparseExplorationModelChecker.h
@@ -0,0 +1,89 @@
+#ifndef STORM_MODELCHECKER_EXPLORATION_SPARSEEXPLORATIONMODELCHECKER_H_
+#define STORM_MODELCHECKER_EXPLORATION_SPARSEEXPLORATIONMODELCHECKER_H_
+
+#include <random>
+
+#include "src/modelchecker/AbstractModelChecker.h"
+
+#include "src/storage/prism/Program.h"
+
+#include "src/generator/CompressedState.h"
+#include "src/generator/VariableInformation.h"
+
+#include "src/utility/ConstantsComparator.h"
+
+namespace storm {
+    namespace storage {
+        class MaximalEndComponent;
+    }
+    namespace prism {
+        class Program;
+    }
+    
+    namespace modelchecker {
+        namespace exploration_detail {
+            template <typename StateType, typename ValueType> class StateGeneration;
+            template <typename StateType, typename ValueType> class ExplorationInformation;
+            template <typename StateType, typename ValueType> class Bounds;
+            template <typename StateType, typename ValueType> class Statistics;
+        }
+        
+        using namespace exploration_detail;
+        
+        template<typename ValueType, typename StateType = uint32_t>
+        class SparseExplorationModelChecker : public AbstractModelChecker {
+        public:
+            typedef StateType ActionType;
+            typedef std::vector<std::pair<StateType, ActionType>> StateActionStack;
+            
+            SparseExplorationModelChecker(storm::prism::Program const& program, boost::optional<std::map<storm::expressions::Variable, storm::expressions::Expression>> const& constantDefinitions = boost::none);
+            
+            virtual bool canHandle(CheckTask<storm::logic::Formula> const& checkTask) const override;
+            
+            virtual std::unique_ptr<CheckResult> computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) override;
+            
+        private:
+            std::tuple<StateType, ValueType, ValueType> performExploration(StateGeneration<StateType, ValueType>& stateGeneration, ExplorationInformation<StateType, ValueType>& explorationInformation) const;
+
+            bool samplePathFromInitialState(StateGeneration<StateType, ValueType>& stateGeneration, ExplorationInformation<StateType, ValueType>& explorationInformation, StateActionStack& stack, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const;
+            
+            bool exploreState(StateGeneration<StateType, ValueType>& stateGeneration, StateType const& currentStateId, storm::generator::CompressedState const& currentState, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const;
+            
+            ActionType sampleActionOfState(StateType const& currentStateId, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const;
+
+            StateType sampleSuccessorFromAction(ActionType const& chosenAction, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const;
+            
+            bool performPrecomputation(StateActionStack const& stack, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const;
+            
+            void collapseMec(storm::storage::MaximalEndComponent const& mec, std::vector<StateType> const& relevantStates, storm::storage::SparseMatrix<ValueType> const& relevantStatesMatrix, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds) const;
+            
+            void updateProbabilityBoundsAlongSampledPath(StateActionStack& stack, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const;
+
+            void updateProbabilityOfAction(StateType const& state, ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const;
+            
+            std::pair<ValueType, ValueType> computeBoundsOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const;
+            ValueType computeBoundOverAllOtherActions(storm::OptimizationDirection const& direction, StateType const& state, ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const;
+            std::pair<ValueType, ValueType> computeBoundsOfState(StateType const& currentStateId, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const;
+            ValueType computeLowerBoundOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const;
+            ValueType computeUpperBoundOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const;
+            
+            std::pair<ValueType, ValueType> getLowestBounds(storm::OptimizationDirection const& direction) const;
+            ValueType getLowestBound(storm::OptimizationDirection const& direction) const;
+            std::pair<ValueType, ValueType> combineBounds(storm::OptimizationDirection const& direction, std::pair<ValueType, ValueType> const& bounds1, std::pair<ValueType, ValueType> const& bounds2) const;
+            
+            // The program that defines the model to check.
+            storm::prism::Program program;
+            
+            // The variable information.
+            storm::generator::VariableInformation variableInformation;
+            
+            // The random number generator.
+            mutable std::default_random_engine randomGenerator;
+            
+            // A comparator used to determine whether values are equal.
+            storm::utility::ConstantsComparator<ValueType> comparator;
+        };
+    }
+}
+
+#endif /* STORM_MODELCHECKER_EXPLORATION_SPARSEEXPLORATIONMODELCHECKER_H_ */
\ No newline at end of file
diff --git a/src/modelchecker/exploration/StateGeneration.cpp b/src/modelchecker/exploration/StateGeneration.cpp
new file mode 100644
index 000000000..71fc4d416
--- /dev/null
+++ b/src/modelchecker/exploration/StateGeneration.cpp
@@ -0,0 +1,69 @@
+#include "src/modelchecker/exploration/StateGeneration.h"
+
+#include "src/modelchecker/exploration/ExplorationInformation.h"
+
+namespace storm {
+    namespace modelchecker {
+        namespace exploration_detail {
+            
+            template <typename StateType, typename ValueType>
+            StateGeneration<StateType, ValueType>::StateGeneration(storm::prism::Program const& program, storm::generator::VariableInformation const& variableInformation, ExplorationInformation<StateType, ValueType>& explorationInformation, storm::expressions::Expression const& conditionStateExpression, storm::expressions::Expression const& targetStateExpression) : generator(program, variableInformation, false), stateStorage(variableInformation.getTotalBitOffset(true)), conditionStateExpression(conditionStateExpression), targetStateExpression(targetStateExpression) {
+                
+                stateToIdCallback = [&explorationInformation, this] (storm::generator::CompressedState const& state) -> StateType {
+                    StateType newIndex = stateStorage.getNumberOfStates();
+                    
+                    // Check, if the state was already registered.
+                    std::pair<StateType, std::size_t> actualIndexBucketPair = stateStorage.stateToId.findOrAddAndGetBucket(state, newIndex);
+                    
+                    if (actualIndexBucketPair.first == newIndex) {
+                        explorationInformation.addUnexploredState(newIndex, state);
+                    }
+                    
+                    return actualIndexBucketPair.first;
+                };
+            }
+            
+            template <typename StateType, typename ValueType>
+            void StateGeneration<StateType, ValueType>::load(storm::generator::CompressedState const& state) {
+                generator.load(state);
+            }
+            
+            template <typename StateType, typename ValueType>
+            std::vector<StateType> StateGeneration<StateType, ValueType>::getInitialStates() {
+                return stateStorage.initialStateIndices;
+            }
+            
+            template <typename StateType, typename ValueType>
+            storm::generator::StateBehavior<ValueType, StateType> StateGeneration<StateType, ValueType>::expand() {
+                return generator.expand(stateToIdCallback);
+            }
+            
+            template <typename StateType, typename ValueType>
+            bool StateGeneration<StateType, ValueType>::isConditionState() const {
+                return generator.satisfies(conditionStateExpression);
+            }
+            
+            template <typename StateType, typename ValueType>
+            bool StateGeneration<StateType, ValueType>::isTargetState() const {
+                return generator.satisfies(targetStateExpression);
+            }
+            
+            template<typename StateType, typename ValueType>
+            void StateGeneration<StateType, ValueType>::computeInitialStates() {
+                stateStorage.initialStateIndices = generator.getInitialStates(stateToIdCallback);
+            }
+            
+            template<typename StateType, typename ValueType>
+            StateType StateGeneration<StateType, ValueType>::getFirstInitialState() const {
+                return stateStorage.initialStateIndices.front();
+            }
+            
+            template<typename StateType, typename ValueType>
+            std::size_t StateGeneration<StateType, ValueType>::getNumberOfInitialStates() const {
+                return stateStorage.initialStateIndices.size();
+            }
+            
+            template class StateGeneration<uint32_t, double>;
+        }
+    }
+}
\ No newline at end of file
diff --git a/src/modelchecker/exploration/StateGeneration.h b/src/modelchecker/exploration/StateGeneration.h
new file mode 100644
index 000000000..f75211e54
--- /dev/null
+++ b/src/modelchecker/exploration/StateGeneration.h
@@ -0,0 +1,56 @@
+#ifndef STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_STATEGENERATION_H_
+#define STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_STATEGENERATION_H_
+
+#include "src/generator/CompressedState.h"
+#include "src/generator/PrismNextStateGenerator.h"
+
+#include "src/storage/sparse/StateStorage.h"
+
+namespace storm {
+    namespace generator {
+        template<typename ValueType, typename StateType>
+        class PrismNextStateGenerator;
+    }
+    
+    namespace modelchecker {
+        namespace exploration_detail {
+            
+            template <typename StateType, typename ValueType>
+            class ExplorationInformation;
+            
+            template <typename StateType, typename ValueType>
+            class StateGeneration {
+            public:
+                StateGeneration(storm::prism::Program const& program, storm::generator::VariableInformation const& variableInformation, ExplorationInformation<StateType, ValueType>& explorationInformation, storm::expressions::Expression const& conditionStateExpression, storm::expressions::Expression const& targetStateExpression);
+                                
+                void load(storm::generator::CompressedState const& state);
+                
+                std::vector<StateType> getInitialStates();
+                
+                storm::generator::StateBehavior<ValueType, StateType> expand();
+                
+                void computeInitialStates();
+                
+                StateType getFirstInitialState() const;
+                
+                std::size_t getNumberOfInitialStates() const;
+                
+                bool isConditionState() const;
+                
+                bool isTargetState() const;
+                
+            private:
+                storm::generator::PrismNextStateGenerator<ValueType, StateType> generator;
+                std::function<StateType (storm::generator::CompressedState const&)> stateToIdCallback;
+                
+                storm::storage::sparse::StateStorage<StateType> stateStorage;
+
+                storm::expressions::Expression conditionStateExpression;
+                storm::expressions::Expression targetStateExpression;
+            };
+            
+        }
+    }
+}
+
+#endif /* STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_STATEGENERATION_H_ */
\ No newline at end of file
diff --git a/src/modelchecker/exploration/Statistics.cpp b/src/modelchecker/exploration/Statistics.cpp
new file mode 100644
index 000000000..d74a62815
--- /dev/null
+++ b/src/modelchecker/exploration/Statistics.cpp
@@ -0,0 +1,46 @@
+#include "src/modelchecker/exploration/Statistics.h"
+
+#include "src/modelchecker/exploration/ExplorationInformation.h"
+
+namespace storm {
+    namespace modelchecker {
+        namespace exploration_detail {
+            
+            template<typename StateType, typename ValueType>
+            Statistics<StateType, ValueType>::Statistics() : pathsSampled(0), pathsSampledSinceLastPrecomputation(0), explorationSteps(0), explorationStepsSinceLastPrecomputation(0), maxPathLength(0), numberOfTargetStates(0), numberOfExploredStates(0), numberOfPrecomputations(0), ecDetections(0), failedEcDetections(0), totalNumberOfEcDetected(0) {
+                // Intentionally left empty.
+            }
+            
+            template<typename StateType, typename ValueType>
+            void Statistics<StateType, ValueType>::explorationStep() {
+                ++explorationSteps;
+                ++explorationStepsSinceLastPrecomputation;
+            }
+            
+            template<typename StateType, typename ValueType>
+            void Statistics<StateType, ValueType>::sampledPath() {
+                ++pathsSampled;
+                ++pathsSampledSinceLastPrecomputation;
+            }
+            
+            template<typename StateType, typename ValueType>
+            void Statistics<StateType, ValueType>::updateMaxPathLength(std::size_t const& currentPathLength) {
+                maxPathLength = std::max(maxPathLength, currentPathLength);
+            }
+            
+            template<typename StateType, typename ValueType>
+            void Statistics<StateType, ValueType>::printToStream(std::ostream& out, ExplorationInformation<StateType, ValueType> const& explorationInformation) const {
+                out << std::endl << "Exploration statistics:" << std::endl;
+                out << "Discovered states: " << explorationInformation.getNumberOfDiscoveredStates() << " (" << numberOfExploredStates << " explored, " << explorationInformation.getNumberOfUnexploredStates() << " unexplored, " << numberOfTargetStates << " target)" << std::endl;
+                out << "Exploration steps: " << explorationSteps << std::endl;
+                out << "Sampled paths: " << pathsSampled << std::endl;
+                out << "Maximal path length: " << maxPathLength << std::endl;
+                out << "Precomputations: " << numberOfPrecomputations << std::endl;
+                out << "EC detections: " << ecDetections << " (" << failedEcDetections << " failed, " << totalNumberOfEcDetected << " EC(s) detected)" << std::endl;
+            }
+         
+            template class Statistics<uint32_t, double>;
+            
+        }
+    }
+}
diff --git a/src/modelchecker/exploration/Statistics.h b/src/modelchecker/exploration/Statistics.h
new file mode 100644
index 000000000..2d6b9d89f
--- /dev/null
+++ b/src/modelchecker/exploration/Statistics.h
@@ -0,0 +1,44 @@
+#ifndef STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_STATISTICS_H_
+#define STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_STATISTICS_H_
+
+#include <cstddef>
+#include <iostream>
+
+namespace storm {
+    namespace modelchecker {
+        namespace exploration_detail {
+            
+            template<typename StateType, typename ValueType>
+            class ExplorationInformation;
+            
+            // A struct that keeps track of certain statistics during the exploration.
+            template<typename StateType, typename ValueType>
+            struct Statistics {
+                Statistics();
+                
+                void explorationStep();
+                
+                void sampledPath();
+                
+                void updateMaxPathLength(std::size_t const& currentPathLength);
+                
+                void printToStream(std::ostream& out, ExplorationInformation<StateType, ValueType> const& explorationInformation) const;
+                
+                std::size_t pathsSampled;
+                std::size_t pathsSampledSinceLastPrecomputation;
+                std::size_t explorationSteps;
+                std::size_t explorationStepsSinceLastPrecomputation;
+                std::size_t maxPathLength;
+                std::size_t numberOfTargetStates;
+                std::size_t numberOfExploredStates;
+                std::size_t numberOfPrecomputations;
+                std::size_t ecDetections;
+                std::size_t failedEcDetections;
+                std::size_t totalNumberOfEcDetected;
+            };
+            
+        }
+    }
+}
+
+#endif /* STORM_MODELCHECKER_EXPLORATION_EXPLORATION_DETAIL_STATISTICS_H_ */
\ No newline at end of file
diff --git a/src/models/sparse/StateAnnotation.h b/src/models/sparse/StateAnnotation.h
index 42067bf76..f608a5186 100644
--- a/src/models/sparse/StateAnnotation.h
+++ b/src/models/sparse/StateAnnotation.h
@@ -1,16 +1,19 @@
-#ifndef STORM_STATEANNOTATION_H
-#define STORM_STATEANNOTATION_H
+#ifndef STORM_MODELS_SPARSE_STATEANNOTATION_H_
+#define STORM_MODELS_SPARSE_STATEANNOTATION_H_
+
+#include "src/storage/sparse/StateType.h"
 
 namespace storm {
     namespace models {
         namespace sparse {
+            
             class StateAnnotation {
             public:
-                virtual std::string stateInfo(uint_fast64_t s) const = 0;
+                virtual std::string stateInfo(storm::storage::sparse::state_type const& state) const = 0;
             };
+            
         }
     }
-
 }
 
-#endif //STORM_STATEANNOTATION_H
\ No newline at end of file
+#endif /* STORM_MODELS_SPARSE_STATEANNOTATION_H_ */
\ No newline at end of file
diff --git a/src/parser/DeterministicModelParser.cpp b/src/parser/DeterministicModelParser.cpp
index 18f14428a..2bc82362f 100644
--- a/src/parser/DeterministicModelParser.cpp
+++ b/src/parser/DeterministicModelParser.cpp
@@ -23,7 +23,7 @@ namespace storm {
             uint_fast64_t stateCount = transitions.getColumnCount();
 
             // Parse the state labeling.
-            storm::models::sparse::StateLabeling labeling(std::move(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(stateCount, labelingFilename)));
+            storm::models::sparse::StateLabeling labeling(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(stateCount, labelingFilename));
 
             // Construct the result.
             DeterministicModelParser<ValueType, RewardValueType>::Result result(std::move(transitions), std::move(labeling));
diff --git a/src/parser/NondeterministicModelParser.cpp b/src/parser/NondeterministicModelParser.cpp
index b2d539c3a..b703937fd 100644
--- a/src/parser/NondeterministicModelParser.cpp
+++ b/src/parser/NondeterministicModelParser.cpp
@@ -25,7 +25,7 @@ namespace storm {
             uint_fast64_t stateCount = transitions.getColumnCount();
 
             // Parse the state labeling.
-            storm::models::sparse::StateLabeling labeling(std::move(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(stateCount, labelingFilename)));
+            storm::models::sparse::StateLabeling labeling(storm::parser::AtomicPropositionLabelingParser::parseAtomicPropositionLabeling(stateCount, labelingFilename));
 
             // Only parse state rewards if a file is given.
             boost::optional<std::vector<RewardValueType>> stateRewards;
diff --git a/src/settings/SettingsManager.cpp b/src/settings/SettingsManager.cpp
index fffb10366..a8ce73080 100644
--- a/src/settings/SettingsManager.cpp
+++ b/src/settings/SettingsManager.cpp
@@ -26,6 +26,7 @@
 #include "src/settings/modules/ParametricSettings.h"
 #include "src/settings/modules/SparseDtmcEliminationModelCheckerSettings.h"
 #include "src/settings/modules/TopologicalValueIterationEquationSolverSettings.h"
+#include "src/settings/modules/ExplorationSettings.h"
 #include "src/utility/macros.h"
 #include "src/settings/Option.h"
 
@@ -48,6 +49,7 @@ namespace storm {
 			this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::TopologicalValueIterationEquationSolverSettings(*this)));
             this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::ParametricSettings(*this)));
             this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::SparseDtmcEliminationModelCheckerSettings(*this)));
+            this->addModule(std::unique_ptr<modules::ModuleSettings>(new modules::ExplorationSettings(*this)));
         }
         
         SettingsManager::~SettingsManager() {
@@ -547,5 +549,9 @@ namespace storm {
         storm::settings::modules::SparseDtmcEliminationModelCheckerSettings const& sparseDtmcEliminationModelCheckerSettings() {
             return dynamic_cast<storm::settings::modules::SparseDtmcEliminationModelCheckerSettings const&>(manager().getModule(storm::settings::modules::SparseDtmcEliminationModelCheckerSettings::moduleName));
         }
+        
+        storm::settings::modules::ExplorationSettings const& explorationSettings() {
+            return dynamic_cast<storm::settings::modules::ExplorationSettings const&>(manager().getModule(storm::settings::modules::ExplorationSettings::moduleName));
+        }
     }
 }
\ No newline at end of file
diff --git a/src/settings/SettingsManager.h b/src/settings/SettingsManager.h
index 8d6f79964..f6a1779d1 100644
--- a/src/settings/SettingsManager.h
+++ b/src/settings/SettingsManager.h
@@ -25,6 +25,7 @@ namespace storm {
             class TopologicalValueIterationEquationSolverSettings;
             class ParametricSettings;
             class SparseDtmcEliminationModelCheckerSettings;
+            class ExplorationSettings;
             class ModuleSettings;
         }
         class Option;
@@ -330,6 +331,12 @@ namespace storm {
          * @return An object that allows accessing the settings of the elimination-based DTMC model checker.
          */
         storm::settings::modules::SparseDtmcEliminationModelCheckerSettings const& sparseDtmcEliminationModelCheckerSettings();
+
+        /* Retrieves the settings of the exploration engine.
+         *
+         * @return An object that allows accessing the settings of the exploration engine.
+         */
+        storm::settings::modules::ExplorationSettings const& explorationSettings();
         
     } // namespace settings
 } // namespace storm
diff --git a/src/settings/modules/ExplorationSettings.cpp b/src/settings/modules/ExplorationSettings.cpp
new file mode 100644
index 000000000..688f4e6b6
--- /dev/null
+++ b/src/settings/modules/ExplorationSettings.cpp
@@ -0,0 +1,96 @@
+#include "src/settings/modules/ExplorationSettings.h"
+#include "src/settings/modules/GeneralSettings.h"
+#include "src/settings/Option.h"
+#include "src/settings/OptionBuilder.h"
+#include "src/settings/ArgumentBuilder.h"
+#include "src/settings/Argument.h"
+#include "src/settings/SettingsManager.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            
+            const std::string ExplorationSettings::moduleName = "exploration";
+            const std::string ExplorationSettings::precomputationTypeOptionName = "precomp";
+            const std::string ExplorationSettings::numberOfExplorationStepsUntilPrecomputationOptionName = "stepsprecomp";
+            const std::string ExplorationSettings::numberOfSampledPathsUntilPrecomputationOptionName = "pathsprecomp";
+            const std::string ExplorationSettings::nextStateHeuristicOptionName = "nextstate";
+            const std::string ExplorationSettings::precisionOptionName = "precision";
+            const std::string ExplorationSettings::precisionOptionShortName = "eps";
+            
+            ExplorationSettings::ExplorationSettings(storm::settings::SettingsManager& settingsManager) : ModuleSettings(settingsManager, moduleName) {
+                std::vector<std::string> types = { "local", "global" };
+                    this->addOption(storm::settings::OptionBuilder(moduleName, precomputationTypeOptionName, true, "Sets the kind of precomputation used. Available are: { local, global }.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the type to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(types)).setDefaultValueString("global").build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, numberOfExplorationStepsUntilPrecomputationOptionName, true, "Sets the number of exploration steps to perform until a precomputation is triggered.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of exploration steps to perform.").setDefaultValueUnsignedInteger(100000).build()).build());
+                this->addOption(storm::settings::OptionBuilder(moduleName, numberOfSampledPathsUntilPrecomputationOptionName, true, "If set, a precomputation is perfomed periodically after the given number of paths has been sampled.").addArgument(storm::settings::ArgumentBuilder::createUnsignedIntegerArgument("count", "The number of paths to sample until a precomputation is triggered.").setDefaultValueUnsignedInteger(100000).build()).build());
+                
+                std::vector<std::string> nextStateHeuristics = { "probdiffs", "prob", "unif" };
+                this->addOption(storm::settings::OptionBuilder(moduleName, nextStateHeuristicOptionName, true, "Sets the next-state heuristic to use. Available are: { probdiffs, prob, unif } where 'prob' samples according to the probabilities in the system, 'probdiffs' takes into account probabilities and the differences between the current bounds and 'unif' samples uniformly.").addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the heuristic to use.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(nextStateHeuristics)).setDefaultValueString("probdiffs").build()).build());
+                
+                this->addOption(storm::settings::OptionBuilder(moduleName, precisionOptionName, false, "The internally used precision.").setShortName(precisionOptionShortName)
+                                .addArgument(storm::settings::ArgumentBuilder::createDoubleArgument("value", "The precision to use.").setDefaultValueDouble(1e-06).addValidationFunctionDouble(storm::settings::ArgumentValidators::doubleRangeValidatorExcluding(0.0, 1.0)).build()).build());
+            }
+            
+            bool ExplorationSettings::isLocalPrecomputationSet() const {
+                if (this->getOption(precomputationTypeOptionName).getArgumentByName("name").getValueAsString() == "local") {
+                    return true;
+                }
+                return false;
+            }
+            
+            bool ExplorationSettings::isGlobalPrecomputationSet() const {
+                if (this->getOption(precomputationTypeOptionName).getArgumentByName("name").getValueAsString() == "global") {
+                    return true;
+                }
+                return false;
+            }
+            
+            ExplorationSettings::PrecomputationType ExplorationSettings::getPrecomputationType() const {
+                std::string typeAsString = this->getOption(precomputationTypeOptionName).getArgumentByName("name").getValueAsString();
+                if (typeAsString == "local") {
+                    return ExplorationSettings::PrecomputationType::Local;
+                } else if (typeAsString == "global") {
+                    return ExplorationSettings::PrecomputationType::Global;
+                }
+                STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown precomputation type '" << typeAsString << "'.");
+            }
+            
+            uint_fast64_t ExplorationSettings::getNumberOfExplorationStepsUntilPrecomputation() const {
+                return this->getOption(numberOfExplorationStepsUntilPrecomputationOptionName).getArgumentByName("count").getValueAsUnsignedInteger();
+            }
+            
+            bool ExplorationSettings::isNumberOfSampledPathsUntilPrecomputationSet() const {
+                return this->getOption(numberOfSampledPathsUntilPrecomputationOptionName).getHasOptionBeenSet();
+            }
+            
+            uint_fast64_t ExplorationSettings::getNumberOfSampledPathsUntilPrecomputation() const {
+                return this->getOption(numberOfSampledPathsUntilPrecomputationOptionName).getArgumentByName("count").getValueAsUnsignedInteger();
+            }
+            
+            ExplorationSettings::NextStateHeuristic ExplorationSettings::getNextStateHeuristic() const {
+                std::string nextStateHeuristicAsString = this->getOption(nextStateHeuristicOptionName).getArgumentByName("name").getValueAsString();
+                if (nextStateHeuristicAsString == "probdiffs") {
+                    return ExplorationSettings::NextStateHeuristic::DifferenceProbabilitySum;
+                } else if (nextStateHeuristicAsString == "prob") {
+                    return ExplorationSettings::NextStateHeuristic::Probability;
+                } else if (nextStateHeuristicAsString == "unif") {
+                    return ExplorationSettings::NextStateHeuristic::Uniform;
+                }
+                STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentValueException, "Unknown next-state heuristic '" << nextStateHeuristicAsString << "'.");
+            }
+            
+            double ExplorationSettings::getPrecision() const {
+                return this->getOption(precisionOptionName).getArgumentByName("value").getValueAsDouble();
+            }
+            
+            bool ExplorationSettings::check() const {
+                bool optionsSet = this->getOption(precomputationTypeOptionName).getHasOptionBeenSet() ||
+                                    this->getOption(numberOfExplorationStepsUntilPrecomputationOptionName).getHasOptionBeenSet() ||
+                                    this->getOption(numberOfSampledPathsUntilPrecomputationOptionName).getHasOptionBeenSet() ||
+                                    this->getOption(nextStateHeuristicOptionName).getHasOptionBeenSet();
+                STORM_LOG_WARN_COND(storm::settings::generalSettings().getEngine() == storm::settings::modules::GeneralSettings::Engine::Exploration || !optionsSet, "Exploration engine is not selected, so setting options for it has no effect.");
+                return true;
+            }
+        } // namespace modules
+    } // namespace settings
+} // namespace storm
\ No newline at end of file
diff --git a/src/settings/modules/ExplorationSettings.h b/src/settings/modules/ExplorationSettings.h
new file mode 100644
index 000000000..8f72785eb
--- /dev/null
+++ b/src/settings/modules/ExplorationSettings.h
@@ -0,0 +1,102 @@
+#ifndef STORM_SETTINGS_MODULES_EXPLORATIONSETTINGS_H_
+#define STORM_SETTINGS_MODULES_EXPLORATIONSETTINGS_H_
+
+#include "src/settings/modules/ModuleSettings.h"
+
+namespace storm {
+    namespace settings {
+        namespace modules {
+            
+            /*!
+             * This class represents the exploration settings.
+             */
+            class ExplorationSettings : public ModuleSettings {
+            public:
+                // An enumeration of all available precomputation types.
+                enum class PrecomputationType { Local, Global };
+                
+                // The available heuristics to choose the next state.
+                enum class NextStateHeuristic { DifferenceProbabilitySum, Probability, Uniform };
+                
+                /*!
+                 * Creates a new set of exploration settings that is managed by the given manager.
+                 *
+                 * @param settingsManager The responsible manager.
+                 */
+                ExplorationSettings(storm::settings::SettingsManager& settingsManager);
+                
+                /*!
+                 * Retrieves whether local precomputation is to be used.
+                 *
+                 * @return True iff local precomputation is to be used.
+                 */
+                bool isLocalPrecomputationSet() const;
+                
+                /*!
+                 * Retrieves whether global precomputation is to be used.
+                 *
+                 * @return True iff global precomputation is to be used.
+                 */
+                bool isGlobalPrecomputationSet() const;
+                
+                /*!
+                 * Retrieves the selected precomputation type.
+                 *
+                 * @return The selected precomputation type.
+                 */
+                PrecomputationType getPrecomputationType() const;
+                
+                /*!
+                 * Retrieves the number of exploration steps to perform until a precomputation is triggered.
+                 *
+                 * @return The number of exploration steps to perform until a precomputation is triggered.
+                 */
+                uint_fast64_t getNumberOfExplorationStepsUntilPrecomputation() const;
+
+                /*
+                 * Retrieves whether the option to perform a precomputation after a given number of sampled paths was set.
+                 *
+                 * @return True iff a precomputation after a given number of sampled paths is to be performed.
+                 */
+                bool isNumberOfSampledPathsUntilPrecomputationSet() const;
+                
+                /*!
+                 * Retrieves the number of paths to sample until a precomputation is triggered.
+                 *
+                 * @return The the number of paths to sample until a precomputation is triggered.
+                 */
+                uint_fast64_t getNumberOfSampledPathsUntilPrecomputation() const;
+                
+                /*!
+                 * Retrieves the selected next-state heuristic.
+                 *
+                 * @return The selected next-state heuristic.
+                 */
+                NextStateHeuristic getNextStateHeuristic() const;
+                
+                /*!
+                 * Retrieves the precision to use for numerical operations.
+                 *
+                 * @return The precision to use for numerical operations.
+                 */
+                double getPrecision() const;
+                
+                virtual bool check() const override;
+                
+                // The name of the module.
+                static const std::string moduleName;
+                
+            private:
+                // Define the string names of the options as constants.
+                static const std::string precomputationTypeOptionName;
+                static const std::string numberOfExplorationStepsUntilPrecomputationOptionName;
+                static const std::string numberOfSampledPathsUntilPrecomputationOptionName;
+                static const std::string nextStateHeuristicOptionName;
+                static const std::string precisionOptionName;
+                static const std::string precisionOptionShortName;
+            };
+        } // namespace modules
+    } // namespace settings
+} // namespace storm
+
+#endif /* STORM_SETTINGS_MODULES_EXPLORATIONSETTINGS_H_ */
diff --git a/src/settings/modules/GeneralSettings.cpp b/src/settings/modules/GeneralSettings.cpp
index 44572d23e..5410651a6 100644
--- a/src/settings/modules/GeneralSettings.cpp
+++ b/src/settings/modules/GeneralSettings.cpp
@@ -107,9 +107,9 @@ namespace storm {
                 this->addOption(storm::settings::OptionBuilder(moduleName, noCutsOptionName, false, "Do not perform cuts when buildings the state space.").build());
                 this->addOption(storm::settings::OptionBuilder(moduleName, dontFixDeadlockOptionName, false, "If the model contains deadlock states, this flag disables automatically fixing them.").setShortName(dontFixDeadlockOptionShortName).build());
                 
-                std::vector<std::string> engines = {"sparse", "hybrid", "dd", "abs"};
+                std::vector<std::string> engines = {"sparse", "hybrid", "dd", "expl", "abs"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, engineOptionName, false, "Sets which engine is used for model building and model checking.").setShortName(engineOptionShortName)
-                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use. Available are {sparse, hybrid, dd, ar}.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(engines)).setDefaultValueString("sparse").build()).build());
+                                .addArgument(storm::settings::ArgumentBuilder::createStringArgument("name", "The name of the engine to use. Available are {sparse, hybrid, dd, expl, abs}.").addValidationFunctionString(storm::settings::ArgumentValidators::stringInListValidator(engines)).setDefaultValueString("sparse").build()).build());
                 
                 std::vector<std::string> linearEquationSolver = {"gmm++", "native"};
                 this->addOption(storm::settings::OptionBuilder(moduleName, eqSolverOptionName, false, "Sets which solver is preferred for solving systems of linear equations.")
@@ -385,6 +385,8 @@ namespace storm {
                     engine = GeneralSettings::Engine::Hybrid;
                 } else if (engineStr == "dd") {
                     engine = GeneralSettings::Engine::Dd;
+                } else if (engineStr == "expl") {
+                    engine = GeneralSettings::Engine::Exploration;
                 } else if (engineStr == "abs") {
                     engine = GeneralSettings::Engine::AbstractionRefinement;
                 } else {
diff --git a/src/settings/modules/GeneralSettings.h b/src/settings/modules/GeneralSettings.h
index 242dc8969..66f754d27 100644
--- a/src/settings/modules/GeneralSettings.h
+++ b/src/settings/modules/GeneralSettings.h
@@ -28,7 +28,7 @@ namespace storm {
             public:
                 // An enumeration of all engines.
                 enum class Engine {
-                    Sparse, Hybrid, Dd, AbstractionRefinement
+                    Sparse, Hybrid, Dd, Exploration, AbstractionRefinement
                 };
 
                 /*!
diff --git a/src/storage/MaximalEndComponentDecomposition.cpp b/src/storage/MaximalEndComponentDecomposition.cpp
index 31c421224..0b9995c08 100644
--- a/src/storage/MaximalEndComponentDecomposition.cpp
+++ b/src/storage/MaximalEndComponentDecomposition.cpp
@@ -74,7 +74,7 @@ namespace storm {
             // from iterator to const_iterator only for "set, multiset, map [and] multimap".
             for (std::list<StateBlock>::const_iterator mecIterator = endComponentStateSets.begin(); mecIterator != endComponentStateSets.end();) {
                 StateBlock const& mec = *mecIterator;
-
+                
                 // Keep track of whether the MEC changed during this iteration.
                 bool mecChanged = false;
                 
@@ -98,6 +98,10 @@ namespace storm {
                             for (uint_fast64_t choice = nondeterministicChoiceIndices[state]; choice < nondeterministicChoiceIndices[state + 1]; ++choice) {
                                 bool choiceContainedInMEC = true;
                                 for (auto const& entry : transitionMatrix.getRow(choice)) {
+                                    if (entry.getValue() == storm::utility::zero<ValueType>()) {
+                                        continue;
+                                    }
+                                        
                                     if (!scc.containsState(entry.getColumn())) {
                                         choiceContainedInMEC = false;
                                         break;
@@ -175,6 +179,7 @@ namespace storm {
                         }
                     }
                     
+                    STORM_LOG_ASSERT(!containedChoices.empty(), "The contained choices of any state in an MEC must be non-empty.");
                     newMec.addState(state, std::move(containedChoices));
                 }
                 
diff --git a/src/storage/SparseMatrix.cpp b/src/storage/SparseMatrix.cpp
index 9795dbe2d..907f97081 100644
--- a/src/storage/SparseMatrix.cpp
+++ b/src/storage/SparseMatrix.cpp
@@ -106,14 +106,11 @@ namespace storm {
         template<typename ValueType>
         void SparseMatrixBuilder<ValueType>::addNextValue(index_type row, index_type column, ValueType const& value) {
             // Check that we did not move backwards wrt. the row.
-            if (row < lastRow) {
-                throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrixBuilder::addNextValue: adding an element in row " << row << ", but an element in row " << lastRow << " has already been added.";
-            }
+            STORM_LOG_THROW(row >= lastRow, storm::exceptions::InvalidArgumentException, "Adding an element in row " << row << ", but an element in row " << lastRow << " has already been added.");
             
-            // Check that we did not move backwards wrt. to column.
-            if (row == lastRow && column < lastColumn) {
-                throw storm::exceptions::InvalidArgumentException() << "Illegal call to SparseMatrixBuilder::addNextValue: adding an element in column " << column << " in row " << row << ", but an element in column " << lastColumn << " has already been added in that row.";
-            }
+            // If the element is in the same row, but was not inserted in the correct order, we need to fix the row after
+            // the insertion.
+            bool fixCurrentRow = row == lastRow && column < lastColumn;
             
             // If we switched to another row, we have to adjust the missing entries in the row indices vector.
             if (row != lastRow) {
@@ -132,6 +129,27 @@ namespace storm {
             highestColumn = std::max(highestColumn, column);
             ++currentEntryCount;
             
+            // If we need to fix the row, do so now.
+            if (fixCurrentRow) {
+                // First, we sort according to columns.
+                std::sort(columnsAndValues.begin() + rowIndications.back(), columnsAndValues.end(), [] (storm::storage::MatrixEntry<index_type, ValueType> const& a, storm::storage::MatrixEntry<index_type, ValueType> const& b) {
+                    return a.getColumn() < b.getColumn();
+                });
+                
+                // Then, we eliminate possible duplicate entries.
+                auto it = std::unique(columnsAndValues.begin() + rowIndications.back(), columnsAndValues.end(), [] (storm::storage::MatrixEntry<index_type, ValueType> const& a, storm::storage::MatrixEntry<index_type, ValueType> const& b) {
+                    return a.getColumn() == b.getColumn();
+                });
+                
+                // Finally, remove the superfluous elements.
+                std::size_t elementsToRemove = std::distance(it, columnsAndValues.end());
+                if (elementsToRemove > 0) {
+                    STORM_LOG_WARN("Unordered insertion into matrix builder caused duplicate entries.");
+                    currentEntryCount -= elementsToRemove;
+                    columnsAndValues.resize(columnsAndValues.size() - elementsToRemove);
+                }
+            }
+            
             // In case we did not expect this value, we throw an exception.
             if (forceInitialDimensions) {
                 STORM_LOG_THROW(!initialRowCountSet || lastRow < initialRowCount, storm::exceptions::OutOfRangeException, "Cannot insert value at illegal row " << lastRow << ".");
@@ -1319,6 +1337,9 @@ namespace storm {
         template std::ostream& operator<<(std::ostream& out, SparseMatrix<double> const& matrix);
         template std::vector<double> SparseMatrix<double>::getPointwiseProductRowSumVector(storm::storage::SparseMatrix<double> const& otherMatrix) const;
         template bool SparseMatrix<double>::isSubmatrixOf(SparseMatrix<double> const& matrix) const;
+
+        template class MatrixEntry<uint32_t, double>;
+        template std::ostream& operator<<(std::ostream& out, MatrixEntry<uint32_t, double> const& entry);
         
         // float
         template class MatrixEntry<typename SparseMatrix<float>::index_type, float>;
diff --git a/src/storage/SparseMatrix.h b/src/storage/SparseMatrix.h
index c5c7133c6..f1debced1 100644
--- a/src/storage/SparseMatrix.h
+++ b/src/storage/SparseMatrix.h
@@ -229,7 +229,7 @@ namespace storm {
              * @return True if replacement took place, False if nothing changed.
              */
             bool replaceColumns(std::vector<index_type> const& replacements, index_type offset);
-            
+                        
         private:
             // A flag indicating whether a row count was set upon construction.
             bool initialRowCountSet;
diff --git a/src/storage/expressions/ToExprtkStringVisitor.cpp b/src/storage/expressions/ToExprtkStringVisitor.cpp
index f3a89b2c5..c0cea43ac 100644
--- a/src/storage/expressions/ToExprtkStringVisitor.cpp
+++ b/src/storage/expressions/ToExprtkStringVisitor.cpp
@@ -10,7 +10,7 @@ namespace storm {
             stream.str("");
             stream.clear();
             expression->accept(*this);
-            return std::move(stream.str());
+            return stream.str();
         }
         
         boost::any ToExprtkStringVisitor::visit(IfThenElseExpression const& expression) {
diff --git a/src/storage/prism/Program.cpp b/src/storage/prism/Program.cpp
index 249fe76ae..f8a556051 100644
--- a/src/storage/prism/Program.cpp
+++ b/src/storage/prism/Program.cpp
@@ -412,6 +412,14 @@ namespace storm {
             return this->labels[labelIndexPair->second].getStatePredicateExpression();
         }
         
+        std::map<std::string, storm::expressions::Expression> Program::getLabelToExpressionMapping() const {
+            std::map<std::string, storm::expressions::Expression> result;
+            for (auto const& label : labels) {
+                result.emplace(label.getName(), label.getStatePredicateExpression());
+            }
+            return result;
+        }
+        
         std::size_t Program::getNumberOfLabels() const {
             return this->getLabels().size();
         }
diff --git a/src/storage/prism/Program.h b/src/storage/prism/Program.h
index a33cb1893..4c0d51196 100644
--- a/src/storage/prism/Program.h
+++ b/src/storage/prism/Program.h
@@ -401,6 +401,13 @@ namespace storm {
              */
             storm::expressions::Expression const& getLabelExpression(std::string const& label) const;
             
+            /*!
+             * Retrieves a mapping from all labels in the program to their defining expressions.
+             *
+             * @return A mapping from label names to their expressions.
+             */
+            std::map<std::string, storm::expressions::Expression> getLabelToExpressionMapping() const;
+            
             /*!
              * Retrieves the number of labels in the program.
              *
diff --git a/src/storage/sparse/StateStorage.cpp b/src/storage/sparse/StateStorage.cpp
new file mode 100644
index 000000000..60af49179
--- /dev/null
+++ b/src/storage/sparse/StateStorage.cpp
@@ -0,0 +1,20 @@
+#include "src/storage/sparse/StateStorage.h"
+
+namespace storm {
+    namespace storage {
+        namespace sparse {
+                        
+            template <typename StateType>
+            StateStorage<StateType>::StateStorage(uint64_t bitsPerState) : stateToId(bitsPerState, 10000000), initialStateIndices(), bitsPerState(bitsPerState) {
+                // Intentionally left empty.
+            }
+
+            template <typename StateType>
+            uint_fast64_t StateStorage<StateType>::getNumberOfStates() const {
+                return stateToId.size();
+            }
+            
+            template class StateStorage<uint32_t>;
+        }
+    }
+}
\ No newline at end of file
diff --git a/src/storage/sparse/StateStorage.h b/src/storage/sparse/StateStorage.h
new file mode 100644
index 000000000..eee1855c0
--- /dev/null
+++ b/src/storage/sparse/StateStorage.h
@@ -0,0 +1,35 @@
+#ifndef STORM_STORAGE_SPARSE_STATESTORAGE_H_
+#define STORM_STORAGE_SPARSE_STATESTORAGE_H_
+
+#include <cstdint>
+
+#include "src/storage/BitVectorHashMap.h"
+
+namespace storm {
+    namespace storage {
+        namespace sparse {
+            
+            // A structure holding information about the reachable state space while building it.
+            template <typename StateType>
+            struct StateStorage {
+                // Creates an empty state storage structure for storing states of the given bit width.
+                StateStorage(uint64_t bitsPerState);
+                
+                // This member stores all the states and maps them to their unique indices.
+                storm::storage::BitVectorHashMap<StateType> stateToId;
+                
+                // A list of initial states in terms of their global indices.
+                std::vector<StateType> initialStateIndices;
+                
+                // The number of bits of each state.
+                uint64_t bitsPerState;
+                
+                // The number of states that were found in the exploration so far.
+                uint_fast64_t getNumberOfStates() const;
+            };
+            
+        }
+    }
+}
+
+#endif /* STORM_STORAGE_SPARSE_STATESTORAGE_H_ */
\ No newline at end of file
diff --git a/src/storage/sparse/StateValuations.cpp b/src/storage/sparse/StateValuations.cpp
new file mode 100644
index 000000000..f3f98818f
--- /dev/null
+++ b/src/storage/sparse/StateValuations.cpp
@@ -0,0 +1,17 @@
+#include "src/storage/sparse/StateValuations.h"
+
+namespace storm {
+    namespace storage {
+        namespace sparse {
+            
+            StateValuations::StateValuations(state_type const& numberOfStates) : valuations(numberOfStates) {
+                // Intentionally left empty.
+            }
+            
+            std::string StateValuations::stateInfo(state_type const& state) const {
+                return valuations[state].toString();
+            }
+            
+        }
+    }
+}
\ No newline at end of file
diff --git a/src/storage/sparse/StateValuations.h b/src/storage/sparse/StateValuations.h
new file mode 100644
index 000000000..b64620efd
--- /dev/null
+++ b/src/storage/sparse/StateValuations.h
@@ -0,0 +1,33 @@
+#ifndef STORM_STORAGE_SPARSE_STATEVALUATIONS_H_
+#define STORM_STORAGE_SPARSE_STATEVALUATIONS_H_
+
+#include <cstdint>
+#include <string>
+
+#include "src/storage/sparse/StateType.h"
+#include "src/storage/expressions/SimpleValuation.h"
+
+#include "src/models/sparse/StateAnnotation.h"
+
+namespace storm {
+    namespace storage {
+        namespace sparse {
+            
+            // A structure holding information about the reachable state space that can be retrieved from the outside.
+            struct StateValuations : public storm::models::sparse::StateAnnotation {
+                /*!
+                 * Constructs a state information object for the given number of states.
+                 */
+                StateValuations(state_type const& numberOfStates);
+                
+                // A mapping from state indices to their variable valuations.
+                std::vector<storm::expressions::SimpleValuation> valuations;
+                
+                virtual std::string stateInfo(state_type const& state) const override;
+            };
+            
+        }
+    }
+}
+
+#endif /* STORM_STORAGE_SPARSE_STATEVALUATIONS_H_ */
\ No newline at end of file
diff --git a/src/utility/prism.cpp b/src/utility/prism.cpp
index 5901d3434..822e01fdc 100644
--- a/src/utility/prism.cpp
+++ b/src/utility/prism.cpp
@@ -1,13 +1,72 @@
 #include "src/utility/prism.h"
+
+#include "src/adapters/CarlAdapter.h"
+
 #include "src/storage/expressions/ExpressionManager.h"
 #include "src/storage/prism/Program.h"
 
+#include "src/utility/macros.h"
+
 #include "src/exceptions/InvalidArgumentException.h"
-#include "macros.h"
 
 namespace storm {
     namespace utility {
         namespace prism {
+            
+            template<typename ValueType>
+            storm::prism::Program preprocessProgram(storm::prism::Program const& program, boost::optional<std::map<storm::expressions::Variable, storm::expressions::Expression>> const& constantDefinitions, boost::optional<std::set<std::string>> const& restrictedLabelSet, boost::optional<std::vector<storm::expressions::Expression>> const& expressionLabels) {
+                storm::prism::Program result;
+                
+                // Start by defining the undefined constants in the model.
+                if (constantDefinitions) {
+                    result = program.defineUndefinedConstants(constantDefinitions.get());
+                } else {
+                    result = program;
+                }
+                
+                // If the program still contains undefined constants and we are not in a parametric setting, assemble an appropriate error message.
+                if (!std::is_same<ValueType, storm::RationalFunction>::value && result.hasUndefinedConstants()) {
+                    std::vector<std::reference_wrapper<storm::prism::Constant const>> undefinedConstants = result.getUndefinedConstants();
+                    std::stringstream stream;
+                    bool printComma = false;
+                    for (auto const& constant : undefinedConstants) {
+                        if (printComma) {
+                            stream << ", ";
+                        } else {
+                            printComma = true;
+                        }
+                        stream << constant.get().getName() << " (" << constant.get().getType() << ")";
+                    }
+                    stream << ".";
+                    STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "Program still contains these undefined constants: " + stream.str());
+                } else if (std::is_same<ValueType, storm::RationalFunction>::value && !result.hasUndefinedConstantsOnlyInUpdateProbabilitiesAndRewards()) {
+                    STORM_LOG_THROW(false, storm::exceptions::InvalidArgumentException, "The program contains undefined constants that appear in some places other than update probabilities and reward value expressions, which is not admitted.");
+                }
+                
+                // If the set of labels we are supposed to built is restricted, we need to remove the other labels from the program.
+                if (restrictedLabelSet) {
+                    result.filterLabels(restrictedLabelSet.get());
+                }
+                
+                // Build new labels.
+                if (expressionLabels) {
+                    std::map<storm::expressions::Variable, storm::expressions::Expression> constantsSubstitution = result.getConstantsSubstitution();
+                    
+                    for (auto const& expression : expressionLabels.get()) {
+                        std::stringstream stream;
+                        stream << expression.substitute(constantsSubstitution);
+                        std::string name = stream.str();
+                        if (!result.hasLabel(name)) {
+                            result.addLabel(name, expression);
+                        }
+                    }
+                }
+                
+                // Now that the program is fixed, we we need to substitute all constants with their concrete value.
+                result = result.substituteConstants();
+                return result;
+            }
+            
             std::map<storm::expressions::Variable, storm::expressions::Expression> parseConstantDefinitionString(storm::prism::Program const& program, std::string const& constantDefinitionString) {
                 std::map<storm::expressions::Variable, storm::expressions::Expression> constantDefinitions;
                 std::set<storm::expressions::Variable> definedConstants;
@@ -64,6 +123,11 @@ namespace storm {
                 
                 return constantDefinitions;
             }
+            
+            template storm::prism::Program preprocessProgram<double>(storm::prism::Program const& program, boost::optional<std::map<storm::expressions::Variable, storm::expressions::Expression>> const& constantDefinitions, boost::optional<std::set<std::string>> const& restrictedLabelSet, boost::optional<std::vector<storm::expressions::Expression>> const& expressionLabels);
+
+            template storm::prism::Program preprocessProgram<storm::RationalFunction>(storm::prism::Program const& program, boost::optional<std::map<storm::expressions::Variable, storm::expressions::Expression>> const& constantDefinitions, boost::optional<std::set<std::string>> const& restrictedLabelSet, boost::optional<std::vector<storm::expressions::Expression>> const& expressionLabels);
+
         }
     }
 }
\ No newline at end of file
diff --git a/src/utility/prism.h b/src/utility/prism.h
index f894b464f..c6a8918b9 100644
--- a/src/utility/prism.h
+++ b/src/utility/prism.h
@@ -1,13 +1,11 @@
 #ifndef STORM_UTILITY_PRISM_H_
 #define STORM_UTILITY_PRISM_H_
 
-#include <memory>
 #include <map>
-#include <boost/algorithm/string.hpp>
-#include <boost/container/flat_set.hpp>
-
-#include "src/utility/OsDetection.h"
+#include <set>
+#include <vector>
 
+#include <boost/optional.hpp>
 
 namespace storm {
     namespace expressions {
@@ -21,185 +19,9 @@ namespace storm {
     
     namespace utility {
         namespace prism {
-            // A structure holding information about a particular choice.
-            template<typename ValueType, typename KeyType=uint32_t, typename Compare=std::less<uint32_t>>
-            struct Choice {
-            public:
-                Choice(uint_fast64_t actionIndex = 0, bool createChoiceLabels = false) : distribution(), actionIndex(actionIndex), choiceLabels(nullptr) {
-                    if (createChoiceLabels) {
-                        choiceLabels = std::shared_ptr<boost::container::flat_set<uint_fast64_t>>(new boost::container::flat_set<uint_fast64_t>());
-                    }
-                }
-                
-                Choice(Choice const& other) = default;
-                Choice& operator=(Choice const& other) = default;
-#ifndef WINDOWS
-                Choice(Choice&& other) = default;
-                Choice& operator=(Choice&& other) = default;
-#endif
-                
-                /*!
-                 * Returns an iterator to the first element of this choice.
-                 *
-                 * @return An iterator to the first element of this choice.
-                 */
-                typename std::map<KeyType, ValueType>::iterator begin() {
-                    return distribution.begin();
-                }
-                
-                /*!
-                 * Returns an iterator to the first element of this choice.
-                 *
-                 * @return An iterator to the first element of this choice.
-                 */
-                typename std::map<KeyType, ValueType>::const_iterator begin() const {
-                    return distribution.cbegin();
-                }
-                
-                /*!
-                 * Returns an iterator that points past the elements of this choice.
-                 *
-                 * @return An iterator that points past the elements of this choice.
-                 */
-                typename std::map<KeyType, ValueType>::iterator end() {
-                    return distribution.end();
-                }
-                
-                /*!
-                 * Returns an iterator that points past the elements of this choice.
-                 *
-                 * @return An iterator that points past the elements of this choice.
-                 */
-                typename std::map<KeyType, ValueType>::const_iterator end() const {
-                    return distribution.cend();
-                }
-                
-                /*!
-                 * Returns an iterator to the element with the given key, if there is one. Otherwise, the iterator points to
-                 * distribution.end().
-                 *
-                 * @param value The value to find.
-                 * @return An iterator to the element with the given key, if there is one.
-                 */
-                typename std::map<KeyType, ValueType>::iterator find(uint_fast64_t value) {
-                    return distribution.find(value);
-                }
-                
-                /*!
-                 * Inserts the contents of this object to the given output stream.
-                 *
-                 * @param out The stream in which to insert the contents.
-                 */
-                friend std::ostream& operator<<(std::ostream& out, Choice<ValueType> const& choice) {
-                    out << "<";
-                    for (auto const& stateProbabilityPair : choice.distribution) {
-                        out << stateProbabilityPair.first << " : " << stateProbabilityPair.second << ", ";
-                    }
-                    out << ">";
-                    return out;
-                }
-                
-                /*!
-                 * Adds the given label to the labels associated with this choice.
-                 *
-                 * @param label The label to associate with this choice.
-                 */
-                void addChoiceLabel(uint_fast64_t label) {
-                    choiceLabels->insert(label);
-                }
-                
-                /*!
-                 * Adds the given label set to the labels associated with this choice.
-                 *
-                 * @param labelSet The label set to associate with this choice.
-                 */
-                void addChoiceLabels(boost::container::flat_set<uint_fast64_t> const& labelSet) {
-                    for (uint_fast64_t label : labelSet) {
-                        addChoiceLabel(label);
-                    }
-                }
-                
-                /*!
-                 * Retrieves the set of labels associated with this choice.
-                 *
-                 * @return The set of labels associated with this choice.
-                 */
-                boost::container::flat_set<uint_fast64_t> const& getChoiceLabels() const {
-                    return *choiceLabels;
-                }
-                
-                /*!
-                 * Retrieves the index of the action of this choice.
-                 *
-                 * @return The index of the action of this choice.
-                 */
-                uint_fast64_t getActionIndex() const {
-                    return actionIndex;
-                }
-                
-                /*!
-                 * Retrieves the total mass of this choice.
-                 *
-                 * @return The total mass.
-                 */
-                ValueType getTotalMass() const {
-                    return totalMass;
-                }
-                
-                /*!
-                 * Retrieves the entry in the choice that is associated with the given state and creates one if none exists,
-                 * yet.
-                 *
-                 * @param state The state for which to add the entry.
-                 * @return A reference to the entry that is associated with the given state.
-                 */
-                ValueType& getOrAddEntry(uint_fast64_t state) {
-                    auto stateProbabilityPair = distribution.find(state);
-                    
-                    if (stateProbabilityPair == distribution.end()) {
-                        distribution[state] = ValueType();
-                    }
-                    return distribution.at(state);
-                }
-                
-                /*!
-                 * Retrieves the entry in the choice that is associated with the given state and creates one if none exists,
-                 * yet.
-                 *
-                 * @param state The state for which to add the entry.
-                 * @return A reference to the entry that is associated with the given state.
-                 */
-                ValueType const& getOrAddEntry(uint_fast64_t state) const {
-                    auto stateProbabilityPair = distribution.find(state);
-                    
-                    if (stateProbabilityPair == distribution.end()) {
-                        distribution[state] = ValueType();
-                    }
-                    return distribution.at(state);
-                }
-                
-                void addProbability(KeyType state, ValueType value) {
-                    totalMass += value;
-                    distribution[state] += value;
-                }
-                
-                std::size_t size() const {
-                    return distribution.size();
-                }
-                
-            private:
-                // The distribution that is associated with the choice.
-                std::map<KeyType, ValueType, Compare> distribution;
-        
-                // The total probability mass (or rates) of this choice.
-                ValueType totalMass;
-        
-                // The index of the action name.
-                uint_fast64_t actionIndex;
-                
-                // The labels that are associated with this choice.
-                std::shared_ptr<boost::container::flat_set<uint_fast64_t>> choiceLabels;
-            };
+            
+            template<typename ValueType>
+            storm::prism::Program preprocessProgram(storm::prism::Program const& program, boost::optional<std::map<storm::expressions::Variable, storm::expressions::Expression>> const& constantDefinitions = boost::none, boost::optional<std::set<std::string>> const& restrictedLabelSet = boost::none, boost::optional<std::vector<storm::expressions::Expression>> const& expressionLabels = boost::none);
             
             std::map<storm::expressions::Variable, storm::expressions::Expression> parseConstantDefinitionString(storm::prism::Program const& program, std::string const& constantDefinitionString);
             
diff --git a/src/utility/storm.h b/src/utility/storm.h
index a887388d9..bceb8178a 100644
--- a/src/utility/storm.h
+++ b/src/utility/storm.h
@@ -58,6 +58,7 @@
 #include "src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h"
 #include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h"
 #include "src/modelchecker/abstraction/GameBasedMdpModelChecker.h"
+#include "src/modelchecker/exploration/SparseExplorationModelChecker.h"
 #include "src/modelchecker/csl/SparseCtmcCslModelChecker.h"
 #include "src/modelchecker/csl/HybridCtmcCslModelChecker.h"
 #include "src/modelchecker/csl/SparseMarkovAutomatonCslModelChecker.h"
@@ -256,7 +257,7 @@ namespace storm {
                 STORM_LOG_THROW(ddModel != nullptr, storm::exceptions::InvalidArgumentException, "Dd engine requires a dd input model");
                 return verifySymbolicModelWithDdEngine(ddModel, formula, onlyInitialStatesRelevant);
             }
-            case storm::settings::modules::GeneralSettings::Engine::AbstractionRefinement: {
+            default: {
                 STORM_LOG_ASSERT(false, "This position should not be reached, as at this point no model has been built.");
             }
         }
diff --git a/src/utility/vector.h b/src/utility/vector.h
index 31b1a5493..731cc4a0d 100644
--- a/src/utility/vector.h
+++ b/src/utility/vector.h
@@ -22,8 +22,6 @@ namespace storm {
     namespace utility {
         namespace vector {
 
-
-
             /*!
              * Sets the provided values at the provided positions in the given vector.
              *
diff --git a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
index 36a139b9c..715489715 100644
--- a/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/GmmxxDtmcPrctlModelCheckerTest.cpp
@@ -157,7 +157,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) {
 
         std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
 
-        std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
+        std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
         storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
 
         EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@@ -181,7 +181,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) {
 
         std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
 
-        std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
+        std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
         storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
 
         EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@@ -205,7 +205,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRASingleBscc) {
 
         std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
 
-        std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
+        std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
         storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
 
         EXPECT_NEAR(1. / 3., quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@@ -268,7 +268,7 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, LRA) {
 
         std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
 
-        std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
+        std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
         storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
 
         EXPECT_NEAR(0.3 / 3., quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
diff --git a/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
index 6af4c51cc..253417bad 100644
--- a/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
@@ -157,8 +157,8 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) {
 
         std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
         
-        std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
-		storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
+        std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
+            storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
 
 		EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
 		EXPECT_NEAR(.5, quantitativeResult1[1], storm::settings::nativeEquationSolverSettings().getPrecision());
@@ -181,8 +181,8 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) {
 
         std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
         
-        std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
-		storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
+        std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
+        storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
 
 		EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
 		EXPECT_NEAR(.5, quantitativeResult1[1], storm::settings::nativeEquationSolverSettings().getPrecision());
@@ -205,8 +205,8 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRASingleBscc) {
 
         std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
         
-        std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
-		storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
+        std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
+        storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
 
 		EXPECT_NEAR(1. / 3., quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
 		EXPECT_NEAR(1. / 3., quantitativeResult1[1], storm::settings::nativeEquationSolverSettings().getPrecision());
@@ -268,8 +268,8 @@ TEST(SparseDtmcPrctlModelCheckerTest, LRA) {
 
         std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRA=? [\"a\"]");
         
-        std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
-		storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
+        std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
+        storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
 
 		EXPECT_NEAR(0.3 / 3., quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
 		EXPECT_NEAR(0.0, quantitativeResult1[3], storm::settings::nativeEquationSolverSettings().getPrecision());
diff --git a/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp b/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
index da5a2cd34..85c38e505 100644
--- a/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
+++ b/test/functional/modelchecker/NativeMdpPrctlModelCheckerTest.cpp
@@ -211,7 +211,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
 
         std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
 
-        std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
+        std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
         storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
 
         EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@@ -219,7 +219,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
 
         formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
 
-        result = std::move(checker.check(*formula));
+        result = checker.check(*formula);
         storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
 
         EXPECT_NEAR(.5, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@@ -243,7 +243,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
 
         std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
 
-        std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
+        std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
         storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
 
         EXPECT_NEAR(.5, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@@ -251,7 +251,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
 
         formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
 
-        result = std::move(checker.check(*formula));
+        result = checker.check(*formula);
         storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
 
         EXPECT_NEAR(.5, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@@ -284,7 +284,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
 
         std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
 
-        std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
+        std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
         storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
 
         EXPECT_NEAR(1. / 3., quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@@ -293,7 +293,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
 
         formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
 
-        result = std::move(checker.check(*formula));
+        result = checker.check(*formula);
         storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
 
         EXPECT_NEAR(0.0, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@@ -302,7 +302,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
 
         formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"b\"]");
 
-        result = std::move(checker.check(*formula));
+        result = checker.check(*formula);
         storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
 
         EXPECT_NEAR(0.5, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@@ -311,7 +311,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
 
         formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"b\"]");
 
-        result = std::move(checker.check(*formula));
+        result = checker.check(*formula);
         storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
 
         EXPECT_NEAR(1. / 3., quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@@ -320,7 +320,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
 
         formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"c\"]");
 
-        result = std::move(checker.check(*formula));
+        result = checker.check(*formula);
         storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
 
         EXPECT_NEAR(2. / 3., quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@@ -329,7 +329,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA_SingleMec) {
 
         formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"c\"]");
 
-        result = std::move(checker.check(*formula));
+        result = checker.check(*formula);
         storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
 
         EXPECT_NEAR(0.5, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@@ -370,7 +370,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {
 
         std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
 
-        std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
+        std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
         storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
 
         EXPECT_NEAR(0.0, quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@@ -379,7 +379,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {
 
         formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
 
-        result = std::move(checker.check(*formula));
+        result = checker.check(*formula);
         storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
 
         EXPECT_NEAR(0.0, quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@@ -388,7 +388,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {
 
         formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"b\"]");
 
-        result = std::move(checker.check(*formula));
+        result = checker.check(*formula);
         storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
 
         EXPECT_NEAR(1.0, quantitativeResult3[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@@ -397,7 +397,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {
 
         formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"b\"]");
 
-        result = std::move(checker.check(*formula));
+        result = checker.check(*formula);
         storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
 
         EXPECT_NEAR(0.0, quantitativeResult4[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@@ -406,7 +406,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {
 
         formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"c\"]");
 
-        result = std::move(checker.check(*formula));
+        result = checker.check(*formula);
         storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
 
         EXPECT_NEAR(1.0, quantitativeResult5[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@@ -415,7 +415,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {
 
         formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"c\"]");
 
-        result = std::move(checker.check(*formula));
+        result = checker.check(*formula);
         storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
 
         EXPECT_NEAR(0.0, quantitativeResult6[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@@ -492,7 +492,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {
 
         std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("LRAmax=? [\"a\"]");
 
-        std::unique_ptr<storm::modelchecker::CheckResult> result = std::move(checker.check(*formula));
+        std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
         storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
 
         EXPECT_NEAR(37. / 60., quantitativeResult1[0], storm::settings::nativeEquationSolverSettings().getPrecision());
@@ -505,7 +505,7 @@ TEST(SparseMdpPrctlModelCheckerTest, LRA) {
 
         formula = formulaParser.parseSingleFormulaFromString("LRAmin=? [\"a\"]");
 
-        result = std::move(checker.check(*formula));
+        result = checker.check(*formula);
         storm::modelchecker::ExplicitQuantitativeCheckResult<double>& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
 
         EXPECT_NEAR(0.3 / 3., quantitativeResult2[0], storm::settings::nativeEquationSolverSettings().getPrecision());
diff --git a/test/functional/modelchecker/SparseExplorationModelCheckerTest.cpp b/test/functional/modelchecker/SparseExplorationModelCheckerTest.cpp
new file mode 100644
index 000000000..0e7304f81
--- /dev/null
+++ b/test/functional/modelchecker/SparseExplorationModelCheckerTest.cpp
@@ -0,0 +1,86 @@
+#include "gtest/gtest.h"
+#include "storm-config.h"
+
+#include "src/logic/Formulas.h"
+#include "src/modelchecker/exploration/SparseExplorationModelChecker.h"
+#include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+#include "src/parser/PrismParser.h"
+#include "src/parser/FormulaParser.h"
+
+#include "src/settings/SettingsManager.h"
+#include "src/settings/modules/ExplorationSettings.h"
+
+TEST(SparseExplorationModelCheckerTest, Dice) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/two_dice.nm");
+    
+    // A parser that we use for conveniently constructing the formulas.
+    storm::parser::FormulaParser formulaParser;
+
+    storm::modelchecker::SparseExplorationModelChecker<double, uint32_t> checker(program);
+    
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"two\"]");
+    
+    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(storm::modelchecker::CheckTask<>(*formula, true));
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
+    
+    EXPECT_NEAR(0.0277777612209320068, quantitativeResult1[0], storm::settings::explorationSettings().getPrecision());
+    
+    formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"two\"]");
+    
+    result = checker.check(storm::modelchecker::CheckTask<>(*formula, true));
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
+    
+    EXPECT_NEAR(0.0277777612209320068, quantitativeResult2[0], storm::settings::explorationSettings().getPrecision());
+    
+    formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"three\"]");
+    
+    result = checker.check(storm::modelchecker::CheckTask<>(*formula, true));
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
+    
+    EXPECT_NEAR(0.0555555224418640136, quantitativeResult3[0], storm::settings::explorationSettings().getPrecision());
+    
+    formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"three\"]");
+    
+    result = checker.check(storm::modelchecker::CheckTask<>(*formula, true));
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult4 = result->asExplicitQuantitativeCheckResult<double>();
+    
+    EXPECT_NEAR(0.0555555224418640136, quantitativeResult4[0], storm::settings::explorationSettings().getPrecision());
+    
+    formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"four\"]");
+    
+    result = checker.check(storm::modelchecker::CheckTask<>(*formula, true));
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult5 = result->asExplicitQuantitativeCheckResult<double>();
+    
+    EXPECT_NEAR(0.083333283662796020508, quantitativeResult5[0], storm::settings::explorationSettings().getPrecision());
+    
+    formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"four\"]");
+    
+    result = checker.check(storm::modelchecker::CheckTask<>(*formula, true));
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult6 = result->asExplicitQuantitativeCheckResult<double>();
+    
+    EXPECT_NEAR(0.083333283662796020508, quantitativeResult6[0], storm::settings::explorationSettings().getPrecision());
+}
+
+
+TEST(SparseExplorationModelCheckerTest, AsynchronousLeader) {
+    storm::prism::Program program = storm::parser::PrismParser::parse(STORM_CPP_TESTS_BASE_PATH "/functional/builder/leader4.nm");
+    
+    // A parser that we use for conveniently constructing the formulas.
+    storm::parser::FormulaParser formulaParser;
+    
+    storm::modelchecker::SparseExplorationModelChecker<double, uint32_t> checker(program);
+    
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("Pmin=? [F \"elected\"]");
+    
+    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(storm::modelchecker::CheckTask<>(*formula, true));
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
+    
+    EXPECT_NEAR(1, quantitativeResult1[0], storm::settings::explorationSettings().getPrecision());
+    
+    formula = formulaParser.parseSingleFormulaFromString("Pmax=? [F \"elected\"]");
+    
+    result = checker.check(storm::modelchecker::CheckTask<>(*formula, true));
+    storm::modelchecker::ExplicitQuantitativeCheckResult<double> const& quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
+    
+    EXPECT_NEAR(1, quantitativeResult2[0], storm::settings::explorationSettings().getPrecision());
+}
diff --git a/test/functional/parser/DeterministicSparseTransitionParserTest.cpp b/test/functional/parser/DeterministicSparseTransitionParserTest.cpp
index 50b545d25..dfffcec9c 100644
--- a/test/functional/parser/DeterministicSparseTransitionParserTest.cpp
+++ b/test/functional/parser/DeterministicSparseTransitionParserTest.cpp
@@ -183,11 +183,9 @@ TEST(DeterministicSparseTransitionParserTest, Whitespaces) {
 TEST(DeterministicSparseTransitionParserTest, MixedTransitionOrder) {
 
     // Since the MatrixBuilder needs sequential input of new elements reordering of transitions or states should throw an exception.
-    ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_mixedTransitionOrder.tra"), storm::exceptions::InvalidArgumentException);
     ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_mixedStateOrder.tra"), storm::exceptions::InvalidArgumentException);
 
     storm::storage::SparseMatrix<double> transitionMatrix = storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/dtmc_general.tra");
-    ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_mixedTransitionOrder.trans.rew", transitionMatrix), storm::exceptions::InvalidArgumentException);
     ASSERT_THROW(storm::parser::DeterministicSparseTransitionParser<>::parseDeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/dtmc_mixedStateOrder.trans.rew", transitionMatrix), storm::exceptions::InvalidArgumentException);
 }
 
diff --git a/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp b/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp
index c5c0807bc..57af1b7d8 100644
--- a/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp
+++ b/test/functional/parser/NondeterministicSparseTransitionParserTest.cpp
@@ -202,11 +202,9 @@ TEST(NondeterministicSparseTransitionParserTest, Whitespaces) {
 
 TEST(NondeterministicSparseTransitionParserTest, MixedTransitionOrder) {
 	// Since the MatrixBuilder needs sequential input of new elements reordering of transitions or states should throw an exception.
-	ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_mixedTransitionOrder.tra"), storm::exceptions::InvalidArgumentException);
 	ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_mixedStateOrder.tra"), storm::exceptions::InvalidArgumentException);
 
 	storm::storage::SparseMatrix<double> modelInformation = storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitions(STORM_CPP_TESTS_BASE_PATH "/functional/parser/tra_files/mdp_general.tra");
-	ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_mixedTransitionOrder.trans.rew", modelInformation), storm::exceptions::InvalidArgumentException);
 	ASSERT_THROW(storm::parser::NondeterministicSparseTransitionParser<>::parseNondeterministicTransitionRewards(STORM_CPP_TESTS_BASE_PATH "/functional/parser/rew_files/mdp_mixedStateOrder.trans.rew", modelInformation), storm::exceptions::InvalidArgumentException);
 }
 
diff --git a/test/functional/utility/ModelInstantiatorTest.cpp b/test/functional/utility/ModelInstantiatorTest.cpp
index fe2ee4a7c..24512d886 100644
--- a/test/functional/utility/ModelInstantiatorTest.cpp
+++ b/test/functional/utility/ModelInstantiatorTest.cpp
@@ -77,8 +77,8 @@ TEST(ModelInstantiatorTest, BrpProb) {
         ASSERT_NE(pL, carl::Variable::NO_VARIABLE);
         storm::Variable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
         ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
-        valuation.insert(std::make_pair(pL,carl::rationalize<storm::RationalNumber>(1)));
-        valuation.insert(std::make_pair(pK,carl::rationalize<storm::RationalNumber>(1)));
+        valuation.insert(std::make_pair(pL,carl::rationalize<storm::RationalNumber>(1.0)));
+        valuation.insert(std::make_pair(pK,carl::rationalize<storm::RationalNumber>(1.0)));
 
         storm::models::sparse::Dtmc<double> const& instantiated(modelInstantiator.instantiate(valuation));
 
@@ -110,7 +110,7 @@ TEST(ModelInstantiatorTest, BrpProb) {
         ASSERT_NE(pL, carl::Variable::NO_VARIABLE);
         storm::Variable const& pK = carl::VariablePool::getInstance().findVariableWithName("pK");
         ASSERT_NE(pK, carl::Variable::NO_VARIABLE);
-        valuation.insert(std::make_pair(pL,carl::rationalize<storm::RationalNumber>(1)));
+        valuation.insert(std::make_pair(pL,carl::rationalize<storm::RationalNumber>(1.0)));
         valuation.insert(std::make_pair(pK,carl::rationalize<storm::RationalNumber>(0.9)));
 
         storm::models::sparse::Dtmc<double> const& instantiated(modelInstantiator.instantiate(valuation));
diff --git a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
index b2a39f5dd..4284ab85c 100644
--- a/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
+++ b/test/performance/modelchecker/GmmxxDtmcPrctModelCheckerTest.cpp
@@ -8,6 +8,7 @@
 #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 #include "src/utility/solver.h"
 #include "src/parser/AutoParser.h"
+#include "src/parser/FormulaParser.h"
 #include "src/models/sparse/StandardRewardModel.h"
 
 TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
@@ -22,26 +23,26 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, Crowds) {
 
     storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
 
-	auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observe0Greater1");
-    auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
+    // A parser that we use for conveniently constructing the formulas.
+    storm::parser::FormulaParser formulaParser;
+    
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
 
-    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*eventuallyFormula);
+    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
 
     EXPECT_NEAR(0.2296800237, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
 
-    labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observeIGreater1");
-    eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
+    formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]");
 
-    result = checker.check(*eventuallyFormula);
+    result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
     
 	EXPECT_NEAR(0.05073232193, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
 
-    labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observeOnlyTrueSender");
-    eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
+    formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]");
 
-    result = checker.check(*eventuallyFormula);
+    result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
     
 	EXPECT_NEAR(0.22742171078, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
@@ -60,27 +61,26 @@ TEST(GmmxxDtmcPrctlModelCheckerTest, SynchronousLeader) {
 
 	storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::GmmxxLinearEquationSolverFactory<double>()));
 
-    auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
-    auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
+    // A parser that we use for conveniently constructing the formulas.
+    storm::parser::FormulaParser formulaParser;
+    
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
 
-    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*eventuallyFormula);
+    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
     
 	EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
 
-    labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
-    auto trueFormula = std::make_shared<storm::logic::BooleanLiteralFormula>(true);
-    auto boundedUntilFormula = std::make_shared<storm::logic::BoundedUntilFormula>(trueFormula, labelFormula, 20);
+    formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]");
 
-    result = checker.check(*boundedUntilFormula);
+    result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
     
 	EXPECT_NEAR(0.9993949793, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
 
-    labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
-    auto reachabilityRewardFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula, storm::logic::FormulaContext::Reward);
+    formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]");
 
-    result = checker.check(*reachabilityRewardFormula);
+    result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
     
 	EXPECT_NEAR(1.025106273, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
diff --git a/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp b/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
index 23949131a..85d6399c9 100644
--- a/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
+++ b/test/performance/modelchecker/NativeDtmcPrctlModelCheckerTest.cpp
@@ -2,13 +2,13 @@
 #include "storm-config.h"
 #include "src/settings/SettingsManager.h"
 #include "src/settings/modules/GmmxxEquationSolverSettings.h"
-
 #include "src/settings/modules/NativeEquationSolverSettings.h"
 #include "src/settings/SettingMemento.h"
 #include "src/modelchecker/prctl/SparseDtmcPrctlModelChecker.h"
 #include "src/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 #include "src/utility/solver.h"
 #include "src/parser/AutoParser.h"
+#include "src/parser/FormulaParser.h"
 #include "src/models/sparse/StandardRewardModel.h"
 
 TEST(NativeDtmcPrctlModelCheckerTest, Crowds) {
@@ -23,26 +23,26 @@ TEST(NativeDtmcPrctlModelCheckerTest, Crowds) {
     
     storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
     
-    auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observe0Greater1");
-    auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
+    // A parser that we use for conveniently constructing the formulas.
+    storm::parser::FormulaParser formulaParser;
+    
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observe0Greater1\"]");
     
-    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*eventuallyFormula);
+    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
     
     EXPECT_NEAR(0.22968140721646868, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
     
-    labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observeIGreater1");
-    eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
+    formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeIGreater1\"]");
     
-    result = checker.check(*eventuallyFormula);
+    result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
     
     EXPECT_NEAR(0.05073232193, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
     
-    labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("observeOnlyTrueSender");
-    eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
+    formula = formulaParser.parseSingleFormulaFromString("P=? [F \"observeOnlyTrueSender\"]");
     
-    result = checker.check(*eventuallyFormula);
+    result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
     
     EXPECT_NEAR(0.22742305378217331, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
@@ -60,28 +60,27 @@ TEST(NativeDtmcPrctlModelCheckerTest, SynchronousLeader) {
     ASSERT_EQ(1574477ull, dtmc->getNumberOfTransitions());
     
     storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<double>> checker(*dtmc, std::unique_ptr<storm::utility::solver::LinearEquationSolverFactory<double>>(new storm::utility::solver::NativeLinearEquationSolverFactory<double>()));
+
+    // A parser that we use for conveniently constructing the formulas.
+    storm::parser::FormulaParser formulaParser;
     
-    auto labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
-    auto eventuallyFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula);
+    std::shared_ptr<const storm::logic::Formula> formula = formulaParser.parseSingleFormulaFromString("P=? [F \"elected\"]");
     
-    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*eventuallyFormula);
+    std::unique_ptr<storm::modelchecker::CheckResult> result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult1 = result->asExplicitQuantitativeCheckResult<double>();
     
     EXPECT_NEAR(1.0, quantitativeResult1[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
     
-    labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
-    auto trueFormula = std::make_shared<storm::logic::BooleanLiteralFormula>(true);
-    auto boundedUntilFormula = std::make_shared<storm::logic::BoundedUntilFormula>(trueFormula, labelFormula, 20);
+    formula = formulaParser.parseSingleFormulaFromString("P=? [F<=20 \"elected\"]");
     
-    result = checker.check(*boundedUntilFormula);
+    result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult2 = result->asExplicitQuantitativeCheckResult<double>();
     
     EXPECT_NEAR(0.9993949793, quantitativeResult2[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());
     
-    labelFormula = std::make_shared<storm::logic::AtomicLabelFormula>("elected");
-    auto reachabilityRewardFormula = std::make_shared<storm::logic::EventuallyFormula>(labelFormula, storm::logic::FormulaContext::Reward);
+    formula = formulaParser.parseSingleFormulaFromString("R=? [F \"elected\"]");
     
-    result = checker.check(*reachabilityRewardFormula);
+    result = checker.check(*formula);
     storm::modelchecker::ExplicitQuantitativeCheckResult<double> quantitativeResult3 = result->asExplicitQuantitativeCheckResult<double>();
     
     EXPECT_NEAR(1.0252174454896057, quantitativeResult3[0], storm::settings::gmmxxEquationSolverSettings().getPrecision());