diff --git a/src/cli/entrypoints.h b/src/cli/entrypoints.h
index 17291f750..8748c5a17 100644
--- a/src/cli/entrypoints.h
+++ b/src/cli/entrypoints.h
@@ -61,7 +61,7 @@ namespace storm {
                 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::SparseMdpExplorationModelChecker<ValueType> checker(program, storm::utility::prism::parseConstantDefinitionString(program, storm::settings::generalSettings().getConstantDefinitionString()));
+                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);
diff --git a/src/logic/FragmentSpecification.cpp b/src/logic/FragmentSpecification.cpp
index 6877496d2..3dd2bf12b 100644
--- a/src/logic/FragmentSpecification.cpp
+++ b/src/logic/FragmentSpecification.cpp
@@ -414,6 +414,7 @@ namespace storm {
         
         FragmentSpecification& FragmentSpecification::setOperatorAtTopLevelRequired(bool newValue) {
             operatorAtTopLevelRequired = newValue;
+            return *this;
         }
         
     }
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/SparseMdpExplorationModelChecker.cpp b/src/modelchecker/exploration/SparseExplorationModelChecker.cpp
similarity index 85%
rename from src/modelchecker/exploration/SparseMdpExplorationModelChecker.cpp
rename to src/modelchecker/exploration/SparseExplorationModelChecker.cpp
index 542273713..322af7999 100644
--- a/src/modelchecker/exploration/SparseMdpExplorationModelChecker.cpp
+++ b/src/modelchecker/exploration/SparseExplorationModelChecker.cpp
@@ -1,4 +1,4 @@
-#include "src/modelchecker/exploration/SparseMdpExplorationModelChecker.h"
+#include "src/modelchecker/exploration/SparseExplorationModelChecker.h"
 
 #include "src/modelchecker/exploration/ExplorationInformation.h"
 #include "src/modelchecker/exploration/StateGeneration.h"
@@ -33,20 +33,20 @@
 namespace storm {
     namespace modelchecker {
         
-        template<typename ValueType>
-        SparseMdpExplorationModelChecker<ValueType>::SparseMdpExplorationModelChecker(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() {
+        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>
-        bool SparseMdpExplorationModelChecker<ValueType>::canHandle(CheckTask<storm::logic::Formula> const& checkTask) const {
+        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>
-        std::unique_ptr<CheckResult> SparseMdpExplorationModelChecker<ValueType>::computeUntilProbabilities(CheckTask<storm::logic::UntilFormula> const& checkTask) {
+        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();
@@ -66,8 +66,8 @@ namespace storm {
             return std::make_unique<ExplicitQuantitativeCheckResult<ValueType>>(std::get<0>(boundsForInitialState), std::get<1>(boundsForInitialState));
         }
         
-        template<typename ValueType>
-        std::tuple<typename SparseMdpExplorationModelChecker<ValueType>::StateType, ValueType, ValueType> SparseMdpExplorationModelChecker<ValueType>::performExploration(StateGeneration<StateType, ValueType>& stateGeneration, ExplorationInformation<StateType, ValueType>& explorationInformation) const {
+        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.");
@@ -119,8 +119,8 @@ namespace storm {
             return std::make_tuple(initialStateIndex, bounds.getLowerBoundForState(initialStateIndex, explorationInformation), bounds.getUpperBoundForState(initialStateIndex, explorationInformation));
         }
         
-        template<typename ValueType>
-        bool SparseMdpExplorationModelChecker<ValueType>::samplePathFromInitialState(StateGeneration<StateType, ValueType>& stateGeneration, ExplorationInformation<StateType, ValueType>& explorationInformation, StateActionStack& stack, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const {
+        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));
             
@@ -181,8 +181,8 @@ namespace storm {
             return foundTerminalState;
         }
         
-        template<typename ValueType>
-        bool SparseMdpExplorationModelChecker<ValueType>::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 {
+        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;
             
@@ -283,8 +283,8 @@ namespace storm {
             return isTerminalState;
         }
         
-        template<typename ValueType>
-        typename SparseMdpExplorationModelChecker<ValueType>::ActionType SparseMdpExplorationModelChecker<ValueType>::sampleActionOfState(StateType const& currentStateId, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const {
+        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);
@@ -321,14 +321,13 @@ namespace storm {
             return actionValues[distribution(randomGenerator)].first;
         }
         
-        template<typename ValueType>
-        typename SparseMdpExplorationModelChecker<ValueType>::StateType SparseMdpExplorationModelChecker<ValueType>::sampleSuccessorFromAction(ActionType const& chosenAction, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
+        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());
@@ -347,14 +346,15 @@ namespace storm {
                 // Now sample according to the probabilities.
                 std::discrete_distribution<StateType> distribution(probabilities.begin(), probabilities.end());
                 return row[distribution(randomGenerator)].getColumn();
-            } else if (explorationInformation.useUniformHeuristic()) {
+            } 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>
-        bool SparseMdpExplorationModelChecker<ValueType>::performPrecomputation(StateActionStack const& stack, ExplorationInformation<StateType, ValueType>& explorationInformation, Bounds<StateType, ValueType>& bounds, Statistics<StateType, ValueType>& stats) const {
+        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:
@@ -370,7 +370,7 @@ namespace storm {
             std::vector<StateType> relevantStates;
             if (explorationInformation.useLocalPrecomputation()) {
                 for (auto const& stateActionPair : stack) {
-                    if (explorationInformation.maximize() || !comparator.isOne(bounds.getLowerBoundForState(stateActionPair.first, explorationInformation))) {
+                    if (explorationInformation.maximize() || !storm::utility::isOne(bounds.getLowerBoundForState(stateActionPair.first, explorationInformation))) {
                         relevantStates.push_back(stateActionPair.first);
                     }
                 }
@@ -486,8 +486,8 @@ namespace storm {
             return true;
         }
         
-        template<typename ValueType>
-        void SparseMdpExplorationModelChecker<ValueType>::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 {
+        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.
@@ -498,7 +498,7 @@ namespace storm {
                 StateType originalRowGroup = explorationInformation.getRowGroup(originalState);
                 
                 // Check whether a target state is contained in the MEC.
-                if (!containsTargetState && comparator.isOne(bounds.getLowerBoundForRowGroup(originalRowGroup))) {
+                if (!containsTargetState && storm::utility::isOne(bounds.getLowerBoundForRowGroup(originalRowGroup))) {
                     containsTargetState = true;
                 }
                 
@@ -555,8 +555,8 @@ namespace storm {
             }
         }
         
-        template<typename ValueType>
-        ValueType SparseMdpExplorationModelChecker<ValueType>::computeLowerBoundOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
+        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);
@@ -564,8 +564,8 @@ namespace storm {
             return result;
         }
         
-        template<typename ValueType>
-        ValueType SparseMdpExplorationModelChecker<ValueType>::computeUpperBoundOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
+        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);
@@ -573,8 +573,8 @@ namespace storm {
             return result;
         }
         
-        template<typename ValueType>
-        std::pair<ValueType, ValueType> SparseMdpExplorationModelChecker<ValueType>::computeBoundsOfAction(ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
+        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)) {
@@ -584,8 +584,8 @@ namespace storm {
             return result;
         }
         
-        template<typename ValueType>
-        std::pair<ValueType, ValueType> SparseMdpExplorationModelChecker<ValueType>::computeBoundsOfState(StateType const& currentStateId, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
+        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) {
@@ -595,8 +595,8 @@ namespace storm {
             return result;
         }
         
-        template<typename ValueType>
-        void SparseMdpExplorationModelChecker<ValueType>::updateProbabilityBoundsAlongSampledPath(StateActionStack& stack, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const {
+        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);
@@ -604,8 +604,8 @@ namespace storm {
             }
         }
         
-        template<typename ValueType>
-        void SparseMdpExplorationModelChecker<ValueType>::updateProbabilityOfAction(StateType const& state, ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType>& bounds) const {
+        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);
             
@@ -639,8 +639,8 @@ namespace storm {
             }
         }
         
-        template<typename ValueType>
-        ValueType SparseMdpExplorationModelChecker<ValueType>::computeBoundOverAllOtherActions(storm::OptimizationDirection const& direction, StateType const& state, ActionType const& action, ExplorationInformation<StateType, ValueType> const& explorationInformation, Bounds<StateType, ValueType> const& bounds) const {
+        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);
@@ -658,14 +658,14 @@ namespace storm {
             return bound;
         }
         
-        template<typename ValueType>
-        std::pair<ValueType, ValueType> SparseMdpExplorationModelChecker<ValueType>::getLowestBounds(storm::OptimizationDirection const& direction) const {
+        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>
-        ValueType SparseMdpExplorationModelChecker<ValueType>::getLowestBound(storm::OptimizationDirection const& direction) const {
+        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 {
@@ -673,8 +673,8 @@ namespace storm {
             }
         }
         
-        template<typename ValueType>
-        std::pair<ValueType, ValueType> SparseMdpExplorationModelChecker<ValueType>::combineBounds(storm::OptimizationDirection const& direction, std::pair<ValueType, ValueType> const& bounds1, std::pair<ValueType, ValueType> const& bounds2) const {
+        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 {
@@ -682,6 +682,6 @@ namespace storm {
             }
         }
         
-        template class SparseMdpExplorationModelChecker<double>;
+        template class SparseExplorationModelChecker<double, uint32_t>;
     }
 }
\ No newline at end of file
diff --git a/src/modelchecker/exploration/SparseMdpExplorationModelChecker.h b/src/modelchecker/exploration/SparseExplorationModelChecker.h
similarity index 90%
rename from src/modelchecker/exploration/SparseMdpExplorationModelChecker.h
rename to src/modelchecker/exploration/SparseExplorationModelChecker.h
index 5db171722..aa13f379a 100644
--- a/src/modelchecker/exploration/SparseMdpExplorationModelChecker.h
+++ b/src/modelchecker/exploration/SparseExplorationModelChecker.h
@@ -1,5 +1,5 @@
-#ifndef STORM_MODELCHECKER_EXPLORATION_SPARSEMDPEXPLORATIONMODELCHECKER_H_
-#define STORM_MODELCHECKER_EXPLORATION_SPARSEMDPEXPLORATIONMODELCHECKER_H_
+#ifndef STORM_MODELCHECKER_EXPLORATION_SPARSEEXPLORATIONMODELCHECKER_H_
+#define STORM_MODELCHECKER_EXPLORATION_SPARSEEXPLORATIONMODELCHECKER_H_
 
 #include <random>
 
@@ -30,14 +30,13 @@ namespace storm {
         
         using namespace exploration_detail;
         
-        template<typename ValueType>
-        class SparseMdpExplorationModelChecker : public AbstractModelChecker {
+        template<typename ValueType, typename StateType = uint32_t>
+        class SparseExplorationModelChecker : public AbstractModelChecker {
         public:
-            typedef uint32_t StateType;
             typedef StateType ActionType;
             typedef std::vector<std::pair<StateType, ActionType>> StateActionStack;
             
-            SparseMdpExplorationModelChecker(storm::prism::Program const& program, boost::optional<std::map<storm::expressions::Variable, storm::expressions::Expression>> const& constantDefinitions);
+            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;
             
@@ -87,4 +86,4 @@ namespace storm {
     }
 }
 
-#endif /* STORM_MODELCHECKER_EXPLORATION_SPARSEMDPEXPLORATIONMODELCHECKER_H_ */
\ No newline at end of file
+#endif /* STORM_MODELCHECKER_EXPLORATION_SPARSEEXPLORATIONMODELCHECKER_H_ */
\ No newline at end of file
diff --git a/src/settings/modules/ExplorationSettings.cpp b/src/settings/modules/ExplorationSettings.cpp
index 306d63aa8..688f4e6b6 100644
--- a/src/settings/modules/ExplorationSettings.cpp
+++ b/src/settings/modules/ExplorationSettings.cpp
@@ -15,6 +15,8 @@ namespace storm {
             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" };
@@ -24,6 +26,9 @@ namespace storm {
                 
                 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 {
@@ -74,6 +79,10 @@ namespace storm {
                 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() ||
diff --git a/src/settings/modules/ExplorationSettings.h b/src/settings/modules/ExplorationSettings.h
index 18126acfe..8f72785eb 100644
--- a/src/settings/modules/ExplorationSettings.h
+++ b/src/settings/modules/ExplorationSettings.h
@@ -74,6 +74,13 @@ namespace storm {
                  */
                 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.
@@ -85,6 +92,8 @@ namespace storm {
                 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
diff --git a/src/utility/storm.h b/src/utility/storm.h
index d5713a142..48020630a 100644
--- a/src/utility/storm.h
+++ b/src/utility/storm.h
@@ -57,7 +57,7 @@
 #include "src/modelchecker/prctl/SymbolicDtmcPrctlModelChecker.h"
 #include "src/modelchecker/prctl/SymbolicMdpPrctlModelChecker.h"
 #include "src/modelchecker/reachability/SparseDtmcEliminationModelChecker.h"
-#include "src/modelchecker/exploration/SparseMdpExplorationModelChecker.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"
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());
+}