diff --git a/src/storm-parsers/parser/FormulaParserGrammar.cpp b/src/storm-parsers/parser/FormulaParserGrammar.cpp
index 95a27d70c..d768fab9b 100644
--- a/src/storm-parsers/parser/FormulaParserGrammar.cpp
+++ b/src/storm-parsers/parser/FormulaParserGrammar.cpp
@@ -52,13 +52,13 @@ namespace storm {
             operatorFormula = probabilityOperator | rewardOperator | longRunAverageOperator | timeOperator;
             operatorFormula.name("operator formulas");
 
-            atomicStateFormula = booleanLiteralFormula | labelFormula | expressionFormula | (qi::lit("(") > stateFormula > qi::lit(")")) | operatorFormula;
+            atomicStateFormula = booleanLiteralFormula | labelFormula | expressionFormula | (qi::lit("(") > untilFormula(qi::_r1) > qi::lit(")")) | operatorFormula;
             atomicStateFormula.name("atomic state formula");
 
-            atomicStateFormulaWithoutExpression = booleanLiteralFormula | labelFormula | (qi::lit("(") > stateFormula > qi::lit(")")) | operatorFormula;
+            atomicStateFormulaWithoutExpression = booleanLiteralFormula | labelFormula | (qi::lit("(") > untilFormula(qi::_r1) > qi::lit(")")) | operatorFormula;
             atomicStateFormula.name("atomic state formula without expression");
 
-            notStateFormula = (unaryBooleanOperator_ >> atomicStateFormulaWithoutExpression)[qi::_val = phoenix::bind(&FormulaParserGrammar::createUnaryBooleanStateFormula, phoenix::ref(*this), qi::_2, qi::_1)] | atomicStateFormula[qi::_val = qi::_1];
+            notStateFormula = (unaryBooleanOperator_ >> atomicStateFormulaWithoutExpression(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createUnaryBooleanStateOrPathFormula, phoenix::ref(*this), qi::_2, qi::_1)] | atomicStateFormula(qi::_r1)[qi::_val = qi::_1];
             notStateFormula.name("negation formula");
 
             eventuallyFormula = (qi::lit("F") >> (-timeBounds) >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createEventuallyFormula, phoenix::ref(*this), qi::_1, qi::_r1, qi::_2)];
@@ -70,7 +70,7 @@ namespace storm {
             nextFormula = (qi::lit("X") >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createNextFormula, phoenix::ref(*this), qi::_1)];
             nextFormula.name("next formula");
 
-            pathFormulaWithoutUntil = eventuallyFormula(qi::_r1) | globallyFormula(qi::_r1) | nextFormula(qi::_r1) | stateFormula;
+            pathFormulaWithoutUntil = eventuallyFormula(qi::_r1) | globallyFormula(qi::_r1) | nextFormula(qi::_r1) | stateFormula(qi::_r1);
             pathFormulaWithoutUntil.name("path formula");
 
             untilFormula = pathFormulaWithoutUntil(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("U") >> (-timeBounds) >> pathFormulaWithoutUntil(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createUntilFormula, phoenix::ref(*this), qi::_val, qi::_1, qi::_2)];
@@ -78,7 +78,7 @@ namespace storm {
 
             hoaPathFormula = qi::lit("HOA:") > qi::lit("{")
                 > quotedString[qi::_val = phoenix::bind(&FormulaParserGrammar::createHOAPathFormula, phoenix::ref(*this), qi::_1)]
-                >> *(qi::lit(",") > quotedString > qi::lit("->") > stateFormula )[phoenix::bind(&FormulaParserGrammar::addHoaAPMapping, phoenix::ref(*this), *qi::_val, qi::_1, qi::_2)]
+                >> *(qi::lit(",") > quotedString > qi::lit("->") > stateFormula(qi::_r1) )[phoenix::bind(&FormulaParserGrammar::addHoaAPMapping, phoenix::ref(*this), *qi::_val, qi::_1, qi::_2)]
                 > qi::lit("}");
 
             basicPathFormula = (hoaPathFormula(qi::_r1)[qi::_val = qi::_1]) | untilFormula(qi::_r1)[qi::_val = qi::_1];
@@ -112,7 +112,7 @@ namespace storm {
             operatorInformation = (-optimalityOperator_[qi::_a = qi::_1] >> ((relationalOperator_[qi::_b = qi::_1] > expressionParser[qi::_c = qi::_1]) | (qi::lit("=") > qi::lit("?"))))[qi::_val = phoenix::bind(&FormulaParserGrammar::createOperatorInformation, phoenix::ref(*this), qi::_a, qi::_b, qi::_c)];
             operatorInformation.name("operator information");
 
-            longRunAverageOperator = ((qi::lit("LRA") | qi::lit("S")) > operatorInformation > qi::lit("[") > stateFormula > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createLongRunAverageOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
+            longRunAverageOperator = ((qi::lit("LRA") | qi::lit("S")) > operatorInformation > qi::lit("[") > stateFormula(storm::logic::FormulaContext::LongRunAverage) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createLongRunAverageOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
             longRunAverageOperator.name("long-run average operator");
 
             rewardModelName = qi::lit("{\"") > label > qi::lit("\"}");
@@ -127,13 +127,13 @@ namespace storm {
             probabilityOperator = (qi::lit("P") > operatorInformation > qi::lit("[") > pathFormula(storm::logic::FormulaContext::Probability) > qi::lit("]"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProbabilityOperatorFormula, phoenix::ref(*this), qi::_1, qi::_2)];
             probabilityOperator.name("probability operator");
 
-            andStateFormula = notStateFormula[qi::_val = qi::_1] >> *(qi::lit("&") >> notStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::And)];
+            andStateFormula = notStateFormula(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("&") >> notStateFormula(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateOrPathFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::And)];
             andStateFormula.name("and state formula");
 
-            orStateFormula = andStateFormula[qi::_val = qi::_1] >> *(qi::lit("|") >> andStateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::Or)];
+            orStateFormula = andStateFormula(qi::_r1)[qi::_val = qi::_1] >> *(qi::lit("|") >> andStateFormula(qi::_r1))[qi::_val = phoenix::bind(&FormulaParserGrammar::createBinaryBooleanStateOrPathFormula, phoenix::ref(*this), qi::_val, qi::_1, storm::logic::BinaryBooleanStateFormula::OperatorType::Or)];
             orStateFormula.name("or state formula");
 
-            multiFormula = (qi::lit("multi") > qi::lit("(") >> ((pathFormula(storm::logic::FormulaContext::Probability) | stateFormula) % qi::lit(",")) >> qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createMultiFormula, phoenix::ref(*this), qi::_1)];
+            multiFormula = (qi::lit("multi") > qi::lit("(") >> ((pathFormula(storm::logic::FormulaContext::Probability) | stateFormula(storm::logic::FormulaContext::Probability)) % qi::lit(",")) >> qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createMultiFormula, phoenix::ref(*this), qi::_1)];
             multiFormula.name("Multi formula");
 
             identifier %= qi::as_string[qi::raw[qi::lexeme[((qi::alpha | qi::char_('_') | qi::char_('.')) >> *(qi::alnum | qi::char_('_')))]]];
@@ -141,7 +141,7 @@ namespace storm {
 
             quantileBoundVariable = (-(qi::lit("min")[qi::_a = storm::solver::OptimizationDirection::Minimize] | qi::lit("max")[qi::_a = storm::solver::OptimizationDirection::Maximize]) >> identifier >> qi::lit(","))[qi::_val = phoenix::bind(&FormulaParserGrammar::createQuantileBoundVariables, phoenix::ref(*this), qi::_a,  qi::_1)];
             quantileBoundVariable.name("quantile bound variable");
-            quantileFormula = (qi::lit("quantile") > qi::lit("(") >> *(quantileBoundVariable) >> stateFormula > qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createQuantileFormula, phoenix::ref(*this), qi::_1, qi::_2)];
+            quantileFormula = (qi::lit("quantile") > qi::lit("(") >> *(quantileBoundVariable) >> stateFormula(storm::logic::FormulaContext::Undefined) > qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createQuantileFormula, phoenix::ref(*this), qi::_1, qi::_2)];
             quantileFormula.name("Quantile formula");
 
             playerCoalition = (-((identifier[phoenix::push_back(qi::_a, qi::_1)] | qi::uint_[phoenix::push_back(qi::_a, qi::_1)]) % ','))[qi::_val = phoenix::bind(&FormulaParserGrammar::createPlayerCoalition, phoenix::ref(*this), qi::_a)];
@@ -166,7 +166,7 @@ namespace storm {
                                  qi::lit("gamma")[qi::_a = storm::logic::ShieldComparison::Absolute]) > qi::lit("=") > probability)[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldComparisonStruct, phoenix::ref(*this), qi::_a, qi::_1)];
             shieldComparison.name("shield comparison type");
 
-            stateFormula = (orStateFormula | multiFormula | quantileFormula | gameFormula);
+            stateFormula = (orStateFormula(qi::_r1) | multiFormula | quantileFormula);
             stateFormula.name("state formula");
 
             quotedString %= qi::as_string[qi::lexeme[qi::omit[qi::char_('"')] > qi::raw[*(!qi::char_('"') >> qi::char_)] > qi::omit[qi::lit('"')]]];
@@ -183,7 +183,7 @@ namespace storm {
 #pragma clang diagnostic push
 #pragma clang diagnostic ignored "-Woverloaded-shift-op-parentheses"
 
-            filterProperty = (-formulaName >> qi::lit("filter") > qi::lit("(") > filterType_ > qi::lit(",") > stateFormula > qi::lit(",") > stateFormula > qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProperty, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)] | (-formulaName >> stateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates, phoenix::ref(*this), qi::_1, qi::_2)] | (-formulaName >> shieldExpression >> stateFormula)[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldingProperty, phoenix::ref(*this), qi::_1, qi::_3, qi::_2)];
+            filterProperty = (-formulaName >> qi::lit("filter") > qi::lit("(") > filterType_ > qi::lit(",") > stateFormula(storm::logic::FormulaContext::Undefined) > qi::lit(",") > stateFormula(storm::logic::FormulaContext::Undefined) > qi::lit(")"))[qi::_val = phoenix::bind(&FormulaParserGrammar::createProperty, phoenix::ref(*this), qi::_1, qi::_2, qi::_3, qi::_4)] | (-formulaName >> stateFormula(storm::logic::FormulaContext::Undefined))[qi::_val = phoenix::bind(&FormulaParserGrammar::createPropertyWithDefaultFilterTypeAndStates, phoenix::ref(*this), qi::_1, qi::_2)] | (-formulaName >> shieldExpression >> stateFormula(storm::logic::FormulaContext::Undefined))[qi::_val = phoenix::bind(&FormulaParserGrammar::createShieldingProperty, phoenix::ref(*this), qi::_1, qi::_3, qi::_2)];
             filterProperty.name("filter property");
 
 #pragma clang diagnostic pop
@@ -452,6 +452,34 @@ namespace storm {
             }
         }
 
+        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createBinaryBooleanPathFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, std::shared_ptr<storm::logic::Formula const> const& rightSubformula, storm::logic::BinaryBooleanPathFormula::OperatorType operatorType) {
+            return std::shared_ptr<storm::logic::Formula const>(new storm::logic::BinaryBooleanPathFormula(operatorType, leftSubformula, rightSubformula));
+        }
+
+        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createUnaryBooleanPathFormula(std::shared_ptr<storm::logic::Formula const> const& subformula, boost::optional<storm::logic::UnaryBooleanPathFormula::OperatorType> const& operatorType) {
+            if (operatorType) {
+                return std::shared_ptr<storm::logic::Formula const>(new storm::logic::UnaryBooleanPathFormula(operatorType.get(), subformula));
+            } else {
+                return subformula;
+            }
+        }
+
+        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createBinaryBooleanStateOrPathFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, std::shared_ptr<storm::logic::Formula const> const& rightSubformula, storm::logic::BinaryBooleanOperatorType operatorType) {
+            if (leftSubformula->isStateFormula() && rightSubformula->isStateFormula()) {
+                return createBinaryBooleanStateFormula(leftSubformula, rightSubformula, operatorType);
+            } else {
+                return createBinaryBooleanPathFormula(leftSubformula, rightSubformula, operatorType);
+            }
+        }
+
+        std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createUnaryBooleanStateOrPathFormula(std::shared_ptr<storm::logic::Formula const> const& subformula, boost::optional<storm::logic::UnaryBooleanOperatorType> const& operatorType) {
+            if (subformula->isStateFormula()) {
+                return createUnaryBooleanStateFormula(subformula, operatorType);
+            } else {
+                return createUnaryBooleanPathFormula(subformula, operatorType);
+            }
+        }
+
         std::shared_ptr<storm::logic::Formula const> FormulaParserGrammar::createMultiFormula(std::vector<std::shared_ptr<storm::logic::Formula const>> const& subformulas) {
             bool isMultiDimensionalBoundedUntilFormula = !subformulas.empty();
             for (auto const& subformula : subformulas) {
diff --git a/src/storm-parsers/parser/FormulaParserGrammar.h b/src/storm-parsers/parser/FormulaParserGrammar.h
index c40842532..2bba99c73 100644
--- a/src/storm-parsers/parser/FormulaParserGrammar.h
+++ b/src/storm-parsers/parser/FormulaParserGrammar.h
@@ -165,19 +165,19 @@ namespace storm {
 
             qi::rule<Iterator, storm::jani::Property(), Skipper> filterProperty;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> simpleFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> stateFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> stateFormula;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> pathFormula;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> pathFormulaWithoutUntil;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> simplePathFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> atomicStateFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> atomicStateFormulaWithoutExpression;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> atomicStateFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> atomicStateFormulaWithoutExpression;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> operatorFormula;
             qi::rule<Iterator, std::string(), Skipper> label;
             qi::rule<Iterator, std::string(), Skipper> rewardModelName;
 
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> andStateFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> orStateFormula;
-            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> notStateFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> andStateFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> orStateFormula;
+            qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(storm::logic::FormulaContext), Skipper> notStateFormula;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> labelFormula;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), Skipper> expressionFormula;
             qi::rule<Iterator, std::shared_ptr<storm::logic::Formula const>(), qi::locals<bool>, Skipper> booleanLiteralFormula;
@@ -250,7 +250,11 @@ namespace storm {
             std::shared_ptr<storm::logic::Formula const> createTimeOperatorFormula(boost::optional<storm::logic::RewardMeasureType> const& rewardMeasureType, storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula const> const& subformula) const;
             std::shared_ptr<storm::logic::Formula const> createProbabilityOperatorFormula(storm::logic::OperatorInformation const& operatorInformation, std::shared_ptr<storm::logic::Formula const> const& subformula);
             std::shared_ptr<storm::logic::Formula const> createBinaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, std::shared_ptr<storm::logic::Formula const> const& rightSubformula, storm::logic::BinaryBooleanStateFormula::OperatorType operatorType);
+            std::shared_ptr<storm::logic::Formula const> createBinaryBooleanPathFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, std::shared_ptr<storm::logic::Formula const> const& rightSubformula, storm::logic::BinaryBooleanPathFormula::OperatorType operatorType);
+            std::shared_ptr<storm::logic::Formula const> createBinaryBooleanStateOrPathFormula(std::shared_ptr<storm::logic::Formula const> const& leftSubformula, std::shared_ptr<storm::logic::Formula const> const& rightSubformula, storm::logic::BinaryBooleanOperatorType operatorType);
             std::shared_ptr<storm::logic::Formula const> createUnaryBooleanStateFormula(std::shared_ptr<storm::logic::Formula const> const& subformula, boost::optional<storm::logic::UnaryBooleanStateFormula::OperatorType> const& operatorType);
+            std::shared_ptr<storm::logic::Formula const> createUnaryBooleanPathFormula(std::shared_ptr<storm::logic::Formula const> const& subformula, boost::optional<storm::logic::UnaryBooleanPathFormula::OperatorType> const& operatorType);
+            std::shared_ptr<storm::logic::Formula const> createUnaryBooleanStateOrPathFormula(std::shared_ptr<storm::logic::Formula const> const& subformula, boost::optional<storm::logic::UnaryBooleanOperatorType> const& operatorType);
             std::shared_ptr<storm::logic::Formula const> createMultiFormula(std::vector<std::shared_ptr<storm::logic::Formula const>> const& subformulas);
             storm::expressions::Variable createQuantileBoundVariables(boost::optional<storm::solver::OptimizationDirection> const& dir, std::string const& variableName);
             std::shared_ptr<storm::logic::Formula const> createQuantileFormula(std::vector<storm::expressions::Variable> const& boundVariables, std::shared_ptr<storm::logic::Formula const> const& subformula);
diff --git a/src/storm/logic/BinaryBooleanOperatorType.h b/src/storm/logic/BinaryBooleanOperatorType.h
new file mode 100644
index 000000000..8c4c141a4
--- /dev/null
+++ b/src/storm/logic/BinaryBooleanOperatorType.h
@@ -0,0 +1,7 @@
+#pragma once
+
+namespace storm {
+    namespace logic {
+        enum class BinaryBooleanOperatorType {And, Or};
+    }
+}
diff --git a/src/storm/logic/BinaryBooleanPathFormula.cpp b/src/storm/logic/BinaryBooleanPathFormula.cpp
new file mode 100644
index 000000000..aa84f23f7
--- /dev/null
+++ b/src/storm/logic/BinaryBooleanPathFormula.cpp
@@ -0,0 +1,47 @@
+#include "storm/logic/BinaryBooleanPathFormula.h"
+
+#include "storm/logic/FormulaVisitor.h"
+
+#include "storm/utility/macros.h"
+#include "storm/exceptions/InvalidPropertyException.h"
+
+namespace storm {
+    namespace logic {
+        BinaryBooleanPathFormula::BinaryBooleanPathFormula(OperatorType operatorType, std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula) : BinaryPathFormula(leftSubformula, rightSubformula), operatorType(operatorType) {
+            STORM_LOG_THROW(this->getLeftSubformula().isStateFormula() || this->getLeftSubformula().isPathFormula(), storm::exceptions::InvalidPropertyException, "Boolean path formula must have either path or state subformulas");
+            STORM_LOG_THROW(this->getRightSubformula().isStateFormula() || this->getRightSubformula().isPathFormula(), storm::exceptions::InvalidPropertyException, "Boolean path formula must have either path or state subformulas");
+        }
+        
+        bool BinaryBooleanPathFormula::isBinaryBooleanPathFormula() const {
+            return true;
+        }
+        
+        boost::any BinaryBooleanPathFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
+            return visitor.visit(*this, data);
+        }
+        
+        BinaryBooleanPathFormula::OperatorType BinaryBooleanPathFormula::getOperator() const {
+            return operatorType;
+        }
+        
+        bool BinaryBooleanPathFormula::isAnd() const {
+            return this->getOperator() == OperatorType::And;
+        }
+        
+        bool BinaryBooleanPathFormula::isOr() const {
+            return this->getOperator() == OperatorType::Or;
+        }
+                
+        std::ostream& BinaryBooleanPathFormula::writeToStream(std::ostream& out) const {
+            out << "(";
+            this->getLeftSubformula().writeToStream(out);
+            switch (operatorType) {
+                case OperatorType::And: out << " & "; break;
+                case OperatorType::Or: out << " | "; break;
+            }
+            this->getRightSubformula().writeToStream(out);
+            out << ")";
+            return out;
+        }
+    }
+}
diff --git a/src/storm/logic/BinaryBooleanPathFormula.h b/src/storm/logic/BinaryBooleanPathFormula.h
new file mode 100644
index 000000000..6f60f06f4
--- /dev/null
+++ b/src/storm/logic/BinaryBooleanPathFormula.h
@@ -0,0 +1,38 @@
+#ifndef STORM_LOGIC_BINARYBOOLEANPATHFORMULA_H_
+#define STORM_LOGIC_BINARYBOOLEANPATHFORMULA_H_
+
+#include <map>
+
+#include "storm/logic/BinaryPathFormula.h"
+#include "storm/logic/BinaryBooleanOperatorType.h"
+
+namespace storm {
+    namespace logic {
+        class BinaryBooleanPathFormula : public BinaryPathFormula {
+        public:
+            typedef storm::logic::BinaryBooleanOperatorType OperatorType;
+
+            BinaryBooleanPathFormula(OperatorType operatorType, std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula);
+            
+            virtual ~BinaryBooleanPathFormula() {
+                // Intentionally left empty.
+            };
+            
+            virtual bool isBinaryBooleanPathFormula() const override;
+            
+            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
+            
+            OperatorType getOperator() const;
+            
+            virtual bool isAnd() const;
+            virtual bool isOr() const;
+                        
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
+            
+        private:
+            OperatorType operatorType;
+        };
+    }
+}
+
+#endif /* STORM_LOGIC_BINARYBOOLEANPATHFORMULA_H_ */
diff --git a/src/storm/logic/BinaryBooleanStateFormula.h b/src/storm/logic/BinaryBooleanStateFormula.h
index 9a884e60a..085b4fb24 100644
--- a/src/storm/logic/BinaryBooleanStateFormula.h
+++ b/src/storm/logic/BinaryBooleanStateFormula.h
@@ -4,12 +4,13 @@
 #include <map>
 
 #include "storm/logic/BinaryStateFormula.h"
+#include "storm/logic/BinaryBooleanOperatorType.h"
 
 namespace storm {
     namespace logic {
         class BinaryBooleanStateFormula : public BinaryStateFormula {
         public:
-            enum class OperatorType {And, Or};
+            typedef storm::logic::BinaryBooleanOperatorType OperatorType;
 
             BinaryBooleanStateFormula(OperatorType operatorType, std::shared_ptr<Formula const> const& leftSubformula, std::shared_ptr<Formula const> const& rightSubformula);
             
diff --git a/src/storm/logic/CloneVisitor.cpp b/src/storm/logic/CloneVisitor.cpp
index 15499c9d9..ca1af66d9 100644
--- a/src/storm/logic/CloneVisitor.cpp
+++ b/src/storm/logic/CloneVisitor.cpp
@@ -24,6 +24,12 @@ namespace storm {
             return std::static_pointer_cast<Formula>(std::make_shared<BinaryBooleanStateFormula>(f.getOperator(), left, right));
         }
 
+        boost::any CloneVisitor::visit(BinaryBooleanPathFormula 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<BinaryBooleanPathFormula>(f.getOperator(), left, right));
+        }
+
         boost::any CloneVisitor::visit(BooleanLiteralFormula const& f, boost::any const&) const {
             return std::static_pointer_cast<Formula>(std::make_shared<BooleanLiteralFormula>(f));
         }
@@ -170,6 +176,11 @@ namespace storm {
             return std::static_pointer_cast<Formula>(std::make_shared<UnaryBooleanStateFormula>(f.getOperator(), subformula));
         }
 
+        boost::any CloneVisitor::visit(UnaryBooleanPathFormula 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<UnaryBooleanPathFormula>(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));
diff --git a/src/storm/logic/CloneVisitor.h b/src/storm/logic/CloneVisitor.h
index 954d46db4..3b5bc1054 100644
--- a/src/storm/logic/CloneVisitor.h
+++ b/src/storm/logic/CloneVisitor.h
@@ -15,6 +15,7 @@ namespace storm {
             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(BinaryBooleanPathFormula 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(BoundedGloballyFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override;
@@ -34,6 +35,7 @@ namespace storm {
             virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override;
             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(UnaryBooleanPathFormula 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 553e15b89..202116dff 100644
--- a/src/storm/logic/Formula.cpp
+++ b/src/storm/logic/Formula.cpp
@@ -43,6 +43,14 @@ namespace storm {
             return false;
         }
 
+        bool Formula::isBinaryBooleanPathFormula() const {
+            return false;
+        }
+
+        bool Formula::isUnaryBooleanPathFormula() const {
+            return false;
+        }
+
         bool Formula::isBooleanLiteralFormula() const {
             return false;
         }
diff --git a/src/storm/logic/Formula.h b/src/storm/logic/Formula.h
index 0014baef4..e4fec35c6 100644
--- a/src/storm/logic/Formula.h
+++ b/src/storm/logic/Formula.h
@@ -47,6 +47,9 @@ namespace storm {
             virtual bool isBinaryBooleanStateFormula() const;
             virtual bool isUnaryBooleanStateFormula() const;
 
+            virtual bool isBinaryBooleanPathFormula() const;
+            virtual bool isUnaryBooleanPathFormula() const;
+
             virtual bool isMultiObjectiveFormula() const;
             virtual bool isQuantileFormula() const;
 
diff --git a/src/storm/logic/FormulaInformationVisitor.cpp b/src/storm/logic/FormulaInformationVisitor.cpp
index 471503e2a..e42bb2cbb 100644
--- a/src/storm/logic/FormulaInformationVisitor.cpp
+++ b/src/storm/logic/FormulaInformationVisitor.cpp
@@ -17,10 +17,14 @@ namespace storm {
             return FormulaInformation();
         }
         
-        boost::any FormulaInformationVisitor::visit(BinaryBooleanStateFormula const&, boost::any const&) const {
-            return FormulaInformation();
+        boost::any FormulaInformationVisitor::visit(BinaryBooleanStateFormula const& f, boost::any const& data) const {
+            return boost::any_cast<FormulaInformation>(f.getLeftSubformula().accept(*this, data)).join(boost::any_cast<FormulaInformation>(f.getRightSubformula().accept(*this)));
         }
         
+        boost::any FormulaInformationVisitor::visit(BinaryBooleanPathFormula const& f, boost::any const& data) const {
+            return boost::any_cast<FormulaInformation>(f.getLeftSubformula().accept(*this, data)).join(boost::any_cast<FormulaInformation>(f.getRightSubformula().accept(*this)));
+        }
+
         boost::any FormulaInformationVisitor::visit(BooleanLiteralFormula const&, boost::any const&) const {
             return FormulaInformation();
         }
@@ -130,6 +134,10 @@ namespace storm {
             return f.getSubformula().accept(*this, data);
         }
         
+        boost::any FormulaInformationVisitor::visit(UnaryBooleanPathFormula const& f, boost::any const& data) const {
+            return f.getSubformula().accept(*this, data);
+        }
+
         boost::any FormulaInformationVisitor::visit(UntilFormula const& f, boost::any const& data) const {
             return boost::any_cast<FormulaInformation>(f.getLeftSubformula().accept(*this, data)).join(boost::any_cast<FormulaInformation>(f.getRightSubformula().accept(*this)));
         }
diff --git a/src/storm/logic/FormulaInformationVisitor.h b/src/storm/logic/FormulaInformationVisitor.h
index a1f3a3fb0..11ba3e80b 100644
--- a/src/storm/logic/FormulaInformationVisitor.h
+++ b/src/storm/logic/FormulaInformationVisitor.h
@@ -14,6 +14,7 @@ namespace storm {
             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(BinaryBooleanPathFormula 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(BoundedGloballyFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override;
@@ -33,6 +34,7 @@ namespace storm {
             virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override;
             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(UnaryBooleanPathFormula 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 b1c6db105..def8cf722 100644
--- a/src/storm/logic/FormulaVisitor.h
+++ b/src/storm/logic/FormulaVisitor.h
@@ -15,6 +15,7 @@ namespace storm {
             virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const = 0;
             virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const = 0;
             virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const = 0;
+            virtual boost::any visit(BinaryBooleanPathFormula const& f, boost::any const& data) const = 0;
             virtual boost::any visit(BooleanLiteralFormula const& f, boost::any const& data) const = 0;
             virtual boost::any visit(BoundedGloballyFormula const& f, boost::any const& data) const = 0;
             virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const = 0;
@@ -34,6 +35,7 @@ namespace storm {
             virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const = 0;
             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(UnaryBooleanPathFormula 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 47ceae22a..82c44604e 100644
--- a/src/storm/logic/Formulas.h
+++ b/src/storm/logic/Formulas.h
@@ -2,6 +2,7 @@
 #include "storm/logic/AtomicExpressionFormula.h"
 #include "storm/logic/AtomicLabelFormula.h"
 #include "storm/logic/BinaryBooleanStateFormula.h"
+#include "storm/logic/BinaryBooleanPathFormula.h"
 #include "storm/logic/BinaryPathFormula.h"
 #include "storm/logic/BinaryStateFormula.h"
 #include "storm/logic/BooleanLiteralFormula.h"
@@ -25,6 +26,7 @@
 #include "storm/logic/TimeOperatorFormula.h"
 #include "storm/logic/TotalRewardFormula.h"
 #include "storm/logic/UnaryBooleanStateFormula.h"
+#include "storm/logic/UnaryBooleanPathFormula.h"
 #include "storm/logic/UnaryPathFormula.h"
 #include "storm/logic/UnaryStateFormula.h"
 #include "storm/logic/UntilFormula.h"
diff --git a/src/storm/logic/FormulasForwardDeclarations.h b/src/storm/logic/FormulasForwardDeclarations.h
index 41aca3c3b..0dc68db03 100644
--- a/src/storm/logic/FormulasForwardDeclarations.h
+++ b/src/storm/logic/FormulasForwardDeclarations.h
@@ -8,6 +8,7 @@ namespace storm {
         class AtomicExpressionFormula;
         class AtomicLabelFormula;
         class BinaryBooleanStateFormula;
+        class BinaryBooleanPathFormula;
         class BinaryPathFormula;
         class BinaryStateFormula;
         class BooleanLiteralFormula;
@@ -33,6 +34,7 @@ namespace storm {
         class StateFormula;
         class TotalRewardFormula;
         class UnaryBooleanStateFormula;
+        class UnaryBooleanPathFormula;
         class UnaryPathFormula;
         class UnaryStateFormula;
         class UntilFormula;
diff --git a/src/storm/logic/FragmentChecker.cpp b/src/storm/logic/FragmentChecker.cpp
index 0c76dec44..c40d703c9 100644
--- a/src/storm/logic/FragmentChecker.cpp
+++ b/src/storm/logic/FragmentChecker.cpp
@@ -52,6 +52,14 @@ namespace storm {
             return result;
         }
 
+        boost::any FragmentChecker::visit(BinaryBooleanPathFormula const& f, boost::any const& data) const {
+            InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
+            bool result = inherited.getSpecification().areBinaryBooleanPathFormulasAllowed();
+            result = result && boost::any_cast<bool>(f.getLeftSubformula().accept(*this, data));
+            result = result && boost::any_cast<bool>(f.getRightSubformula().accept(*this, data));
+            return result;
+        }
+
         boost::any FragmentChecker::visit(BooleanLiteralFormula const&, boost::any const& data) const {
             InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
             return inherited.getSpecification().areBooleanLiteralFormulasAllowed();
@@ -311,6 +319,13 @@ namespace storm {
             return result;
         }
 
+        boost::any FragmentChecker::visit(UnaryBooleanPathFormula const& f, boost::any const& data) const {
+            InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
+            bool result = inherited.getSpecification().areUnaryBooleanPathFormulasAllowed();
+            result = result && boost::any_cast<bool>(f.getSubformula().accept(*this, data));
+            return result;
+        }
+
         boost::any FragmentChecker::visit(UntilFormula const& f, boost::any const& data) const {
             InheritedInformation const& inherited = boost::any_cast<InheritedInformation const&>(data);
             bool result = inherited.getSpecification().areUntilFormulasAllowed();
diff --git a/src/storm/logic/FragmentChecker.h b/src/storm/logic/FragmentChecker.h
index e027f7c46..3d9f50a2b 100644
--- a/src/storm/logic/FragmentChecker.h
+++ b/src/storm/logic/FragmentChecker.h
@@ -15,6 +15,7 @@ namespace storm {
             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(BinaryBooleanPathFormula 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(BoundedGloballyFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override;
@@ -34,6 +35,7 @@ namespace storm {
             virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override;
             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(UnaryBooleanPathFormula 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 445ae0b8c..c00d53cf7 100644
--- a/src/storm/logic/FragmentSpecification.cpp
+++ b/src/storm/logic/FragmentSpecification.cpp
@@ -175,6 +175,8 @@ namespace storm {
             booleanLiteralFormula = false;
             unaryBooleanStateFormula = false;
             binaryBooleanStateFormula = false;
+            unaryBooleanPathFormula = false;
+            binaryBooleanPathFormula = false;
 
             cumulativeRewardFormula = false;
             instantaneousRewardFormula = false;
@@ -372,12 +374,21 @@ namespace storm {
             return *this;
         }
 
-        bool FragmentSpecification::areBinaryBooleanStateFormulasAllowed() const {
-            return binaryBooleanStateFormula;
+        bool FragmentSpecification::areUnaryBooleanPathFormulasAllowed() const {
+            return unaryBooleanPathFormula;
         }
 
-        FragmentSpecification& FragmentSpecification::setBinaryBooleanStateFormulasAllowed(bool newValue) {
-            this->binaryBooleanStateFormula = newValue;
+        FragmentSpecification& FragmentSpecification::setUnaryBooleanPathFormulasAllowed(bool newValue) {
+            this->unaryBooleanPathFormula = newValue;
+            return *this;
+        }
+
+        bool FragmentSpecification::areBinaryBooleanPathFormulasAllowed() const {
+            return binaryBooleanPathFormula;
+        }
+
+        FragmentSpecification& FragmentSpecification::setBinaryBooleanPathFormulasAllowed(bool newValue) {
+            this->binaryBooleanPathFormula = newValue;
             return *this;
         }
 
diff --git a/src/storm/logic/FragmentSpecification.h b/src/storm/logic/FragmentSpecification.h
index 5f656695e..07dd5c3da 100644
--- a/src/storm/logic/FragmentSpecification.h
+++ b/src/storm/logic/FragmentSpecification.h
@@ -70,9 +70,15 @@ namespace storm {
             bool areUnaryBooleanStateFormulasAllowed() const;
             FragmentSpecification& setUnaryBooleanStateFormulasAllowed(bool newValue);
 
+            bool areUnaryBooleanPathFormulasAllowed() const;
+            FragmentSpecification& setUnaryBooleanPathFormulasAllowed(bool newValue);
+
             bool areBinaryBooleanStateFormulasAllowed() const;
             FragmentSpecification& setBinaryBooleanStateFormulasAllowed(bool newValue);
 
+            bool areBinaryBooleanPathFormulasAllowed() const;
+            FragmentSpecification& setBinaryBooleanPathFormulasAllowed(bool newValue);
+
             bool areCumulativeRewardFormulasAllowed() const;
             FragmentSpecification& setCumulativeRewardFormulasAllowed(bool newValue);
 
@@ -190,6 +196,8 @@ namespace storm {
             bool booleanLiteralFormula;
             bool unaryBooleanStateFormula;
             bool binaryBooleanStateFormula;
+            bool unaryBooleanPathFormula;
+            bool binaryBooleanPathFormula;
 
             bool cumulativeRewardFormula;
             bool instantaneousRewardFormula;
diff --git a/src/storm/logic/LiftableTransitionRewardsVisitor.cpp b/src/storm/logic/LiftableTransitionRewardsVisitor.cpp
index 5a0219242..fbb215440 100644
--- a/src/storm/logic/LiftableTransitionRewardsVisitor.cpp
+++ b/src/storm/logic/LiftableTransitionRewardsVisitor.cpp
@@ -23,9 +23,15 @@ namespace storm {
         }
 
         boost::any LiftableTransitionRewardsVisitor::visit(BinaryBooleanStateFormula const&, boost::any const&) const {
+	  // TODO joachim: is this correct?
             return true;
         }
 
+        boost::any LiftableTransitionRewardsVisitor::visit(BinaryBooleanPathFormula const& f, boost::any const& data) const {
+            return boost::any_cast<bool>(f.getLeftSubformula().accept(*this, data)) && boost::any_cast<bool>(f.getRightSubformula().accept(*this));
+        }
+
+
         boost::any LiftableTransitionRewardsVisitor::visit(BooleanLiteralFormula const&, boost::any const&) const {
             return true;
         }
@@ -143,6 +149,10 @@ namespace storm {
             return f.getSubformula().accept(*this, data);
         }
 
+        boost::any LiftableTransitionRewardsVisitor::visit(UnaryBooleanPathFormula const& f, boost::any const& data) const {
+            return f.getSubformula().accept(*this, data);
+        }
+
         boost::any LiftableTransitionRewardsVisitor::visit(UntilFormula const& f, boost::any const& data) const {
             return boost::any_cast<bool>(f.getLeftSubformula().accept(*this, data)) && boost::any_cast<bool>(f.getRightSubformula().accept(*this));
         }
diff --git a/src/storm/logic/LiftableTransitionRewardsVisitor.h b/src/storm/logic/LiftableTransitionRewardsVisitor.h
index db5530cad..bf2b6a4f5 100644
--- a/src/storm/logic/LiftableTransitionRewardsVisitor.h
+++ b/src/storm/logic/LiftableTransitionRewardsVisitor.h
@@ -21,6 +21,7 @@ namespace storm {
             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(BinaryBooleanPathFormula 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(BoundedGloballyFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override;
@@ -40,6 +41,7 @@ namespace storm {
             virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override;
             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(UnaryBooleanPathFormula 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/ToExpressionVisitor.cpp b/src/storm/logic/ToExpressionVisitor.cpp
index 41688ad8e..ff1025fca 100644
--- a/src/storm/logic/ToExpressionVisitor.cpp
+++ b/src/storm/logic/ToExpressionVisitor.cpp
@@ -37,6 +37,10 @@ namespace storm {
             return boost::any();
         }
         
+        boost::any ToExpressionVisitor::visit(BinaryBooleanPathFormula 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(BooleanLiteralFormula const& f, boost::any const& data) const {
             storm::expressions::Expression result;
             if (f.isTrueFormula()) {
@@ -124,7 +128,11 @@ namespace storm {
             }
             return boost::any();
         }
-        
+
+        boost::any ToExpressionVisitor::visit(UnaryBooleanPathFormula 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(UntilFormula 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 eb7e261f2..a97a9a4b0 100644
--- a/src/storm/logic/ToExpressionVisitor.h
+++ b/src/storm/logic/ToExpressionVisitor.h
@@ -15,6 +15,7 @@ namespace storm {
             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(BinaryBooleanPathFormula 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(BoundedGloballyFormula const& f, boost::any const& data) const override;
             virtual boost::any visit(BoundedUntilFormula const& f, boost::any const& data) const override;
@@ -34,6 +35,7 @@ namespace storm {
             virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override;
             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(UnaryBooleanPathFormula 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/UnaryBooleanOperatorType.h b/src/storm/logic/UnaryBooleanOperatorType.h
new file mode 100644
index 000000000..915a11f8a
--- /dev/null
+++ b/src/storm/logic/UnaryBooleanOperatorType.h
@@ -0,0 +1,7 @@
+#pragma once
+
+namespace storm {
+    namespace logic {
+        enum class UnaryBooleanOperatorType {Not};
+    }
+}
diff --git a/src/storm/logic/UnaryBooleanPathFormula.cpp b/src/storm/logic/UnaryBooleanPathFormula.cpp
new file mode 100644
index 000000000..61b699d55
--- /dev/null
+++ b/src/storm/logic/UnaryBooleanPathFormula.cpp
@@ -0,0 +1,39 @@
+#include "storm/logic/UnaryBooleanPathFormula.h"
+
+#include "storm/logic/FormulaVisitor.h"
+
+#include "storm/utility/macros.h"
+#include "storm/exceptions/InvalidPropertyException.h"
+
+namespace storm {
+    namespace logic {
+        UnaryBooleanPathFormula::UnaryBooleanPathFormula(OperatorType operatorType, std::shared_ptr<Formula const> const& subformula) : UnaryPathFormula(subformula), operatorType(operatorType) {
+            STORM_LOG_THROW(this->getSubformula().isStateFormula() || this->getSubformula().isPathFormula(), storm::exceptions::InvalidPropertyException, "Boolean path formula must have either path or state subformulas");
+        }
+        
+        bool UnaryBooleanPathFormula::isUnaryBooleanPathFormula() const {
+            return true;
+        }
+
+        boost::any UnaryBooleanPathFormula::accept(FormulaVisitor const& visitor, boost::any const& data) const {
+            return visitor.visit(*this, data);
+        }
+        
+        UnaryBooleanPathFormula::OperatorType UnaryBooleanPathFormula::getOperator() const {
+            return operatorType;
+        }
+        
+        bool UnaryBooleanPathFormula::isNot() const {
+            return this->getOperator() == OperatorType::Not;
+        }
+                
+        std::ostream& UnaryBooleanPathFormula::writeToStream(std::ostream& out) const {
+            switch (operatorType) {
+                case OperatorType::Not: out << "!("; break;
+            }
+            this->getSubformula().writeToStream(out);
+            out << ")";
+            return out;
+        }
+    }
+}
diff --git a/src/storm/logic/UnaryBooleanPathFormula.h b/src/storm/logic/UnaryBooleanPathFormula.h
new file mode 100644
index 000000000..bbef7aeac
--- /dev/null
+++ b/src/storm/logic/UnaryBooleanPathFormula.h
@@ -0,0 +1,35 @@
+#ifndef STORM_LOGIC_UNARYBOOLEANPATHFORMULA_H_
+#define STORM_LOGIC_UNARYBOOLEANPATHFORMULA_H_
+
+#include "storm/logic/UnaryPathFormula.h"
+#include "storm/logic/UnaryBooleanOperatorType.h"
+
+namespace storm {
+    namespace logic {
+        class UnaryBooleanPathFormula : public UnaryPathFormula {
+        public:
+            typedef storm::logic::UnaryBooleanOperatorType OperatorType;
+
+            UnaryBooleanPathFormula(OperatorType operatorType, std::shared_ptr<Formula const> const& subformula);
+            
+            virtual ~UnaryBooleanPathFormula() {
+                // Intentionally left empty.
+            };
+            
+            virtual bool isUnaryBooleanPathFormula() const override;
+
+            virtual boost::any accept(FormulaVisitor const& visitor, boost::any const& data) const override;
+            
+            OperatorType getOperator() const;
+            
+            virtual bool isNot() const;
+            
+            virtual std::ostream& writeToStream(std::ostream& out) const override;
+
+        private:
+            OperatorType operatorType;
+        };
+    }
+}
+
+#endif /* STORM_LOGIC_UNARYBOOLEANPATHFORMULA_H_ */
diff --git a/src/storm/logic/UnaryBooleanStateFormula.h b/src/storm/logic/UnaryBooleanStateFormula.h
index 19420ec16..4c3cd3c17 100644
--- a/src/storm/logic/UnaryBooleanStateFormula.h
+++ b/src/storm/logic/UnaryBooleanStateFormula.h
@@ -2,12 +2,13 @@
 #define STORM_LOGIC_UNARYBOOLEANSTATEFORMULA_H_
 
 #include "storm/logic/UnaryStateFormula.h"
+#include "storm/logic/UnaryBooleanOperatorType.h"
 
 namespace storm {
     namespace logic {
         class UnaryBooleanStateFormula : public UnaryStateFormula {
         public:
-            enum class OperatorType { Not };
+            typedef storm::logic::UnaryBooleanOperatorType OperatorType;
 
             UnaryBooleanStateFormula(OperatorType operatorType, std::shared_ptr<Formula const> const& subformula);
             
diff --git a/src/storm/storage/jani/JSONExporter.cpp b/src/storm/storage/jani/JSONExporter.cpp
index f89e1cab5..5706618c6 100644
--- a/src/storm/storage/jani/JSONExporter.cpp
+++ b/src/storm/storage/jani/JSONExporter.cpp
@@ -208,6 +208,14 @@ namespace storm {
             opDecl["right"] = anyToJson(f.getRightSubformula().accept(*this, data));
             return opDecl;
         }
+        boost::any FormulaToJaniJson::visit(storm::logic::BinaryBooleanPathFormula const& f, boost::any const& data) const{
+            ExportJsonType opDecl;
+            storm::logic::BinaryBooleanPathFormula::OperatorType op = f.getOperator();
+            opDecl["op"] = op == storm::logic::BinaryBooleanPathFormula::OperatorType::And ? "∧" : "∨";
+            opDecl["left"] = boost::any_cast<ExportJsonType>(f.getLeftSubformula().accept(*this, data));
+            opDecl["right"] = boost::any_cast<ExportJsonType>(f.getRightSubformula().accept(*this, data));
+            return opDecl;
+        }
         boost::any FormulaToJaniJson::visit(storm::logic::BooleanLiteralFormula const& f, boost::any const&) const {
             ExportJsonType opDecl(f.isTrueFormula() ? true : false);
             return opDecl;
@@ -588,6 +596,15 @@ namespace storm {
             return opDecl;
         }
 
+        boost::any FormulaToJaniJson::visit(storm::logic::UnaryBooleanPathFormula const& f, boost::any const& data) const {
+            ExportJsonType opDecl;
+            storm::logic::UnaryBooleanPathFormula::OperatorType op = f.getOperator();
+            assert(op == storm::logic::UnaryBooleanPathFormula::OperatorType::Not);
+            opDecl["op"] = "¬";
+            opDecl["exp"] = boost::any_cast<ExportJsonType>(f.getSubformula().accept(*this, data));
+            return opDecl;
+        }
+
         boost::any FormulaToJaniJson::visit(storm::logic::UntilFormula const& f, boost::any const& data) const {
             ExportJsonType opDecl;
             opDecl["op"] = "U";
diff --git a/src/storm/storage/jani/JSONExporter.h b/src/storm/storage/jani/JSONExporter.h
index c14524f69..a00088cb1 100644
--- a/src/storm/storage/jani/JSONExporter.h
+++ b/src/storm/storage/jani/JSONExporter.h
@@ -52,6 +52,7 @@ namespace storm {
             virtual boost::any visit(storm::logic::AtomicExpressionFormula const& f, boost::any const& data) const;
             virtual boost::any visit(storm::logic::AtomicLabelFormula const& f, boost::any const& data) const;
             virtual boost::any visit(storm::logic::BinaryBooleanStateFormula const& f, boost::any const& data) const;
+            virtual boost::any visit(storm::logic::BinaryBooleanPathFormula const& f, boost::any const& data) const;
             virtual boost::any visit(storm::logic::BooleanLiteralFormula const& f, boost::any const& data) const;
             virtual boost::any visit(storm::logic::BoundedGloballyFormula const& f, boost::any const& data) const;
             virtual boost::any visit(storm::logic::BoundedUntilFormula const& f, boost::any const& data) const;
@@ -71,6 +72,7 @@ namespace storm {
             virtual boost::any visit(storm::logic::RewardOperatorFormula const& f, boost::any const& data) const;
             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::UnaryBooleanPathFormula 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;