diff --git a/stormpy/lib/stormpy/logic/__init__.py b/stormpy/lib/stormpy/logic/__init__.py
new file mode 100644
index 000000000..9ab762097
--- /dev/null
+++ b/stormpy/lib/stormpy/logic/__init__.py
@@ -0,0 +1,2 @@
+from . import logic
+from .logic import *
diff --git a/stormpy/setup.py b/stormpy/setup.py
index 612385160..08204ff4d 100755
--- a/stormpy/setup.py
+++ b/stormpy/setup.py
@@ -11,6 +11,7 @@ PROJECT_DIR = os.path.abspath(os.path.dirname(os.path.realpath(__file__)))
 # Glob source files for modules
 core_sources = glob(os.path.join('src', 'core', '*.cpp'))
 expressions_sources = glob(os.path.join('src', 'expressions', '*.cpp'))
+logic_sources = glob(os.path.join('src', 'logic', '*.cpp'))
 
 # Configuration shared between external modules follows
 
@@ -67,6 +68,17 @@ ext_expressions = Extension(
     extra_link_args=extra_link_args
 )
 
+ext_logic = Extension(
+    name='logic.logic',
+    sources=['src/mod_logic.cpp'] + logic_sources,
+    include_dirs=include_dirs,
+    libraries=libraries,
+    library_dirs=library_dirs,
+    extra_compile_args=extra_compile_args,
+    define_macros=define_macros,
+    extra_link_args=extra_link_args
+)
+
 class stormpy_build_ext(build_ext):
     """Extend build_ext to provide CLN toggle option
     """
@@ -110,10 +122,10 @@ setup(name="stormpy",
       maintainer_email="sebastian.junges@cs.rwth-aachen.de",
       url="http://moves.rwth-aachen.de",
       description="stormpy - Python Bindings for Storm",
-      packages=['stormpy', 'stormpy.info', 'stormpy.expressions'],
+      packages=['stormpy', 'stormpy.info', 'stormpy.expressions', 'stormpy.logic'],
       package_dir={'':'lib'},
       ext_package='stormpy',
-      ext_modules=[ext_core, ext_info, ext_expressions
+      ext_modules=[ext_core, ext_info, ext_expressions, ext_logic
                    ],
       cmdclass={
         'build_ext': stormpy_build_ext,
diff --git a/stormpy/src/logic/formulas.cpp b/stormpy/src/logic/formulas.cpp
new file mode 100644
index 000000000..e3c448301
--- /dev/null
+++ b/stormpy/src/logic/formulas.cpp
@@ -0,0 +1,99 @@
+#include "formulas.h"
+
+#include "common.h"
+
+#include <src/logic/Formulas.h>
+#include <src/logic/ComparisonType.h>
+
+void define_formulas(py::module& m) {
+    
+    py::enum_<storm::logic::ComparisonType>(m, "ComparisonType")
+        .value("LESS", storm::logic::ComparisonType::Less)
+        .value("LEQ", storm::logic::ComparisonType::LessEqual)
+        .value("GREATER", storm::logic::ComparisonType::Greater)
+        .value("GEQ", storm::logic::ComparisonType::GreaterEqual)
+    ;
+    
+    /*defineClass<std::vector<std::shared_ptr<storm::logic::Formula>>, void, void>("FormulaVec", "Vector of formulas")
+        .def(vector_indexing_suite<std::vector<std::shared_ptr<storm::logic::Formula>>, true>())
+    ;
+    
+    ////////////////////////////////////////////
+    // Formula
+    ////////////////////////////////////////////
+    defineClass<storm::logic::Formula, void, boost::noncopyable>("Formula",
+    "Generic Storm Formula")
+        .def("__str__", &storm::logic::Formula::toString)
+    ;
+
+    //
+    // Path Formulae
+    //
+    defineClass<storm::logic::PathFormula, storm::logic::Formula, boost::noncopyable>("PathFormula",
+    "Formula about the probability of a set of paths in an automaton");
+    defineClass<storm::logic::UnaryPathFormula, storm::logic::PathFormula, boost::noncopyable>("UnaryPathFormula",
+    "Path formula with one operand");
+    defineClass<storm::logic::EventuallyFormula, storm::logic::UnaryPathFormula>("EventuallyFormula",
+    "Formula for eventually");
+    defineClass<storm::logic::GloballyFormula, storm::logic::UnaryPathFormula>("GloballyFormula",
+    "Formula for globally");
+    defineClass<storm::logic::BinaryPathFormula, storm::logic::PathFormula, boost::noncopyable>("BinaryPathFormula",
+    "Path formula with two operands");
+    defineClass<storm::logic::BoundedUntilFormula, storm::logic::BinaryPathFormula, boost::noncopyable>("BoundedUntilFormula",
+    "Until Formula with either a step or a time bound.");
+    defineClass<storm::logic::ConditionalPathFormula, storm::logic::BinaryPathFormula>("ConditionalPathFormula",
+    "Path Formula with the right hand side being a condition.");
+    defineClass<storm::logic::UntilFormula, storm::logic::BinaryPathFormula>("UntilFormula",
+    "Path Formula for unbounded until");
+
+
+    //
+    // Reward Path Formulae
+    //
+    defineClass<storm::logic::RewardPathFormula, storm::logic::Formula, boost::noncopyable>("RewardPathFormula",
+    "Formula about the rewards of a set of paths in an automaton");
+    defineClass<storm::logic::CumulativeRewardFormula, storm::logic::RewardPathFormula>("CumulativeRewardFormula",
+    "Summed rewards over a the paths");
+    defineClass<storm::logic::InstantaneousRewardFormula, storm::logic::RewardPathFormula>("InstanteneousRewardFormula",
+    "");
+    defineClass<storm::logic::LongRunAverageRewardFormula, storm::logic::RewardPathFormula>("LongRunAverageRewardFormula",
+    "");
+    defineClass<storm::logic::ReachabilityRewardFormula, storm::logic::RewardPathFormula>("ReachabilityRewardFormula",
+    "");
+
+
+    //
+    // State Formulae
+    //
+    defineClass<storm::logic::StateFormula, storm::logic::Formula, boost::noncopyable>("StateFormula",
+    "Formula about a state of an automaton");
+    defineClass<storm::logic::AtomicExpressionFormula, storm::logic::StateFormula>("AtomicExpressionFormula",
+    "");
+    defineClass<storm::logic::AtomicLabelFormula, storm::logic::StateFormula>("AtomicLabelFormula",
+    "");
+    defineClass<storm::logic::BooleanLiteralFormula, storm::logic::StateFormula>("BooleanLiteralFormula",
+    "");
+    defineClass<storm::logic::UnaryStateFormula, storm::logic::StateFormula, boost::noncopyable>("UnaryStateFormula",
+    "State formula with one operand");
+    defineClass<storm::logic::UnaryBooleanStateFormula, storm::logic::UnaryStateFormula>("UnaryBooleanStateFormula",
+    "");
+    defineClass<storm::logic::OperatorFormula, storm::logic::UnaryStateFormula, boost::noncopyable>("OperatorFormula",
+    "")
+        .add_property("has_bound", &storm::logic::OperatorFormula::hasBound)
+        .add_property("bound", &storm::logic::OperatorFormula::getBound, &storm::logic::OperatorFormula::setBound)
+        .add_property("comparison_type", &storm::logic::OperatorFormula::getComparisonType, &storm::logic::OperatorFormula::setComparisonType)
+    ;
+    defineClass<storm::logic::ExpectedTimeOperatorFormula, storm::logic::OperatorFormula>("ExpectedTimeOperator",
+    "The expected time between two events");
+    defineClass<storm::logic::LongRunAverageOperatorFormula, storm::logic::OperatorFormula>("LongRunAvarageOperator",
+    "");
+    defineClass<storm::logic::ProbabilityOperatorFormula, storm::logic::OperatorFormula>("ProbabilityOperator",
+    "");
+    defineClass<storm::logic::RewardOperatorFormula, storm::logic::OperatorFormula>("RewardOperatorFormula",
+    "");
+    defineClass<storm::logic::BinaryStateFormula, storm::logic::StateFormula, boost::noncopyable>("BinaryStateFormula",
+    "State formula with two operands");
+    defineClass<storm::logic::BinaryBooleanStateFormula, storm::logic::BinaryStateFormula>("BooleanBinaryStateFormula",
+    "");
+    */
+}
diff --git a/stormpy/src/logic/formulas.h b/stormpy/src/logic/formulas.h
new file mode 100644
index 000000000..965ca32c8
--- /dev/null
+++ b/stormpy/src/logic/formulas.h
@@ -0,0 +1,8 @@
+#ifndef PYTHON_LOGIC_FORMULAS_H_
+#define PYTHON_LOGIC_FORMULAS_H_
+
+#include "src/common.h"
+
+void define_formulas(py::module& m);
+
+#endif /* PYTHON_LOGIC_FORMULAS_H_ */
diff --git a/stormpy/src/mod_logic.cpp b/stormpy/src/mod_logic.cpp
new file mode 100644
index 000000000..eb9d1f7f8
--- /dev/null
+++ b/stormpy/src/mod_logic.cpp
@@ -0,0 +1,9 @@
+#include "common.h"
+
+#include "logic/formulas.h"
+
+PYBIND11_PLUGIN(logic) {
+    py::module m("stormpy.logic", "Logic module for Storm");
+    define_formulas(m);
+    return m.ptr();
+}