diff --git a/src/storm-dft-cli/storm-dft.cpp b/src/storm-dft-cli/storm-dft.cpp
index 185908d61..ebc7a73f8 100644
--- a/src/storm-dft-cli/storm-dft.cpp
+++ b/src/storm-dft-cli/storm-dft.cpp
@@ -5,7 +5,7 @@
 #include "storm-dft/settings/modules/DftGspnSettings.h"
 #include "storm-dft/settings/modules/DftIOSettings.h"
 #include "storm-dft/settings/modules/FaultTreeSettings.h"
-#include <storm/exceptions/UnmetRequirementException.h>
+#include "storm/exceptions/UnmetRequirementException.h"
 #include "storm/settings/modules/GeneralSettings.h"
 #include "storm/settings/modules/DebugSettings.h"
 #include "storm/settings/modules/IOSettings.h"
@@ -66,10 +66,8 @@ void processOptions() {
         dft = dftTransformator.transformBinaryFDEPs(*dft);
     }
     // Check well-formedness of DFT
-    std::stringstream stream;
-    if (!dft->checkWellFormedness(stream)) {
-        STORM_LOG_THROW(false, storm::exceptions::UnmetRequirementException, "DFT is not well-formed: " << stream.str());
-    }
+    auto wellFormedResult = storm::api::isWellFormed(*dft, false);
+    STORM_LOG_THROW(wellFormedResult.first, storm::exceptions::UnmetRequirementException, "DFT is not well-formed: " << wellFormedResult.second);
 
     if (dftGspnSettings.isTransformToGspn()) {
         // Transform to GSPN
diff --git a/src/storm-dft/api/storm-dft.h b/src/storm-dft/api/storm-dft.h
index 1d053dc87..fdeddd7be 100644
--- a/src/storm-dft/api/storm-dft.h
+++ b/src/storm-dft/api/storm-dft.h
@@ -1,6 +1,7 @@
 #pragma once
 
 #include <type_traits>
+#include <utility>
 
 #include "storm-dft/parser/DFTGalileoParser.h"
 #include "storm-dft/parser/DFTJsonParser.h"
@@ -59,12 +60,14 @@ namespace storm {
          * Check whether the DFT is well-formed.
          *
          * @param dft DFT.
-         * @return True iff the DFT is well-formed.
+         * @param validForAnalysis  If true, additional (more restrictive) checks are performed to check whether the DFT is valid for analysis.
+         * @return Pair where the first entry is true iff the DFT is well-formed. The second entry contains the error messages for illformed parts.
          */
         template<typename ValueType>
-        bool isWellFormed(storm::storage::DFT<ValueType> const& dft) {
+        std::pair<bool, std::string> isWellFormed(storm::storage::DFT<ValueType> const& dft, bool validForAnalysis = true) {
             std::stringstream stream;
-            return dft.checkWellFormedness(stream);
+            bool wellFormed = dft.checkWellFormedness(validForAnalysis, stream);
+            return std::pair<bool, std::string>(wellFormed, stream.str());
         }
 
         /*!
diff --git a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
index ca62ea406..4940dc0e6 100644
--- a/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
+++ b/src/storm-dft/modelchecker/dft/DFTModelChecker.cpp
@@ -3,12 +3,14 @@
 #include "storm/settings/modules/IOSettings.h"
 #include "storm/settings/modules/GeneralSettings.h"
 #include "storm/builder/ParallelCompositionBuilder.h"
+#include "storm/exceptions/UnmetRequirementException.h"
 #include "storm/utility/bitoperations.h"
 #include "storm/utility/DirectEncodingExporter.h"
 #include "storm/modelchecker/results/ExplicitQuantitativeCheckResult.h"
 #include "storm/modelchecker/results/ExplicitQualitativeCheckResult.h"
 #include "storm/models/ModelType.h"
 
+#include "storm-dft/api/storm-dft.h"
 #include "storm-dft/builder/ExplicitDFTModelBuilder.h"
 #include "storm-dft/storage/dft/DFTIsomorphism.h"
 #include "storm-dft/settings/modules/FaultTreeSettings.h"
@@ -18,16 +20,19 @@ namespace storm {
     namespace modelchecker {
 
         template<typename ValueType>
-        typename DFTModelChecker<ValueType>::dft_results
-        DFTModelChecker<ValueType>::check(storm::storage::DFT<ValueType> const &origDft,
-                                          std::vector<std::shared_ptr<const storm::logic::Formula>> const &properties,
-                                          bool symred, bool allowModularisation, std::set<size_t> const &relevantEvents,
-                                          bool allowDCForRelevantEvents, double approximationError,
-                                          storm::builder::ApproximationHeuristic approximationHeuristic,
-                                          bool eliminateChains, bool ignoreLabeling) {
+        typename DFTModelChecker<ValueType>::dft_results DFTModelChecker<ValueType>::check(storm::storage::DFT<ValueType> const& origDft,
+                                                                                           std::vector<std::shared_ptr<const storm::logic::Formula>> const& properties, bool symred,
+                                                                                           bool allowModularisation, std::set<size_t> const& relevantEvents,
+                                                                                           bool allowDCForRelevantEvents, double approximationError,
+                                                                                           storm::builder::ApproximationHeuristic approximationHeuristic, bool eliminateChains,
+                                                                                           bool ignoreLabeling) {
             totalTimer.start();
             dft_results results;
 
+            // Check well-formedness of DFT
+            auto wellFormedResult = storm::api::isWellFormed(origDft, true);
+            STORM_LOG_THROW(wellFormedResult.first, storm::exceptions::UnmetRequirementException, "DFT is not well-formed for analysis: " << wellFormedResult.second);
+
             // Optimizing DFT
             storm::storage::DFT<ValueType> dft = origDft.optimize();
 
@@ -37,18 +42,14 @@ namespace storm {
             // TODO: distinguish for all properties, not only for first one
             if (properties[0]->isTimeOperatorFormula() && allowModularisation) {
                 // Use parallel composition as modularisation approach for expected time
-                std::shared_ptr<storm::models::sparse::Model<ValueType>> model = buildModelViaComposition(dft,
-                                                                                                          properties,
-                                                                                                          symred, true,
-                                                                                                          relevantEvents);
+                std::shared_ptr<storm::models::sparse::Model<ValueType>> model = buildModelViaComposition(dft, properties, symred, true, relevantEvents);
                 // Model checking
                 std::vector<ValueType> resultsValue = checkModel(model, properties);
                 for (ValueType result : resultsValue) {
                     results.push_back(result);
                 }
             } else {
-                results = checkHelper(dft, properties, symred, allowModularisation, relevantEvents,
-                                      allowDCForRelevantEvents, approximationError, approximationHeuristic,
+                results = checkHelper(dft, properties, symred, allowModularisation, relevantEvents, allowDCForRelevantEvents, approximationError, approximationHeuristic,
                                       eliminateChains, ignoreLabeling);
             }
             totalTimer.stop();
@@ -56,13 +57,11 @@ namespace storm {
         }
 
         template<typename ValueType>
-        typename DFTModelChecker<ValueType>::dft_results
-        DFTModelChecker<ValueType>::checkHelper(storm::storage::DFT<ValueType> const &dft,
-                                                property_vector const &properties, bool symred,
-                                                bool allowModularisation, std::set<size_t> const &relevantEvents,
-                                                bool allowDCForRelevantEvents, double approximationError,
-                                                storm::builder::ApproximationHeuristic approximationHeuristic,
-                                                bool eliminateChains, bool ignoreLabeling) {
+        typename DFTModelChecker<ValueType>::dft_results DFTModelChecker<ValueType>::checkHelper(storm::storage::DFT<ValueType> const& dft, property_vector const& properties,
+                                                                                                 bool symred, bool allowModularisation, std::set<size_t> const& relevantEvents,
+                                                                                                 bool allowDCForRelevantEvents, double approximationError,
+                                                                                                 storm::builder::ApproximationHeuristic approximationHeuristic,
+                                                                                                 bool eliminateChains, bool ignoreLabeling) {
             STORM_LOG_TRACE("Check helper called");
             std::vector<storm::storage::DFT<ValueType>> dfts;
             bool invResults = false;
diff --git a/src/storm-dft/storage/dft/DFT.cpp b/src/storm-dft/storage/dft/DFT.cpp
index 6c3324bf2..daa6c33f2 100644
--- a/src/storm-dft/storage/dft/DFT.cpp
+++ b/src/storm-dft/storage/dft/DFT.cpp
@@ -760,7 +760,7 @@ namespace storm {
         }
 
         template<typename ValueType>
-        bool DFT<ValueType>::checkWellFormedness(std::ostream& stream) const {
+        bool DFT<ValueType>::checkWellFormedness(bool validForAnalysis, std::ostream& stream) const {
             bool wellformed = true;
             // Check independence of spare modules
             // TODO: comparing one element of each spare module sufficient?
@@ -776,6 +776,21 @@ namespace storm {
                     }
                 }
             }
+
+            if (validForAnalysis) {
+                // Check that each dependency is binary
+                for (size_t idDependency : this->getDependencies()) {
+                    std::shared_ptr<DFTDependency<ValueType> const> dependency = this->getDependency(idDependency);
+                    if (dependency->dependentEvents().size() != 1) {
+                        if (!wellformed) {
+                            stream << std::endl;
+                        }
+                        stream << "Dependency '" << dependency->name() << "' is not binary.";
+                        wellformed = false;
+                    }
+
+                }
+            }
             // TODO check VOT gates
             // TODO check only one constant failed event
             return wellformed;
diff --git a/src/storm-dft/storage/dft/DFT.h b/src/storm-dft/storage/dft/DFT.h
index 6a00be126..c7c790350 100644
--- a/src/storm-dft/storage/dft/DFT.h
+++ b/src/storm-dft/storage/dft/DFT.h
@@ -243,10 +243,12 @@ namespace storm {
 
             /*!
              * Check if the DFT is well-formed.
+             *
+             * @param validForAnalysis If true, additional (more restrictive) checks are performed to check whether the DFT is valid for analysis.
              * @param stream Output stream where warnings about non-well-formed parts are written.
              * @return True iff the DFT is well-formed.
              */
-            bool checkWellFormedness(std::ostream& stream) const;
+            bool checkWellFormedness(bool validForAnalysis, std::ostream& stream) const;
 
             uint64_t maxRank() const;
             
diff --git a/src/test/storm-dft/api/DftApproximationTest.cpp b/src/test/storm-dft/api/DftApproximationTest.cpp
index e17fa200c..40c3eb6ff 100644
--- a/src/test/storm-dft/api/DftApproximationTest.cpp
+++ b/src/test/storm-dft/api/DftApproximationTest.cpp
@@ -54,7 +54,7 @@ namespace {
 
         std::pair<double, double> analyzeMTTF(std::string const& file, double errorBound) {
             std::shared_ptr<storm::storage::DFT<double>> dft = storm::api::loadDFTGalileoFile<double>(file);
-            EXPECT_TRUE(storm::api::isWellFormed(*dft));
+            EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
             std::string property = "T=? [F \"failed\"]";
             std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
             typename storm::modelchecker::DFTModelChecker<double>::dft_results results = storm::api::analyzeDFT<double>(*dft, properties, config.useSR, false, {}, true, errorBound,
@@ -64,7 +64,7 @@ namespace {
 
         std::pair<double, double> analyzeTimebound(std::string const& file, double timeBound, double errorBound) {
             std::shared_ptr<storm::storage::DFT<double>> dft = storm::api::loadDFTGalileoFile<double>(file);
-            EXPECT_TRUE(storm::api::isWellFormed(*dft));
+            EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
             std::stringstream propertyStream;
             propertyStream << "P=? [F<=" << timeBound << " \"failed\"]";
             std::vector <std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(propertyStream.str()));
diff --git a/src/test/storm-dft/api/DftModelBuildingTest.cpp b/src/test/storm-dft/api/DftModelBuildingTest.cpp
index a934ea1e2..8e4a6262a 100644
--- a/src/test/storm-dft/api/DftModelBuildingTest.cpp
+++ b/src/test/storm-dft/api/DftModelBuildingTest.cpp
@@ -11,7 +11,7 @@ namespace {
         // Initialize
         std::string file = STORM_TEST_RESOURCES_DIR "/dft/dont_care.dft";
         std::shared_ptr<storm::storage::DFT<double>> dft = storm::api::loadDFTGalileoFile<double>(file);
-        EXPECT_TRUE(storm::api::isWellFormed(*dft));
+        EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
         std::string property = "Tmin=? [F \"failed\"]";
         std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
         std::map<size_t, std::vector<std::vector<size_t>>> emptySymmetry;
diff --git a/src/test/storm-dft/api/DftModelCheckerTest.cpp b/src/test/storm-dft/api/DftModelCheckerTest.cpp
index 14d640e1f..1d4501132 100644
--- a/src/test/storm-dft/api/DftModelCheckerTest.cpp
+++ b/src/test/storm-dft/api/DftModelCheckerTest.cpp
@@ -77,7 +77,7 @@ namespace {
             storm::transformations::dft::DftTransformator<double> dftTransformator = storm::transformations::dft::DftTransformator<double>();
             std::shared_ptr<storm::storage::DFT<double>> dft = dftTransformator.transformBinaryFDEPs(
                     *(storm::api::loadDFTGalileoFile<double>(file)));
-            EXPECT_TRUE(storm::api::isWellFormed(*dft));
+            EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
             std::string property = "Tmin=? [F \"failed\"]";
             std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(storm::api::parseProperties(property));
             std::set<size_t> relevantEvents;
@@ -92,7 +92,7 @@ namespace {
         double analyzeReliability(std::string const &file, double bound) {
             storm::transformations::dft::DftTransformator<double> dftTransformator = storm::transformations::dft::DftTransformator<double>();
             std::shared_ptr<storm::storage::DFT<double>> dft = dftTransformator.transformBinaryFDEPs(*(storm::api::loadDFTGalileoFile<double>(file)));
-            EXPECT_TRUE(storm::api::isWellFormed(*dft));
+            EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
             std::string property = "Pmin=? [F<=" + std::to_string(bound) + " \"failed\"]";
             std::vector<std::shared_ptr<storm::logic::Formula const>> properties = storm::api::extractFormulasFromProperties(
                     storm::api::parseProperties(property));
diff --git a/src/test/storm-dft/api/DftParserTest.cpp b/src/test/storm-dft/api/DftParserTest.cpp
index dfa7ad769..e57502889 100644
--- a/src/test/storm-dft/api/DftParserTest.cpp
+++ b/src/test/storm-dft/api/DftParserTest.cpp
@@ -10,7 +10,7 @@ namespace {
         std::shared_ptr<storm::storage::DFT<double>> dft = storm::api::loadDFTGalileoFile<double>(file);
         EXPECT_EQ(3ul, dft->nrElements());
         EXPECT_EQ(2ul, dft->nrBasicElements());
-        EXPECT_TRUE(storm::api::isWellFormed(*dft));
+        EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
     }
 
     TEST(DftParserTest, LoadFromJsonFile) {
@@ -18,7 +18,7 @@ namespace {
         std::shared_ptr<storm::storage::DFT<double>> dft = storm::api::loadDFTJsonFile<double>(file);
         EXPECT_EQ(3ul, dft->nrElements());
         EXPECT_EQ(2ul, dft->nrBasicElements());
-        EXPECT_TRUE(storm::api::isWellFormed(*dft));
+        EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
     }
 
     TEST(DftParserTest, CatchCycles) {
diff --git a/src/test/storm-dft/api/DftSmtTest.cpp b/src/test/storm-dft/api/DftSmtTest.cpp
index c367a8c52..fb6ab15de 100644
--- a/src/test/storm-dft/api/DftSmtTest.cpp
+++ b/src/test/storm-dft/api/DftSmtTest.cpp
@@ -7,7 +7,7 @@ namespace {
     TEST(DftSmtTest, AndTest) {
         std::shared_ptr<storm::storage::DFT<double>> dft =
                 storm::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/and.dft");
-        EXPECT_TRUE(storm::api::isWellFormed(*dft));
+        EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
         storm::modelchecker::DFTASFChecker smtChecker(*dft);
         smtChecker.convert();
         smtChecker.toSolver();
@@ -17,7 +17,7 @@ namespace {
     TEST(DftSmtTest, PandTest) {
         std::shared_ptr<storm::storage::DFT<double>> dft =
                 storm::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/pand.dft");
-        EXPECT_TRUE(storm::api::isWellFormed(*dft));
+        EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
         storm::modelchecker::DFTASFChecker smtChecker(*dft);
         smtChecker.convert();
         smtChecker.toSolver();
@@ -27,7 +27,7 @@ namespace {
     TEST(DftSmtTest, SpareTest) {
         std::shared_ptr<storm::storage::DFT<double>> dft =
                 storm::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/spare_two_modules.dft");
-        EXPECT_TRUE(storm::api::isWellFormed(*dft));
+        EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
         storm::modelchecker::DFTASFChecker smtChecker(*dft);
         smtChecker.convert();
         smtChecker.toSolver();
@@ -38,7 +38,7 @@ namespace {
     TEST(DftSmtTest, BoundTest) {
         std::shared_ptr<storm::storage::DFT<double>> dft =
                 storm::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/spare5.dft");
-        EXPECT_TRUE(storm::api::isWellFormed(*dft));
+        EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
         storm::modelchecker::DFTASFChecker smtChecker(*dft);
         smtChecker.convert();
         smtChecker.toSolver();
@@ -49,7 +49,7 @@ namespace {
     TEST(DftSmtTest, FDEPBoundTest) {
         std::shared_ptr<storm::storage::DFT<double>> dft =
                 storm::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/fdep_bound.dft");
-        EXPECT_TRUE(storm::api::isWellFormed(*dft));
+        EXPECT_TRUE(storm::api::isWellFormed(*dft, false).first);
         storm::modelchecker::DFTASFChecker smtChecker(*dft);
         smtChecker.convert();
         smtChecker.toSolver();
@@ -60,7 +60,7 @@ namespace {
     TEST(DftSmtTest, FDEPConflictTest) {
         std::shared_ptr<storm::storage::DFT<double>> dft =
                 storm::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/spare_conflict_test.dft");
-        EXPECT_TRUE(storm::api::isWellFormed(*dft));
+        EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
         std::vector<bool> true_vector(10, true);
 
         dft->setDynamicBehaviorInfo();
@@ -72,7 +72,7 @@ namespace {
     TEST(DftSmtTest, FDEPConflictSPARETest) {
         std::shared_ptr<storm::storage::DFT<double>> dft =
                 storm::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/spare_conflict_test.dft");
-        EXPECT_TRUE(storm::api::isWellFormed(*dft));
+        EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
         std::vector<bool> true_vector(10, true);
 
         dft->setDynamicBehaviorInfo();
@@ -84,7 +84,7 @@ namespace {
     TEST(DftSmtTest, FDEPConflictSEQTest) {
         std::shared_ptr<storm::storage::DFT<double>> dft =
                 storm::api::loadDFTGalileoFile<double>(STORM_TEST_RESOURCES_DIR "/dft/seq_conflict_test.dft");
-        EXPECT_TRUE(storm::api::isWellFormed(*dft));
+        EXPECT_TRUE(storm::api::isWellFormed(*dft).first);
         std::vector<bool> expected_dynamic_vector(dft->nrElements(), true);
         expected_dynamic_vector.at(dft->getTopLevelIndex()) = false;