diff --git a/src/storm/logic/BoundedUntilFormula.cpp b/src/storm/logic/BoundedUntilFormula.cpp
index 387fa95c8f..7bddd2c960 100644
--- a/src/storm/logic/BoundedUntilFormula.cpp
+++ b/src/storm/logic/BoundedUntilFormula.cpp
@@ -251,6 +251,14 @@ storm::expressions::Expression const& BoundedUntilFormula::getUpperBound(unsigne
     return upperBound.at(i).value().getBound();
 }
 
+std::optional<TimeBound> BoundedUntilFormula::getLowerBoundAsOptionalTimeBound(unsigned i) const {
+    return lowerBound.at(i);
+}
+
+std::optional<TimeBound> BoundedUntilFormula::getUpperBoundAsOptionalTimeBound(unsigned i) const {
+    return upperBound.at(i);
+}
+
 template<>
 double BoundedUntilFormula::getLowerBound(unsigned i) const {
     if (!hasLowerBound(i)) {
diff --git a/src/storm/logic/BoundedUntilFormula.h b/src/storm/logic/BoundedUntilFormula.h
index 06d7515bf1..827dbdda8f 100644
--- a/src/storm/logic/BoundedUntilFormula.h
+++ b/src/storm/logic/BoundedUntilFormula.h
@@ -58,6 +58,9 @@ class BoundedUntilFormula : public PathFormula {
     storm::expressions::Expression const& getLowerBound(unsigned i = 0) const;
     storm::expressions::Expression const& getUpperBound(unsigned i = 0) const;
 
+    std::optional<TimeBound> getLowerBoundAsOptionalTimeBound(unsigned i = 0) const;
+    std::optional<TimeBound> getUpperBoundAsOptionalTimeBound(unsigned i = 0) const;
+
     template<typename ValueType>
     ValueType getLowerBound(unsigned i = 0) const;
 
diff --git a/src/storm/transformer/SparseRationalModelToDoubleTransformer.cpp b/src/storm/transformer/SparseRationalModelToDoubleTransformer.cpp
new file mode 100644
index 0000000000..296e2e62d8
--- /dev/null
+++ b/src/storm/transformer/SparseRationalModelToDoubleTransformer.cpp
@@ -0,0 +1,111 @@
+#include "SparseRationalModelToDoubleTransformer.h"
+
+#include "storm/exceptions/IllegalArgumentTypeException.h"
+#include "storm/models/sparse/Ctmc.h"
+#include "storm/models/sparse/Dtmc.h"
+#include "storm/models/sparse/MarkovAutomaton.h"
+#include "storm/models/sparse/Mdp.h"
+#include "storm/models/sparse/Pomdp.h"
+#include "storm/models/sparse/Smg.h"
+#include "storm/models/sparse/StochasticTwoPlayerGame.h"
+#include "storm/storage/sparse/ModelComponents.h"
+#include "storm/utility/macros.h"
+#include "storm/utility/vector.h"
+
+namespace storm::transformer {
+std::shared_ptr<storm::models::sparse::Model<double>> sparseRationalModelToDouble(
+    std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> const& inputModel, double precision) {
+    STORM_LOG_THROW(inputModel, storm::exceptions::IllegalArgumentTypeException, "Cannot transform a null model.");
+    storm::storage::sparse::ModelComponents<double> convertedComponents;
+    convertedComponents.transitionMatrix = inputModel->getTransitionMatrix().toValueType<double>();
+    if (inputModel->getType() != storm::models::ModelType::Ctmc) {
+        if (!convertedComponents.transitionMatrix.isProbabilistic(precision)) {
+            convertedComponents.transitionMatrix.divideRowsInPlace(convertedComponents.transitionMatrix.getRowSumVector());
+        }
+    }
+    convertedComponents.choiceLabeling = inputModel->getOptionalChoiceLabeling();
+    convertedComponents.stateLabeling = inputModel->getStateLabeling();
+    convertedComponents.stateValuations = inputModel->getOptionalStateValuations();
+    convertedComponents.choiceOrigins = inputModel->getOptionalChoiceOrigins();
+    for (auto const& [rewardModelName, rewardModel] : inputModel->getRewardModels()) {
+        // Transform reward models
+        std::optional<std::vector<double>> optionalStateRewardVector = std::nullopt;
+        std::optional<std::vector<double>> optionalStateActionRewardVector = std::nullopt;
+        std::optional<storm::storage::SparseMatrix<double>> optionalTransitionRewardMatrix = std::nullopt;
+        if (rewardModel.hasStateRewards()) {
+            std::vector<double> resultVector;
+            resultVector.reserve(rewardModel.getStateRewardVector().size());
+            for (auto const& oldValue : rewardModel.getStateRewardVector()) {
+                resultVector.push_back(storm::utility::convertNumber<double>(oldValue));
+            }
+            optionalStateRewardVector = resultVector;
+        }
+        if (rewardModel.hasStateActionRewards()) {
+            std::vector<double> resultVector;
+            resultVector.reserve(rewardModel.getStateActionRewardVector().size());
+            for (auto const& oldValue : rewardModel.getStateActionRewardVector()) {
+                resultVector.push_back(storm::utility::convertNumber<double>(oldValue));
+            }
+            optionalStateActionRewardVector = resultVector;
+        }
+        if (rewardModel.hasTransitionRewards()) {
+            optionalTransitionRewardMatrix = rewardModel.getTransitionRewardMatrix().toValueType<double>();
+        }
+        convertedComponents.rewardModels.emplace(
+            rewardModelName, storm::models::sparse::StandardRewardModel<double>(
+                                 std::move(optionalStateRewardVector), std::move(optionalStateActionRewardVector), std::move(optionalTransitionRewardMatrix)));
+    }
+    switch (inputModel->getType()) {
+        case storm::models::ModelType::Dtmc:
+            return std::make_shared<storm::models::sparse::Dtmc<double>>(storm::models::sparse::Dtmc<double>(convertedComponents));
+        case storm::models::ModelType::Mdp:
+            return std::make_shared<storm::models::sparse::Mdp<double>>(storm::models::sparse::Mdp<double>(convertedComponents));
+        case storm::models::ModelType::Ctmc: {
+            auto ctmc = inputModel->as<storm::models::sparse::Ctmc<storm::RationalNumber>>();
+            std::vector<double> resultVector;
+            resultVector.reserve(ctmc->getExitRateVector().size());
+            for (auto const& oldValue : ctmc->getExitRateVector()) {
+                resultVector.push_back(storm::utility::convertNumber<double>(oldValue));
+            }
+            convertedComponents.exitRates = resultVector;
+            convertedComponents.rateTransitions = true;
+            return std::make_shared<storm::models::sparse::Ctmc<double>>(storm::models::sparse::Ctmc<double>(convertedComponents));
+        }
+        case storm::models::ModelType::MarkovAutomaton: {
+            auto ma = inputModel->as<storm::models::sparse::MarkovAutomaton<storm::RationalNumber>>();
+            std::vector<double> resultVector;
+            resultVector.reserve(ma->getExitRates().size());
+            for (auto const& oldValue : ma->getExitRates()) {
+                resultVector.push_back(storm::utility::convertNumber<double>(oldValue));
+            }
+            convertedComponents.exitRates = resultVector;
+            // Markov automata store probabilities in their transition matrix and rates separately in exitRates.
+            convertedComponents.rateTransitions = false;
+            convertedComponents.markovianStates = ma->getMarkovianStates();
+            return std::make_shared<storm::models::sparse::MarkovAutomaton<double>>(storm::models::sparse::MarkovAutomaton<double>(convertedComponents));
+        }
+        case storm::models::ModelType::Pomdp: {
+            auto pomdp = inputModel->as<storm::models::sparse::Pomdp<storm::RationalNumber>>();
+            convertedComponents.observabilityClasses = pomdp->getObservations();
+            convertedComponents.observationValuations = pomdp->getOptionalObservationValuations();
+            return std::make_shared<models::sparse::Pomdp<double>>(models::sparse::Pomdp<double>(convertedComponents, pomdp->isCanonic()));
+        }
+        case storm::models::ModelType::Smg: {
+            auto smg = inputModel->as<storm::models::sparse::Smg<storm::RationalNumber>>();
+            convertedComponents.statePlayerIndications = smg->getStatePlayerIndications();
+            convertedComponents.playerNameToIndexMap = smg->getPlayerNamesToIndex();
+            return std::make_shared<storm::models::sparse::Smg<double>>(models::sparse::Smg<double>(convertedComponents));
+        }
+        case storm::models::ModelType::S2pg: {
+            auto s2pg = inputModel->as<storm::models::sparse::StochasticTwoPlayerGame<storm::RationalNumber>>();
+            convertedComponents.player1Matrix = s2pg->getPlayer1Matrix();
+            return std::make_shared<storm::models::sparse::StochasticTwoPlayerGame<double>>(
+                models::sparse::StochasticTwoPlayerGame<double>(convertedComponents));
+        }
+        default:
+            STORM_LOG_THROW(false, storm::exceptions::IllegalArgumentTypeException,
+                            "Value type transformation is not supported for models of type " << inputModel->getType() << ".");
+    }
+    return nullptr;
+}
+}  // namespace storm::transformer
diff --git a/src/storm/transformer/SparseRationalModelToDoubleTransformer.h b/src/storm/transformer/SparseRationalModelToDoubleTransformer.h
new file mode 100644
index 0000000000..06ff990651
--- /dev/null
+++ b/src/storm/transformer/SparseRationalModelToDoubleTransformer.h
@@ -0,0 +1,19 @@
+#pragma once
+
+#include <memory>
+
+#include "storm/adapters/RationalNumberForward.h"
+#include "storm/models/sparse/Model.h"
+
+namespace storm::transformer {
+
+/**
+ * Returns a model equivalent to @p inputModel with all probabilities, rates, and rewards converted to double.
+ *
+ * @param precision The tolerance used to determine whether the converted transition matrix needs to be normalized. Ignored for CTMCs.
+ * @pre inputModel is not null.
+ */
+std::shared_ptr<storm::models::sparse::Model<double>> sparseRationalModelToDouble(
+    std::shared_ptr<models::sparse::Model<storm::RationalNumber>> const& inputModel, double precision);
+
+}  // namespace storm::transformer
diff --git a/src/storm/transformer/TransitionToActionRewardTransformer.cpp b/src/storm/transformer/TransitionToActionRewardTransformer.cpp
new file mode 100644
index 0000000000..e8047e0bef
--- /dev/null
+++ b/src/storm/transformer/TransitionToActionRewardTransformer.cpp
@@ -0,0 +1,257 @@
+#include "storm/transformer/TransitionToActionRewardTransformer.h"
+
+#include "storm/adapters/IntervalAdapter.h"
+#include "storm/adapters/RationalFunctionAdapter.h"
+#include "storm/adapters/RationalNumberAdapter.h"
+#include "storm/exceptions/UnexpectedException.h"
+#include "storm/models/sparse/MarkovAutomaton.h"
+#include "storm/models/sparse/StandardRewardModel.h"
+#include "storm/storage/SparseMatrix.h"
+#include "storm/storage/sparse/ModelComponents.h"
+#include "storm/utility/OptionalRef.h"
+#include "storm/utility/builder.h"
+#include "storm/utility/macros.h"
+#include "storm/utility/vector.h"
+
+namespace storm::transformer {
+
+namespace detail {
+template<typename RewardValueType>
+using MultiRewardVector = std::vector<RewardValueType>;
+
+template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>>
+class RewardTransitionIterator {
+   public:
+    RewardTransitionIterator(storm::storage::SparseMatrix<ValueType> const& m) : transitionMatrix(m) {}
+
+    void addRewardModel(RewardModelType const& rewardModel) {
+        if (rewardModel.hasTransitionRewards()) {
+            transitionRewards.emplace_back(rewardModel.getTransitionRewardMatrix());
+            STORM_LOG_ASSERT(transitionRewards.back()->isSubmatrixOf(transitionMatrix), "Invalid reward matrix.");
+        } else {
+            transitionRewards.emplace_back();
+        }
+    }
+
+    template<typename CallBackType>
+    void forEachRowEntry(uint64_t rowIndex, bool skip0RewardEntries, CallBackType&& callBack) {
+        // Set-up iterators
+        std::vector<typename storm::storage::SparseMatrix<typename RewardModelType::ValueType>::const_iterator> rewardIterators;
+        std::vector<typename storm::storage::SparseMatrix<typename RewardModelType::ValueType>::const_iterator> rewardIteratorsEnd;
+        for (auto const& rewardMatrix : transitionRewards) {
+            if (rewardMatrix) {
+                rewardIterators.push_back(rewardMatrix->begin(rowIndex));
+                rewardIteratorsEnd.push_back(rewardMatrix->end(rowIndex));
+            } else {
+                rewardIterators.emplace_back();
+                rewardIteratorsEnd.emplace_back();
+            }
+        }
+
+        std::vector<typename RewardModelType::ValueType> rewards(transitionRewards.size());
+        for (auto const& entry : transitionMatrix.getRow(rowIndex)) {
+            // Fill in rewards for this entry
+            bool skipEntry = skip0RewardEntries;
+            for (uint64_t i = 0; i < transitionRewards.size(); ++i) {
+                if (rewardIterators[i] != rewardIteratorsEnd[i] && rewardIterators[i]->getColumn() == entry.getColumn()) {
+                    rewards[i] = rewardIterators[i]->getValue();
+                    ++rewardIterators[i];
+                    skipEntry = skipEntry && storm::utility::isZero(rewards[i]);
+                } else {
+                    rewards[i] = storm::utility::zero<typename RewardModelType::ValueType>();
+                }
+            }
+            if (!skipEntry) {
+                callBack(entry.getColumn(), entry.getValue(), rewards);
+            }
+        }
+    }
+
+   private:
+    storm::storage::SparseMatrix<ValueType> const& transitionMatrix;
+    std::vector<storm::OptionalRef<storm::storage::SparseMatrix<typename RewardModelType::ValueType> const>> transitionRewards;
+};
+
+}  // namespace detail
+
+template<typename ValueType, typename RewardModelType>
+TransitionToActionRewardTransformerReturnType<ValueType, RewardModelType> transformTransitionToActionRewards(
+    std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> originalModel, std::vector<std::string> const& relevantRewardModelNames) {
+    using RewardValueType = RewardModelType::ValueType;
+    STORM_LOG_ASSERT(originalModel, "Model must not be null.");
+    detail::RewardTransitionIterator<ValueType, RewardModelType> rewardTransitionIterator(originalModel->getTransitionMatrix());
+    bool hasTransitionRewards = false;
+    for (auto const& rewardModelName : relevantRewardModelNames) {
+        auto const& rewardModel = originalModel->getRewardModel(rewardModelName);
+        if (rewardModel.hasTransitionRewards()) {
+            hasTransitionRewards = true;
+        }
+        rewardTransitionIterator.addRewardModel(rewardModel);
+    }
+    if (!hasTransitionRewards) {
+        return {originalModel->template as<storm::models::sparse::Model<ValueType, RewardModelType>>(),
+                {storm::utility::vector::buildVectorForRange<uint64_t>(0, originalModel->getNumberOfStates())}};
+    }
+
+    // Make a pass to find the different unique rewards with which a state is entered.
+    // We do not use std::set here as the interval ordering is not a strict weak ordering for overlapping intervals.
+    // Equality-based deduplication preserves distinct overlapping rewards.
+    std::vector<std::vector<detail::MultiRewardVector<RewardValueType>>> incomingRewards(originalModel->getNumberOfStates());
+    auto const& transitions = originalModel->getTransitionMatrix();
+    for (uint64_t row = 0; row < transitions.getRowCount(); ++row) {
+        rewardTransitionIterator.forEachRowEntry(
+            row, true, [&incomingRewards](uint64_t column, RewardValueType, detail::MultiRewardVector<RewardValueType> const& rewards) {
+                storm::utility::vector::findOrInsert(incomingRewards[column], detail::MultiRewardVector<RewardValueType>(rewards));
+            });
+    }
+
+    // Create a mapping from original to new indices
+    std::vector<uint64_t> originalToNewIndex;
+    uint64_t numStates = 0;
+    for (auto const& incomingRewardVectors : incomingRewards) {
+        numStates += incomingRewardVectors.size();
+        originalToNewIndex.push_back(numStates);
+        ++numStates;
+    }
+
+    // Populate the new transition matrix and (action) rewards for intermediate states
+    uint64_t const numIntermediateStates = numStates - originalModel->getNumberOfStates();
+    bool const useGroups = !transitions.hasTrivialRowGrouping();
+    storm::storage::SparseMatrixBuilder<ValueType> newTransitionsBuilder(transitions.getRowCount() + numIntermediateStates, numStates,
+                                                                         transitions.getEntryCount() + numIntermediateStates, true, useGroups,
+                                                                         useGroups ? numStates : 0ull);
+    std::vector<std::vector<RewardValueType>> newActionRewards(relevantRewardModelNames.size(),
+                                                               std::vector<RewardValueType>(transitions.getRowCount() + numIntermediateStates));
+    uint64_t currNewRow = 0;
+    for (uint64_t currOrigState = 0; currOrigState < originalModel->getNumberOfStates(); ++currOrigState) {
+        uint64_t const currNewState = originalToNewIndex[currOrigState];
+        // First add the transitions and rewards for the intermediate states
+        for (auto const& incomingRewardVector : incomingRewards[currOrigState]) {
+            if (useGroups) {
+                newTransitionsBuilder.newRowGroup(currNewRow);
+            }
+            newTransitionsBuilder.addNextValue(currNewRow, currNewState, storm::utility::one<ValueType>());
+            auto newRewIt = newActionRewards.begin();
+            for (auto const& rew : incomingRewardVector) {
+                (*newRewIt)[currNewRow] = rew;
+                ++newRewIt;
+            }
+            ++currNewRow;
+        }
+        // Add the transitions and rewards for the original state
+        if (useGroups) {
+            newTransitionsBuilder.newRowGroup(currNewRow);
+        }
+        for (auto origRowIndex : transitions.getRowGroupIndices(currOrigState)) {
+            rewardTransitionIterator.forEachRowEntry(
+                origRowIndex, false,
+                [&newTransitionsBuilder, &originalToNewIndex, &incomingRewards, &currNewRow](uint64_t column, ValueType prob,
+                                                                                             detail::MultiRewardVector<RewardValueType> const& rewards) {
+                    if (std::all_of(rewards.begin(), rewards.end(), [](RewardValueType const& r) { return storm::utility::isZero(r); })) {
+                        // No transition reward collected so use original state
+                        newTransitionsBuilder.addNextValue(currNewRow, originalToNewIndex[column], prob);
+                    } else {
+                        // Redirect to intermediate state
+                        auto incomingRewardsIt = std::find(incomingRewards[column].begin(), incomingRewards[column].end(), rewards);
+                        STORM_LOG_ASSERT(incomingRewardsIt != incomingRewards[column].end(), "Invalid incoming rewards.");
+                        uint64_t const intermediateStateIndex =
+                            originalToNewIndex[column] - incomingRewards[column].size() + std::distance(incomingRewards[column].begin(), incomingRewardsIt);
+                        newTransitionsBuilder.addNextValue(currNewRow, intermediateStateIndex, prob);
+                    }
+                });
+            ++currNewRow;
+        }
+    }
+
+    // create new state labels and init components
+    storm::models::sparse::StateLabeling newLabeling(numStates);
+    for (auto const& l : originalModel->getStateLabeling().getLabels()) {
+        newLabeling.addLabel(l);
+        for (auto origIndex : originalModel->getStateLabeling().getStates(l)) {
+            newLabeling.addLabelToState(l, originalToNewIndex[origIndex]);
+        }
+    }
+    storm::storage::sparse::ModelComponents<ValueType, RewardModelType> components(newTransitionsBuilder.build(), std::move(newLabeling));
+
+    // create new reward models
+    uint64_t rewardIndex = 0;
+    for (auto const& rewardModelName : relevantRewardModelNames) {
+        auto& newActionRewardVector = newActionRewards[rewardIndex++];
+        auto const& oldRewardModel = originalModel->getRewardModel(rewardModelName);
+        for (uint64_t oldState = 0; oldState < originalModel->getNumberOfStates(); ++oldState) {
+            uint64_t const oldStartRow = transitions.getRowGroupIndices()[oldState];
+            uint64_t const newState = originalToNewIndex[oldState];
+            uint64_t const newStartRow = useGroups ? components.transitionMatrix.getRowGroupIndices()[newState] : newState;
+            uint64_t const numRowsInGroup = useGroups ? transitions.getRowGroupSize(oldState) : 1ull;
+            for (uint64_t groupOffset = 0; groupOffset < numRowsInGroup; ++groupOffset) {
+                auto& rewValue = newActionRewardVector[newStartRow + groupOffset];
+                if (oldRewardModel.hasStateRewards()) {
+                    rewValue += oldRewardModel.getStateReward(oldState);
+                }
+                if (oldRewardModel.hasStateActionRewards()) {
+                    rewValue += oldRewardModel.getStateActionReward(oldStartRow + groupOffset);
+                }
+            }
+        }
+        RewardModelType newRewardModel(std::nullopt, std::move(newActionRewardVector));
+        components.rewardModels.emplace(rewardModelName, std::move(newRewardModel));
+    }
+
+    STORM_LOG_WARN_COND(!originalModel->hasChoiceLabeling(), "Choice labellings will be dropped as the transformation is currently not implemented.");
+    STORM_LOG_WARN_COND(!originalModel->hasStateValuations(), "State valuations will be dropped as the transformation is currently not implemented.");
+    STORM_LOG_WARN_COND(!originalModel->hasChoiceOrigins(), "Choice origins will be dropped as the transformation is currently not implemented.");
+
+    // Model type specific components
+    if (originalModel->isOfType(storm::models::ModelType::MarkovAutomaton)) {
+        auto const& ma = *originalModel->template as<storm::models::sparse::MarkovAutomaton<ValueType>>();
+        components.markovianStates = storm::storage::BitVector(numStates);
+        components.exitRates = std::vector<ValueType>(numStates, storm::utility::zero<ValueType>());
+        for (uint64_t origState = 0; origState < originalModel->getNumberOfStates(); ++origState) {
+            uint64_t const newState = originalToNewIndex[origState];
+            if (ma.isMarkovianState(origState)) {
+                components.markovianStates->set(newState, true);
+                components.exitRates->at(newState) = ma.getExitRate(origState);
+            }
+        }
+        components.rateTransitions = false;  // Note that originalModel->getTransitionMatrix() contains probabilities
+    } else if (originalModel->isOfType(storm::models::ModelType::Ctmc)) {
+        components.rateTransitions = true;
+    } else {
+        STORM_LOG_THROW(originalModel->isOfType(storm::models::ModelType::Dtmc) || originalModel->isOfType(storm::models::ModelType::Mdp),
+                        storm::exceptions::UnexpectedException, "Unhandled model type.");
+    }
+    return {storm::utility::builder::buildModelFromComponents(originalModel->getType(), std::move(components)), std::move(originalToNewIndex)};
+}
+
+template struct TransitionToActionRewardTransformerReturnType<double>;
+template struct TransitionToActionRewardTransformerReturnType<storm::RationalNumber>;
+template struct TransitionToActionRewardTransformerReturnType<storm::RationalFunction>;
+template struct TransitionToActionRewardTransformerReturnType<storm::Interval>;
+template struct TransitionToActionRewardTransformerReturnType<storm::RationalInterval>;
+template struct TransitionToActionRewardTransformerReturnType<double, storm::models::sparse::StandardRewardModel<storm::Interval>>;
+template struct TransitionToActionRewardTransformerReturnType<storm::RationalNumber, storm::models::sparse::StandardRewardModel<storm::RationalInterval>>;
+
+template TransitionToActionRewardTransformerReturnType<double> transformTransitionToActionRewards<double, storm::models::sparse::StandardRewardModel<double>>(
+    std::shared_ptr<storm::models::sparse::Model<double>> originalModel, std::vector<std::string> const& relevantRewardModelNames);
+template TransitionToActionRewardTransformerReturnType<storm::RationalNumber>
+transformTransitionToActionRewards<storm::RationalNumber, storm::models::sparse::StandardRewardModel<storm::RationalNumber>>(
+    std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber>> originalModel, std::vector<std::string> const& relevantRewardModelNames);
+template TransitionToActionRewardTransformerReturnType<storm::RationalFunction>
+transformTransitionToActionRewards<storm::RationalFunction, storm::models::sparse::StandardRewardModel<storm::RationalFunction>>(
+    std::shared_ptr<storm::models::sparse::Model<storm::RationalFunction>> originalModel, std::vector<std::string> const& relevantRewardModelNames);
+template TransitionToActionRewardTransformerReturnType<storm::Interval>
+transformTransitionToActionRewards<storm::Interval, storm::models::sparse::StandardRewardModel<storm::Interval>>(
+    std::shared_ptr<storm::models::sparse::Model<storm::Interval>> originalModel, std::vector<std::string> const& relevantRewardModelNames);
+template TransitionToActionRewardTransformerReturnType<storm::RationalInterval>
+transformTransitionToActionRewards<storm::RationalInterval, storm::models::sparse::StandardRewardModel<storm::RationalInterval>>(
+    std::shared_ptr<storm::models::sparse::Model<storm::RationalInterval>> originalModel, std::vector<std::string> const& relevantRewardModelNames);
+template TransitionToActionRewardTransformerReturnType<double, storm::models::sparse::StandardRewardModel<storm::Interval>>
+transformTransitionToActionRewards<double, storm::models::sparse::StandardRewardModel<storm::Interval>>(
+    std::shared_ptr<storm::models::sparse::Model<double, storm::models::sparse::StandardRewardModel<storm::Interval>>> originalModel,
+    std::vector<std::string> const& relevantRewardModelNames);
+template TransitionToActionRewardTransformerReturnType<storm::RationalNumber, storm::models::sparse::StandardRewardModel<storm::RationalInterval>>
+transformTransitionToActionRewards<storm::RationalNumber, storm::models::sparse::StandardRewardModel<storm::RationalInterval>>(
+    std::shared_ptr<storm::models::sparse::Model<storm::RationalNumber, storm::models::sparse::StandardRewardModel<storm::RationalInterval>>> originalModel,
+    std::vector<std::string> const& relevantRewardModelNames);
+
+}  // namespace storm::transformer
diff --git a/src/storm/transformer/TransitionToActionRewardTransformer.h b/src/storm/transformer/TransitionToActionRewardTransformer.h
new file mode 100644
index 0000000000..e180e68b22
--- /dev/null
+++ b/src/storm/transformer/TransitionToActionRewardTransformer.h
@@ -0,0 +1,48 @@
+#pragma once
+
+#include <memory>
+#include <string>
+#include <vector>
+
+#include "storm/models/sparse/Model.h"
+#include "storm/storage/BitVector.h"
+
+namespace storm::transformer {
+
+template<typename ValueType, typename RewardModelType = storm::models::sparse::StandardRewardModel<ValueType>>
+struct TransitionToActionRewardTransformerReturnType {
+    std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> model;
+    std::vector<uint64_t> originalToNewStateIndices;
+};
+/*!
+ *
+ * Replaces transition branch rewards from all given reward models and replaces them by equivalent state-action based rewards.
+ * This is done by potentially adding intermediate states at which the corresponding reward is collected and which have a Dirac transition to the original
+ * state.
+ * Notes:
+ * - this construction potentially invalidates step-based properties, e.g., step-bounded reachability or discrete-time LRA properties.
+ * Also Until formulas with non-trivial left-hand-side will likely be invalidated
+ * - originalToNewStateIndices maps states of the original model to their positions within the transformed model. Those states are kept in the same order.
+ * - the introduced intermediate states that lead to original state 's' are located directly in front of 's'.
+ * - the number of intermediate states is kept small, e.g., if two distinct states 's_1' and 's_2' transition to 's' with the same transition reward
+ *   (w.r.t. *all* reward models), only one intermediate state is introduced.
+ * - for Markov automata, the intermediate states are probabilistic (instantaneous). For CTMCs, the intermediate states have rate 1.
+ * - intermediate states do not get any label. All labels from the original model are preserved at the original states
+ *
+ * possible improvement: Preprocessing: move transition rewards to action if it is the same for all successor states
+ *
+ * @param originalModel The original model.
+ * @param relevantRewardModelNames The names of the reward models that should be transformed. Error if the model does not contain a reward model with this name.
+ * @return The transformed model and the positions of the original model states in the new (larger) transformed model.
+ */
+template<typename ValueType, typename RewardModelType>
+TransitionToActionRewardTransformerReturnType<ValueType, RewardModelType> transformTransitionToActionRewards(
+    std::shared_ptr<storm::models::sparse::Model<ValueType, RewardModelType>> originalModel, std::vector<std::string> const& relevantRewardModelNames);
+
+template<typename ValueType>
+TransitionToActionRewardTransformerReturnType<ValueType> transformTransitionToActionRewards(
+    std::shared_ptr<storm::models::sparse::Model<ValueType>> originalModel, std::vector<std::string> const& relevantRewardModelNames) {
+    return transformTransitionToActionRewards<ValueType, storm::models::sparse::StandardRewardModel<ValueType>>(originalModel, relevantRewardModelNames);
+}
+
+}  // namespace storm::transformer
diff --git a/src/test/storm/transformer/SparseRationalModelToDoubleTransformerTest.cpp b/src/test/storm/transformer/SparseRationalModelToDoubleTransformerTest.cpp
new file mode 100644
index 0000000000..2b19a6fa38
--- /dev/null
+++ b/src/test/storm/transformer/SparseRationalModelToDoubleTransformerTest.cpp
@@ -0,0 +1,50 @@
+#include "test/storm_gtest.h"
+
+#include "storm/adapters/RationalNumberAdapter.h"
+#include "storm/models/sparse/Ctmc.h"
+#include "storm/models/sparse/Dtmc.h"
+#include "storm/models/sparse/MarkovAutomaton.h"
+#include "storm/storage/SparseMatrix.h"
+#include "storm/transformer/SparseRationalModelToDoubleTransformer.h"
+
+namespace {
+
+constexpr double standardPrecision = 1e-9;
+
+storm::storage::SparseMatrix<storm::RationalNumber> buildProbabilityMatrix() {
+    storm::storage::SparseMatrixBuilder<storm::RationalNumber> builder(3, 3, 5);
+    builder.addNextValue(0, 0, storm::RationalNumber("1/5"));
+    builder.addNextValue(0, 1, storm::RationalNumber("3/5"));
+    builder.addNextValue(0, 2, storm::RationalNumber("1/5"));
+    builder.addNextValue(1, 1, storm::RationalNumber(1));
+    builder.addNextValue(2, 2, storm::RationalNumber(1));
+    return builder.build();
+}
+
+TEST(SparseRationalModelToDoubleTransformerTest, PreservesDtmcWithinConfiguredPrecision) {
+    auto matrix = buildProbabilityMatrix();
+    auto convertedMatrix = matrix.toValueType<double>();
+
+    auto inputModel = std::make_shared<storm::models::sparse::Dtmc<storm::RationalNumber>>(std::move(matrix), storm::models::sparse::StateLabeling(3));
+    auto result = storm::transformer::sparseRationalModelToDouble(inputModel, standardPrecision)->as<storm::models::sparse::Dtmc<double>>();
+
+    EXPECT_EQ(convertedMatrix, result->getTransitionMatrix());
+}
+
+TEST(SparseRationalModelToDoubleTransformerTest, PreservesCtmcRates) {
+    storm::storage::SparseMatrixBuilder<storm::RationalNumber> builder(2, 2, 4);
+    builder.addNextValue(0, 0, storm::RationalNumber(2));
+    builder.addNextValue(0, 1, storm::RationalNumber(1));
+    builder.addNextValue(1, 0, storm::RationalNumber(1));
+    builder.addNextValue(1, 1, storm::RationalNumber(3));
+    auto matrix = builder.build();
+    auto convertedMatrix = matrix.toValueType<double>();
+
+    auto inputModel = std::make_shared<storm::models::sparse::Ctmc<storm::RationalNumber>>(std::move(matrix), storm::models::sparse::StateLabeling(2));
+    auto result = storm::transformer::sparseRationalModelToDouble(inputModel, standardPrecision)->as<storm::models::sparse::Ctmc<double>>();
+
+    EXPECT_EQ(convertedMatrix, result->getTransitionMatrix());
+    EXPECT_EQ((std::vector<double>{3.0, 4.0}), result->getExitRateVector());
+}
+
+}  // namespace
diff --git a/src/test/storm/transformer/TransitionToActionRewardTransformerTest.cpp b/src/test/storm/transformer/TransitionToActionRewardTransformerTest.cpp
new file mode 100644
index 0000000000..bd0ac9eaa6
--- /dev/null
+++ b/src/test/storm/transformer/TransitionToActionRewardTransformerTest.cpp
@@ -0,0 +1,206 @@
+#include "storm-config.h"
+#include "test/storm_gtest.h"
+
+#include <optional>
+
+#include "storm-parsers/api/storm-parsers.h"
+#include "storm-parsers/parser/AutoParser.h"
+#include "storm-parsers/parser/DeterministicModelParser.h"
+#include "storm-parsers/parser/MarkovAutomatonParser.h"
+#include "storm/adapters/IntervalAdapter.h"
+#include "storm/adapters/RationalNumberAdapter.h"
+#include "storm/api/storm.h"
+#include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
+#include "storm/models/sparse/Ctmc.h"
+#include "storm/models/sparse/Dtmc.h"
+#include "storm/models/sparse/MarkovAutomaton.h"
+#include "storm/models/sparse/StandardRewardModel.h"
+#include "storm/storage/SparseMatrix.h"
+#include "storm/storage/sparse/ModelComponents.h"
+#include "storm/transformer/TransitionToActionRewardTransformer.h"
+#include "storm/utility/constants.h"
+
+namespace {
+template<typename TransitionValueType, typename RewardValueType>
+std::shared_ptr<storm::models::sparse::Dtmc<TransitionValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>> buildDtmcWithTransitionRewards(
+    RewardValueType const& firstReward, RewardValueType const& secondReward) {
+    storm::storage::SparseMatrixBuilder<TransitionValueType> transitionBuilder(3, 3, 3);
+    transitionBuilder.addNextValue(0, 2, storm::utility::one<TransitionValueType>());
+    transitionBuilder.addNextValue(1, 2, storm::utility::one<TransitionValueType>());
+    transitionBuilder.addNextValue(2, 2, storm::utility::one<TransitionValueType>());
+
+    storm::storage::SparseMatrixBuilder<RewardValueType> rewardBuilder(3, 3, 2);
+    rewardBuilder.addNextValue(0, 2, firstReward);
+    rewardBuilder.addNextValue(1, 2, secondReward);
+
+    storm::models::sparse::StateLabeling labeling(3);
+    labeling.addLabel("init");
+    labeling.addLabelToState("init", 0);
+    storm::storage::sparse::ModelComponents<TransitionValueType, storm::models::sparse::StandardRewardModel<RewardValueType>> components(
+        transitionBuilder.build(), std::move(labeling));
+    std::optional<storm::storage::SparseMatrix<RewardValueType>> transitionRewards(rewardBuilder.build());
+    components.rewardModels.emplace("rew",
+                                    storm::models::sparse::StandardRewardModel<RewardValueType>(std::nullopt, std::nullopt, std::move(transitionRewards)));
+    return std::make_shared<storm::models::sparse::Dtmc<TransitionValueType, storm::models::sparse::StandardRewardModel<RewardValueType>>>(
+        std::move(components));
+}
+
+template<typename TransitionValueType, typename RewardValueType>
+void checkTransformedDtmc(storm::transformer::TransitionToActionRewardTransformerReturnType<
+                              TransitionValueType, storm::models::sparse::StandardRewardModel<RewardValueType>> const& transformed,
+                          RewardValueType const& firstReward, RewardValueType const& secondReward) {
+    ASSERT_EQ(5ull, transformed.model->getNumberOfStates());
+    EXPECT_EQ((std::vector<uint64_t>{0, 1, 4}), transformed.originalToNewStateIndices);
+
+    auto const& transitionMatrix = transformed.model->getTransitionMatrix();
+    auto checkTransition = [&transitionMatrix](uint64_t row, uint64_t column) {
+        auto const rowEntries = transitionMatrix.getRow(row);
+        ASSERT_EQ(1ull, rowEntries.getNumberOfEntries());
+        auto const& entry = *rowEntries.begin();
+        EXPECT_EQ(column, entry.getColumn());
+        EXPECT_EQ(storm::utility::one<TransitionValueType>(), entry.getValue());
+    };
+    checkTransition(0, 2);
+    checkTransition(1, 3);
+    checkTransition(2, 4);
+    checkTransition(3, 4);
+    checkTransition(4, 4);
+
+    auto const& rewardModel = transformed.model->getRewardModel("rew");
+    ASSERT_TRUE(rewardModel.hasStateActionRewards());
+    ASSERT_FALSE(rewardModel.hasTransitionRewards());
+    auto const& actionRewards = rewardModel.getStateActionRewardVector();
+    ASSERT_EQ(5ull, actionRewards.size());
+    EXPECT_EQ(firstReward, actionRewards[2]);
+    EXPECT_EQ(secondReward, actionRewards[3]);
+}
+
+double computeInitialReward(std::shared_ptr<storm::models::sparse::Model<double>> const& model, std::string const& formulaString) {
+    auto const formula = storm::api::extractFormulasFromProperties(storm::api::parseProperties(formulaString)).front();
+    auto const result = storm::api::verifyWithSparseEngine(model, storm::api::createTask<double>(formula, true));
+    return result->asExplicitQuantitativeCheckResult<double>()[*model->getInitialStates().begin()];
+}
+
+TEST(TransitionToActionRewardTransformerTest, DtmcDie) {
+    auto const model = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/dtmc/die.tra", STORM_TEST_RESOURCES_DIR "/dtmc/die.lab", "",
+                                                               STORM_TEST_RESOURCES_DIR "/rew/die.coin_flips.trans.rew");
+
+    auto const transformed = storm::transformer::transformTransitionToActionRewards<double>(model, {""});
+
+    EXPECT_EQ(25ull, transformed.model->getNumberOfStates());
+    EXPECT_EQ(32ull, transformed.model->getNumberOfTransitions());
+    EXPECT_EQ((std::vector<uint64_t>{0, 2, 4, 6, 8, 10, 12, 14, 16, 18, 20, 22, 24}), transformed.originalToNewStateIndices);
+    EXPECT_TRUE(transformed.model->getRewardModel("").hasStateActionRewards());
+    EXPECT_FALSE(transformed.model->getRewardModel("").hasTransitionRewards());
+
+    EXPECT_NEAR(11.0 / 3.0, computeInitialReward(transformed.model, "R=? [F \"done\"]"), 1e-6);
+}
+
+TEST(TransitionToActionRewardTransformerTest, CtmcDie) {
+    auto const model = std::make_shared<storm::models::sparse::Ctmc<double>>(storm::parser::DeterministicModelParser<>::parseCtmc(
+        STORM_TEST_RESOURCES_DIR "/tra/die.tra", STORM_TEST_RESOURCES_DIR "/lab/die.lab", "", STORM_TEST_RESOURCES_DIR "/rew/die.coin_flips.trans.rew"));
+
+    auto const transformed = storm::transformer::transformTransitionToActionRewards<double>(model, {""});
+
+    EXPECT_EQ(storm::models::ModelType::Ctmc, transformed.model->getType());
+    EXPECT_EQ(25ull, transformed.model->getNumberOfStates());
+    EXPECT_EQ(32ull, transformed.model->getNumberOfTransitions());
+    EXPECT_TRUE(transformed.model->getRewardModel("").hasStateActionRewards());
+    EXPECT_FALSE(transformed.model->getRewardModel("").hasTransitionRewards());
+
+    EXPECT_NEAR(11.0 / 3.0, computeInitialReward(transformed.model, "R=? [F \"done\"]"), 1e-6);
+}
+
+TEST(TransitionToActionRewardTransformerTest, MdpTwoDice) {
+    auto const model = storm::parser::AutoParser<>::parseModel(STORM_TEST_RESOURCES_DIR "/tra/two_dice.tra", STORM_TEST_RESOURCES_DIR "/lab/two_dice.lab", "",
+                                                               STORM_TEST_RESOURCES_DIR "/rew/two_dice.flip.trans.rew");
+
+    auto const transformed = storm::transformer::transformTransitionToActionRewards<double>(model, {""});
+
+    EXPECT_EQ(storm::models::ModelType::Mdp, transformed.model->getType());
+    EXPECT_EQ(337ull, transformed.model->getNumberOfStates());
+    EXPECT_EQ(604ull, transformed.model->getNumberOfTransitions());
+    ASSERT_EQ(169ull, transformed.originalToNewStateIndices.size());
+    for (uint64_t state = 0; state < transformed.originalToNewStateIndices.size(); ++state) {
+        EXPECT_EQ(2 * state, transformed.originalToNewStateIndices[state]);
+    }
+    EXPECT_TRUE(transformed.model->getRewardModel("").hasStateActionRewards());
+    EXPECT_FALSE(transformed.model->getRewardModel("").hasTransitionRewards());
+
+    EXPECT_NEAR(22.0 / 3.0, computeInitialReward(transformed.model, "Rmin=? [F \"done\"]"), 1e-6);
+}
+
+TEST(TransitionToActionRewardTransformerTest, MarkovAutomatonGeneral) {
+    auto const model = std::make_shared<storm::models::sparse::MarkovAutomaton<double>>(storm::parser::MarkovAutomatonParser<>::parseMarkovAutomaton(
+        STORM_TEST_RESOURCES_DIR "/tra/ma_general.tra", STORM_TEST_RESOURCES_DIR "/lab/ma_general.lab", STORM_TEST_RESOURCES_DIR "/rew/ma_general.state.rew"));
+    auto transitionRewards = model->getTransitionMatrix();
+    for (auto& entry : transitionRewards) {
+        entry.setValue(1.0);
+    }
+    auto const stateRewards = model->getRewardModel("").getOptionalStateRewardVector();
+    model->getRewardModel("") = storm::models::sparse::StandardRewardModel<double>(std::move(stateRewards), std::nullopt, std::move(transitionRewards));
+
+    auto const transformed = storm::transformer::transformTransitionToActionRewards<double>(model, {""});
+
+    EXPECT_EQ(storm::models::ModelType::MarkovAutomaton, transformed.model->getType());
+    EXPECT_EQ(12ull, transformed.model->getNumberOfStates());
+    EXPECT_EQ(18ull, transformed.model->getNumberOfTransitions());
+    EXPECT_EQ((std::vector<uint64_t>{1, 3, 5, 7, 9, 11}), transformed.originalToNewStateIndices);
+    EXPECT_TRUE(transformed.model->getRewardModel("").hasStateActionRewards());
+    EXPECT_FALSE(transformed.model->getRewardModel("").hasTransitionRewards());
+
+    auto transformedMa = transformed.model->as<storm::models::sparse::MarkovAutomaton<double>>();
+    EXPECT_EQ(2ull, transformedMa->getMarkovianStates().getNumberOfSetBits());
+    EXPECT_TRUE(transformedMa->isMarkovianState(1));
+    EXPECT_EQ(2.0, transformedMa->getExitRate(1));
+    EXPECT_TRUE(transformedMa->isMarkovianState(5));
+    EXPECT_EQ(15.0, transformedMa->getExitRate(5));
+    for (uint64_t state = 0; state < transformedMa->getNumberOfStates(); state += 2) {
+        EXPECT_TRUE(transformedMa->isProbabilisticState(state));
+    }
+}
+
+TEST(TransitionToActionRewardTransformerTest, OverlappingIntervalRewardsAreNotMerged) {
+    storm::Interval const firstReward(1.0, 3.0);
+    storm::Interval const secondReward(2.0, 4.0);
+    auto const model = buildDtmcWithTransitionRewards<storm::Interval>(firstReward, secondReward);
+
+    auto const transformed = storm::transformer::transformTransitionToActionRewards<storm::Interval>(model, {"rew"});
+
+    checkTransformedDtmc(transformed, firstReward, secondReward);
+}
+
+TEST(TransitionToActionRewardTransformerTest, OverlappingRationalIntervalRewardsAreNotMerged) {
+    storm::RationalInterval const firstReward(storm::RationalNumber(1), storm::RationalNumber(3));
+    storm::RationalInterval const secondReward(storm::RationalNumber(2), storm::RationalNumber(4));
+    auto const model = buildDtmcWithTransitionRewards<storm::RationalInterval>(firstReward, secondReward);
+
+    auto const transformed = storm::transformer::transformTransitionToActionRewards<storm::RationalInterval>(model, {"rew"});
+
+    checkTransformedDtmc(transformed, firstReward, secondReward);
+}
+
+TEST(TransitionToActionRewardTransformerTest, DoubleOverlappingIntervalRewardsAreNotMerged) {
+    storm::Interval const firstReward(1.0, 3.0);
+    storm::Interval const secondReward(2.0, 4.0);
+    auto const model = buildDtmcWithTransitionRewards<double>(firstReward, secondReward);
+
+    auto const transformed =
+        storm::transformer::transformTransitionToActionRewards<double, storm::models::sparse::StandardRewardModel<storm::Interval>>(model, {"rew"});
+
+    checkTransformedDtmc(transformed, firstReward, secondReward);
+}
+
+TEST(TransitionToActionRewardTransformerTest, RationalOverlappingRationalIntervalRewardsAreNotMerged) {
+    storm::RationalInterval const firstReward(storm::RationalNumber(1), storm::RationalNumber(3));
+    storm::RationalInterval const secondReward(storm::RationalNumber(2), storm::RationalNumber(4));
+    auto const model = buildDtmcWithTransitionRewards<storm::RationalNumber>(firstReward, secondReward);
+
+    auto const transformed =
+        storm::transformer::transformTransitionToActionRewards<storm::RationalNumber, storm::models::sparse::StandardRewardModel<storm::RationalInterval>>(
+            model, {"rew"});
+
+    checkTransformedDtmc(transformed, firstReward, secondReward);
+}
+
+}  // namespace