diff --git a/src/storm/logic/Formula.h b/src/storm/logic/Formula.h
index 0c83e718c..29eba01ff 100644
--- a/src/storm/logic/Formula.h
+++ b/src/storm/logic/Formula.h
@@ -149,9 +149,6 @@ namespace storm {
             HOAPathFormula& asHOAPathFormula();
             HOAPathFormula const& asHOAPathFormula() const;
 
-            HOAPathFormula& asHOAPathFormula();
-            HOAPathFormula const& asHOAPathFormula() const;
-
             BoundedUntilFormula& asBoundedUntilFormula();
             BoundedUntilFormula const& asBoundedUntilFormula() const;
 
diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp
index b75dca240..2272ef61f 100644
--- a/src/storm/logic/FragmentSpecification.cpp
+++ b/src/storm/logic/FragmentSpecification.cpp
@@ -114,35 +114,6 @@ namespace storm {
             return rpatl;
         }
 
-        FragmentSpecification prctl() {
-            FragmentSpecification prctl = pctl();
-
-            prctl.setRewardOperatorsAllowed(true);
-            prctl.setCumulativeRewardFormulasAllowed(true);
-            prctl.setInstantaneousFormulasAllowed(true);
-            prctl.setReachabilityRewardFormulasAllowed(true);
-            prctl.setLongRunAverageOperatorsAllowed(true);
-            prctl.setStepBoundedCumulativeRewardFormulasAllowed(true);
-            prctl.setTimeBoundedCumulativeRewardFormulasAllowed(true);
-
-            return prctl;
-        }
-
-        FragmentSpecification prctlstar() {
-            FragmentSpecification prctlstar = pctlstar();
-
-            prctlstar.setRewardOperatorsAllowed(true);
-            prctlstar.setCumulativeRewardFormulasAllowed(true);
-            prctlstar.setInstantaneousFormulasAllowed(true);
-            prctlstar.setReachabilityRewardFormulasAllowed(true);
-            prctlstar.setLongRunAverageOperatorsAllowed(true);
-            prctlstar.setStepBoundedCumulativeRewardFormulasAllowed(true);
-            prctlstar.setTimeBoundedCumulativeRewardFormulasAllowed(true);
-
-            return prctlstar;
-
-        }
-
         FragmentSpecification csl() {
             FragmentSpecification csl = pctl();
 
diff --git a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
index 645564aa6..09791cf34 100644
--- a/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
+++ b/src/storm/modelchecker/prctl/SparseDtmcPrctlModelChecker.cpp
@@ -117,41 +117,14 @@ namespace storm {
         template<typename SparseDtmcModelType>
         std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeHOAPathProbabilities(Environment const& env, CheckTask<storm::logic::HOAPathFormula, ValueType> const& checkTask) {
             storm::logic::HOAPathFormula const& pathFormula = checkTask.getFormula();
-            
-            storm::modelchecker::helper::SparseLTLHelper<ValueType, false> helper(this->getModel().getTransitionMatrix());
-            storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel());
-            
-            auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); };
-            auto apSets = helper.computeApSets(pathFormula.getAPMapping(), formulaChecker);
-            std::vector<ValueType> numericResult = helper.computeDAProductProbabilities(env, *pathFormula.readAutomaton(), apSets);
-            
-            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
-        }
-
-        template<typename SparseDtmcModelType>
-        std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeLTLProbabilities(Environment const& env, CheckTask<storm::logic::PathFormula, ValueType> const& checkTask) {
-            storm::logic::PathFormula const& pathFormula = checkTask.getFormula();
 
             storm::modelchecker::helper::SparseLTLHelper<ValueType, false> helper(this->getModel().getTransitionMatrix());
             storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel());
-            
-            auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); };
-            std::vector<ValueType> numericResult = helper.computeLTLProbabilities(env, pathFormula, formulaChecker);
-
-            return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
-        }
 
-        template<typename SparseDtmcModelType>
-        std::unique_ptr<CheckResult> SparseDtmcPrctlModelChecker<SparseDtmcModelType>::computeHOAPathProbabilities(Environment const& env, CheckTask<storm::logic::HOAPathFormula, ValueType> const& checkTask) {
-            storm::logic::HOAPathFormula const& pathFormula = checkTask.getFormula();
-            
-            storm::modelchecker::helper::SparseLTLHelper<ValueType, false> helper(this->getModel().getTransitionMatrix());
-            storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel());
-            
             auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); };
             auto apSets = helper.computeApSets(pathFormula.getAPMapping(), formulaChecker);
             std::vector<ValueType> numericResult = helper.computeDAProductProbabilities(env, *pathFormula.readAutomaton(), apSets);
-            
+
             return std::unique_ptr<CheckResult>(new ExplicitQuantitativeCheckResult<ValueType>(std::move(numericResult)));
         }
 
@@ -161,7 +134,7 @@ namespace storm {
 
             storm::modelchecker::helper::SparseLTLHelper<ValueType, false> helper(this->getModel().getTransitionMatrix());
             storm::modelchecker::helper::setInformationFromCheckTaskDeterministic(helper, checkTask, this->getModel());
-            
+
             auto formulaChecker = [&] (storm::logic::Formula const& formula) { return this->check(env, formula)->asExplicitQualitativeCheckResult().getTruthValuesVector(); };
             std::vector<ValueType> numericResult = helper.computeLTLProbabilities(env, pathFormula, formulaChecker);