diff --git a/.gitignore b/.gitignore
index 28f42c3176..356a7aa716 100644
--- a/.gitignore
+++ b/.gitignore
@@ -9,6 +9,9 @@ dist/
 __pycache__/
 _build/
 .pytest_cache/
+.idea/
+.vscode/
 cmake-build-debug/
-
+.cache/
 .DS_Store
+.venv/
diff --git a/CMakeLists.txt b/CMakeLists.txt
index d2606bc448..d12008f65f 100644
--- a/CMakeLists.txt
+++ b/CMakeLists.txt
@@ -411,4 +411,4 @@ if (PYCARL_HAS_PARSE)
     endif()
 else()
     MESSAGE(WARNING "Stormpy - No support for carl-parser")
-endif()
+endif()
\ No newline at end of file
diff --git a/lib/stormpy/pomdp/__init__.py b/lib/stormpy/pomdp/__init__.py
index c43ceb50ec..a518cf7a26 100644
--- a/lib/stormpy/pomdp/__init__.py
+++ b/lib/stormpy/pomdp/__init__.py
@@ -16,6 +16,8 @@ def make_canonic(model):
 
     if model.supports_parameters:
         return _pomdp._make_canonic_Rf(model)
+    elif model.is_exact:
+        return _pomdp._make_canonic_Exact(model)
     else:
         return _pomdp._make_canonic_Double(model)
 
@@ -73,15 +75,19 @@ def create_nondeterminstic_belief_tracker(model, reduction_timeout, track_timeou
         return _pomdp.NondeterministicBeliefTrackerDoubleSparse(model, opts)
 
 
-def create_observation_trace_unfolder(model, risk_assessment, expr_manager):
+def create_observation_trace_unfolder(model, risk_assessment, expr_manager, options=None):
     """
 
     :param model:
     :param risk_assessment:
     :param expr_manager:
+    :param options:
     :return:
     """
+    if options is None:
+        options = ObservationTraceUnfolderOptions()
+
     if model.is_exact:
-        return _pomdp.ObservationTraceUnfolderExact(model, risk_assessment, expr_manager)
+        return _pomdp.ObservationTraceUnfolderExact(model, risk_assessment, expr_manager, options)
     else:
-        return _pomdp.ObservationTraceUnfolderDouble(model, risk_assessment, expr_manager)
+        return _pomdp.ObservationTraceUnfolderDouble(model, risk_assessment, expr_manager, options)
diff --git a/src/core/environment.cpp b/src/core/environment.cpp
index e89007057c..6c4e348d90 100644
--- a/src/core/environment.cpp
+++ b/src/core/environment.cpp
@@ -1,8 +1,15 @@
 #include "environment.h"
+#include <pybind11/pytypes.h>
+#include <storm/settings/SettingsManager.h>
+#include <storm/utility/constants.h>
 #include "src/helpers.h"
 #include "storm/environment/Environment.h"
 #include "storm/environment/solver/SolverEnvironment.h"
 #include "storm/environment/solver/AllSolverEnvironments.h"
+#include "storm/environment/modelchecker/ConditionalModelCheckerEnvironment.h"
+#include "storm/environment/modelchecker/ModelCheckerEnvironment.h"
+#include "storm/environment/modelchecker/MultiObjectiveModelCheckerEnvironment.h"
+#include "storm/storage/SchedulerClass.h"
 
 void define_environment(py::module& m) {
     py::enum_<storm::solver::EquationSolverType>(m, "EquationSolverType", "Solver type for equation systems")
@@ -36,9 +43,111 @@ void define_environment(py::module& m) {
         .value("optimistic_value_iteration", storm::solver::MinMaxMethod::OptimisticValueIteration)
     ;
 
+    // Multi-objective related enums
+    py::enum_<storm::modelchecker::multiobjective::MultiObjectiveMethod>(m, "MultiObjectiveMethod", "Multi-objective model checking method")
+        .value("pcaa", storm::modelchecker::multiobjective::MultiObjectiveMethod::Pcaa)
+        .value("constraint_based", storm::modelchecker::multiobjective::MultiObjectiveMethod::ConstraintBased)
+    ;
+
+    // Added enums for model checker environment
+    py::enum_<storm::SteadyStateDistributionAlgorithm>(m, "SteadyStateDistributionAlgorithm", "Algorithm for steady state distribution computation")
+        .value("automatic", storm::SteadyStateDistributionAlgorithm::Automatic)
+        .value("equation_system", storm::SteadyStateDistributionAlgorithm::EquationSystem)
+        .value("expected_visiting_times", storm::SteadyStateDistributionAlgorithm::ExpectedVisitingTimes)
+        .value("classic", storm::SteadyStateDistributionAlgorithm::Classic)
+    ;
+
+    py::enum_<storm::ConditionalAlgorithmSetting>(m, "ConditionalAlgorithmSetting", "Algorithm used for conditional model checking")
+        .value("default", storm::ConditionalAlgorithmSetting::Default)
+        .value("restart", storm::ConditionalAlgorithmSetting::Restart)
+        .value("bisection", storm::ConditionalAlgorithmSetting::Bisection)
+        .value("bisection_advanced", storm::ConditionalAlgorithmSetting::BisectionAdvanced)
+        .value("bisection_pt", storm::ConditionalAlgorithmSetting::BisectionPolicyTracking)
+        .value("bisection_advanced_pt", storm::ConditionalAlgorithmSetting::BisectionAdvancedPolicyTracking)
+        .value("policy_iteration", storm::ConditionalAlgorithmSetting::PolicyIteration)
+    ;
+
+    py::enum_<storm::MultiObjectiveModelCheckerEnvironment::PrecisionType>(m, "MultiObjectivePrecisionType", "Type of precision for multi-objective model checking")
+        .value("absolute", storm::MultiObjectiveModelCheckerEnvironment::PrecisionType::Absolute)
+        .value("relative_to_diff", storm::MultiObjectiveModelCheckerEnvironment::PrecisionType::RelativeToDiff)
+    ;
+
+    py::enum_<storm::MultiObjectiveModelCheckerEnvironment::EncodingType>(m, "MultiObjectiveEncodingType", "Encoding type for multi-objective model checking")
+        .value("auto", storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Auto)
+        .value("classic", storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Classic)
+        .value("flow", storm::MultiObjectiveModelCheckerEnvironment::EncodingType::Flow)
+    ;
+
+    // Scheduler class bindings (needed for scheduler restriction)
+    py::enum_<storm::storage::SchedulerClass::MemoryPattern>(m, "SchedulerMemoryPattern", "Memory pattern of a scheduler")
+        .value("arbitrary", storm::storage::SchedulerClass::MemoryPattern::Arbitrary)
+        .value("goal_memory", storm::storage::SchedulerClass::MemoryPattern::GoalMemory)
+        .value("counter", storm::storage::SchedulerClass::MemoryPattern::Counter)
+    ;
+
+    py::class_<storm::storage::SchedulerClass>(m, "SchedulerClass", "Scheduler class restriction")
+        .def(py::init<>())
+        .def_property("deterministic", &storm::storage::SchedulerClass::isDeterministic, [](storm::storage::SchedulerClass& sc, bool v){ sc.setIsDeterministic(v); })
+        .def_property("memory_states",
+            [](storm::storage::SchedulerClass const& sc)->py::object { if (sc.isMemoryBounded()) return py::cast(sc.getMemoryStates()); return py::none(); },
+            [](storm::storage::SchedulerClass& sc, py::object obj){ if (obj.is_none()) sc.unsetMemoryStates(); else sc.setMemoryStates(obj.cast<uint64_t>()); })
+        .def_property_readonly("is_memory_bounded", &storm::storage::SchedulerClass::isMemoryBounded)
+        .def_property_readonly("memory_pattern", &storm::storage::SchedulerClass::getMemoryPattern)
+        .def("set_memory_pattern", [](storm::storage::SchedulerClass& sc, storm::storage::SchedulerClass::MemoryPattern p){ sc.setMemoryPattern(p); })
+        .def("set_positional", &storm::storage::SchedulerClass::setPositional)
+    ;
+
     py::class_<storm::Environment>(m, "Environment", "Environment")
         .def(py::init<>(), "Construct default environment")
         .def_property_readonly("solver_environment", [](storm::Environment& env) -> auto& {return env.solver();}, "solver part of environment")
+        .def_property_readonly("model_checker_environment", [](storm::Environment& env) -> auto& {return env.modelchecker();}, "model checker part of environment")
+    ;
+
+    py::class_<storm::ConditionalModelCheckerEnvironment>(m, "ConditionalModelCheckerEnvironment", "Environment for conditional model checking")
+        .def_property("algorithm", &storm::ConditionalModelCheckerEnvironment::getAlgorithm, &storm::ConditionalModelCheckerEnvironment::setAlgorithm, "algorithm for conditional model checking")
+        .def_property("precision", &storm::ConditionalModelCheckerEnvironment::getPrecision, [](storm::ConditionalModelCheckerEnvironment& env, storm::RationalNumber value){ env.setPrecision(value, false); }, "precision for conditional model checking")
+        .def_property("relative", &storm::ConditionalModelCheckerEnvironment::isRelativePrecision, &storm::ConditionalModelCheckerEnvironment::setRelativePrecision, "whether the precision is relative")
+    ;
+
+    py::class_<storm::ModelCheckerEnvironment>(m, "ModelCheckerEnvironment", "Environment for the model checker")
+        .def_property("steady_state_distribution_algorithm", &storm::ModelCheckerEnvironment::getSteadyStateDistributionAlgorithm, &storm::ModelCheckerEnvironment::setSteadyStateDistributionAlgorithm, "steady state distribution algorithm used")
+        .def_property("ltl2da_tool",
+            [](storm::ModelCheckerEnvironment const& env)->py::object { if (env.isLtl2daToolSet()) return py::cast(env.getLtl2daTool()); return py::none(); },
+            [](storm::ModelCheckerEnvironment& env, py::object obj){ if (obj.is_none()) env.unsetLtl2daTool(); else env.setLtl2daTool(obj.cast<std::string>()); },
+            "Path to external ltl2da tool (None to unset)")
+        .def_property_readonly("conditional", [](storm::ModelCheckerEnvironment& env)->storm::ConditionalModelCheckerEnvironment& { return env.conditional(); }, py::return_value_policy::reference, "Access conditional model checking sub-environment")
+        .def_property_readonly("multi", [](storm::ModelCheckerEnvironment& env)->storm::MultiObjectiveModelCheckerEnvironment& { return env.multi(); }, py::return_value_policy::reference, "Access multi-objective sub-environment")
+    ;
+
+    py::class_<storm::MultiObjectiveModelCheckerEnvironment>(m, "MultiObjectiveModelCheckerEnvironment", "Environment for multi-objective model checking")
+        .def_property("method",
+            [](storm::MultiObjectiveModelCheckerEnvironment const& env){ return env.getMethod(); },
+            &storm::MultiObjectiveModelCheckerEnvironment::setMethod,
+            "multi-objective model checking method")
+        .def_property("precision", &storm::MultiObjectiveModelCheckerEnvironment::getPrecision, &storm::MultiObjectiveModelCheckerEnvironment::setPrecision)
+        .def_property("precision_type", &storm::MultiObjectiveModelCheckerEnvironment::getPrecisionType, &storm::MultiObjectiveModelCheckerEnvironment::setPrecisionType)
+        .def_property("encoding_type", &storm::MultiObjectiveModelCheckerEnvironment::getEncodingType, &storm::MultiObjectiveModelCheckerEnvironment::setEncodingType)
+        .def_property("use_indicator_constraints", &storm::MultiObjectiveModelCheckerEnvironment::getUseIndicatorConstraints, &storm::MultiObjectiveModelCheckerEnvironment::setUseIndicatorConstraints)
+        .def_property("use_bscc_order_encoding", &storm::MultiObjectiveModelCheckerEnvironment::getUseBsccOrderEncoding, &storm::MultiObjectiveModelCheckerEnvironment::setUseBsccOrderEncoding)
+        .def_property("use_redundant_bscc_constraints", &storm::MultiObjectiveModelCheckerEnvironment::getUseRedundantBsccConstraints, &storm::MultiObjectiveModelCheckerEnvironment::setUseRedundantBsccConstraints)
+        .def_property_readonly("export_plot_set", &storm::MultiObjectiveModelCheckerEnvironment::isExportPlotSet)
+        .def_property("plot_path_under_approximation",
+            [](storm::MultiObjectiveModelCheckerEnvironment const& env)->py::object { auto p = env.getPlotPathUnderApproximation(); if (p) return py::cast(*p); return py::none(); },
+            [](storm::MultiObjectiveModelCheckerEnvironment& env, py::object obj){ if (obj.is_none()) env.unsetPlotPathUnderApproximation(); else env.setPlotPathUnderApproximation(obj.cast<std::string>()); })
+        .def_property("plot_path_over_approximation",
+            [](storm::MultiObjectiveModelCheckerEnvironment const& env)->py::object { auto p = env.getPlotPathOverApproximation(); if (p) return py::cast(*p); return py::none(); },
+            [](storm::MultiObjectiveModelCheckerEnvironment& env, py::object obj){ if (obj.is_none()) env.unsetPlotPathOverApproximation(); else env.setPlotPathOverApproximation(obj.cast<std::string>()); })
+        .def_property("plot_path_pareto_points",
+            [](storm::MultiObjectiveModelCheckerEnvironment const& env)->py::object { auto p = env.getPlotPathParetoPoints(); if (p) return py::cast(*p); return py::none(); },
+            [](storm::MultiObjectiveModelCheckerEnvironment& env, py::object obj){ if (obj.is_none()) env.unsetPlotPathParetoPoints(); else env.setPlotPathParetoPoints(obj.cast<std::string>()); })
+        .def_property("max_steps",
+            [](storm::MultiObjectiveModelCheckerEnvironment const& env)->py::object { if (env.isMaxStepsSet()) return py::cast(env.getMaxSteps()); return py::none(); },
+            [](storm::MultiObjectiveModelCheckerEnvironment& env, py::object obj){ if (obj.is_none()) env.unsetMaxSteps(); else env.setMaxSteps(obj.cast<uint64_t>()); })
+        .def_property("scheduler_restriction",
+            [](storm::MultiObjectiveModelCheckerEnvironment const& env)->py::object { if (env.isSchedulerRestrictionSet()) return py::cast(env.getSchedulerRestriction()); return py::none(); },
+            [](storm::MultiObjectiveModelCheckerEnvironment& env, py::object obj){ if (obj.is_none()) env.unsetSchedulerRestriction(); else env.setSchedulerRestriction(obj.cast<storm::storage::SchedulerClass>()); })
+        .def_property("print_results", &storm::MultiObjectiveModelCheckerEnvironment::isPrintResultsSet, &storm::MultiObjectiveModelCheckerEnvironment::setPrintResults)
+        .def_property("lexicographic_model_checking", &storm::MultiObjectiveModelCheckerEnvironment::isLexicographicModelCheckingSet, &storm::MultiObjectiveModelCheckerEnvironment::setLexicographicModelChecking)
     ;
 
     py::class_<storm::SolverEnvironment>(m, "SolverEnvironment", "Environment for solvers")
@@ -62,4 +171,3 @@ void define_environment(py::module& m) {
 
 
 }
-
diff --git a/src/core/result.cpp b/src/core/result.cpp
index c4618e9250..4f111786fd 100644
--- a/src/core/result.cpp
+++ b/src/core/result.cpp
@@ -28,7 +28,7 @@ std::shared_ptr<storm::modelchecker::QualitativeCheckResult> createFilterSymboli
 void define_result(py::module& m) {
 
     // CheckResult
-    py::class_<storm::modelchecker::CheckResult, std::shared_ptr<storm::modelchecker::CheckResult>>(m, "_CheckResult", "Base class for all modelchecking results")
+    auto checkResult = py::class_<storm::modelchecker::CheckResult, std::shared_ptr<storm::modelchecker::CheckResult>>(m, "_CheckResult", "Base class for all modelchecking results")
         .def_property_readonly("_symbolic", &storm::modelchecker::CheckResult::isSymbolic, "Flag if result is symbolic")
         .def_property_readonly("_hybrid", &storm::modelchecker::CheckResult::isHybrid, "Flag if result is hybrid")
         .def_property_readonly("_quantitative", &storm::modelchecker::CheckResult::isQuantitative, "Flag if result is quantitative")
@@ -69,10 +69,10 @@ void define_result(py::module& m) {
     ;
 
     // QualitativeCheckResult
-    py::class_<storm::modelchecker::QualitativeCheckResult, std::shared_ptr<storm::modelchecker::QualitativeCheckResult>, storm::modelchecker::CheckResult>(m, "_QualitativeCheckResult", "Abstract class for qualitative model checking results");
+    py::class_<storm::modelchecker::QualitativeCheckResult, std::shared_ptr<storm::modelchecker::QualitativeCheckResult>> qualitativeCheckResult(m, "_QualitativeCheckResult", "Abstract class for qualitative model checking results", checkResult);
 
-    py::class_<storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>, std::shared_ptr<storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>>, storm::modelchecker::QualitativeCheckResult>(m, "SymbolicQualitativeCheckResult", "Symbolic qualitative model checking result")
-        .def("get_truth_values", &storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>::getTruthValuesVector, "Get Dd representing the truth values")
+    py::class_<storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>, std::shared_ptr<storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>>>(m, "SymbolicQualitativeCheckResult", "Symbolic qualitative model checking result", qualitativeCheckResult)
+            .def("get_truth_values", &storm::modelchecker::SymbolicQualitativeCheckResult<storm::dd::DdType::Sylvan>::getTruthValuesVector, "Get Dd representing the truth values")
     ;
 }
 
@@ -84,6 +84,7 @@ void define_typed_result(py::module& m, std::string const& vtSuffix) {
                 return result[state];
             }, py::arg("state"), "Get result for given state")
         .def("get_truth_values", &storm::modelchecker::ExplicitQualitativeCheckResult<ValueType>::getTruthValuesVector, "Get BitVector representing the truth values")
+        .def_property_readonly("scheduler", [](storm::modelchecker::ExplicitQualitativeCheckResult<ValueType> const& res) {return res.getScheduler();}, "get scheduler")
     ;
 
     py::class_<storm::modelchecker::QuantitativeCheckResult<ValueType>, std::shared_ptr<storm::modelchecker::QuantitativeCheckResult<ValueType>>, storm::modelchecker::CheckResult> quantitativeCheckResult(m, ("_" + vtSuffix + "QuantitativeCheckResult").c_str(), "Abstract class for quantitative model checking results");
@@ -126,4 +127,4 @@ void define_typed_result(py::module& m, std::string const& vtSuffix) {
 
 template void define_typed_result<double>(py::module& m, std::string const& vtSuffix);
 template void define_typed_result<storm::RationalNumber>(py::module& m, std::string const& vtSuffix);
-template void define_typed_result<storm::RationalFunction>(py::module& m, std::string const& vtSuffix);
\ No newline at end of file
+template void define_typed_result<storm::RationalFunction>(py::module& m, std::string const& vtSuffix);
diff --git a/src/core/transformation.cpp b/src/core/transformation.cpp
index c7d99ac6ed..cf43d7a627 100644
--- a/src/core/transformation.cpp
+++ b/src/core/transformation.cpp
@@ -5,6 +5,7 @@
 #include "storm/models/symbolic/StandardRewardModel.h"
 #include "storm/transformer/SubsystemBuilder.h"
 #include "storm/transformer/EndComponentEliminator.h"
+#include "storm/transformer/AddUncertainty.h"
 
 // Thin wrappers.
 template<typename VT>
@@ -84,6 +85,16 @@ void define_transformation_typed(py::module& m, std::string const& vtSuffix) {
     m.def(("_construct_subsystem_" + vtSuffix).c_str(), &constructSubsystem<ValueType>, "build a subsystem of a sparse model");
 }
 
+template<typename ValueType>
+void define_transformation_typed_only_numbers(py::module& m, std::string const& vtSuffix) {
+    py::class_<storm::transformer::AddUncertainty<ValueType>>(m, ("AddUncertainty" + vtSuffix).c_str(), "Transform model into interval model with specified uncertainty")
+        .def(py::init<std::shared_ptr<storm::models::sparse::Model<ValueType>> const&>(), py::arg("model"))
+        .def("transform", &storm::transformer::AddUncertainty<ValueType>::transform, "transform the model", py::arg("additiveUncertainty"), py::arg("minimalValue") = storm::utility::convertNumber<ValueType>(0.0001), py::arg("maxSuccessors") = std::optional<uint64_t>{});
+}
+
 template void define_transformation_typed<double>(py::module& m, std::string const& vtSuffix);
 template void define_transformation_typed<storm::RationalNumber>(py::module& m, std::string const& vtSuffix);
 template void define_transformation_typed<storm::RationalFunction>(py::module& m, std::string const& vtSuffix);
+
+template void define_transformation_typed_only_numbers<double>(py::module& m, std::string const& vtSuffix);
+template void define_transformation_typed_only_numbers<storm::RationalNumber>(py::module& m, std::string const& vtSuffix);
diff --git a/src/core/transformation.h b/src/core/transformation.h
index 7bd010bb8d..b9691d82cc 100644
--- a/src/core/transformation.h
+++ b/src/core/transformation.h
@@ -5,3 +5,5 @@
 void define_transformation(py::module& m);
 template<typename ValueType>
 void define_transformation_typed(py::module& m, std::string const& suffix);
+template<typename ValueType>
+void define_transformation_typed_only_numbers(py::module& m, std::string const& vtSuffix);
diff --git a/src/logic/formulae.cpp b/src/logic/formulae.cpp
index 46ccaed610..c5364bddc2 100644
--- a/src/logic/formulae.cpp
+++ b/src/logic/formulae.cpp
@@ -32,13 +32,15 @@ void define_formulae(py::module& m) {
         .def_property_readonly("is_bounded_until_formula", &storm::logic::Formula::isBoundedUntilFormula)
         .def_property_readonly("is_until_formula", &storm::logic::Formula::isUntilFormula)
         .def_property_readonly("is_multi_objective_formula", &storm::logic::Formula::isMultiObjectiveFormula)
+        .def("_as_eventually_formula", [](storm::logic::Formula const& f) { return f.asEventuallyFormula(); }, "Get as eventually formula")
             ;
 
     // Path Formulae
     py::class_<storm::logic::PathFormula, std::shared_ptr<storm::logic::PathFormula>> pathFormula(m, "PathFormula", "Formula about the probability of a set of paths in an automaton", formula);
     py::class_<storm::logic::UnaryPathFormula, std::shared_ptr<storm::logic::UnaryPathFormula>> unaryPathFormula(m, "UnaryPathFormula", "Path formula with one operand", pathFormula);
     unaryPathFormula.def_property_readonly("subformula", &storm::logic::UnaryPathFormula::getSubformula, "the subformula");
-    py::class_<storm::logic::EventuallyFormula, std::shared_ptr<storm::logic::EventuallyFormula>>(m, "EventuallyFormula", "Formula for eventually", unaryPathFormula);
+    py::class_<storm::logic::EventuallyFormula, std::shared_ptr<storm::logic::EventuallyFormula>>(m, "EventuallyFormula", "Formula for eventually", unaryPathFormula)
+    .def_property_readonly("subformula", &storm::logic::EventuallyFormula::getSubformula, "the subformula");
     py::class_<storm::logic::GloballyFormula, std::shared_ptr<storm::logic::GloballyFormula>>(m, "GloballyFormula", "Formula for globally", unaryPathFormula);
     py::class_<storm::logic::BinaryPathFormula, std::shared_ptr<storm::logic::BinaryPathFormula>> binaryPathFormula(m, "BinaryPathFormula", "Path formula with two operands", pathFormula);
     binaryPathFormula.def_property_readonly("left_subformula", &storm::logic::BinaryPathFormula::getLeftSubformula);
@@ -49,7 +51,9 @@ void define_formulae(py::module& m) {
     .def_property_readonly("upper_bound_expression", [](storm::logic::BoundedUntilFormula const& form) { return form.getUpperBound(); } )
     .def_property_readonly("left_subformula", [](storm::logic::BoundedUntilFormula const& form) -> storm::logic::Formula const& { return form.getLeftSubformula(); }, py::return_value_policy::reference_internal)
     .def_property_readonly("right_subformula", [](storm::logic::BoundedUntilFormula const& form)-> storm::logic::Formula const& { return form.getRightSubformula(); }, py::return_value_policy::reference_internal);
-    py::class_<storm::logic::ConditionalFormula, std::shared_ptr<storm::logic::ConditionalFormula>>(m, "ConditionalFormula", "Formula with the right hand side being a condition.", formula);
+    py::class_<storm::logic::ConditionalFormula, std::shared_ptr<storm::logic::ConditionalFormula>>(m, "ConditionalFormula", "Formula with the right hand side being a condition.", formula)
+    .def_property_readonly("main_subformula", &storm::logic::ConditionalFormula::getSubformula, "the subformula")
+    .def_property_readonly("conditional_subformula", &storm::logic::ConditionalFormula::getConditionFormula, "the conditional subformula");
     py::class_<storm::logic::UntilFormula, std::shared_ptr<storm::logic::UntilFormula>>(m, "UntilFormula", "Path Formula for unbounded until", binaryPathFormula);
 
     // Reward Path Formulae
diff --git a/src/mod_core.cpp b/src/mod_core.cpp
index 2422a6ab71..76a7fee234 100644
--- a/src/mod_core.cpp
+++ b/src/mod_core.cpp
@@ -43,8 +43,9 @@ PYBIND11_MODULE(_core, m) {
     define_transformation_typed<double>(m, "Double");
     define_transformation_typed<storm::RationalNumber>(m, "Exact");
     define_transformation_typed<storm::RationalFunction>(m, "RatFunc");
+    define_transformation_typed_only_numbers<double>(m, "Double");
+    define_transformation_typed_only_numbers<storm::RationalNumber>(m, "Exact");
     define_sparse_model_simulator<double>(m, "Double");
     define_sparse_model_simulator<storm::RationalNumber>(m, "Exact");
     define_prism_program_simulator<double>(m, "Double");
-
 }
diff --git a/src/mod_pomdp.cpp b/src/mod_pomdp.cpp
index a26a9e50f0..6cdd333046 100644
--- a/src/mod_pomdp.cpp
+++ b/src/mod_pomdp.cpp
@@ -1,12 +1,15 @@
 
 #include "common.h"
 
-#include "pomdp/tracker.h"
-#include "pomdp/qualitative_analysis.h"
-#include "pomdp/transformations.h"
+#include <storm/adapters/RationalFunctionAdapter.h>
+#include <storm/adapters/RationalNumberAdapter.h>
+#include <storm/adapters/IntervalAdapter.h>
+#include "pomdp/generator.h"
 #include "pomdp/memory.h"
+#include "pomdp/qualitative_analysis.h"
 #include "pomdp/quantitative_analysis.h"
-#include <storm/adapters/RationalFunctionAdapter.h>
+#include "pomdp/tracker.h"
+#include "pomdp/transformations.h"
 
 PYBIND11_MODULE(_pomdp, m) {
     m.doc() = "Functionality for POMDP analysis";
@@ -21,9 +24,18 @@ PYBIND11_MODULE(_pomdp, m) {
     define_qualitative_policy_search_nt(m);
     define_memory(m);
     define_transformations_nt(m);
+
     define_transformations<double>(m, "Double");
     define_transformations<storm::RationalNumber>(m, "Exact");
-    define_belief_exploration<double>(m, "Double");
-
     define_transformations<storm::RationalFunction>(m, "Rf");
+
+    define_transformations_int<double>(m, "Double");
+    define_transformations_int<storm::RationalNumber>(m, "Exact");
+    define_transformations_int<storm::RationalFunction>(m, "Rf");
+    define_transformations_int<storm::Interval>(m, "Interval");
+    define_transformations_int<storm::RationalInterval>(m, "RationalInterval");
+
+    define_belief_exploration<double>(m, "Double");
+    define_verimon_generator<double>(m, "Double");
+    define_verimon_generator<storm::RationalNumber>(m, "Exact");
 }
diff --git a/src/pomdp/generator.cpp b/src/pomdp/generator.cpp
new file mode 100644
index 0000000000..8093d9d443
--- /dev/null
+++ b/src/pomdp/generator.cpp
@@ -0,0 +1,48 @@
+#include "generator.h"
+#include <cstdint>
+#include <string>
+#include "storm-pomdp/generator/GenerateMonitorVerifier.h"
+#include "storm/adapters/RationalNumberAdapter.h"
+#include "storm/storage/expressions/ExpressionManager.h"
+
+template<typename ValueType>
+using GenerateMonitorVerifier = storm::generator::GenerateMonitorVerifier<ValueType>;
+template<typename ValueType>
+using SparseDtmc = storm::models::sparse::Dtmc<ValueType>;
+template<typename ValueType>
+using SparseMdp = storm::models::sparse::Mdp<ValueType>;
+template<typename ValueType>
+using SparsePomdp = storm::models::sparse::Pomdp<ValueType>;
+template<typename ValueType>
+using GenerateMonitorVerifierOptions = typename storm::generator::GenerateMonitorVerifier<ValueType>::Options;
+
+template<typename ValueType>
+void define_verimon_generator(py::module &m, std::string const &vtSuffix) {
+    py::class_<storm::generator::MonitorVerifier<ValueType>, std::shared_ptr<storm::generator::MonitorVerifier<ValueType>>> mv(
+        m, ("MonitorVerifier" + vtSuffix).c_str(), "Container for monitor verifier POMDP with associated objects");
+    mv.def(py::init<const SparsePomdp<ValueType> &, const std::map<std::pair<uint32_t, bool>, uint32_t> &, const std::map<uint32_t, std::string> &>(),
+           py::arg("product"), py::arg("observation_map"), py::arg("default_action_map"));
+    mv.def("get_product", &storm::generator::MonitorVerifier<ValueType>::getProduct, py::return_value_policy::copy);
+    mv.def_property_readonly("observation_map", &storm::generator::MonitorVerifier<ValueType>::getObservationMap, py::return_value_policy::copy);
+    mv.def_property_readonly("default_action_map", &storm::generator::MonitorVerifier<ValueType>::getObservationDefaultAction, py::return_value_policy::copy);
+
+    py::class_<storm::generator::GenerateMonitorVerifier<ValueType>> gmv(m, ("GenerateMonitorVerifier" + vtSuffix).c_str(),
+                                                                         "Generator of POMDP used in verifying monitors against markov chains");
+    gmv.def(py::init<SparseDtmc<ValueType> const &, SparseMdp<ValueType> const &, std::shared_ptr<storm::expressions::ExpressionManager> &,
+                     GenerateMonitorVerifierOptions<ValueType> const &>(),
+            py::arg("mc"), py::arg("monitor"), py::arg("expr_manager"), py::arg("options"));
+    gmv.def("create_product", &storm::generator::GenerateMonitorVerifier<ValueType>::createProduct, py::return_value_policy::copy,
+            "Created the verification POMDP");
+    gmv.def("set_risk", &storm::generator::GenerateMonitorVerifier<ValueType>::setRisk, py::arg("risk"));
+
+    py::class_<GenerateMonitorVerifierOptions<ValueType>> gmvopts(m, ("GenerateMonitorVerifier" + vtSuffix + "Options").c_str(),
+                                                                  "Options for corresponding generator");
+    gmvopts.def(py::init<>());
+    gmvopts.def_readwrite("accepting_label", &GenerateMonitorVerifierOptions<ValueType>::acceptingLabel);
+    gmvopts.def_readwrite("step_prefix", &GenerateMonitorVerifierOptions<ValueType>::stepPrefix);
+    gmvopts.def_readwrite("horizon_label", &GenerateMonitorVerifierOptions<ValueType>::horizonLabel);
+    gmvopts.def_readwrite("use_restart_semantics", &GenerateMonitorVerifierOptions<ValueType>::useRestartSemantics);
+}
+
+template void define_verimon_generator<double>(py::module &m, std::string const &vtSuffix);
+template void define_verimon_generator<storm::RationalNumber>(py::module &m, std::string const &vtSuffix);
diff --git a/src/pomdp/generator.h b/src/pomdp/generator.h
new file mode 100644
index 0000000000..bd28415441
--- /dev/null
+++ b/src/pomdp/generator.h
@@ -0,0 +1,5 @@
+#pragma once
+#include "common.h"
+
+template<typename ValueType>
+void define_verimon_generator(py::module& m, std::string const& vtSuffix);
diff --git a/src/pomdp/transformations.cpp b/src/pomdp/transformations.cpp
index 2eb05ef222..01cff7858c 100644
--- a/src/pomdp/transformations.cpp
+++ b/src/pomdp/transformations.cpp
@@ -1,41 +1,49 @@
 #include "transformations.h"
 
-#include "storm-pomdp/transformer/PomdpMemoryUnfolder.h"
-#include "storm-pomdp/transformer/BinaryPomdpTransformer.h"
 #include "storm-pomdp/transformer/ApplyFiniteSchedulerToPomdp.h"
+#include "storm-pomdp/transformer/BinaryPomdpTransformer.h"
 #include "storm-pomdp/transformer/ObservationTraceUnfolder.h"
+#include "storm-pomdp/transformer/PomdpMemoryUnfolder.h"
 #include "storm/adapters/RationalFunctionAdapter.h"
 #include "storm/storage/expressions/ExpressionManager.h"
 #include "storm/transformer/MakePOMDPCanonic.h"
 
 template<typename ValueType>
-std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> make_canonic(storm::models::sparse::Pomdp<ValueType> const& pomdp) {
+std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> make_canonic(storm::models::sparse::Pomdp<ValueType> const &pomdp) {
     storm::transformer::MakePOMDPCanonic<ValueType> makeCanonic(pomdp);
     return makeCanonic.transform();
 }
 
 template<typename ValueType>
-std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> unfold_memory(storm::models::sparse::Pomdp<ValueType> const& pomdp, storm::storage::PomdpMemory const& memory, bool addMemoryLabels, bool keepStateValuations) {
+std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> unfold_memory(storm::models::sparse::Pomdp<ValueType> const &pomdp,
+                                                                       storm::storage::PomdpMemory const &memory, bool addMemoryLabels,
+                                                                       bool keepStateValuations) {
     storm::transformer::PomdpMemoryUnfolder<ValueType> unfolder(pomdp, memory, addMemoryLabels, keepStateValuations);
     return unfolder.transform();
 }
 
 template<typename ValueType>
-std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> make_simple(storm::models::sparse::Pomdp<ValueType> const& pomdp, bool keepStateValuations) {
+std::shared_ptr<storm::models::sparse::Pomdp<ValueType>> make_simple(storm::models::sparse::Pomdp<ValueType> const &pomdp, bool keepStateValuations) {
     storm::transformer::BinaryPomdpTransformer<ValueType> transformer;
-    return transformer.transform(pomdp,true, keepStateValuations).transformedPomdp;
+    return transformer.transform(pomdp, true, keepStateValuations).transformedPomdp;
 }
 
 template<typename ValueType>
-std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> apply_unknown_fsc(storm::models::sparse::Pomdp<ValueType> const& pomdp, storm::transformer::PomdpFscApplicationMode const& applicationMode) {
+std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> apply_unknown_fsc(storm::models::sparse::Pomdp<ValueType> const &pomdp,
+                                                                                         storm::transformer::PomdpFscApplicationMode const &applicationMode) {
     storm::transformer::ApplyFiniteSchedulerToPomdp<ValueType> transformer(pomdp);
     return transformer.transform(applicationMode);
 }
 
 template<typename ValueType>
-std::shared_ptr<storm::models::sparse::Mdp<ValueType>> unfold_trace(storm::models::sparse::Pomdp<ValueType> const& pomdp, std::shared_ptr<storm::expressions::ExpressionManager>& exprManager, std::vector<uint32_t> const& observationTrace, std::vector<ValueType> const& riskDef ) {
-    storm::pomdp::ObservationTraceUnfolder<ValueType> transformer(pomdp, exprManager);
-    return transformer.transform(observationTrace, riskDef);
+std::shared_ptr<storm::models::sparse::Mdp<ValueType>> unfold_trace(storm::models::sparse::Pomdp<ValueType> const &pomdp,
+                                                                    std::shared_ptr<storm::expressions::ExpressionManager> &exprManager,
+                                                                    std::vector<uint32_t> const &observationTrace, std::vector<ValueType> const &riskDef,
+                                                                    bool restartSemantics = true) {
+    storm::pomdp::ObservationTraceUnfolderOptions options = storm::pomdp::ObservationTraceUnfolderOptions();
+    options.useRestartSemantics = restartSemantics;
+    storm::pomdp::ObservationTraceUnfolder<ValueType> transformer(pomdp, riskDef, exprManager, options);
+    return transformer.transform(observationTrace);
 }
 
 // STANDARD, SIMPLE_LINEAR, SIMPLE_LINEAR_INVERSE, SIMPLE_LOG, FULL
@@ -54,20 +62,32 @@ void define_transformations_nt(py::module &m) {
 }
 
 template<typename ValueType>
-void define_transformations(py::module& m, std::string const& vtSuffix) {
+void define_transformations(py::module &m, std::string const &vtSuffix) {
     m.def(("_make_canonic_" + vtSuffix).c_str(), &make_canonic<ValueType>, "Return a canonicly-ordered POMDP", py::arg("pomdp"));
     m.def(("_unfold_memory_" + vtSuffix).c_str(), &unfold_memory<ValueType>, "Unfold memory into a POMDP", py::arg("pomdp"), py::arg("memorystructure"), py::arg("memorylabels") = false, py::arg("keep_state_valuations")=false);
     m.def(("_make_simple_"+ vtSuffix).c_str(), &make_simple<ValueType>, "Make POMDP simple", py::arg("pomdp"), py::arg("keep_state_valuations")=false);
     m.def(("_apply_unknown_fsc_" + vtSuffix).c_str(), &apply_unknown_fsc<ValueType>, "Apply unknown FSC",py::arg("pomdp"), py::arg("application_mode")=storm::transformer::PomdpFscApplicationMode::SIMPLE_LINEAR);
-    //m.def(("_unfold_trace_" + vtSuffix).c_str(), &unfold_trace<ValueType>, "Unfold observed trace", py::arg("pomdp"), py::arg("expression_manager"),py::arg("observation_trace"), py::arg("risk_definition"));
+}
 
-    py::class_<storm::pomdp::ObservationTraceUnfolder<ValueType>> unfolder(m, ("ObservationTraceUnfolder" + vtSuffix).c_str(), "Unfolds observation traces in models");
-    unfolder.def(py::init<storm::models::sparse::Pomdp<ValueType> const&,  std::vector<ValueType> const&, std::shared_ptr<storm::expressions::ExpressionManager>&, storm::pomdp::ObservationTraceUnfolderOptions const &>(), py::arg("model"), py::arg("risk"), py::arg("expression_manager"), py::arg("options"), py::keep_alive<2, 1>());
+template<typename ValueType>
+void define_transformations_int(py::module &m, std::string const &vtSuffix) {
+    py::class_<storm::pomdp::ObservationTraceUnfolder<ValueType>> unfolder(m, ("ObservationTraceUnfolder" + vtSuffix).c_str(),
+                                                                           "Unfolds observation traces in models");
+    unfolder.def(py::init<storm::models::sparse::Pomdp<ValueType>, std::vector<ValueType> const &, std::shared_ptr<storm::expressions::ExpressionManager> &,
+                          storm::pomdp::ObservationTraceUnfolderOptions const &>(),
+                 py::arg("model"), py::arg("risk"), py::arg("expression_manager"), py::arg("options"), py::keep_alive<2, 1>());
+    unfolder.def("is_restart_semantics_set", &storm::pomdp::ObservationTraceUnfolder<ValueType>::isRestartSemanticsSet);
     unfolder.def("transform", &storm::pomdp::ObservationTraceUnfolder<ValueType>::transform, py::arg("trace"));
-    unfolder.def("extend", &storm::pomdp::ObservationTraceUnfolder<ValueType>::extend, py::arg("new_observation"));
     unfolder.def("reset", &storm::pomdp::ObservationTraceUnfolder<ValueType>::reset, py::arg("new_observation"));
+    unfolder.def("extend", &storm::pomdp::ObservationTraceUnfolder<ValueType>::extend, py::arg("new_observation"));
 }
 
-template void define_transformations<double>(py::module& m, std::string const& vtSuffix);
-template void define_transformations<storm::RationalNumber>(py::module& m, std::string const& vtSuffix);
-template void define_transformations<storm::RationalFunction>(py::module& m, std::string const& vtSuffix);
+template void define_transformations<double>(py::module &m, std::string const &vtSuffix);
+template void define_transformations<storm::RationalNumber>(py::module &m, std::string const &vtSuffix);
+template void define_transformations<storm::RationalFunction>(py::module &m, std::string const &vtSuffix);
+
+template void define_transformations_int<double>(py::module &m, std::string const &vtSuffix);
+template void define_transformations_int<storm::RationalNumber>(py::module &m, std::string const &vtSuffix);
+template void define_transformations_int<storm::RationalFunction>(py::module &m, std::string const &vtSuffix);
+template void define_transformations_int<storm::Interval>(py::module &m, std::string const &vtSuffix);
+template void define_transformations_int<storm::RationalInterval>(py::module &m, std::string const &vtSuffix);
diff --git a/src/pomdp/transformations.h b/src/pomdp/transformations.h
index 4410946f9c..fca131f8ae 100644
--- a/src/pomdp/transformations.h
+++ b/src/pomdp/transformations.h
@@ -2,6 +2,8 @@
 
 #include "common.h"
 
-void define_transformations_nt(py::module& m);
-template<typename VT>
-void define_transformations(py::module& m, std::string const& vtSuffix);
+void define_transformations_nt(py::module &m);
+template <typename VT>
+void define_transformations(py::module &m, std::string const &vtSuffix);
+template <typename VT>
+void define_transformations_int(py::module &m, std::string const &vtSuffix);
diff --git a/src/storage/scheduler.cpp b/src/storage/scheduler.cpp
index 05a6d81c0e..b2cade6195 100644
--- a/src/storage/scheduler.cpp
+++ b/src/storage/scheduler.cpp
@@ -31,6 +31,13 @@ void define_scheduler(py::module& m, std::string vt_suffix) {
                     s.printJsonToStream(str, model, skipUniqueChoices, skipDontCareStates);
                     return str.str();
                 }, py::arg("model"), py::arg("skip_unique_choices") = false, py::arg("skip_dont_care_states") = false)
+            .def("to_str", [](Scheduler const& s, std::shared_ptr<storm::models::sparse::Model<ValueType>> model, bool skipUniqueChoices,
+                               bool skipDontCareStates) {
+                    std::stringstream str;
+                    s.printToStream(str, model, skipUniqueChoices, skipDontCareStates);
+                    return str.str();
+                }, py::arg("model") = nullptr, py::arg("skip_unique_choices") = false, py::arg("skip_dont_care_states") = false)
+            .def("get_memoryless_scheduler_for_memory_state", &Scheduler::getMemorylessSchedulerForMemoryState, py::arg("memory_state") = 0, "Get the memoryless scheduler corresponding to the given memory state")
     ;
 
     if constexpr (!storm::IsIntervalType<ValueType>) {
@@ -43,6 +50,7 @@ void define_scheduler(py::module& m, std::string vt_suffix) {
         if constexpr (!std::is_same_v<ValueType, storm::RationalFunction>) {
             // Conversion from RationalFunction to Interval not implemented
             scheduler.def("cast_to_interval_datatype", &Scheduler::template toValueType<storm::Interval>, "Construct the scheduler with `interval` value type");
+            scheduler.def("cast_to_exact_interval_datatype", &Scheduler::template toValueType<storm::RationalInterval>, "Construct the scheduler with `interval` value type");
         }
     }