diff --git a/src/models/AtomicPropositionsLabeling.h b/src/models/AtomicPropositionsLabeling.h
index b5ebfba8b..1969a525a 100644
--- a/src/models/AtomicPropositionsLabeling.h
+++ b/src/models/AtomicPropositionsLabeling.h
@@ -142,6 +142,21 @@ public:
 		return addAtomicProposition(ap, storage::BitVector(stateCount));
 	}
 	
+    /*!
+     * Retrieves the set of atomic propositions contained in this labeling.
+     *
+     * @return The set of known atomic propositions.
+     */
+    std::set<std::string> getAtomicPropositions() const {
+        std::set<std::string> result;
+        
+        for (auto const& apIndexPair : this->nameToLabelingMap) {
+            result.insert(apIndexPair.first);
+        }
+        
+        return result;
+    }
+    
 	/**
 	 * Creates a new atomic proposition and attaches the given states with the label.
      * @param ap
diff --git a/src/models/Dtmc.h b/src/models/Dtmc.h
index 4dfefdcc9..43e30a647 100644
--- a/src/models/Dtmc.h
+++ b/src/models/Dtmc.h
@@ -290,6 +290,36 @@ public:
         storm::storage::SparseMatrix<T> newTransitionMatrix = storm::utility::matrix::applyScheduler(this->getTransitionMatrix(), scheduler);
         return std::shared_ptr<AbstractModel<T>>(new Dtmc(newTransitionMatrix, this->getStateLabeling(), this->hasStateRewards() ? this->getStateRewardVector() : boost::optional<std::vector<T>>(), this->hasTransitionRewards() ? this->getTransitionRewardMatrix() :  boost::optional<storm::storage::SparseMatrix<T>>(), this->hasChoiceLabeling() ? this->getChoiceLabeling() : boost::optional<std::vector<boost::container::flat_set<uint_fast64_t>>>()));
     }
+    
+    void dumpToExplicitFormat(std::string const& traFilename, std::string const& labFilename) const {
+        std::ofstream transStream(traFilename);
+        transStream << "dtmc" << std::endl;
+        for (uint_fast64_t stateIndex = 0; stateIndex < this->getNumberOfStates(); ++stateIndex) {
+            for (auto const& element : this->getTransitionMatrix().getRow(stateIndex)) {
+                transStream << stateIndex << " " << element.first << " " << element.second << std::endl;
+            }
+        }
+        transStream.close();
+        
+        std::ofstream labStream(labFilename);
+        labStream << "#DECLARATION" << std::endl;
+        for (auto const& label : this->getStateLabeling().getAtomicPropositions()) {
+            labStream << label << " ";
+        }
+        labStream << std::endl;
+        labStream << "#END" << std::endl;
+        for (uint_fast64_t stateIndex = 0; stateIndex < this->getNumberOfStates(); ++stateIndex) {
+            std::set<std::string> labels = this->getLabelsForState(stateIndex);
+            if (!labels.empty()) {
+                labStream << stateIndex << " ";
+                for (auto const& label : labels) {
+                    labStream << label << " ";
+                }
+                labStream << std::endl;
+            }
+        }
+        labStream.close();
+    }
 
 private:
 	/*!