diff --git a/src/storm-cli-utilities/model-handling.h b/src/storm-cli-utilities/model-handling.h
index 1d71c3639..61a1eead1 100644
--- a/src/storm-cli-utilities/model-handling.h
+++ b/src/storm-cli-utilities/model-handling.h
@@ -42,6 +42,7 @@
 #include "storm/settings/modules/AbstractionSettings.h"
 #include "storm/settings/modules/ResourceSettings.h"
 #include "storm/settings/modules/ModelCheckerSettings.h"
+#include "storm/settings/modules/TransformationSettings.h"
 #include "storm/storage/Qvbs.h"
 
 #include "storm/utility/Stopwatch.h"
@@ -350,11 +351,18 @@ namespace storm {
             auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
             auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
             auto ioSettings = storm::settings::getModule<storm::settings::modules::IOSettings>();
+            auto transformationSettings = storm::settings::getModule<storm::settings::modules::TransformationSettings>();
             
             std::pair<std::shared_ptr<storm::models::sparse::Model<ValueType>>, bool> result = std::make_pair(model, false);
             
             if (result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) {
                 result.first = preprocessSparseMarkovAutomaton(result.first->template as<storm::models::sparse::MarkovAutomaton<ValueType>>());
+                if (transformationSettings.isChainEliminationSet() &&
+                    result.first->isOfType(storm::models::ModelType::MarkovAutomaton)) {
+                    result.first = storm::transformer::NonMarkovianChainTransformer<ValueType>::eliminateNonmarkovianStates(
+                            result.first->template as<storm::models::sparse::MarkovAutomaton<ValueType>>(),
+                            !transformationSettings.isIgnoreLabelingSet());
+                }
                 result.second = true;
             }
             
@@ -629,19 +637,31 @@ namespace storm {
         
         template<typename ValueType>
         void verifyProperties(SymbolicInput const& input, std::function<std::unique_ptr<storm::modelchecker::CheckResult>(std::shared_ptr<storm::logic::Formula const> const& formula, std::shared_ptr<storm::logic::Formula const> const& states)> const& verificationCallback, std::function<void(std::unique_ptr<storm::modelchecker::CheckResult> const&)> const& postprocessingCallback = PostprocessingIdentity()) {
+            auto transformationSettings = storm::settings::getModule<storm::settings::modules::TransformationSettings>();
             auto const& properties = input.preprocessedProperties ? input.preprocessedProperties.get() : input.properties;
             for (auto const& property : properties) {
                 printModelCheckingProperty(property);
+                bool ignored = false;
                 storm::utility::Stopwatch watch(true);
                 std::unique_ptr<storm::modelchecker::CheckResult> result;
                 try {
-                    result = verificationCallback(property.getRawFormula(), property.getFilter().getStatesFormula());
+                    auto rawFormula = property.getRawFormula();
+                    if (transformationSettings.isChainEliminationSet() &&
+                        !storm::transformer::NonMarkovianChainTransformer<ValueType>::preservesFormula(*rawFormula)) {
+                        STORM_LOG_WARN("Property is not preserved by elimination of non-markovian states.");
+                        ignored = true;
+                    } else {
+                        result = verificationCallback(property.getRawFormula(),
+                                                      property.getFilter().getStatesFormula());
+                    }
                 } catch (storm::exceptions::BaseException const& ex) {
                     STORM_LOG_WARN("Cannot handle property: " << ex.what());
                 }
                 watch.stop();
-                postprocessingCallback(result);
-                printResult<ValueType>(result, property, &watch);
+                if (!ignored) {
+                    postprocessingCallback(result);
+                    printResult<ValueType>(result, property, &watch);
+                }
             }
         }
         
diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
index 4af4c28c5..4a03692ab 100644
--- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
@@ -8,7 +8,6 @@
 #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
 #include "storm/models/ModelType.h"
-#include "storm/transformer/NonMarkovianChainTransformer.h"
 
 #include "storm-dft/builder/ExplicitDFTModelBuilder.h"
 #include "storm-dft/storage/dft/DFTIsomorphism.h"
diff --git a/src/storm-pars-cli/storm-pars.cpp b/src/storm-pars-cli/storm-pars.cpp
index fe5f50993..18b27627d 100644
--- a/src/storm-pars-cli/storm-pars.cpp
+++ b/src/storm-pars-cli/storm-pars.cpp
@@ -21,6 +21,7 @@
 #include "storm/settings/modules/CoreSettings.h"
 #include "storm/settings/modules/IOSettings.h"
 #include "storm/settings/modules/BisimulationSettings.h"
+#include "storm/settings/modules/TransformationSettings.h"
 
 #include "storm/exceptions/BaseException.h"
 #include "storm/exceptions/InvalidSettingsException.h"
@@ -141,6 +142,7 @@ namespace storm {
             auto generalSettings = storm::settings::getModule<storm::settings::modules::GeneralSettings>();
             auto bisimulationSettings = storm::settings::getModule<storm::settings::modules::BisimulationSettings>();
             auto parametricSettings = storm::settings::getModule<storm::settings::modules::ParametricSettings>();
+            auto transformationSettings = storm::settings::getModule<storm::settings::modules::TransformationSettings>();
             
             PreprocessResult result(model, false);
             
@@ -153,6 +155,18 @@ namespace storm {
                 result.model = storm::cli::preprocessSparseModelBisimulation(result.model->template as<storm::models::sparse::Model<ValueType>>(), input, bisimulationSettings);
                 result.changed = true;
             }
+
+            if (transformationSettings.isChainEliminationSet() &&
+                model->isOfType(storm::models::ModelType::MarkovAutomaton)) {
+                auto eliminationResult = storm::api::eliminateNonMarkovianChains(
+                        result.model->template as<storm::models::sparse::MarkovAutomaton<ValueType>>(),
+                        storm::api::extractFormulasFromProperties(input.properties),
+                        transformationSettings.isIgnoreLabelingSet());
+                result.model = eliminationResult.first;
+                // Set transformed properties as new properties in input
+                result.formulas = eliminationResult.second;
+                result.changed = true;
+            }
             
             if (parametricSettings.transformContinuousModel() && (model->isOfType(storm::models::ModelType::Ctmc) || model->isOfType(storm::models::ModelType::MarkovAutomaton))) {
                 auto transformResult = storm::api::transformContinuousToDiscreteTimeSparseModel(std::move(*model->template as<storm::models::sparse::Model<ValueType>>()), storm::api::extractFormulasFromProperties(input.properties));
diff --git a/src/storm/api/transformation.h b/src/storm/api/transformation.h
index 0fb25b2f2..4dcaf7f61 100644
--- a/src/storm/api/transformation.h
+++ b/src/storm/api/transformation.h
@@ -2,6 +2,7 @@
 
 #include "storm/transformer/ContinuousToDiscreteTimeModelTransformer.h"
 #include "storm/transformer/SymbolicToSparseTransformer.h"
+#include "storm/transformer/NonMarkovianChainTransformer.h"
 
 #include "storm/utility/macros.h"
 #include "storm/utility/builder.h"
@@ -10,7 +11,30 @@
 
 namespace storm {
     namespace api {
-        
+
+        /*!
+         * Eliminates chains of non-Markovian states from a given Markov Automaton
+         */
+        template<typename ValueType>
+        std::pair<std::shared_ptr<storm::models::sparse::Model<ValueType>>, std::vector<std::shared_ptr<storm::logic::Formula const>>>
+        eliminateNonMarkovianChains(std::shared_ptr<storm::models::sparse::MarkovAutomaton<ValueType>> const &ma,
+                                    std::vector<std::shared_ptr<storm::logic::Formula const>> const &formulas,
+                                    bool ignoreLabeling) {
+
+            auto newFormulas = storm::transformer::NonMarkovianChainTransformer<ValueType>::checkAndTransformFormulas(
+                    formulas);
+            STORM_LOG_WARN_COND(newFormulas.size() == formulas.size(),
+                                "The state elimination does not preserve all properties.");
+            STORM_LOG_WARN_COND(!ignoreLabeling,
+                                "Labels are ignored for the state elimination. This may cause incorrect results.");
+            return std::make_pair(
+                    storm::transformer::NonMarkovianChainTransformer<ValueType>::eliminateNonmarkovianStates(ma,
+                                                                                                             !ignoreLabeling),
+                    newFormulas);
+
+        }
+
+
         /*!
          * Transforms the given continuous model to a discrete time model.
          * If such a transformation does not preserve one of the given formulas, a warning is issued.