diff --git a/src/storm/logic/CloneVisitor.cpp b/src/storm/logic/CloneVisitor.cpp
index 57c8ce377..15499c9d9 100644
--- a/src/storm/logic/CloneVisitor.cpp
+++ b/src/storm/logic/CloneVisitor.cpp
@@ -176,5 +176,13 @@ namespace storm {
             return std::static_pointer_cast<Formula>(std::make_shared<UntilFormula>(left, right));
         }
 
+        boost::any CloneVisitor::visit(HOAPathFormula const& f, boost::any const& data) const {
+            std::shared_ptr<HOAPathFormula> result =  std::make_shared<HOAPathFormula>(f.getAutomatonFile());
+            for (auto& mapped : f.getAPMapping()) {
+                std::shared_ptr<Formula> clonedExpression = boost::any_cast<std::shared_ptr<Formula>>(mapped.second->accept(*this, data));
+                result->addAPMapping(mapped.first, clonedExpression);
+            }
+            return std::static_pointer_cast<Formula>(result);
+        }
     }
 }
diff --git a/src/storm/logic/CloneVisitor.h b/src/storm/logic/CloneVisitor.h
index 61578bdca..954d46db4 100644
--- a/src/storm/logic/CloneVisitor.h
+++ b/src/storm/logic/CloneVisitor.h
@@ -35,6 +35,7 @@ namespace storm {
             virtual boost::any visit(TotalRewardFormula 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;
+            virtual boost::any visit(HOAPathFormula const& f, boost::any const& data) const override;
         };
         
     }
diff --git a/src/storm/logic/Formula.cpp b/src/storm/logic/Formula.cpp
index b4e6c13bc..553e15b89 100644
--- a/src/storm/logic/Formula.cpp
+++ b/src/storm/logic/Formula.cpp
@@ -83,6 +83,10 @@ namespace storm {
             return false;
         }
 
+        bool Formula::isHOAPathFormula() const {
+            return false;
+        }
+
         bool Formula::isBinaryPathFormula() const {
             return false;
         }
@@ -289,6 +293,14 @@ namespace storm {
             return dynamic_cast<AtomicLabelFormula const&>(*this);
         }
 
+        HOAPathFormula& Formula::asHOAPathFormula() {
+            return dynamic_cast<HOAPathFormula&>(*this);
+        }
+
+        HOAPathFormula const& Formula::asHOAPathFormula() const {
+            return dynamic_cast<HOAPathFormula const&>(*this);
+        }
+
         UntilFormula& Formula::asUntilFormula() {
             return dynamic_cast<UntilFormula&>(*this);
         }
diff --git a/src/storm/logic/Formula.h b/src/storm/logic/Formula.h
index 62aab0dde..0014baef4 100644
--- a/src/storm/logic/Formula.h
+++ b/src/storm/logic/Formula.h
@@ -21,17 +21,17 @@ namespace storm {
 
         // Forward-declare fragment specification for isInFragment() method.
         class FragmentSpecification;
-        
+
         // Forward-declare formula information class for info() method.
         class FormulaInformation;
-        
+
         class Formula : public std::enable_shared_from_this<Formula> {
         public:
             // Make the destructor virtual to allow deletion of objects of subclasses via a pointer to this class.
             virtual ~Formula() {
                 // Intentionally left empty.
             };
-            
+
             friend std::ostream& operator<<(std::ostream& out, Formula const& formula);
 
             // Basic formula types.
@@ -39,14 +39,14 @@ namespace storm {
             virtual bool isStateFormula() const;
             virtual bool isConditionalProbabilityFormula() const;
             virtual bool isConditionalRewardFormula() const;
-            
+
             virtual bool isProbabilityPathFormula() const;
             virtual bool isRewardPathFormula() const;
             virtual bool isTimePathFormula() const;
 
             virtual bool isBinaryBooleanStateFormula() const;
             virtual bool isUnaryBooleanStateFormula() const;
-            
+
             virtual bool isMultiObjectiveFormula() const;
             virtual bool isQuantileFormula() const;
 
@@ -95,34 +95,34 @@ namespace storm {
             // Accessors for the return type of a formula.
             virtual bool hasQualitativeResult() const;
             virtual bool hasQuantitativeResult() const;
-            
+
             bool isInFragment(FragmentSpecification const& fragment) const;
             FormulaInformation info() const;
 
             virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data = boost::any()) const = 0;
-            
+
             static std::shared_ptr<Formula const> getTrueFormula();
 
             bool isInitialFormula() const;
-            
+
             PathFormula& asPathFormula();
             PathFormula const& asPathFormula() const;
-        
+
             StateFormula& asStateFormula();
             StateFormula const& asStateFormula() const;
-            
+
             MultiObjectiveFormula& asMultiObjectiveFormula();
             MultiObjectiveFormula const& asMultiObjectiveFormula() const;
-            
+
             QuantileFormula& asQuantileFormula();
             QuantileFormula const& asQuantileFormula() const;
-            
+
             BinaryStateFormula& asBinaryStateFormula();
             BinaryStateFormula const& asBinaryStateFormula() const;
-            
+
             UnaryStateFormula& asUnaryStateFormula();
             UnaryStateFormula const& asUnaryStateFormula() const;
-            
+
             BinaryBooleanStateFormula& asBinaryBooleanStateFormula();
             BinaryBooleanStateFormula const& asBinaryBooleanStateFormula() const;
 
@@ -131,25 +131,28 @@ namespace storm {
 
             BooleanLiteralFormula& asBooleanLiteralFormula();
             BooleanLiteralFormula const& asBooleanLiteralFormula() const;
-            
+
             AtomicExpressionFormula& asAtomicExpressionFormula();
             AtomicExpressionFormula const& asAtomicExpressionFormula() const;
-            
+
             AtomicLabelFormula& asAtomicLabelFormula();
             AtomicLabelFormula const& asAtomicLabelFormula() const;
-            
+
             UntilFormula& asUntilFormula();
             UntilFormula const& asUntilFormula() const;
-            
+
+            HOAPathFormula& asHOAPathFormula();
+            HOAPathFormula const& asHOAPathFormula() const;
+
             BoundedUntilFormula& asBoundedUntilFormula();
             BoundedUntilFormula const& asBoundedUntilFormula() const;
-            
+
             EventuallyFormula& asEventuallyFormula();
             EventuallyFormula const& asEventuallyFormula() const;
-            
+
             EventuallyFormula& asReachabilityProbabilityFormula();
             EventuallyFormula const& asReachabilityProbabilityFormula() const;
-            
+
             EventuallyFormula& asReachabilityRewardFormula();
             EventuallyFormula const& asReachabilityRewardFormula() const;
 
@@ -161,16 +164,16 @@ namespace storm {
 
             GloballyFormula& asGloballyFormula();
             GloballyFormula const& asGloballyFormula() const;
-            
+
             BinaryPathFormula& asBinaryPathFormula();
             BinaryPathFormula const& asBinaryPathFormula() const;
-            
+
             UnaryPathFormula& asUnaryPathFormula();
             UnaryPathFormula const& asUnaryPathFormula() const;
-            
+
             ConditionalFormula& asConditionalFormula();
             ConditionalFormula const& asConditionalFormula() const;
-            
+
             NextFormula& asNextFormula();
             NextFormula const& asNextFormula() const;
 
@@ -182,36 +185,36 @@ namespace storm {
 
             TimeOperatorFormula& asTimeOperatorFormula();
             TimeOperatorFormula const& asTimeOperatorFormula() const;
-            
+
             CumulativeRewardFormula& asCumulativeRewardFormula();
             CumulativeRewardFormula const& asCumulativeRewardFormula() const;
-            
+
             TotalRewardFormula& asTotalRewardFormula();
             TotalRewardFormula const& asTotalRewardFormula() const;
-            
+
             InstantaneousRewardFormula& asInstantaneousRewardFormula();
             InstantaneousRewardFormula const& asInstantaneousRewardFormula() const;
-            
+
             LongRunAverageRewardFormula& asLongRunAverageRewardFormula();
             LongRunAverageRewardFormula const& asLongRunAverageRewardFormula() const;
-            
+
             ProbabilityOperatorFormula& asProbabilityOperatorFormula();
             ProbabilityOperatorFormula const& asProbabilityOperatorFormula() const;
-            
+
             RewardOperatorFormula& asRewardOperatorFormula();
             RewardOperatorFormula const& asRewardOperatorFormula() const;
-            
+
             OperatorFormula& asOperatorFormula();
             OperatorFormula const& asOperatorFormula() const;
-            
+
             std::vector<std::shared_ptr<AtomicExpressionFormula const>> getAtomicExpressionFormulas() const;
             std::vector<std::shared_ptr<AtomicLabelFormula const>> getAtomicLabelFormulas() const;
             std::set<storm::expressions::Variable> getUsedVariables() const;
             std::set<std::string> getReferencedRewardModels() const;
-            
+
             std::shared_ptr<Formula const> asSharedPointer();
             std::shared_ptr<Formula const> asSharedPointer() const;
-            
+
             std::shared_ptr<Formula> substitute(std::map<storm::expressions::Variable, storm::expressions::Expression> const& substitution) const;
             std::shared_ptr<Formula> substitute(std::function<storm::expressions::Expression(storm::expressions::Expression const&)> const& expressionSubstitution) const;
             std::shared_ptr<Formula> substitute(std::map<std::string, storm::expressions::Expression> const& labelSubstitution) const;
@@ -228,10 +231,10 @@ namespace storm {
              * @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;
-            
+
             virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const;
             virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const;
             virtual void gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const;
@@ -240,7 +243,7 @@ namespace storm {
         private:
             // Currently empty.
         };
-        
+
         std::ostream& operator<<(std::ostream& out, Formula const& formula);
     }
 }
diff --git a/src/storm/logic/FormulaInformationVisitor.cpp b/src/storm/logic/FormulaInformationVisitor.cpp
index 41417eeed..471503e2a 100644
--- a/src/storm/logic/FormulaInformationVisitor.cpp
+++ b/src/storm/logic/FormulaInformationVisitor.cpp
@@ -134,5 +134,13 @@ namespace storm {
             return boost::any_cast<FormulaInformation>(f.getLeftSubformula().accept(*this, data)).join(boost::any_cast<FormulaInformation>(f.getRightSubformula().accept(*this)));
         }
 
+        boost::any FormulaInformationVisitor::visit(HOAPathFormula const& f, boost::any const& data) const {
+            FormulaInformation info;
+            for (auto& mapped : f.getAPMapping()) {
+                info = info.join(boost::any_cast<FormulaInformation>(mapped.second->accept(*this, data)));
+            }
+            return info;
+        }
+
     }
 }
diff --git a/src/storm/logic/FormulaInformationVisitor.h b/src/storm/logic/FormulaInformationVisitor.h
index ecf5a1ab7..a1f3a3fb0 100644
--- a/src/storm/logic/FormulaInformationVisitor.h
+++ b/src/storm/logic/FormulaInformationVisitor.h
@@ -34,6 +34,7 @@ namespace storm {
             virtual boost::any visit(TotalRewardFormula 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;
+            virtual boost::any visit(HOAPathFormula const& f, boost::any const& data) const override;
         };
         
     }
diff --git a/src/storm/logic/FormulaVisitor.h b/src/storm/logic/FormulaVisitor.h
index 23673ff50..b1c6db105 100644
--- a/src/storm/logic/FormulaVisitor.h
+++ b/src/storm/logic/FormulaVisitor.h
@@ -35,6 +35,7 @@ namespace storm {
             virtual boost::any visit(TotalRewardFormula const& f, boost::any const& data) const = 0;
             virtual boost::any visit(UnaryBooleanStateFormula const& f, boost::any const& data) const = 0;
             virtual boost::any visit(UntilFormula const& f, boost::any const& data) const = 0;
+            virtual boost::any visit(HOAPathFormula const& f, boost::any const& data) const = 0;
         };
         
     }
diff --git a/src/storm/logic/Formulas.h b/src/storm/logic/Formulas.h
index cc59b93b6..47ceae22a 100644
--- a/src/storm/logic/Formulas.h
+++ b/src/storm/logic/Formulas.h
@@ -28,6 +28,7 @@
 #include "storm/logic/UnaryPathFormula.h"
 #include "storm/logic/UnaryStateFormula.h"
 #include "storm/logic/UntilFormula.h"
+#include "storm/logic/HOAPathFormula.h"
 #include "storm/logic/ConditionalFormula.h"
 #include "storm/logic/ProbabilityOperatorFormula.h"
 #include "storm/logic/RewardOperatorFormula.h"
diff --git a/src/storm/logic/FormulasForwardDeclarations.h b/src/storm/logic/FormulasForwardDeclarations.h
index 1a6611f13..41aca3c3b 100644
--- a/src/storm/logic/FormulasForwardDeclarations.h
+++ b/src/storm/logic/FormulasForwardDeclarations.h
@@ -36,6 +36,7 @@ namespace storm {
         class UnaryPathFormula;
         class UnaryStateFormula;
         class UntilFormula;
+        class HOAPathFormula;
     }
 }
 
diff --git a/src/storm/logic/FragmentChecker.cpp b/src/storm/logic/FragmentChecker.cpp
index df79d22a5..0c76dec44 100644
--- a/src/storm/logic/FragmentChecker.cpp
+++ b/src/storm/logic/FragmentChecker.cpp
@@ -322,5 +322,15 @@ namespace storm {
             result = result && boost::any_cast<bool>(f.getRightSubformula().accept(*this, data));
             return result;
         }
+
+        boost::any FragmentChecker::visit(HOAPathFormula const& f, boost::any const& data) const {
+            InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
+            bool result = inherited.getSpecification().areHOAPathFormulasAllowed();
+            // TODO: check
+            for (auto& mapped : f.getAPMapping()) {
+                result = result && boost::any_cast<bool>(mapped.second->accept(*this, data));
+            }
+            return result;
+        }
     }
 }
diff --git a/src/storm/logic/FragmentChecker.h b/src/storm/logic/FragmentChecker.h
index 0b0d179aa..e027f7c46 100644
--- a/src/storm/logic/FragmentChecker.h
+++ b/src/storm/logic/FragmentChecker.h
@@ -35,6 +35,7 @@ namespace storm {
             virtual boost::any visit(TotalRewardFormula 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;
+            virtual boost::any visit(HOAPathFormula const& f, boost::any const& data) const override;
         };
         
     }
diff --git a/src/storm/logic/FragmentSpecification.cpp b/src/storm/logic/FragmentSpecification.cpp
index dc93f7f9c..445ae0b8c 100644
--- a/src/storm/logic/FragmentSpecification.cpp
+++ b/src/storm/logic/FragmentSpecification.cpp
@@ -168,6 +168,7 @@ namespace storm {
             nextFormula = false;
             untilFormula = false;
             boundedUntilFormula = false;
+            hoaPathFormula = false;
 
             atomicExpressionFormula = false;
             atomicLabelFormula = false;
@@ -326,6 +327,15 @@ namespace storm {
             return *this;
         }
 
+        bool FragmentSpecification::areHOAPathFormulasAllowed() const {
+            return hoaPathFormula;
+        }
+
+        FragmentSpecification& FragmentSpecification::setHOAPathFormulasAllowed(bool newValue) {
+            this->hoaPathFormula = newValue;
+            return *this;
+        }
+
         bool FragmentSpecification::areAtomicExpressionFormulasAllowed() const {
             return atomicExpressionFormula;
         }
diff --git a/src/storm/logic/FragmentSpecification.h b/src/storm/logic/FragmentSpecification.h
index f097e940f..5f656695e 100644
--- a/src/storm/logic/FragmentSpecification.h
+++ b/src/storm/logic/FragmentSpecification.h
@@ -55,6 +55,9 @@ namespace storm {
             bool areBoundedGloballyFormulasAllowed() const;
             FragmentSpecification& setBoundedGloballyFormulasAllowed(bool newValue);
 
+            bool areHOAPathFormulasAllowed() const;
+            FragmentSpecification& setHOAPathFormulasAllowed(bool newValue);
+
             bool areAtomicExpressionFormulasAllowed() const;
             FragmentSpecification& setAtomicExpressionFormulasAllowed(bool newValue);
 
@@ -180,6 +183,7 @@ namespace storm {
             bool untilFormula;
             bool boundedUntilFormula;
             bool boundedGloballyFormula;
+            bool hoaPathFormula;
 
             bool atomicExpressionFormula;
             bool atomicLabelFormula;
diff --git a/src/storm/logic/HOAPathFormula.cpp b/src/storm/logic/HOAPathFormula.cpp
new file mode 100644
index 000000000..915f4f13d
--- /dev/null
+++ b/src/storm/logic/HOAPathFormula.cpp
@@ -0,0 +1,90 @@
+#include "storm/logic/HOAPathFormula.h"
+#include "storm/logic/FormulaVisitor.h"
+
+#include "storm/utility/macros.h"
+#include "storm/automata/DeterministicAutomaton.h"
+#include "storm/exceptions/ExpressionEvaluationException.h"
+#include "storm/exceptions/IllegalArgumentException.h"
+#include "storm/exceptions/InvalidPropertyException.h"
+#include "storm/exceptions/FileIoException.h"
+
+namespace storm {
+    namespace logic {
+        HOAPathFormula::HOAPathFormula(const std::string& automatonFile, FormulaContext context) : automatonFile(automatonFile), context(context) {
+            STORM_LOG_THROW(context == FormulaContext::Probability, storm::exceptions::InvalidPropertyException, "Invalid context for formula.");
+        }
+
+        FormulaContext const& HOAPathFormula::getContext() const {
+            return context;
+        }
+
+        const std::string& HOAPathFormula::getAutomatonFile() const {
+            return automatonFile;
+        }
+
+        const HOAPathFormula::ap_to_formula_map &HOAPathFormula::getAPMapping() const {
+            return apToFormulaMap;
+        }
+
+        void HOAPathFormula::addAPMapping(const std::string& ap, const std::shared_ptr<Formula const>& formula) {
+            STORM_LOG_THROW(apToFormulaMap.find(ap) == apToFormulaMap.end(), storm::exceptions::IllegalArgumentException, "HOA path formula: Mapping for atomic proposition \"" + ap + "\" already exists.");
+            apToFormulaMap[ap] = formula;
+        }
+
+        bool HOAPathFormula::isProbabilityPathFormula() const {
+            return true;
+        }
+
+        bool HOAPathFormula::isHOAPathFormula() const {
+            return true;
+        }
+
+        bool HOAPathFormula::hasQuantitativeResult() const {
+            return true;
+        }
+
+        boost::any HOAPathFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
+            return visitor.visit(*this, data);
+        }
+
+        void HOAPathFormula::gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const {
+            for (auto& mapped : getAPMapping()) {
+                mapped.second->gatherAtomicExpressionFormulas(atomicExpressionFormulas);
+            }
+        }
+
+        void HOAPathFormula::gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const {
+            for (auto& mapped : getAPMapping()) {
+                mapped.second->gatherAtomicLabelFormulas(atomicLabelFormulas);
+            }
+        }
+
+        void HOAPathFormula::gatherReferencedRewardModels(std::set<std::string>& referencedRewardModels) const {
+            for (auto& mapped : getAPMapping()) {
+                mapped.second->gatherReferencedRewardModels(referencedRewardModels);
+            }
+        }
+
+        storm::automata::DeterministicAutomaton::ptr HOAPathFormula::readAutomaton() const {
+            std::ifstream in(automatonFile);
+            STORM_LOG_THROW(in.good(), storm::exceptions::FileIoException, "Can not open '" << automatonFile << "' for reading.");
+            storm::automata::DeterministicAutomaton::ptr automaton = storm::automata::DeterministicAutomaton::parse(in);
+            for (auto& ap : automaton->getAPSet().getAPs()) {
+                STORM_LOG_THROW(apToFormulaMap.find(ap) != apToFormulaMap.end(), storm::exceptions::ExpressionEvaluationException, "For '" << automatonFile << "' HOA automaton, expression for atomic proposition '" << ap << "' is missing.");
+            }
+            return automaton;
+        }
+
+
+        std::ostream& HOAPathFormula::writeToStream(std::ostream& out) const {
+            out << "HOA: { ";
+            out << "\"" <<  automatonFile << "\"";
+            for (auto& mapping : apToFormulaMap) {
+                out << ", \"" << mapping.first << "\" -> ";
+                mapping.second->writeToStream(out);
+            }
+            out << " }";
+            return out;
+        }
+    }
+}
diff --git a/src/storm/logic/HOAPathFormula.h b/src/storm/logic/HOAPathFormula.h
new file mode 100644
index 000000000..81352243e
--- /dev/null
+++ b/src/storm/logic/HOAPathFormula.h
@@ -0,0 +1,54 @@
+#pragma once
+
+#include "storm/logic/PathFormula.h"
+#include "storm/logic/FormulaContext.h"
+
+#include <map>
+#include <memory>
+
+namespace storm {
+    namespace automata {
+      // fwd
+      class DeterministicAutomaton;
+    }
+
+    namespace logic {
+        class HOAPathFormula  : public PathFormula {
+        public:
+            typedef std::map<std::string, std::shared_ptr<Formula const>> ap_to_formula_map;
+
+            HOAPathFormula(const std::string& automatonFile, FormulaContext context = FormulaContext::Probability);
+
+            virtual ~HOAPathFormula() {
+                // Intentionally left empty.
+            }
+
+            FormulaContext const& getContext() const;
+            const std::string& getAutomatonFile() const;
+            const ap_to_formula_map &getAPMapping() const;
+
+            void addAPMapping(const std::string& ap, const std::shared_ptr<Formula const>& formula);
+
+            virtual bool isHOAPathFormula() const override;
+            virtual bool isProbabilityPathFormula() const override;
+            virtual bool hasQuantitativeResult() const override;
+
+            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) 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;
+
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
+
+	    std::shared_ptr<storm::automata::DeterministicAutomaton> readAutomaton() const;
+
+        private:
+            std::string automatonFile;
+            ap_to_formula_map apToFormulaMap;
+
+            FormulaContext context;
+        };
+    }
+}
+
diff --git a/src/storm/logic/LiftableTransitionRewardsVisitor.cpp b/src/storm/logic/LiftableTransitionRewardsVisitor.cpp
index a61dccf7c..5a0219242 100644
--- a/src/storm/logic/LiftableTransitionRewardsVisitor.cpp
+++ b/src/storm/logic/LiftableTransitionRewardsVisitor.cpp
@@ -147,6 +147,15 @@ namespace storm {
             return boost::any_cast<bool>(f.getLeftSubformula().accept(*this, data)) && boost::any_cast<bool>(f.getRightSubformula().accept(*this));
         }
 
+        boost::any LiftableTransitionRewardsVisitor::visit(HOAPathFormula const& f, boost::any const& data) const {
+            for (auto const& ap : f.getAPMapping()) {
+                if (!boost::any_cast<bool>(ap.second->accept(*this, data))) {
+                    return false;
+                }
+            }
+            return true;
+        }
+
         bool LiftableTransitionRewardsVisitor::rewardModelHasTransitionRewards(std::string const& rewardModelName) const {
             if (symbolicModelDescription.hasModel()) {
                 if (symbolicModelDescription.isJaniModel()) {
diff --git a/src/storm/logic/LiftableTransitionRewardsVisitor.h b/src/storm/logic/LiftableTransitionRewardsVisitor.h
index 52a791237..db5530cad 100644
--- a/src/storm/logic/LiftableTransitionRewardsVisitor.h
+++ b/src/storm/logic/LiftableTransitionRewardsVisitor.h
@@ -41,6 +41,7 @@ namespace storm {
             virtual boost::any visit(TotalRewardFormula 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;
+	    virtual boost::any visit(HOAPathFormula const& f, boost::any const& data) const override;
         
         private:
             storm::storage::SymbolicModelDescription const& symbolicModelDescription;
diff --git a/src/storm/logic/ToExpressionVisitor.cpp b/src/storm/logic/ToExpressionVisitor.cpp
index 1e6852d84..41688ad8e 100644
--- a/src/storm/logic/ToExpressionVisitor.cpp
+++ b/src/storm/logic/ToExpressionVisitor.cpp
@@ -129,5 +129,8 @@ namespace storm {
             STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
         }
         
+        boost::any ToExpressionVisitor::visit(HOAPathFormula const&, boost::any const&) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Cannot assemble expression from formula that contains illegal elements.");
+        }
     }
 }
diff --git a/src/storm/logic/ToExpressionVisitor.h b/src/storm/logic/ToExpressionVisitor.h
index b68b5c438..eb7e261f2 100644
--- a/src/storm/logic/ToExpressionVisitor.h
+++ b/src/storm/logic/ToExpressionVisitor.h
@@ -35,6 +35,7 @@ namespace storm {
             virtual boost::any visit(TotalRewardFormula 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;
+            virtual boost::any visit(HOAPathFormula const& f, boost::any const& data) const override;
         };
         
     }
diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp
index 2e900bb92..f89e1cab5 100644
--- a/src/storm/storage/jani/JSONExporter.cpp
+++ b/src/storm/storage/jani/JSONExporter.cpp
@@ -596,6 +596,10 @@ namespace storm {
             return opDecl;
         }
 
+        boost::any FormulaToJaniJson::visit(storm::logic::HOAPathFormula const&, boost::any const&) const {
+            STORM_LOG_THROW(false, storm::exceptions::NotSupportedException, "Jani currently does not support HOA path formulae");
+        }
+
         std::string operatorTypeToJaniString(storm::expressions::OperatorType optype) {
 
             using OpType = storm::expressions::OperatorType;
diff --git a/src/storm/storage/jani/JSONExporter.h b/src/storm/storage/jani/JSONExporter.h
index cee374f02..c14524f69 100644
--- a/src/storm/storage/jani/JSONExporter.h
+++ b/src/storm/storage/jani/JSONExporter.h
@@ -72,6 +72,7 @@ namespace storm {
             virtual boost::any visit(storm::logic::TotalRewardFormula const& f, boost::any const& data) const;
             virtual boost::any visit(storm::logic::UnaryBooleanStateFormula const& f, boost::any const& data) const;
             virtual boost::any visit(storm::logic::UntilFormula const& f, boost::any const& data) const;
+            virtual boost::any visit(storm::logic::HOAPathFormula const& f, boost::any const& data) const;
       
         private:
             FormulaToJaniJson(storm::jani::Model const& model) : model(model), stateExitRewards(false) { }