diff --git a/lib/stormpy/__init__.py b/lib/stormpy/__init__.py
index 02be704ce9..a535e85b12 100644
--- a/lib/stormpy/__init__.py
+++ b/lib/stormpy/__init__.py
@@ -27,6 +27,7 @@ class _ValueType(Enum):
     EXACT = 2
     PARAMETRIC = 3
     INTERVAL = 4
+    EXACT_INTERVAL = 5
 
 
 def _convert_sparse_model(model, value_type=_ValueType.DOUBLE):
@@ -103,6 +104,22 @@ def _convert_sparse_model(model, value_type=_ValueType.DOUBLE):
                 return model._as_sparse_ismg()
             else:
                 raise stormpy.exceptions.StormError("Not supported interval model constructed")
+        case _ValueType.EXACT_INTERVAL:
+            assert model.supports_uncertainty and model.is_exact
+            if model.model_type == ModelType.DTMC:
+                return model._as_sparse_exact_idtmc()
+            elif model.model_type == ModelType.MDP:
+                return model._as_sparse_exact_imdp()
+            elif model.model_type == ModelType.POMDP:
+                return model._as_sparse_exact_ipomdp()
+            elif model.model_type == ModelType.CTMC:
+                return model._as_sparse_exact_ictmc()
+            elif model.model_type == ModelType.MA:
+                return model._as_sparse_exact_ima()
+            elif model.model_type == ModelType.SMG:
+                return model._as_sparse_exact_ismg()
+            else:
+                raise stormpy.exceptions.StormError("Not supported exact interval model constructed")
         case _:
             raise stormpy.exceptions.StormError("Not supported model type constructed")
 
@@ -238,6 +255,25 @@ def build_sparse_interval_model(symbolic_description, properties=None):
     return _convert_sparse_model(intermediate, value_type=_ValueType.INTERVAL)
 
 
+def build_sparse_exact_interval_model(symbolic_description, properties=None):
+    """
+    Build an exact interval model in sparse representation from a symbolic description.
+
+    :param symbolic_description: Symbolic model description to translate into a model.
+    :param List[Property] properties: List of properties that should be preserved during the translation. If None, then all properties are preserved.
+    :return: Exact interval model in sparse representation.
+    """
+    if not symbolic_description.undefined_constants_are_graph_preserving:
+        raise stormpy.exceptions.StormError("Program still contains undefined constants")
+
+    if properties:
+        formulae = [(prop.raw_formula if isinstance(prop, Property) else prop) for prop in properties]
+        intermediate = _core._build_sparse_exact_interval_model_from_symbolic_description(symbolic_description, formulae)
+    else:
+        intermediate = _core._build_sparse_exact_interval_model_from_symbolic_description(symbolic_description)
+    return _convert_sparse_model(intermediate, value_type=_ValueType.EXACT_INTERVAL)
+
+
 def build_symbolic_model(symbolic_description, properties=None):
     """
     Build a model in symbolic representation from a symbolic description.
@@ -312,6 +348,18 @@ def build_interval_model_from_drn(file, options=DirectEncodingParserOptions()):
     return _convert_sparse_model(intermediate, value_type=_ValueType.INTERVAL)
 
 
+def build_exact_interval_model_from_drn(file, options=DirectEncodingParserOptions()):
+    """
+    Build an exact interval model in sparse representation from the explicit DRN representation.
+
+    :param String file: DRN file containing the model.
+    :param DirectEncodingParserOptions: Options for the parser.
+    :return: Exact Interval model in sparse representation.
+    """
+    intermediate = _core._build_sparse_exact_interval_model_from_drn(file, options)
+    return _convert_sparse_model(intermediate, value_type=_ValueType.EXACT_INTERVAL)
+
+
 def perform_bisimulation(model, properties, bisimulation_type, graph_preserving=True):
     """
     Perform bisimulation on model.
@@ -741,6 +789,8 @@ def export_to_drn(model, file, options=DirectEncodingExporterOptions()):
     """
     if model.supports_parameters:
         return _core._export_parametric_to_drn(model, file, options)
+    if model.supports_uncertainty and model.is_exact:
+        return _core._export_exact_to_drn_interval(model, file, options)
     if model.supports_uncertainty:
         return _core._export_to_drn_interval(model, file, options)
     if model.is_exact:
diff --git a/lib/stormpy/storage/__init__.py b/lib/stormpy/storage/__init__.py
index eea332c77f..cf2ad4a227 100644
--- a/lib/stormpy/storage/__init__.py
+++ b/lib/stormpy/storage/__init__.py
@@ -69,6 +69,8 @@ def get_maximal_end_components(model):
     """
     if model.supports_parameters:
         return stormpy.MaximalEndComponentDecomposition_ratfunc(model)
+    elif model.supports_uncertainty and model.is_exact:
+        return stormpy.MaximalEndComponentDecomposition_ratinterval(model)
     elif model.is_exact:
         return stormpy.MaximalEndComponentDecomposition_exact(model)
     elif model.supports_uncertainty:
diff --git a/src/core/core.cpp b/src/core/core.cpp
index b93e53f1b2..29335f90b1 100644
--- a/src/core/core.cpp
+++ b/src/core/core.cpp
@@ -124,16 +124,19 @@ void define_build(py::module& m) {
     m.def("_build_sparse_exact_model_from_symbolic_description", &buildSparseModel<storm::RationalNumber>, "Build the model in sparse representation with exact number representation", py::arg("model_description"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>());
     m.def("_build_sparse_parametric_model_from_symbolic_description", &buildSparseModel<storm::RationalFunction>, "Build the parametric model in sparse representation", py::arg("model_description"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>());
     m.def("_build_sparse_interval_model_from_symbolic_description", &buildSparseModel<storm::Interval>, "Build the interval model in sparse representation", py::arg("model_description"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>());
+    m.def("_build_sparse_exact_interval_model_from_symbolic_description", &buildSparseModel<storm::RationalInterval>, "Build the exact interval model in sparse representation", py::arg("model_description"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>());
     m.def("build_sparse_model_with_options", &buildSparseModelWithOptions<double>, "Build the model in sparse representation", py::arg("model_description"), py::arg("options"));
     m.def("build_sparse_exact_model_with_options", &buildSparseModelWithOptions<storm::RationalNumber>, "Build the model in sparse representation with exact number representation", py::arg("model_description"), py::arg("options"));
     m.def("build_sparse_parametric_model_with_options", &buildSparseModelWithOptions<storm::RationalFunction>, "Build the model in sparse representation", py::arg("model_description"), py::arg("options"));
     m.def("build_sparse_interval_model_with_options", &buildSparseModelWithOptions<storm::Interval>, "Build the interval model in sparse representation", py::arg("model_description"), py::arg("options"));
+    m.def("build_sparse_exact_interval_model_with_options", &buildSparseModelWithOptions<storm::RationalInterval>, "Build the exact interval model in sparse representation", py::arg("model_description"), py::arg("options"));
     m.def("_build_symbolic_model_from_symbolic_description", &buildSymbolicModel<storm::dd::DdType::Sylvan, double>, "Build the model in symbolic representation", py::arg("model_description"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>());
     m.def("_build_symbolic_parametric_model_from_symbolic_description", &buildSymbolicModel<storm::dd::DdType::Sylvan, storm::RationalFunction>, "Build the parametric model in symbolic representation", py::arg("model_description"), py::arg("formulas") = std::vector<std::shared_ptr<storm::logic::Formula const>>());
     m.def("_build_sparse_model_from_drn", &storm::api::buildExplicitDRNModel<double>, "Build the model from DRN", py::arg("file"), py::arg("options") = storm::parser::DirectEncodingParserOptions());
     m.def("_build_sparse_exact_model_from_drn", &storm::api::buildExplicitDRNModel<storm::RationalNumber>, "Build the model from DRN", py::arg("file"), py::arg("options") = storm::parser::DirectEncodingParserOptions());
     m.def("_build_sparse_parametric_model_from_drn", &storm::api::buildExplicitDRNModel<storm::RationalFunction>, "Build the parametric model from DRN", py::arg("file"), py::arg("options") = storm::parser::DirectEncodingParserOptions());
     m.def("_build_sparse_interval_model_from_drn", &storm::api::buildExplicitDRNModel<storm::Interval>, "Build the interval model from DRN", py::arg("file"), py::arg("options") = storm::parser::DirectEncodingParserOptions());
+    m.def("_build_sparse_exact_interval_model_from_drn", &storm::api::buildExplicitDRNModel<storm::RationalInterval>, "Build the exact interval model from DRN", py::arg("file"), py::arg("options") = storm::parser::DirectEncodingParserOptions());
     m.def("build_sparse_model_from_explicit", &storm::api::buildExplicitModel<double>, "Build the model model from explicit input", py::arg("transition_file"), py::arg("labeling_file"), py::arg("state_reward_file") = "", py::arg("transition_reward_file") = "", py::arg("choice_labeling_file") = "");
 
     m.def("make_sparse_model_builder", &storm::api::makeExplicitModelBuilder<double>, "Construct a builder instance", py::arg("model_description"), py::arg("options"), py::arg("action_mask") = nullptr);
@@ -207,6 +210,7 @@ void define_export(py::module& m) {
     // Export
     m.def("_export_to_drn", &exportDRN<double>, "Export model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::io::DirectEncodingExporterOptions());
     m.def("_export_to_drn_interval", &exportDRN<storm::Interval>, "Export model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::io::DirectEncodingExporterOptions());
+    m.def("_export_exact_to_drn_interval", &exportDRN<storm::RationalInterval>, "Export model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::io::DirectEncodingExporterOptions());
     m.def("_export_exact_to_drn", &exportDRN<storm::RationalNumber>, "Export model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::io::DirectEncodingExporterOptions());
     m.def("_export_parametric_to_drn", &exportDRN<storm::RationalFunction>, "Export parametric model in DRN format", py::arg("model"), py::arg("file"), py::arg("options")=storm::io::DirectEncodingExporterOptions());
 }
diff --git a/src/core/modelchecking.cpp b/src/core/modelchecking.cpp
index 5ebf428f76..a4b26e74d6 100644
--- a/src/core/modelchecking.cpp
+++ b/src/core/modelchecking.cpp
@@ -54,11 +54,21 @@ std::shared_ptr<storm::modelchecker::CheckResult> checkIntervalDtmc(std::shared_
     return checker.check(env, task);
 }
 
+std::shared_ptr<storm::modelchecker::CheckResult> checkRationalIntervalDtmc(std::shared_ptr<storm::models::sparse::Dtmc<storm::RationalInterval>> dtmc, CheckTask<storm::RationalNumber> const& task, storm::Environment& env) {
+    auto checker = storm::modelchecker::SparseDtmcPrctlModelChecker<storm::models::sparse::Dtmc<storm::RationalInterval>>(*dtmc);
+    return checker.check(env, task);
+}
+
 std::shared_ptr<storm::modelchecker::CheckResult> checkIntervalMdp(std::shared_ptr<storm::models::sparse::Mdp<storm::Interval>> mdp, CheckTask<double> const& task, storm::Environment& env) {
     auto checker = storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<storm::Interval>>(*mdp);
     return checker.check(env, task);
 }
 
+std::shared_ptr<storm::modelchecker::CheckResult> checkRationalIntervalMdp(std::shared_ptr<storm::models::sparse::Mdp<storm::RationalInterval>> mdp, CheckTask<storm::RationalNumber> const& task, storm::Environment& env) {
+    auto checker = storm::modelchecker::SparseMdpPrctlModelChecker<storm::models::sparse::Mdp<storm::RationalInterval>>(*mdp);
+    return checker.check(env, task);
+}
+
 std::vector<double> computeAllUntilProbabilities(storm::Environment const& env, CheckTask<double> const& task, std::shared_ptr<storm::models::sparse::Ctmc<double>> ctmc, storm::storage::BitVector const& phiStates, storm::storage::BitVector const& psiStates) {
     storm::solver::SolveGoal<double> goal(*ctmc, task);
     return storm::modelchecker::helper::SparseCtmcCslHelper::computeAllUntilProbabilities(env, std::move(goal), ctmc->getTransitionMatrix(), ctmc->getExitRateVector(), ctmc->getInitialStates(), phiStates, psiStates);
@@ -146,7 +156,9 @@ void define_modelchecking(py::module& m) {
     m.def("_model_checking_hybrid_engine", &modelCheckingHybridEngine<storm::dd::DdType::Sylvan, double>, "Perform model checking using the hybrid engine", py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment());
     m.def("_parametric_model_checking_hybrid_engine", &modelCheckingHybridEngine<storm::dd::DdType::Sylvan, storm::RationalFunction>, "Perform parametric model checking using the hybrid engine", py::arg("model"), py::arg("task"), py::arg("environment") = storm::Environment());
     m.def("check_interval_dtmc", &checkIntervalDtmc, "Check interval DTMC");
+    m.def("check_exact_interval_dtmc", &checkRationalIntervalDtmc, "Check exact interval DTMC");
     m.def("check_interval_mdp", &checkIntervalMdp, "Check interval MDP");
+    m.def("check_exact_interval_mdp", &checkRationalIntervalMdp, "Check exact interval MDP");
     m.def("compute_all_until_probabilities", &computeAllUntilProbabilities, "Compute forward until probabilities");
     m.def("compute_transient_probabilities", &computeTransientProbabilities, "Compute transient probabilities");
     m.def("_compute_prob01states_double", &computeProb01<double>, "Compute prob-0-1 states", py::arg("model"), py::arg("phi_states"), py::arg("psi_states"));
diff --git a/src/helpers.h b/src/helpers.h
index 9aec2ad854..052737ca33 100644
--- a/src/helpers.h
+++ b/src/helpers.h
@@ -28,4 +28,3 @@ std::string containerToString(T& t) {
 // Be warned: Enabling something like this will break everything about Monomial,
 // as to Python the shared_ptr (Arg) IS the Monomial
 //  //PYBIND11_DECLARE_HOLDER_TYPE(T, std::shared_ptr<T>);
-
diff --git a/src/mod_core.cpp b/src/mod_core.cpp
index a246a5bf32..2422a6ab71 100644
--- a/src/mod_core.cpp
+++ b/src/mod_core.cpp
@@ -1,15 +1,15 @@
 #include "common.h"
 
-#include "core/core.h"
-#include "core/result.h"
-#include "core/modelchecking.h"
-#include "core/bisimulation.h"
-#include "core/input.h"
 #include "core/analysis.h"
+#include "core/bisimulation.h"
+#include "core/core.h"
 #include "core/counterexample.h"
 #include "core/environment.h"
-#include "core/transformation.h"
+#include "core/input.h"
+#include "core/modelchecking.h"
+#include "core/result.h"
 #include "core/simulator.h"
+#include "core/transformation.h"
 
 PYBIND11_MODULE(_core, m) {
     m.doc() = "core";
diff --git a/src/mod_storage.cpp b/src/mod_storage.cpp
index f88d6bf9ed..c4291e5374 100644
--- a/src/mod_storage.cpp
+++ b/src/mod_storage.cpp
@@ -1,22 +1,22 @@
 #include "common.h"
 
 #include "storage/bitvector.h"
+#include "storage/choiceorigins.h"
 #include "storage/dd.h"
-#include "storage/model.h"
 #include "storage/decomposition.h"
+#include "storage/distribution.h"
+#include "storage/expressions.h"
+#include "storage/geometry.h"
+#include "storage/jani.h"
+#include "storage/labeling.h"
 #include "storage/matrix.h"
 #include "storage/memorystructure.h"
+#include "storage/model.h"
 #include "storage/model_components.h"
-#include "storage/distribution.h"
-#include "storage/scheduler.h"
 #include "storage/prism.h"
-#include "storage/jani.h"
+#include "storage/scheduler.h"
 #include "storage/state.h"
 #include "storage/valuation.h"
-#include "storage/choiceorigins.h"
-#include "storage/labeling.h"
-#include "storage/expressions.h"
-#include "storage/geometry.h"
 
 #include "storm/adapters/IntervalAdapter.h"
 #include "storm/storage/dd/DdType.h"
@@ -37,12 +37,14 @@ PYBIND11_MODULE(_storage, m) {
     define_sparse_model<storm::RationalNumber>(m, "Exact");
     define_sparse_model<storm::Interval>(m, "Interval");
     define_sparse_model<storm::RationalFunction>(m, "Parametric");
+    define_sparse_model<storm::RationalInterval>(m, "RationalInterval");
     define_statevaluation(m);
     define_statevaluation_transformer(m);
     define_simplevaluation(m);
     define_sparse_matrix<double>(m, "");
     define_sparse_matrix<storm::RationalNumber>(m, "Exact");
     define_sparse_matrix<storm::Interval>(m, "Interval");
+    define_sparse_matrix<storm::RationalInterval>(m, "RationalInterval");
     define_sparse_matrix<storm::RationalFunction>(m, "Parametric");
     define_sparse_matrix_nt(m);
     define_symbolic_model<storm::dd::DdType::Sylvan, double>(m, "Sylvan");
@@ -51,6 +53,7 @@ PYBIND11_MODULE(_storage, m) {
     define_state<double>(m, "");
     define_state<storm::RationalNumber>(m, "Exact");
     define_state<storm::Interval>(m, "Interval");
+    define_state<storm::RationalInterval>(m, "RationalInterval");
     define_state<storm::RationalFunction>(m, "Parametric");
     define_memorystructure_typed<double>(m, "");
     define_memorystructure_typed<storm::RationalNumber>(m, "Exact");
@@ -66,13 +69,16 @@ PYBIND11_MODULE(_storage, m) {
     define_scheduler<double>(m, "");
     define_scheduler<storm::RationalNumber>(m, "Exact");
     define_scheduler<storm::Interval>(m, "Interval");
+    define_scheduler<storm::RationalInterval>(m, "RationalInterval");
     define_scheduler<storm::RationalFunction>(m, "Parametric");
     define_distribution<double>(m, "");
     define_distribution<storm::RationalNumber>(m, "Exact");
     define_distribution<storm::Interval>(m, "Interval");
+    define_distribution<storm::RationalInterval>(m, "RationalInterval");
     define_sparse_model_components<double>(m, "");
     define_sparse_model_components<storm::RationalNumber>(m, "Exact");
     define_sparse_model_components<storm::Interval>(m, "Interval");
+    define_sparse_model_components<storm::RationalInterval>(m, "RationalInterval");
     define_sparse_model_components<storm::RationalFunction>(m, "Parametric");
     define_geometry<double>(m, "Double");
     define_geometry<storm::RationalNumber>(m, "Exact");
@@ -81,6 +87,6 @@ PYBIND11_MODULE(_storage, m) {
     define_maximal_end_component_decomposition<double>(m, "_double");
     define_maximal_end_component_decomposition<storm::RationalNumber>(m, "_exact");
     define_maximal_end_component_decomposition<storm::Interval>(m, "_interval");
+    define_maximal_end_component_decomposition<storm::RationalInterval>(m, "_ratinterval");
     define_maximal_end_component_decomposition<storm::RationalFunction>(m, "_ratfunc");
-
 }
diff --git a/src/mod_utility.cpp b/src/mod_utility.cpp
index dd53606bed..d2510cb400 100644
--- a/src/mod_utility.cpp
+++ b/src/mod_utility.cpp
@@ -1,22 +1,24 @@
 #include "common.h"
 
-#include "utility/shortestPaths.h"
-#include "utility/smtsolver.h"
+#include "storm/adapters/RationalNumberAdapter.h"
 #include "utility/chrono.h"
 #include "utility/json.h"
-#include "storm/adapters/RationalNumberAdapter.h"
+#include "utility/kwekMehlhorn.h"
+#include "utility/shortestPaths.h"
+#include "utility/smtsolver.h"
 
 PYBIND11_MODULE(_utility, m) {
-    m.doc() = "Utilities for Storm";
+  m.doc() = "Utilities for Storm";
 
 #ifdef STORMPY_DISABLE_SIGNATURE_DOC
-    py::options options;
-    options.disable_function_signatures();
+  py::options options;
+  options.disable_function_signatures();
 #endif
 
-    define_ksp(m);
-    define_smt(m);
-    define_chrono(m);
-    define_json<double>(m, "Double");
-    define_json<storm::RationalNumber>(m, "Rational");
+  define_ksp(m);
+  define_smt(m);
+  define_chrono(m);
+  define_json<double>(m, "Double");
+  define_json<storm::RationalNumber>(m, "Rational");
+  define_kwek_mehlhorn<storm::RationalNumber>(m, "");
 }
diff --git a/src/storage/decomposition.cpp b/src/storage/decomposition.cpp
index 08db02b9fb..c1a060ea12 100644
--- a/src/storage/decomposition.cpp
+++ b/src/storage/decomposition.cpp
@@ -38,4 +38,5 @@ void define_maximal_end_component_decomposition(py::module& m, std::string const
 template void define_maximal_end_component_decomposition<double>(py::module& m, std::string const& vt_suffix);
 template void define_maximal_end_component_decomposition<storm::RationalNumber>(py::module& m, std::string const& vt_suffix);
 template void define_maximal_end_component_decomposition<storm::Interval>(py::module& m, std::string const& vt_suffix);
+template void define_maximal_end_component_decomposition<storm::RationalInterval>(py::module& m, std::string const& vt_suffix);
 template void define_maximal_end_component_decomposition<storm::RationalFunction>(py::module& m, std::string const& vt_suffix);
diff --git a/src/storage/distribution.cpp b/src/storage/distribution.cpp
index f970e73d75..122e9ba42c 100644
--- a/src/storage/distribution.cpp
+++ b/src/storage/distribution.cpp
@@ -19,3 +19,4 @@ void define_distribution(py::module& m, std::string vt_suffix) {
 template void define_distribution<double>(py::module&, std::string vt_suffix);
 template void define_distribution<storm::RationalNumber>(py::module&, std::string vt_suffix);
 template void define_distribution<storm::Interval>(py::module&, std::string vt_suffix);
+template void define_distribution<storm::RationalInterval>(py::module&, std::string vt_suffix);
diff --git a/src/storage/matrix.cpp b/src/storage/matrix.cpp
index 15c01ecc41..b52356650a 100644
--- a/src/storage/matrix.cpp
+++ b/src/storage/matrix.cpp
@@ -134,5 +134,6 @@ void define_sparse_matrix(py::module& m, std::string const& vtSuffix) {
 template void define_sparse_matrix<double>(py::module& m, std::string const& vtSuffix);
 template void define_sparse_matrix<storm::RationalNumber>(py::module& m, std::string const& vtSuffix);
 template void define_sparse_matrix<storm::Interval>(py::module& m, std::string const& vtSuffix);
+template void define_sparse_matrix<storm::RationalInterval>(py::module& m, std::string const& vtSuffix);
 template void define_sparse_matrix<storm::RationalFunction>(py::module& m, std::string const& vtSuffix);
 
diff --git a/src/storage/model.cpp b/src/storage/model.cpp
index 16f17ee1a1..bf7eb852c7 100644
--- a/src/storage/model.cpp
+++ b/src/storage/model.cpp
@@ -116,6 +116,12 @@ void define_model(py::module& m) {
         .def("_as_sparse_pdtmc", [](ModelBase &modelbase) {
                 return modelbase.as<SparseDtmc<storm::RationalFunction>>();
             }, "Get model as sparse parametric DTMC")
+        .def("_as_sparse_idtmc", [](ModelBase &modelbase) {
+                return modelbase.as<SparseDtmc<storm::Interval>>();
+            }, "Get model as sparse interval DTMC")
+        .def("_as_sparse_exact_idtmc", [](ModelBase &modelbase) {
+                return modelbase.as<SparseDtmc<storm::RationalInterval>>();
+            }, "Get model as sparse exact interval DTMC")
         .def("_as_sparse_mdp", [](ModelBase &modelbase) {
                 return modelbase.as<SparseMdp<double>>();
             }, "Get model as sparse MDP")
@@ -125,18 +131,24 @@ void define_model(py::module& m) {
         .def("_as_sparse_imdp", [](ModelBase &modelbase) {
                 return modelbase.as<SparseMdp<storm::Interval>>();
             }, "Get model as sparse interval MDP")
+        .def("_as_sparse_exact_imdp", [](ModelBase &modelbase) {
+                return modelbase.as<SparseMdp<storm::RationalInterval>>();
+            }, "Get model as sparse exact interval MDP")
         .def("_as_sparse_pmdp", [](ModelBase &modelbase) {
                 return modelbase.as<SparseMdp<storm::RationalFunction>>();
             }, "Get model as sparse parametric MDP")
         .def("_as_sparse_pomdp", [](ModelBase &modelbase) {
                 return modelbase.as<SparsePomdp<double>>();
             }, "Get model as sparse POMDP")
+        .def("_as_sparse_ipomdp", [](ModelBase &modelbase) {
+                return modelbase.as<SparsePomdp<storm::Interval>>();
+            }, "Get model as sparse interval POMDP")
+        .def("_as_sparse_exact_ipomdp", [](ModelBase &modelbase) {
+                return modelbase.as<SparsePomdp<storm::RationalInterval>>();
+            }, "Get model as sparse interval exact POMDP")
         .def("_as_sparse_exact_pomdp", [](ModelBase &modelbase) {
                 return modelbase.as<SparsePomdp<storm::RationalNumber>>();
             }, "Get model as sparse exact POMDP")
-        .def("_as_sparse_ipomdp", [](ModelBase &modelbase) {
-            return modelbase.as<SparsePomdp<storm::Interval>>();
-            }, "Get model as sparse interval POMDP")
         .def("_as_sparse_ppomdp", [](ModelBase &modelbase) {
             return modelbase.as<SparsePomdp<storm::RationalFunction>>();
             }, "Get model as sparse parametric POMDP")
@@ -149,6 +161,9 @@ void define_model(py::module& m) {
         .def("_as_sparse_ictmc", [](ModelBase &modelbase) {
                 return modelbase.as<SparseCtmc<storm::Interval>>();
             }, "Get model as sparse interval CTMC")
+        .def("_as_sparse_exact_ictmc", [](ModelBase &modelbase) {
+                return modelbase.as<SparseCtmc<storm::RationalInterval>>();
+            }, "Get model as sparse exact interval CTMC")
         .def("_as_sparse_pctmc", [](ModelBase &modelbase) {
                 return modelbase.as<SparseCtmc<storm::RationalFunction>>();
             }, "Get model as sparse parametric CTMC")
@@ -161,6 +176,9 @@ void define_model(py::module& m) {
         .def("_as_sparse_ima", [](ModelBase &modelbase) {
                 return modelbase.as<SparseMarkovAutomaton<storm::Interval>>();
             }, "Get model as sparse interval MA")
+        .def("_as_sparse_exact_ima", [](ModelBase &modelbase) {
+                return modelbase.as<SparseMarkovAutomaton<storm::RationalInterval>>();
+            }, "Get model as sparse exact interval MA")
         .def("_as_sparse_pma", [](ModelBase &modelbase) {
                 return modelbase.as<SparseMarkovAutomaton<storm::RationalFunction>>();
             }, "Get model as sparse parametric MA")
@@ -173,6 +191,9 @@ void define_model(py::module& m) {
         .def("_as_sparse_ismg", [](ModelBase &modelbase) {
                 return modelbase.as<SparseSmg<storm::Interval>>();
             }, "Get model as sparse interval SMG")
+        .def("_as_sparse_exact_ismg", [](ModelBase &modelbase) {
+                return modelbase.as<SparseSmg<storm::RationalInterval>>();
+            }, "Get model as sparse exact interval SMG")
         .def("_as_sparse_psmg", [](ModelBase &modelbase) {
                 return modelbase.as<SparseSmg<storm::RationalFunction>>();
             }, "Get model as sparse parametric SMG")
@@ -393,6 +414,7 @@ void define_symbolic_model(py::module& m, std::string vt_suffix) {
 template void define_sparse_model<double>(py::module& m, std::string const& vt_suffix);
 template void define_sparse_model<storm::RationalNumber>(py::module& m, std::string const& vt_suffix);
 template void define_sparse_model<storm::Interval>(py::module& m, std::string const& vt_suffix);
+template void define_sparse_model<storm::RationalInterval>(py::module& m, std::string const& vt_suffix);
 template void define_sparse_model<storm::RationalFunction>(py::module& m, std::string const& vt_suffix);
 
 template void define_symbolic_model<storm::dd::DdType::Sylvan, double>(py::module& m, std::string vt_suffix);
diff --git a/src/storage/model_components.cpp b/src/storage/model_components.cpp
index 9f46bbe874..57252740f8 100644
--- a/src/storage/model_components.cpp
+++ b/src/storage/model_components.cpp
@@ -40,6 +40,7 @@ void define_sparse_model_components(py::module& m, std::string const& vtSuffix)
 
         // POMDP specific components
         .def_readwrite("observability_classes", &SparseModelComponents<ValueType>::observabilityClasses, "The POMDP observations")
+        .def_readwrite("observation_valuations", &SparseModelComponents<ValueType>::observationValuations, "The POMDP observation valuations")
 
         // Continuous time specific components (CTMCs, Markov Automata):
         .def_readwrite("rate_transitions", &SparseModelComponents<ValueType>::rateTransitions, "True iff the transition values (for Markovian choices) are interpreted as rates")
@@ -59,4 +60,5 @@ void define_sparse_model_components(py::module& m, std::string const& vtSuffix)
 template void define_sparse_model_components<double>(py::module& m, std::string const& vtSuffix);
 template void define_sparse_model_components<storm::RationalNumber>(py::module& m, std::string const& vtSuffix);
 template void define_sparse_model_components<storm::Interval>(py::module& m, std::string const& vtSuffix);
+template void define_sparse_model_components<storm::RationalInterval>(py::module& m, std::string const& vtSuffix);
 template void define_sparse_model_components<storm::RationalFunction>(py::module& m, std::string const& vtSuffix);
diff --git a/src/storage/scheduler.cpp b/src/storage/scheduler.cpp
index 263ec7bd55..05a6d81c0e 100644
--- a/src/storage/scheduler.cpp
+++ b/src/storage/scheduler.cpp
@@ -33,7 +33,7 @@ void define_scheduler(py::module& m, std::string vt_suffix) {
                 }, py::arg("model"), py::arg("skip_unique_choices") = false, py::arg("skip_dont_care_states") = false)
     ;
 
-    if constexpr (!std::is_same_v<ValueType, storm::Interval>) {
+    if constexpr (!storm::IsIntervalType<ValueType>) {
         // Conversion from Interval not implemented
         scheduler
             .def("cast_to_double_datatype", &Scheduler::template toValueType<double>, "Construct the scheduler with `double` value type")
@@ -62,4 +62,5 @@ void define_scheduler(py::module& m, std::string vt_suffix) {
 template void define_scheduler<double>(py::module& m, std::string vt_suffix);
 template void define_scheduler<storm::RationalNumber>(py::module& m, std::string vt_suffix);
 template void define_scheduler<storm::Interval>(py::module& m, std::string vt_suffix);
+template void define_scheduler<storm::RationalInterval>(py::module& m, std::string vt_suffix);
 template void define_scheduler<storm::RationalFunction>(py::module& m, std::string vt_suffix);
diff --git a/src/storage/state.cpp b/src/storage/state.cpp
index e73323cfb1..8125541e48 100644
--- a/src/storage/state.cpp
+++ b/src/storage/state.cpp
@@ -40,5 +40,6 @@ void define_state(py::module& m, std::string const& vtSuffix) {
 template void define_state<double>(py::module& m, std::string const& vtSuffix);
 template void define_state<storm::RationalNumber>(py::module& m, std::string const& vtSuffix);
 template void define_state<storm::Interval>(py::module& m, std::string const& vtSuffix);
+template void define_state<storm::RationalInterval>(py::module& m, std::string const& vtSuffix);
 template void define_state<storm::RationalFunction>(py::module& m, std::string const& vtSuffix);
 
diff --git a/src/storage/valuation.cpp b/src/storage/valuation.cpp
index a73aeabe85..5a71aab0cc 100644
--- a/src/storage/valuation.cpp
+++ b/src/storage/valuation.cpp
@@ -32,7 +32,7 @@ void define_statevaluation(py::module& m) {
         .def("get_string", &storm::storage::sparse::StateValuations::toString, py::arg("state"), py::arg("pretty")=true, py::arg("selected_variables")=boost::none)
         .def("get_json", &toJson, py::arg("state"), py::arg("selected_variables")=boost::none)
         .def("get_nr_of_states", &storm::storage::sparse::StateValuations::getNumberOfStates)
-        .def_property_readonly("manager", &storm::storage::sparse::StateValuations::getManager);
+        .def_property_readonly("manager", &storm::storage::sparse::StateValuations::getManager)
     ;
 
 
diff --git a/src/utility/kwekMehlhorn.cpp b/src/utility/kwekMehlhorn.cpp
new file mode 100644
index 0000000000..50bcb5438a
--- /dev/null
+++ b/src/utility/kwekMehlhorn.cpp
@@ -0,0 +1,22 @@
+#include "kwekMehlhorn.h"
+#include "src/common.h"
+#include <pybind11/pybind11.h>
+#include <storm/adapters/RationalNumberAdapter.h>
+#include <storm/utility/KwekMehlhorn.h>
+
+template <typename RationalValueType>
+void define_kwek_mehlhorn(py::module &m, std::string const &vtSuffix) {
+  m.def(
+      "sharpen",
+      [](uint64_t precision, double value) {
+        return storm::utility::kwek_mehlhorn::sharpen<RationalValueType,
+                                                      double>(precision, value);
+      },
+      "Convert a float to the nearest rational within precision using Kwek "
+      "Mehlhorn",
+      py::arg("precision"), py::arg("value"));
+}
+
+template void
+define_kwek_mehlhorn<storm::RationalNumber>(py::module &m,
+                                            std::string const &vtSuffix);
\ No newline at end of file
diff --git a/src/utility/kwekMehlhorn.h b/src/utility/kwekMehlhorn.h
new file mode 100644
index 0000000000..42292ca4f7
--- /dev/null
+++ b/src/utility/kwekMehlhorn.h
@@ -0,0 +1,6 @@
+#pragma once
+
+#include "src/common.h"
+
+template <typename RationalValueType>
+void define_kwek_mehlhorn(py::module &m, std::string const &vtSuffix);
\ No newline at end of file
diff --git a/tests/core/test_modelchecking.py b/tests/core/test_modelchecking.py
index 21b8a6e1ea..6975f1c94e 100644
--- a/tests/core/test_modelchecking.py
+++ b/tests/core/test_modelchecking.py
@@ -96,6 +96,58 @@ def test_model_checking_interval_mdp(self):
         result = stormpy.check_interval_mdp(model, task, env)
         assert math.isclose(result.at(initial_state), 0.4, rel_tol=1e-4)
 
+    def test_model_checking_exact_interval_dtmc(self):
+        program = stormpy.parse_prism_program(get_example_path("idtmc", "die-intervals.pm"))
+        formulas = stormpy.parse_properties('P=? [ F "one"]')
+        model = stormpy.build_sparse_exact_interval_model(program, formulas)
+        initial_state = model.initial_states[0]
+        assert initial_state == 0
+
+        env = stormpy.Environment()
+        env.solver_environment.minmax_solver_environment.method = stormpy.MinMaxMethod.value_iteration
+
+        task = stormpy.ExactCheckTask(formulas[0].raw_formula, only_initial_states=True)
+        task.set_produce_schedulers()
+        # Compute maximal
+        task.set_uncertainty_resolution_mode(stormpy.UncertaintyResolutionMode.MAXIMIZE)
+        result = stormpy.check_exact_interval_dtmc(model, task, env)
+        assert math.isclose(result.at(initial_state), 72.0 / 189.0, rel_tol=1e-4)
+        # Compute minimal
+        task.set_uncertainty_resolution_mode(stormpy.UncertaintyResolutionMode.MINIMIZE)
+        result = stormpy.check_exact_interval_dtmc(model, task, env)
+        assert math.isclose(result.at(initial_state), 9.0 / 189.0, rel_tol=1e-4)
+
+    def test_model_checking_exact_interval_mdp(self):
+        model = stormpy.build_exact_interval_model_from_drn(get_example_path("imdp", "tiny-01.drn"))
+        formulas = stormpy.parse_properties('Pmax=? [ F "target"];Pmin=? [ F "target"]')
+        initial_state = model.initial_states[0]
+        assert initial_state == 0
+
+        env = stormpy.Environment()
+        env.solver_environment.minmax_solver_environment.method = stormpy.MinMaxMethod.value_iteration
+
+        task = stormpy.ExactCheckTask(formulas[0].raw_formula, only_initial_states=True)
+        task.set_produce_schedulers()
+        # Compute maximal robust
+        task.set_uncertainty_resolution_mode(stormpy.UncertaintyResolutionMode.ROBUST)
+        result = stormpy.check_exact_interval_mdp(model, task, env)
+        assert math.isclose(result.at(initial_state), 0.4, rel_tol=1e-4)
+        # Compute maximal cooperative
+        task.set_uncertainty_resolution_mode(stormpy.UncertaintyResolutionMode.COOPERATIVE)
+        result = stormpy.check_exact_interval_mdp(model, task, env)
+        assert math.isclose(result.at(initial_state), 0.5, rel_tol=1e-4)
+
+        task = stormpy.ExactCheckTask(formulas[1].raw_formula, only_initial_states=True)
+        task.set_produce_schedulers()
+        # Compute minimal robust
+        task.set_uncertainty_resolution_mode(stormpy.UncertaintyResolutionMode.ROBUST)
+        result = stormpy.check_exact_interval_mdp(model, task, env)
+        assert math.isclose(result.at(initial_state), 0.5, rel_tol=1e-4)
+        # Compute minimal cooperative
+        task.set_uncertainty_resolution_mode(stormpy.UncertaintyResolutionMode.COOPERATIVE)
+        result = stormpy.check_exact_interval_mdp(model, task, env)
+        assert math.isclose(result.at(initial_state), 0.4, rel_tol=1e-4)
+
     def test_model_checking_jani_dtmc(self):
         jani_model, formulas = stormpy.parse_jani_model(get_example_path("dtmc", "die.jani"))
         formulas = stormpy.eliminate_reward_accumulations(jani_model, formulas)
diff --git a/tests/storage/test_model.py b/tests/storage/test_model.py
index 939dabb2f8..ae875d7664 100644
--- a/tests/storage/test_model.py
+++ b/tests/storage/test_model.py
@@ -1,3 +1,5 @@
+from numbers import Rational
+
 import stormpy
 from helpers.helper import get_example_path
 import pytest
@@ -322,3 +324,21 @@ def test_build_ipomdp(self):
 
         assert model.model_type == stormpy.ModelType.POMDP
         assert type(model) is stormpy.SparseIntervalPomdp
+
+    def test_build_exact_ipomdp(self):
+        model = stormpy.build_exact_interval_model_from_drn(get_example_path("ipomdp", "tiny-01.drn"))
+        assert model.nr_states == 4
+        assert model.nr_choices == 5
+        assert model.nr_transitions == 8
+        assert model.nr_observations == 3
+
+        for transition in model.transition_matrix.row_iter(0, 0):
+            if transition.column == 1:
+                assert transition.value().lower() == stormpy.Rational("1/5")
+                assert transition.value().upper() == stormpy.Rational("7/10")
+            elif transition.column == 2:
+                assert transition.value().lower() == stormpy.Rational("3/10")
+                assert transition.value().upper() == stormpy.Rational("4/5")
+
+        assert model.model_type == stormpy.ModelType.POMDP
+        assert type(model) is stormpy.SparseRationalIntervalPomdp