diff --git a/src/storm/logic/Formula.cpp b/src/storm/logic/Formula.cpp
index 7cefa26d1..752389b36 100644
--- a/src/storm/logic/Formula.cpp
+++ b/src/storm/logic/Formula.cpp
@@ -8,6 +8,7 @@
 #include "storm/logic/LabelSubstitutionVisitor.h"
 #include "storm/logic/RewardModelNameSubstitutionVisitor.h"
 #include "storm/logic/ToExpressionVisitor.h"
+#include "storm/logic/ToPrefixStringVisitor.h"
 
 namespace storm {
     namespace logic {
@@ -567,5 +568,11 @@ namespace storm {
         std::ostream& operator<<(std::ostream& out, Formula const& formula) {
             return formula.writeToStream(out);
         }
+
+        std::string Formula::toPrefixString() const {
+            ToPrefixStringVisitor visitor;
+            return visitor.toPrefixString(*this);
+        }
+
     }
 }
diff --git a/src/storm/logic/Formula.h b/src/storm/logic/Formula.h
index 452ef0f73..72631e2fe 100644
--- a/src/storm/logic/Formula.h
+++ b/src/storm/logic/Formula.h
@@ -237,6 +237,7 @@ namespace storm {
 
             std::string toString() const;
             virtual std::ostream& writeToStream(std::ostream& out) const = 0;
+            std::string toPrefixString() const;
 
             virtual void gatherAtomicExpressionFormulas(std::vector<std::shared_ptr<AtomicExpressionFormula const>>& atomicExpressionFormulas) const;
             virtual void gatherAtomicLabelFormulas(std::vector<std::shared_ptr<AtomicLabelFormula const>>& atomicLabelFormulas) const;
diff --git a/src/storm/logic/ToPrefixStringVisitor.cpp b/src/storm/logic/ToPrefixStringVisitor.cpp
new file mode 100644
index 000000000..a3d55b994
--- /dev/null
+++ b/src/storm/logic/ToPrefixStringVisitor.cpp
@@ -0,0 +1,155 @@
+#include "storm/logic/ToPrefixStringVisitor.h"
+
+#include "storm/logic/Formulas.h"
+
+#include "storm/utility/macros.h"
+#include "storm/exceptions/InvalidOperationException.h"
+
+namespace storm {
+    namespace logic {
+        
+        std::string ToPrefixStringVisitor::toPrefixString(Formula const& f) const {
+            boost::any result = f.accept(*this, boost::any());
+            return boost::any_cast<std::string>(result);
+        }
+        
+        boost::any ToPrefixStringVisitor::visit(AtomicExpressionFormula const&, boost::any const&) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string");
+        }
+        
+        boost::any ToPrefixStringVisitor::visit(AtomicLabelFormula const& f, boost::any const&) const {
+            return std::string("\"" + f.getLabel() + "\"");
+        }
+        
+        boost::any ToPrefixStringVisitor::visit(BinaryBooleanStateFormula const& f, boost::any const& data) const {
+            std::string left = boost::any_cast<std::string>(f.getLeftSubformula().accept(*this, data));
+            std::string right = boost::any_cast<std::string>(f.getRightSubformula().accept(*this, data));
+            switch (f.getOperator()) {
+                case BinaryBooleanStateFormula::OperatorType::And:
+                    return std::string("& ") + left + " " + right;
+                    break;
+                case BinaryBooleanStateFormula::OperatorType::Or:
+                    return std::string("| ") + left + " " + right;
+                    break;
+            }
+            return boost::any();
+        }
+        
+        boost::any ToPrefixStringVisitor::visit(BinaryBooleanPathFormula const& f, boost::any const& data) const {
+            std::string left = boost::any_cast<std::string>(f.getLeftSubformula().accept(*this, data));
+            std::string right = boost::any_cast<std::string>(f.getRightSubformula().accept(*this, data));
+            switch (f.getOperator()) {
+                case BinaryBooleanPathFormula::OperatorType::And:
+                    return std::string("& ") + left + " " + right;
+                    break;
+                case BinaryBooleanPathFormula::OperatorType::Or:
+                    return std::string("| ") + left + " " + right;
+                    break;
+            }
+            return boost::any();
+        }
+
+        boost::any ToPrefixStringVisitor::visit(BooleanLiteralFormula const& f, boost::any const&) const {
+            storm::expressions::Expression result;
+            if (f.isTrueFormula()) {
+                return std::string("t");
+            } else {
+                return std::string("f");
+            }
+            return result;
+        }
+        
+        boost::any ToPrefixStringVisitor::visit(BoundedUntilFormula const&, boost::any const&) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string");
+        }
+        
+        boost::any ToPrefixStringVisitor::visit(ConditionalFormula const&, boost::any const&) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string");
+        }
+        
+        boost::any ToPrefixStringVisitor::visit(CumulativeRewardFormula const&, boost::any const&) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string");
+        }
+        
+        boost::any ToPrefixStringVisitor::visit(EventuallyFormula const& f, boost::any const& data) const {
+            std::string subexpression = boost::any_cast<std::string>(f.getSubformula().accept(*this, data));
+            return std::string("F ") + subexpression;
+        }
+        
+        boost::any ToPrefixStringVisitor::visit(TimeOperatorFormula const&, boost::any const&) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string");
+        }
+        
+        boost::any ToPrefixStringVisitor::visit(GloballyFormula const& f, boost::any const& data) const {
+            std::string subexpression = boost::any_cast<std::string>(f.getSubformula().accept(*this, data));
+            return std::string("G ") + subexpression;
+        }
+        
+        boost::any ToPrefixStringVisitor::visit(InstantaneousRewardFormula const&, boost::any const&) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string");
+        }
+        
+        boost::any ToPrefixStringVisitor::visit(LongRunAverageOperatorFormula const&, boost::any const&) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string");
+        }
+        
+        boost::any ToPrefixStringVisitor::visit(LongRunAverageRewardFormula const&, boost::any const&) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string");
+        }
+        
+        boost::any ToPrefixStringVisitor::visit(MultiObjectiveFormula const&, boost::any const&) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string");
+        }
+        
+        boost::any ToPrefixStringVisitor::visit(QuantileFormula const&, boost::any const&) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string");
+        }
+
+        boost::any ToPrefixStringVisitor::visit(NextFormula const& f, boost::any const& data) const {
+            std::string subexpression = boost::any_cast<std::string>(f.getSubformula().accept(*this, data));
+            return std::string("X ") + subexpression;
+        }
+        
+        boost::any ToPrefixStringVisitor::visit(ProbabilityOperatorFormula const&, boost::any const&) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string");
+        }
+        
+        boost::any ToPrefixStringVisitor::visit(RewardOperatorFormula const&, boost::any const&) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string");
+        }
+        
+        boost::any ToPrefixStringVisitor::visit(TotalRewardFormula const&, boost::any const&) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string");
+        }
+        
+        boost::any ToPrefixStringVisitor::visit(UnaryBooleanStateFormula const& f, boost::any const& data) const {
+            std::string subexpression = boost::any_cast<std::string>(f.getSubformula().accept(*this, data));
+            switch (f.getOperator()) {
+                case UnaryBooleanStateFormula::OperatorType::Not:
+                    return std::string("! ") + subexpression;
+                    break;
+            }
+            return boost::any();
+        }
+
+        boost::any ToPrefixStringVisitor::visit(UnaryBooleanPathFormula const& f, boost::any const& data) const {
+            std::string subexpression = boost::any_cast<std::string>(f.getSubformula().accept(*this, data));
+            switch (f.getOperator()) {
+                case UnaryBooleanPathFormula::OperatorType::Not:
+                    return std::string("! ") + subexpression;
+                    break;
+            }
+            return boost::any();
+        }
+
+        boost::any ToPrefixStringVisitor::visit(UntilFormula const& f, boost::any const& data) const {
+            std::string left = boost::any_cast<std::string>(f.getLeftSubformula().accept(*this, data));
+            std::string right = boost::any_cast<std::string>(f.getRightSubformula().accept(*this, data));
+            return std::string("U ") + left + " " + right;
+        }
+        
+        boost::any ToPrefixStringVisitor::visit(HOAPathFormula const&, boost::any const&) const {
+            STORM_LOG_THROW(false, storm::exceptions::InvalidOperationException, "Can not convert to prefix string");
+        }
+    }
+}
diff --git a/src/storm/logic/ToPrefixStringVisitor.h b/src/storm/logic/ToPrefixStringVisitor.h
new file mode 100644
index 000000000..95d1bc585
--- /dev/null
+++ b/src/storm/logic/ToPrefixStringVisitor.h
@@ -0,0 +1,42 @@
+#pragma once
+
+#include "storm/logic/FormulaVisitor.h"
+
+#include <string>
+
+namespace storm {
+    namespace logic {
+        
+        class ToPrefixStringVisitor : public FormulaVisitor {
+        public:
+            std::string toPrefixString(Formula const& f) const;
+            
+            virtual boost::any visit(AtomicExpressionFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(AtomicLabelFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(BinaryBooleanStateFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(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(BoundedUntilFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(ConditionalFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(CumulativeRewardFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(EventuallyFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(TimeOperatorFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(GloballyFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(InstantaneousRewardFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(LongRunAverageOperatorFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(LongRunAverageRewardFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(MultiObjectiveFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(QuantileFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(NextFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(ProbabilityOperatorFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(RewardOperatorFormula const& f, boost::any const& data) const override;
+            virtual boost::any visit(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;
+        };
+        
+    }
+}
+